program Abp

var 


boolean rs; 
boolean rr;
boolean bs;  
boolean br;




int cs, domain -1 .. 1;
int cr, domain -1 .. 1;




process  sender

begin

((rs == 1)) -> rs = 0;  cs = bs ; 

| 

(cr != -1) ->  rs = 1; cr = -1; bs = (bs+1)%2 ; 


read rs, cs , bs ,cr;
 
write rs, cs , bs ,cr;

end




process receiver

begin

( cs != -1) -> cs = -1;  rr = 1; br = (br+1)%2  ; 
 
|

( rr == 1) -> rr = 0; cr = br ; 


read cs, rr , br , cr;
 
write  cs, rr , br , cr;

end




fault FC
begin


((cs != -1)) -> cs = -1;


|


((cr != -1)) -> cr = -1;



end



invariant
(
(((rr != 1) && (cr == -1))  || (br == bs)) &&
(((rs != 1) && (cs == -1))  || (br != bs)) &&
((cs == -1) || (cs == bs)) &&
((cs != -1) || (cr != -1) || ((rr + rs) == 1)) &&
((cs == -1) || (cr != -1) || ((rr + rs) == 0)) &&
((cs != -1) || (cr == -1) || ((rr + rs) == 0)) 

)

specification


noSource


noDestination



noRelation

init

state
rs = 1;
rr = 0;

cs = -1;
cr = -1;

bs = 1;
br = 0;