COSTABS MHP analysis prototype

Write your ABS code in the text area:

/*
Adaptation of the example of Figure 7 from the paper
M. Emmi, A. Lal, and S. Qadeer. Asynchronous programs with prioritized task-buffers. 
In SIGSOFT FSE, page 48. ACM, 2012.
*/


module Emmi1;

interface Emmi1I{
  Unit bar();
  Unit foo();
}

class Emmi1(Int x, Int cont) implements Emmi1I{

  [priority(10)] Unit bar(){
    Int t=x;
    suspend;
    x=t+1;
    suspend;
    if (x>0) {
      cont=1;
    }
    suspend;
  }
  

  [priority(5)] Unit foo(){
    if (cont==1)
     {
        cont=0;
        suspend;
        this ! bar();
        suspend;
        this ! foo();
        suspend;
      }
  }
}
  
{
  Emmi1I e= new local Emmi1(0,1);
  e!foo();
}

Or you can choose one of our examples:

priorities/emmi1.abs
priorities/emmi2.abs
priorities/Running.abs
priorities/Prio1.abs
priorities/Prio2.abs
priorities/Prio3.abs
ReplicationSystem.abs
fullTradingSystem.abs
MailServer.abs
DemoExample.abs
BookShop.abs
PeerToPeer.abs
BoundedBuffer.abs
Chat.abs