law(pingpongplus,language(prolog)).

/* the pingPong protocol*/
 sent(X,ping(M),Y) :- not(pingTo(Y)@CS), do(add(pingTo(Y))),do(forward).

 arrived(X,ping(M),Y) :- do(add(pingFrom(X))), do(deliver).

 sent(X,pong(M),Y) :- pingFrom(Y)@CS, do(remove(pingFrom(Y))),do(forward).

 arrived(X,pong(M),Y) :- do(remove(pingTo(X))), do(deliver).

/* for querying the state */
sent(Self,getCS,Z) :- do(discloseCS(all)).

/*disconnection and reconnection */
disconnected :- do(imposeObligation(toQuit,10, min)).

reconnected :- do(repealObligation(toQuit)).

obligationDue(toQuit) :- do(quit).

/* for automatic state monitoring: */

sent(S,display(DT),Z) :- do(imposeObligation(display,DT,sec)), do(add(obTime(DT))),
    do(show(possibleEvent(all), cs(all))).

obligationDue(display) :- obTime(DT)@CS, do(imposeObligation(display,DT,sec)), 
    do(show(possibleEvent(all), cs(all))).

sent(S,stopDisplay,Z) :- obTime(T)@CS, do(remove(obTime(T))),
	              do(repealObligation(display)).

/*exception handling*/
exception(forward(Self,ping(M),[Y,L]),D) :- do(remove(pingTo(Y))),
    do(deliver(Self,exc(ping(M)),Y)).

exception(E,D) :- do(deliver(Self,exception(E,D),Self)).

/*sentinel rule*/
sent(X,N,Y) :- do(deliver(Self,messageIgnored,Self)).