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
|
# while true do begin
# <noncritical section>
# b_i := true;
# while k != i do begin
# while b_j do skip;
# k := i;
# end;
# <critical section>
# b_i := false;
# end;
var1 $;
var2 PC1', PC1'', PC1''', PC2', PC2'', PC2''', b1, b2, K;
pred p1_at_line_1(var1 t) = t notin PC1' & t notin PC1'' & t notin PC1''';
pred p1_at_line_2(var1 t) = t notin PC1' & t notin PC1'' & t in PC1''';
pred p1_at_line_3(var1 t) = t notin PC1' & t in PC1'' & t notin PC1''';
pred p1_at_line_4(var1 t) = t notin PC1' & t in PC1'' & t in PC1''';
pred p1_at_line_5(var1 t) = t in PC1' & t notin PC1'' & t notin PC1''';
pred p1_at_line_6(var1 t) = t in PC1' & t notin PC1'' & t in PC1''';
pred p1_at_line_7(var1 t) = t in PC1' & t in PC1'' & t notin PC1''';
pred p2_at_line_1(var1 t) = t notin PC2' & t notin PC2'' & t notin PC2''';
pred p2_at_line_2(var1 t) = t notin PC2' & t notin PC2'' & t in PC2''';
pred p2_at_line_3(var1 t) = t notin PC2' & t in PC2'' & t notin PC2''';
pred p2_at_line_4(var1 t) = t notin PC2' & t in PC2'' & t in PC2''';
pred p2_at_line_5(var1 t) = t in PC2' & t notin PC2'' & t notin PC2''';
pred p2_at_line_6(var1 t) = t in PC2' & t notin PC2'' & t in PC2''';
pred p2_at_line_7(var1 t) = t in PC2' & t in PC2'' & t notin PC2''';
pred b1_false(var1 t) = t notin b1;
pred b1_true(var1 t) = t in b1;
pred b2_false(var1 t) = t notin b2;
pred b2_true(var1 t) = t in b2;
pred K_is_2(var1 t) = t notin K;
pred K_is_1(var1 t) = t in K;
pred unchanged(var1 t, var2 Track) = t in Track <=> t+1 in Track;
pred unchanged_PC1(var1 t) = unchanged(t, PC1') &
unchanged(t, PC1'') &
unchanged(t, PC1''');
pred unchanged_PC2(var1 t) = unchanged(t, PC2') &
unchanged(t, PC2'') &
unchanged(t, PC2''');
pred unchanged_K(var1 t) = unchanged(t, K);
pred unchanged_b1(var1 t) = unchanged(t, b1);
pred unchanged_b2(var1 t) = unchanged(t, b2);
pred unchanged_vars(var1 t) = unchanged_K(t) & unchanged_b1(t) & unchanged_b2(t);
pred p1_proc_step(var1 t) =
(p1_at_line_1(t) => p1_at_line_2(t+1) & unchanged_vars(t)) &
(p1_at_line_2(t) => p1_at_line_3(t+1) & b1_true(t+1) &
unchanged_K(t) & unchanged_b2(t)) &
(p1_at_line_3(t) => (unchanged_vars(t) &
(K_is_1(t) =>
p1_at_line_6(t+1)) &
(K_is_2(t) =>
p1_at_line_4(t+1)))) &
(p1_at_line_4(t) => (unchanged_vars(t) &
(b2_false(t) =>
p1_at_line_5(t+1)) &
(~b2_false(t) =>
p1_at_line_4(t+1)))) &
(p1_at_line_5(t) => K_is_1(t+1) &
unchanged_b1(t) & unchanged_b2(t) &
p1_at_line_3(t+1)) &
(p1_at_line_6(t) => p1_at_line_7(t+1) & unchanged_vars(t)) &
(p1_at_line_7(t) => p1_at_line_1(t+1) & b1_false(t+1) &
unchanged_K(t) & unchanged_b2(t));
pred p2_proc_step(var1 t) =
(p2_at_line_1(t) => p2_at_line_2(t+1) & unchanged_vars(t)) &
(p2_at_line_2(t) => p2_at_line_3(t+1) & b2_true(t+1) &
unchanged_K(t) & unchanged_b1(t)) &
(p2_at_line_3(t) => (unchanged_vars(t) &
(K_is_2(t) =>
p2_at_line_6(t+1)) &
(K_is_1(t) =>
p2_at_line_4(t+1)))) &
(p2_at_line_4(t) => (unchanged_vars(t) &
(b1_false(t) =>
p2_at_line_5(t+1)) &
(~b1_false(t) =>
p2_at_line_4(t+1)))) &
(p2_at_line_5(t) => K_is_2(t+1) &
unchanged_b1(t) & unchanged_b2(t) &
p2_at_line_3(t+1)) &
(p2_at_line_6(t) => p2_at_line_7(t+1) & unchanged_vars(t)) &
(p2_at_line_7(t) => p2_at_line_1(t+1) & b2_false(t+1) &
unchanged_K(t) & unchanged_b1(t));
pred Valid = p1_at_line_1(0) & p2_at_line_1(0) & b1_false(0) & b2_false(0) & K_is_2(0) &
(all1 t: t < $ =>
((p1_proc_step(t) & unchanged_PC2(t))
| (p2_proc_step(t) & unchanged_PC1(t))));
#Mutual exclusion
Valid => all1 p: (p<=$ => ~(p1_at_line_6(p) & p2_at_line_6(p)));
|
