COSTABS MHP analysis prototype

Write your ABS code in the text area:

/*
Running example of the paper "May-Happen-in-Parallel Analysis for Priority-based Scheduling"
*/

module Running;

interface Paper{
  Unit task();
  Unit  f();
  Unit m();
  Unit h();
  Unit main();
}


class PaperImpl( Int g1, Int g2 ) implements Paper {

  [priority(0)] Unit task(){
    g2 = g2 + 1;
  }

  [priority(10)] Unit f(){
    while( g1 > 0 ){
      g1 = g1 - 1;
      g2 = g2 + 1;
      suspend;
    }
  }
  
  [priority(5)] Unit m()
  {
    while( g1 < 0 ){
      g1 = g1 + 1;
      suspend;
    }
  }
  
  [priority(10)] Unit h(){
    while( g1 < 0 ){
      g1 = g1 + 2;
      suspend;
    }
  }
  
  [priority(0)] Unit main(){
    this ! f();
    Fut<Unit> x = this ! m();
    await x?;
    this ! h();
    Paper o = new local PaperImpl(1,2);
    o ! task();
  }
  
}

{
  Paper p = new local PaperImpl(1,2);
  p ! main();
}

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