mtype = { ready, exec, success }; mtype pc1=ready; mtype pc2= ready; mtype pc3= ready; #define inv ( ((pc1 != ready) && (pc2 != ready) && (pc3 != ready)) || \ ((pc1 != exec) && (pc2 != exec) && (pc3 != exec)) ||\ ((pc1 != success) && (pc2 != success) && (pc3 != success)) ) active proctype process1 () { do ::atomic{ inv && (pc1 == ready) && ( ((pc2 != success) && (pc3!=success)) || ((pc2 == success) && (pc3==success)) ) -> pc1 = exec; } ::atomic{ inv && (pc1 == exec) && (pc2 != ready) && (pc3 !=ready) -> pc1 = success; } ::atomic{ inv && (pc1 == success) && ( ((pc2 == ready) && (pc3 ==ready)) || ((pc2 == success) && (pc3 ==success)) ) -> pc1 = ready; } od } active proctype process2 () { do ::atomic{ inv && (pc2 == ready) && ( ((pc1 != success) && (pc3!=success)) || ((pc1 == success) && (pc3==success)) ) -> pc2 = exec; } ::atomic{ inv && (pc2 == exec) && (pc1 != ready) && (pc3 !=ready) -> pc2 = success; } ::atomic{ inv && (pc2 == success) && ( ((pc1 == ready) && (pc3 ==ready)) || ((pc1 == success) && (pc3 ==success)) ) -> pc2 = ready; } od } active proctype process3() { do ::atomic{ inv && (pc3 == ready) && ( ((pc2 != success) && (pc1!=success)) || ((pc2 == success) && (pc1==success)) ) -> pc3 = exec; } ::atomic{ inv && (pc3 == exec) && (pc2 != ready) && (pc1 !=ready) -> pc3 = success; } ::atomic{ inv && (pc3 == success) && ( ((pc2 == ready) && (pc1 ==ready)) || ((pc2 == success) && (pc1 ==success)) ) -> pc3 = ready; } od }