COSTABS MHP analysis prototype

Write your ABS code in the text area:

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

module Emmi2;

interface Emmi2I{
  Unit main2( Int x );
  Unit main1();
  Unit bar();
}

class Emmi2(Int x) implements Emmi2I{

  [priority(0)] Unit main2(){
    Int j=0;
    suspend;
    while (j<x)
    {
      suspend;
      Fut<Unit> f = this!bar();
      suspend;
      j = j+1;
    }
  }

  [priority(0)] Unit main1(){
    Int i=0;
    suspend;
    while (i<x)
    {
      suspend;
      Fut<Unit> f = this!bar();
      suspend;
      i = i+1;
    }
  }

 

  [priority(5)] Unit bar(){
    Int t=x;
    x=t+1;
  }
}
  
{
  Emmi2I e= new local Emmi2(0);
  e!main1();
  Emmi2I e2= new local Emmi2(0);
  e2!main2();  
}

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