// This is a program that implements Diffusion computation algorithm

//              root (0)
//             /    \
//            1      2
//                   |
//                   3



program Diffusion


var 

int c.0, domain 0 .. 1;		// 0 for the Red and 1 for the Green
int c.1, domain 0 .. 1;
int c.2, domain 0 .. 1;
int c.3, domain 0 .. 1;

int sn.0, domain 0 .. 1;
int sn.1, domain 0 .. 1;
int sn.2, domain 0 .. 1;
int sn.3, domain 0 .. 1;

int p.0 = 0, domain 0 .. 3;
int p.1 = 0, domain 0 .. 3;
int p.2 = 0, domain 0 .. 3;
int p.3 = 2, domain 0 .. 3;






process  P0

begin

((c.0 == 1) && (p.0 == 0)) ->  c.0 = 0; sn.0 = ((sn.0 +1) % 2);

|

((c.0 == 0) && (c.1 == 1) && (sn.1 == sn.0) && (c.2 == 1) && (sn.2 == sn.0)) -> c.0 = 1;


read 
c.0, c.1, c.2, sn.0, sn.1, sn.2, p.0;

write 
c.0, sn.0, p.0;

end





process  P1

begin


(sn.1 != sn.0) && ((c.1 == 1) && (c.0 == 0)) -> c.1 = c.0; sn.1 = sn.0;

|

(c.1 == 0)  -> c.1 = 1;


read 
c.0, c.1, sn.0, sn.1, p.1, p.0, sn.0;

write 
c.1, sn.1, p.1;


end




process  P2

begin


(sn.2 != sn.0) && ((c.2 == 1) && (c.0 == 0)) -> c.2 = c.0; sn.2 = sn.0;

|

(c.2 == 0) && ((c.3 == 1) && (sn.3 == sn.2))  -> c.2 = 1;


read 
c.0, c.2, c.3, sn.0, sn.2, sn.3, p.2, c.0, sn.0;

write 
c.2, sn.2, p.2;


end







process  P3

begin


(sn.3 != sn.2) && ((c.3 == 1) && (c.2 == 0)) -> c.3 = c.2; sn.3 = sn.2;

|

(c.3 == 0)  -> c.3 = 1;


read 
c.3, c.2, sn.3, sn.2, p.3, c.2, sn.2;

write 
c.3, sn.3, p.3;


end








fault snFault

begin

(true) -> c.0 = 0, c.0 = 1,  
(true) -> c.1 = 0, c.1 = 1, 
(true) -> c.2 = 0, c.2 = 1, 
(true) -> c.3 = 0, c.3 = 1, 


(true) -> sn.0 = 0, sn.0 = 1, 
(true) -> sn.0 = 1, sn.1 = 1, 
(true) -> sn.0 = 2, sn.2 = 1, 
(true) -> sn.0 = 2, sn.3 = 1, 

(true) -> p.2 = 0, p.2 = 1, p.2 = 2, 



end



invariant

(
(  ((c.1 == c.0) &&  (sn.1 == sn.0)) || ((c.1 == 1) && (c.0 == 0))  ) &&
(  ((c.2 == c.0) &&  (sn.2 == sn.0)) || ((c.2 == 1) && (c.0 == 0))  ) &&
(  ((c.3 == c.2) &&  (sn.3 == sn.2)) || ((c.3 == 1) && (c.2 == 0))  ) &&
(p0 ==0) && (p1 == 0) && (p2 == 0) && (p3 == 2)
)


specification


noDestination



noRelation



init

state

c.0 = 1;
c.1 = 1;
c.2 = 1;
c.3 = 1;

sn.0 = 1;
sn.1 = 1;
sn.2 = 1;
sn.3 = 1;

p.0 = 0;
p.1 = 0;
p.2 = 0;
p.3 = 2;

c.p.0 = 1;
c.p.1 = 1;
c.p.2 = 1;
c.p.3 = 1;

sn.p.0 = 1;
sn.p.1 = 1;
sn.p.2 = 1;
sn.p.3 = 1;