COSTABS MHP analysis prototype

Write your ABS code in the text area:

module Prio1;

interface A{
  Unit f();
  Unit g();
  Unit f1();
  Unit g1();
  Unit m();
}

class AImpl(Int field) implements A {

  [priority(10)] Unit f1(){
    while( field > 0 ){
      field = field - 1;
      suspend;
    }
  }
  
  [priority(1)] Unit g1(){
    this ! f1();
  }
  
  [priority(2)] Unit f(){
    this ! f1();
  }
  
  [priority(2)] Unit g(){
    this ! g1();
  }
  
  [priority(0)]
  Unit m()
  {
    this ! f();
    this ! g();
  }
}

// f1() cannot happen in parallel with itself

{
  A q = new local AImpl(34);
  q ! m();
}

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