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
|
Considering object completion on:
rl [enter] : go([N]) < [N] : Proc | mode : wait > => < [N] : Proc | mode :
critical > .
Transformed rule:
rl [enter] : go([N]) < [N] : V:Proc | mode : wait, Atts:AttributeSet > => < [
N] : V:Proc | mode : critical, Atts:AttributeSet > .
Considering object completion on:
rl [exit] : < [N] : Proc | mode : critical > => < [N] : Proc | mode : wait >
go([s N]) .
Transformed rule:
rl [exit] : < [N] : V:Proc | mode : critical, Atts:AttributeSet > => < [N] :
V:Proc | mode : wait, Atts:AttributeSet > go([s N]) .
Considering object completion on:
eq (< X : Proc | mode : critical > C) |= inCrit(X) = true .
Transformed equation:
eq (< X : V:Proc | mode : critical, Atts:AttributeSet > C) |= inCrit(X) =
true .
Considering object completion on:
eq (< X : Proc | mode : critical > < Y : Proc | mode : critical > C) |=
twoInCrit = true .
Transformed equation:
eq (< X : V:Proc | mode : critical, Atts:AttributeSet > < Y : V2:Proc | mode
: critical, Atts2:AttributeSet > C) |= twoInCrit = true .
op _`,_ left-identity collapse from AttributeSet to Attribute is unequal.
op __ left-identity collapse from [State] to State is unequal.
op __ left-identity collapse from TransitionList to Transition is unequal.
op __ right-identity collapse from TransitionList to Transition is unequal.
==========================================
reduce in CHECK-RROBIN-5 : modelCheck(init, []~ twoInCrit) .
ModelChecker: Property automaton has 2 states.
ModelCheckerSymbol: Examined 10 system states.
rewrites: 52
result Bool: true
==========================================
reduce in CHECK-RROBIN-5 : modelCheck(init, []guaranteedReentrance) .
ModelChecker: Property automaton has 52 states.
ModelCheckerSymbol: Examined 10 system states.
rewrites: 2263
result Bool: true
==========================================
reduce in CHECK-RROBIN-5 : modelCheck(init, [](inCrit([1]) -> O O O inCrit([
1]))) .
ModelChecker: Property automaton has 5 states.
ModelCheckerSymbol: Examined 10 system states.
rewrites: 67
result ModelCheckResult: counterexample({go([0]) < [0] : Proc | mode : wait > <
[1] : Proc | mode : wait > < [2] : Proc | mode : wait > < [3] : Proc | mode
: wait > < [4] : Proc | mode : wait >, 'enter} {< [0] : Proc | mode :
critical > < [1] : Proc | mode : wait > < [2] : Proc | mode : wait > < [3]
: Proc | mode : wait > < [4] : Proc | mode : wait >, 'exit} {go([1]) < [0]
: Proc | mode : wait > < [1] : Proc | mode : wait > < [2] : Proc | mode :
wait > < [3] : Proc | mode : wait > < [4] : Proc | mode : wait >, 'enter} {
< [0] : Proc | mode : wait > < [1] : Proc | mode : critical > < [2] : Proc
| mode : wait > < [3] : Proc | mode : wait > < [4] : Proc | mode : wait >,
'exit} {go([2]) < [0] : Proc | mode : wait > < [1] : Proc | mode : wait > <
[2] : Proc | mode : wait > < [3] : Proc | mode : wait > < [4] : Proc | mode
: wait >, 'enter} {< [0] : Proc | mode : wait > < [1] : Proc | mode : wait
> < [2] : Proc | mode : critical > < [3] : Proc | mode : wait > < [4] :
Proc | mode : wait >, 'exit}, {go([3]) < [0] : Proc | mode : wait > < [1] :
Proc | mode : wait > < [2] : Proc | mode : wait > < [3] : Proc | mode :
wait > < [4] : Proc | mode : wait >, 'enter} {< [0] : Proc | mode : wait >
< [1] : Proc | mode : wait > < [2] : Proc | mode : wait > < [3] : Proc |
mode : critical > < [4] : Proc | mode : wait >, 'exit} {go([4]) < [0] :
Proc | mode : wait > < [1] : Proc | mode : wait > < [2] : Proc | mode :
wait > < [3] : Proc | mode : wait > < [4] : Proc | mode : wait >, 'enter} {
< [0] : Proc | mode : wait > < [1] : Proc | mode : wait > < [2] : Proc |
mode : wait > < [3] : Proc | mode : wait > < [4] : Proc | mode : critical
>, 'exit} {go([0]) < [0] : Proc | mode : wait > < [1] : Proc | mode : wait
> < [2] : Proc | mode : wait > < [3] : Proc | mode : wait > < [4] : Proc |
mode : wait >, 'enter} {< [0] : Proc | mode : critical > < [1] : Proc |
mode : wait > < [2] : Proc | mode : wait > < [3] : Proc | mode : wait > < [
4] : Proc | mode : wait >, 'exit} {go([1]) < [0] : Proc | mode : wait > < [
1] : Proc | mode : wait > < [2] : Proc | mode : wait > < [3] : Proc | mode
: wait > < [4] : Proc | mode : wait >, 'enter} {< [0] : Proc | mode : wait
> < [1] : Proc | mode : critical > < [2] : Proc | mode : wait > < [3] :
Proc | mode : wait > < [4] : Proc | mode : wait >, 'exit} {go([2]) < [0] :
Proc | mode : wait > < [1] : Proc | mode : wait > < [2] : Proc | mode :
wait > < [3] : Proc | mode : wait > < [4] : Proc | mode : wait >, 'enter} {
< [0] : Proc | mode : wait > < [1] : Proc | mode : wait > < [2] : Proc |
mode : critical > < [3] : Proc | mode : wait > < [4] : Proc | mode : wait
>, 'exit})
Bye.
|
