COSTABS: Web interface

Step 1a: Write your ABS code in the text area:

// Running example of the paper
// main4

module Running4;

interface TaskQueueInter{
  Unit addTask(Task tk);
  Unit addTasks(List<Task> list);
  Unit consumeAsync();
  Unit consumeSync();
}

class TaskQueue( List<Task> pending ) implements TaskQueueInter {
  
Unit addTask(Task tk){
  pending = appendright(pending,tk);
}

Unit addTasks(List<Task> list){
  while (list != Nil) {
    Task tk = head(list);
    list = tail(list);     
    Fut<Unit> f = this!addTask(tk);
    await f?;
  }
}

Unit consumeAsync(){
  while (pending != Nil) {
    Task tk = head(pending);
    pending = tail(pending);            
    Fut<Unit> f = tk!start();
  }
}

Unit consumeSync(){
  while (pending != Nil) {
    Task tk = head(pending);
    pending = tail(pending);            
    Fut<Unit> f=tk!start();
    await f?;
  }
}

}

interface Task{
  Unit start();
}

class TaskImpl implements Task{
  Unit start(){
  }
}

{
  //Init List<Task> l
  Task t1 = new local TaskImpl();
  Task t2 = new local TaskImpl();
  Task t3 = new local TaskImpl();  
  List<Task> l = Cons( t1, Cons( t2, Cons( t3, Nil)));
  
  TaskQueueInter q = new local TaskQueue(Nil);  
  while( True ){
    Fut<Unit> x = q!addTasks(l);
    Fut<Unit> y = q!consumeSync();
    await x?;
    await y?;
  }
}

Step 1b: or you can upload a file with ABS code:

File:

Step 1c: or you can choose one of our examples:

Step 1d: Choose the analysis you want to use:

Traditional Termination and Cost Analysis
Rely-guarantee Termination Analysis
Rely-guarantee Cost Analysis (Under development)
Deadlock Analysis