COSTABS MHP analysis prototype

Write your ABS code in the text area:

/*
 * A working version of a program with two producers and 
 * two consumers comunicating via a shared bounded-buffer
 *
 */

module BoundedBuffer;
import * from ABS.StdLib;

type Data = Int ;
//type Buffer = DataList
data DataList = DataNil | ConsData(Data, DataList) ;

def Data dataHead(DataList dl) = case dl { ConsData(d,l) => d ; };  
def DataList dataTail(DataList dl) = case dl { ConsData(d,l) => l ; }; 

def DataList appendData(Data d, DataList list)
  = concat(list, ConsData(d,DataNil));

def DataList concat(DataList l1 , DataList l2) = 
case l1 { 
    DataNil => l2 ; 
    ConsData(hd,tl) => ConsData(hd, concat(tl,l2)) ; 
};
    
interface Buffer {

    //Unit init();
    Unit append(Data d);
    Data remove();
}

interface Consumer {
    Unit loop(Data d);
} 

interface Producer {
    Unit loop(Data d);
}


class BoundedBuffer implements Buffer {
    
    //A bounded buffer
    DataList buffer = DataNil; 
    Int max = 10;
    Int n = 0;

    [buffer <= max(buffer)]
    Unit append(Data d){
	[buffer <= max(buffer)]
        await (n < max) ; 
        buffer = appendData(d,buffer);
        n = n + 1 ; 
    }
    
    Data remove() {
        Data d = 0;
        await n > 0 ; 
        d = dataHead(buffer);
        buffer = dataTail(buffer);
        n = n - 1 ; 
        return d ; 
    }
}

class ProducerImpl (Buffer b) implements Producer {
    
    Unit loop(Data d) {
        if (d > 0) {
            b!append(d);
            this!loop(d - 1);
        }
    }
}

class ConsumerImpl (Buffer b) implements Consumer {
    
    Unit loop(Data d) {
        if (d > 0) {
            b!remove();
            this!loop(d - 1);
        }
    }
}

//Main
{
    Buffer buff;
    Producer p1;
    Producer p2;
    Consumer c1;
    Consumer c2;  
    buff = new BoundedBuffer(); 
    p1 = new ProducerImpl(buff);   
    p2 = new ProducerImpl(buff); 
    c1 = new ConsumerImpl(buff);
    c2 = new ConsumerImpl(buff);
    p1!loop(5);
    p2!loop(5);
    c1!loop(5);
    c2!loop(5);
}
Or you can choose one of our examples: