MODULE main DEFINE NumOfForks := 5; NumOfPhilosophers := 5; TRANS (_trans=1)|(_trans=2)|(_trans=3)|(_trans=4)|(_trans=5)|(_trans=6)|(_trans=7)|(_trans=8)|(_trans=9)|(_trans=10)|(_trans=11)|(_trans=12)|(_trans=13)|(_trans=14)|(_trans=15)|(_trans=16)|(_trans=17)|(_trans=18)|(_trans=19)|(_trans=20)|(_trans=21)|(_trans=22)|(_trans=23)|(_trans=24)|(_trans=25)|(_trans=26)|(_trans=27)|(_trans=28)|(_trans=29)|(_trans=30)|(_trans=31)|(_trans=32)|(_trans=33)|(_trans=34)|(_trans=35)|(_trans=36)|(_trans=37)|(_trans=38)|(_trans=39)|(_trans=40)|(_trans=41)|(_trans=42)|(_trans=43)|(_trans=44)|(_trans=45)|(_trans=46)|(_trans=47)|(_trans=48)|(_trans=49)|(_trans=50) INVAR !_fail VAR _trans : 1..50; _terminate : boolean; _fail : boolean; p4 : -100..100; p3 : -100..100; p2 : -100..100; p1 : -100..100; p0 : -100..100; philosophers : array 0..4 of { eating,thinking }; forks : array 0..4 of { nonavailable,available }; ASSIGN _terminate := case !(((((p4=0))&((philosophers[0]=eating))))|(((((p4=4))&((philosophers[4]=eating))))|(((((p4=3))&((philosophers[3]=eating))))|(((((p4=2))&((philosophers[2]=eating))))|(((((p4=1))&((philosophers[1]=eating))))|(((((((p4=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))|(((((((p4=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))|(((((((p4=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))|(((((((p4=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))|(((((((p4=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))|(((((p3=0))&((philosophers[0]=eating))))|(((((p3=4))&((philosophers[4]=eating))))|(((((p3=3))&((philosophers[3]=eating))))|(((((p3=2))&((philosophers[2]=eating))))|(((((p3=1))&((philosophers[1]=eating))))|(((((((p3=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))|(((((((p3=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))|(((((((p3=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))|(((((((p3=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))|(((((((p3=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))|(((((p2=0))&((philosophers[0]=eating))))|(((((p2=4))&((philosophers[4]=eating))))|(((((p2=3))&((philosophers[3]=eating))))|(((((p2=2))&((philosophers[2]=eating))))|(((((p2=1))&((philosophers[1]=eating))))|(((((((p2=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))|(((((((p2=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))|(((((((p2=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))|(((((((p2=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))|(((((((p2=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))|(((((p1=0))&((philosophers[0]=eating))))|(((((p1=4))&((philosophers[4]=eating))))|(((((p1=3))&((philosophers[3]=eating))))|(((((p1=2))&((philosophers[2]=eating))))|(((((p1=1))&((philosophers[1]=eating))))|(((((((p1=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))|(((((((p1=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))|(((((((p1=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))|(((((((p1=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))|(((((((p1=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))|(((((((p0=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))|(((((((p0=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))|(((((((p0=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))|(((((((p0=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))|(((((((p0=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))|(((((p0=1))&((philosophers[1]=eating))))|(((((p0=2))&((philosophers[2]=eating))))|(((((p0=3))&((philosophers[3]=eating))))|(((((p0=4))&((philosophers[4]=eating))))|((((p0=0))&((philosophers[0]=eating))))))))))))))))))))))))))))))))))))))))))))))))))))) : 1; 1 : 0; esac; _fail := case _terminate : 0; (((((((((((((((((((((((((((((((((((((((((((((((((((_trans=50)&!((((p0=0))&((philosophers[0]=eating)))))|((_trans=49)&!((((p0=4))&((philosophers[4]=eating))))))|((_trans=48)&!((((p0=3))&((philosophers[3]=eating))))))|((_trans=47)&!((((p0=2))&((philosophers[2]=eating))))))|((_trans=46)&!((((p0=1))&((philosophers[1]=eating))))))|((_trans=45)&!((((((p0=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))))|((_trans=44)&!((((((p0=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))))|((_trans=43)&!((((((p0=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))))|((_trans=42)&!((((((p0=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))))|((_trans=41)&!((((((p0=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))))|((_trans=40)&!((((((p1=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))))|((_trans=39)&!((((((p1=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))))|((_trans=38)&!((((((p1=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))))|((_trans=37)&!((((((p1=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))))|((_trans=36)&!((((((p1=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))))|((_trans=35)&!((((p1=1))&((philosophers[1]=eating))))))|((_trans=34)&!((((p1=2))&((philosophers[2]=eating))))))|((_trans=33)&!((((p1=3))&((philosophers[3]=eating))))))|((_trans=32)&!((((p1=4))&((philosophers[4]=eating))))))|((_trans=31)&!((((p1=0))&((philosophers[0]=eating))))))|((_trans=30)&!((((((p2=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))))|((_trans=29)&!((((((p2=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))))|((_trans=28)&!((((((p2=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))))|((_trans=27)&!((((((p2=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))))|((_trans=26)&!((((((p2=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))))|((_trans=25)&!((((p2=1))&((philosophers[1]=eating))))))|((_trans=24)&!((((p2=2))&((philosophers[2]=eating))))))|((_trans=23)&!((((p2=3))&((philosophers[3]=eating))))))|((_trans=22)&!((((p2=4))&((philosophers[4]=eating))))))|((_trans=21)&!((((p2=0))&((philosophers[0]=eating))))))|((_trans=20)&!((((((p3=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))))|((_trans=19)&!((((((p3=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))))|((_trans=18)&!((((((p3=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))))|((_trans=17)&!((((((p3=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))))|((_trans=16)&!((((((p3=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))))|((_trans=15)&!((((p3=1))&((philosophers[1]=eating))))))|((_trans=14)&!((((p3=2))&((philosophers[2]=eating))))))|((_trans=13)&!((((p3=3))&((philosophers[3]=eating))))))|((_trans=12)&!((((p3=4))&((philosophers[4]=eating))))))|((_trans=11)&!((((p3=0))&((philosophers[0]=eating))))))|((_trans=10)&!((((((p4=1))&((philosophers[1]=thinking)))&((forks[1]=available)))&((forks[2]=available))))))|((_trans=9)&!((((((p4=2))&((philosophers[2]=thinking)))&((forks[2]=available)))&((forks[3]=available))))))|((_trans=8)&!((((((p4=3))&((philosophers[3]=thinking)))&((forks[3]=available)))&((forks[4]=available))))))|((_trans=7)&!((((((p4=4))&((philosophers[4]=thinking)))&((forks[4]=available)))&((forks[0]=available))))))|((_trans=6)&!((((((p4=0))&((philosophers[0]=thinking)))&((forks[0]=available)))&((forks[1]=available))))))|((_trans=5)&!((((p4=1))&((philosophers[1]=eating))))))|((_trans=4)&!((((p4=2))&((philosophers[2]=eating))))))|((_trans=3)&!((((p4=3))&((philosophers[3]=eating))))))|((_trans=2)&!((((p4=4))&((philosophers[4]=eating))))))|((_trans=1)&!((((p4=0))&((philosophers[0]=eating)))))) : 1; 1 : 0; esac; init(p4) := 4; next(p4) := p4; init(p3) := 3; next(p3) := p3; init(p2) := 2; next(p2) := p2; init(p1) := 1; next(p1) := p1; init(p0) := 0; next(p0) := p0; init(philosophers[4]) := thinking; next(philosophers[4]) := case (next(_trans)=49) : thinking; (next(_trans)=44) : eating; (next(_trans)=37) : eating; (next(_trans)=32) : thinking; (next(_trans)=27) : eating; (next(_trans)=22) : thinking; (next(_trans)=17) : eating; (next(_trans)=12) : thinking; (next(_trans)=7) : eating; (next(_trans)=2) : thinking; 1 : philosophers[4]; esac; init(philosophers[3]) := thinking; next(philosophers[3]) := case (next(_trans)=48) : thinking; (next(_trans)=43) : eating; (next(_trans)=38) : eating; (next(_trans)=33) : thinking; (next(_trans)=28) : eating; (next(_trans)=23) : thinking; (next(_trans)=18) : eating; (next(_trans)=13) : thinking; (next(_trans)=8) : eating; (next(_trans)=3) : thinking; 1 : philosophers[3]; esac; init(philosophers[2]) := thinking; next(philosophers[2]) := case (next(_trans)=47) : thinking; (next(_trans)=42) : eating; (next(_trans)=39) : eating; (next(_trans)=34) : thinking; (next(_trans)=29) : eating; (next(_trans)=24) : thinking; (next(_trans)=19) : eating; (next(_trans)=14) : thinking; (next(_trans)=9) : eating; (next(_trans)=4) : thinking; 1 : philosophers[2]; esac; init(philosophers[1]) := thinking; next(philosophers[1]) := case (next(_trans)=46) : thinking; (next(_trans)=41) : eating; (next(_trans)=40) : eating; (next(_trans)=35) : thinking; (next(_trans)=30) : eating; (next(_trans)=25) : thinking; (next(_trans)=20) : eating; (next(_trans)=15) : thinking; (next(_trans)=10) : eating; (next(_trans)=5) : thinking; 1 : philosophers[1]; esac; init(philosophers[0]) := thinking; next(philosophers[0]) := case (next(_trans)=50) : thinking; (next(_trans)=45) : eating; (next(_trans)=36) : eating; (next(_trans)=31) : thinking; (next(_trans)=26) : eating; (next(_trans)=21) : thinking; (next(_trans)=16) : eating; (next(_trans)=11) : thinking; (next(_trans)=6) : eating; (next(_trans)=1) : thinking; 1 : philosophers[0]; esac; init(forks[4]) := available; next(forks[4]) := case (next(_trans)=49) : available; (next(_trans)=48) : available; (next(_trans)=44) : nonavailable; (next(_trans)=43) : nonavailable; (next(_trans)=38) : nonavailable; (next(_trans)=37) : nonavailable; (next(_trans)=33) : available; (next(_trans)=32) : available; (next(_trans)=28) : nonavailable; (next(_trans)=27) : nonavailable; (next(_trans)=23) : available; (next(_trans)=22) : available; (next(_trans)=18) : nonavailable; (next(_trans)=17) : nonavailable; (next(_trans)=13) : available; (next(_trans)=12) : available; (next(_trans)=8) : nonavailable; (next(_trans)=7) : nonavailable; (next(_trans)=3) : available; (next(_trans)=2) : available; 1 : forks[4]; esac; init(forks[3]) := available; next(forks[3]) := case (next(_trans)=48) : available; (next(_trans)=47) : available; (next(_trans)=43) : nonavailable; (next(_trans)=42) : nonavailable; (next(_trans)=39) : nonavailable; (next(_trans)=38) : nonavailable; (next(_trans)=34) : available; (next(_trans)=33) : available; (next(_trans)=29) : nonavailable; (next(_trans)=28) : nonavailable; (next(_trans)=24) : available; (next(_trans)=23) : available; (next(_trans)=19) : nonavailable; (next(_trans)=18) : nonavailable; (next(_trans)=14) : available; (next(_trans)=13) : available; (next(_trans)=9) : nonavailable; (next(_trans)=8) : nonavailable; (next(_trans)=4) : available; (next(_trans)=3) : available; 1 : forks[3]; esac; init(forks[2]) := available; next(forks[2]) := case (next(_trans)=47) : available; (next(_trans)=46) : available; (next(_trans)=42) : nonavailable; (next(_trans)=41) : nonavailable; (next(_trans)=40) : nonavailable; (next(_trans)=39) : nonavailable; (next(_trans)=35) : available; (next(_trans)=34) : available; (next(_trans)=30) : nonavailable; (next(_trans)=29) : nonavailable; (next(_trans)=25) : available; (next(_trans)=24) : available; (next(_trans)=20) : nonavailable; (next(_trans)=19) : nonavailable; (next(_trans)=15) : available; (next(_trans)=14) : available; (next(_trans)=10) : nonavailable; (next(_trans)=9) : nonavailable; (next(_trans)=5) : available; (next(_trans)=4) : available; 1 : forks[2]; esac; init(forks[1]) := available; next(forks[1]) := case (next(_trans)=50) : available; (next(_trans)=46) : available; (next(_trans)=45) : nonavailable; (next(_trans)=41) : nonavailable; (next(_trans)=40) : nonavailable; (next(_trans)=36) : nonavailable; (next(_trans)=35) : available; (next(_trans)=31) : available; (next(_trans)=30) : nonavailable; (next(_trans)=26) : nonavailable; (next(_trans)=25) : available; (next(_trans)=21) : available; (next(_trans)=20) : nonavailable; (next(_trans)=16) : nonavailable; (next(_trans)=15) : available; (next(_trans)=11) : available; (next(_trans)=10) : nonavailable; (next(_trans)=6) : nonavailable; (next(_trans)=5) : available; (next(_trans)=1) : available; 1 : forks[1]; esac; init(forks[0]) := available; next(forks[0]) := case (next(_trans)=50) : available; (next(_trans)=49) : available; (next(_trans)=45) : nonavailable; (next(_trans)=44) : nonavailable; (next(_trans)=37) : nonavailable; (next(_trans)=36) : nonavailable; (next(_trans)=32) : available; (next(_trans)=31) : available; (next(_trans)=27) : nonavailable; (next(_trans)=26) : nonavailable; (next(_trans)=22) : available; (next(_trans)=21) : available; (next(_trans)=17) : nonavailable; (next(_trans)=16) : nonavailable; (next(_trans)=12) : available; (next(_trans)=11) : available; (next(_trans)=7) : nonavailable; (next(_trans)=6) : nonavailable; (next(_trans)=2) : available; (next(_trans)=1) : available; 1 : forks[0]; esac;