1Maude> ==========================================
2reduce in CHECK : modelCheck(initial, []~ (enterCrit(1) /\ enterCrit(2))) .
3rewrites: 1048
4result Bool: true
5==========================================
6reduce in CHECK : modelCheck(initial, []<> exec(1) -> []<> enterCrit(1)) .
7rewrites: 100
8result ModelCheckResult: counterexample({{[1,repeat 'c1 := 0 ; while 'c2 = 0 do
9    if 'turn = 2 then 'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ;
10    crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [2,repeat 'c2 := 0 ; while
11    'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 :=
12    0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,1] ['c2,1] [
13    'turn,1],0},unlabeled} {{[1,'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then
14    'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2
15    ; 'c1 := 1 ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1
16    := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ;
17    'c1 := 1 ; rem forever] | [2,repeat 'c2 := 0 ; while 'c1 = 0 do if 'turn =
18    1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ;
19    'turn := 1 ; 'c2 := 1 ; rem forever],['c1,1] ['c2,1] ['turn,1],1},
20    unlabeled} {{[1,while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn =
21    2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem ; repeat
22    'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn = 2 do
23    skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [
24    2,repeat 'c2 := 0 ; while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while
25    'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem
26    forever],['c1,0] ['c2,1] ['turn,1],1},unlabeled} {{[1,while 'c2 = 0 do if
27    'turn = 2 then 'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ;
28    crit ; 'turn := 2 ; 'c1 := 1 ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if
29    'turn = 2 then 'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ;
30    crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [2,'c2 := 0 ; while 'c1 = 0
31    do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi od
32    ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ; while 'c1 = 0 do
33    if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi od ;
34    crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,1] ['turn,1],2},
35    unlabeled} {{[1,while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn =
36    2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem ; repeat
37    'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn = 2 do
38    skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [
39    2,while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od
40    ; 'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ;
41    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
42    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,
43    0] ['turn,1],2},unlabeled} {{[1,if 'turn = 2 then 'c1 := 1 ; while 'turn =
44    2 do skip od ; 'c1 := 0 fi ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
45    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
46    ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
47    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
48    ; rem forever] | [2,while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while
49    'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem
50    ; repeat 'c2 := 0 ; while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while
51    'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem
52    forever],['c1,0] ['c2,0] ['turn,1],1},unlabeled} {{[1,while 'c2 = 0 do if
53    'turn = 2 then 'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ;
54    crit ; 'turn := 2 ; 'c1 := 1 ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if
55    'turn = 2 then 'c1 := 1 ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ;
56    crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [2,while 'c1 = 0 do if 'turn
57    = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ;
58    'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ; while 'c1 = 0 do if 'turn =
59    1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi od ; crit ;
60    'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,0] ['turn,1],1},
61    unlabeled} {{[1,while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn =
62    2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem ; repeat
63    'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ; while 'turn = 2 do
64    skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1 ; rem forever] | [
65    2,if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 fi ;
66    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
67    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ;
68    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
69    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,
70    0] ['turn,1],2},unlabeled} {{[1,while 'c2 = 0 do if 'turn = 2 then 'c1 := 1
71    ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 :=
72    1 ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
73    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
74    ; rem forever] | [2,'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 ;
75    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
76    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ;
77    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
78    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,
79    0] ['turn,1],2},unlabeled}, {{[1,if 'turn = 2 then 'c1 := 1 ; while 'turn =
80    2 do skip od ; 'c1 := 0 fi ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
81    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
82    ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
83    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
84    ; rem forever] | [2,'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 ;
85    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
86    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ;
87    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
88    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,
89    0] ['turn,1],1},unlabeled} {{[1,while 'c2 = 0 do if 'turn = 2 then 'c1 := 1
90    ; while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 :=
91    1 ; rem ; repeat 'c1 := 0 ; while 'c2 = 0 do if 'turn = 2 then 'c1 := 1 ;
92    while 'turn = 2 do skip od ; 'c1 := 0 fi od ; crit ; 'turn := 2 ; 'c1 := 1
93    ; rem forever] | [2,'c2 := 1 ; while 'turn = 1 do skip od ; 'c2 := 0 ;
94    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
95    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem ; repeat 'c2 := 0 ;
96    while 'c1 = 0 do if 'turn = 1 then 'c2 := 1 ; while 'turn = 1 do skip od ;
97    'c2 := 0 fi od ; crit ; 'turn := 1 ; 'c2 := 1 ; rem forever],['c1,0] ['c2,
98    0] ['turn,1],1},unlabeled})
99==========================================
100reduce in CHECK : modelCheck(initial, []<> exec(1) /\ []<> exec(2) -> []<>
101    enterCrit(1) /\ []<> enterCrit(2)) .
102rewrites: 1319
103result Bool: true
104Maude> Bye.
105