// mutual exclusion [PZ82] // dxp/gxn 19/12/99 mdp // atomic formula // none in low, high, tie formula none_lht = p2!=4..13 & p3!=4..13; // some in admit formula some_a = p2=14..15 | p3=14..15; // some in high, admit formula some_ha = p2=4..5,10..15 | p3=4..5,10..15; // none in high, tie, admit formula none_hta = p2=0..3,7..8 & p3=0..3,7..8; // none in enter formula none_e = p2!=2..3 & p3!=2..3; // process 1 module process1 p1: [0..15]; [] p1=0 -> (p1'=0); [] p1=0 -> (p1'=1); [] p1=1 -> (p1'=2); [] p1=2 & (none_lht | some_a) -> (p1'=3); [] p1=2 & !(none_lht | some_a) -> (p1'=2); [] p1=3 -> (p1'=4); [] p1=3 -> (p1'=7); [] p1=4 & some_ha -> (p1'=5); [] p1=4 & !some_ha -> (p1'=10); [] p1=5 -> (p1'=6); [] p1=6 & some_ha -> (p1'=6); [] p1=6 & !some_ha -> (p1'=9); [] p1=7 & none_hta -> (p1'=8); [] p1=7 & !none_hta -> (p1'=7); [] p1=8 -> (p1'=9); [] p1=9 -> 0.5 : (p1'=4) + 0.5 : (p1'=7); [] p1=10 -> (p1'=11); [] p1=11 & none_lht -> (p1'=13); [] p1=11 & !none_lht -> (p1'=12); [] p1=12 -> (p1'=0); [] p1=13 -> (p1'=14); [] p1=14 & none_e -> (p1'=15); [] p1=14 & !none_e -> (p1'=14); [] p1=15 -> (p1'=0); endmodule // construct further modules through renaming module process2 = process1 [p1=p2, p2=p1] endmodule module process3 = process1 [p1=p3, p3=p1] endmodule