COSTABS MHP analysis prototype

Write your ABS code in the text area:

module Prio2;

interface A{
  Unit f();
  Unit g();
  Unit h();
}

class AImpl(Int field) implements A {

  [priority(5)] Unit f(Int i){
    this ! g();
    this ! h();
    suspend;
    if( field > 0 )
    {
      while( i > 0 )
      {
        i = i - field;
        suspend;
      }
    }
  }
  
  [priority(10)] Unit g(){
    field = 1;
  }
  
  [priority(0)] Unit h(){
    field = -1;
  }
   
}

// L26 or L30 cannot happen in parallel with the release at L20, so the value
// of "field" will not change between iterations

{
  A q = new local AImpl(324);
  q ! f(12);
}

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