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