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
105
106
107
108
109
110
111
112
|
% Preamble --------------
DATATYPE UNIT = Unit END;
DATATYPE BOOL = Truth | Falsity END;
% Decls --------------
resource$type: TYPE;
process$type: TYPE;
null: resource$type;
S$elem$type: TYPE = process$type;
S$t$type: TYPE;
S$empty: S$t$type;
S$mem:(S$elem$type, S$t$type) -> BOOL;
S$add:(S$elem$type, S$t$type) -> S$t$type;
S$remove:(S$elem$type, S$t$type) -> S$t$type;
S$cardinality:(S$t$type) -> INT;
S$mem_empty: BOOLEAN = (FORALL (e: S$elem$type): (NOT ((S$mem((e), (S$empty))) =
(Truth))));
ASSERT S$mem_empty;
S$mem_add: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type):
((S$mem((x), (S$add((y), (s))))) = (IF (((x) = (y)) OR
((S$mem((x), (s))) =
(Truth))) THEN
(Truth) ELSE
(Falsity) ENDIF)));
ASSERT S$mem_add;
S$mem_remove: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type):
((S$mem((x), (S$remove((y), (s))))) = (IF ((NOT
((x) =
(y))) AND
((S$mem(
(x), (s))) =
(Truth))) THEN
(Truth) ELSE
(Falsity) ENDIF)));
ASSERT S$mem_remove;
S$card_empty: BOOLEAN = ((S$cardinality((S$empty))) = (0));
ASSERT S$card_empty;
S$card_zero: BOOLEAN = (FORALL (s: S$t$type): (((S$cardinality((s))) = (0)) =>
((s) = (S$empty))));
ASSERT S$card_zero;
S$card_non_negative: BOOLEAN = (FORALL (s: S$t$type): ((S$cardinality((s))) >=
(0)));
ASSERT S$card_non_negative;
S$card_add: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
(S$add(
(x), (s))))) =
(IF ((S$mem(
(x), (s))) =
(Truth)) THEN
(S$cardinality(
(s))) ELSE (
(S$cardinality(
(s))) +
(1)) ENDIF)));
ASSERT S$card_add;
S$card_remove: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
(S$remove(
(x), (s))))) =
(IF (
(S$mem(
(x), (s))) =
(Truth)) THEN (
(S$cardinality(
(s))) -
(1)) ELSE
(S$cardinality(
(s))) ENDIF)));
ASSERT S$card_remove;
% Var Decls --------------
count: ARRAY resource$type OF INT;
ref: ARRAY process$type OF resource$type;
valid: ARRAY resource$type OF BOOL;
destroy$r: resource$type;
valid$1: ARRAY resource$type OF BOOL;
% Asserts --------------
ASSERT (NOT ((FORALL (p: process$type): ((NOT
(
(
(ref)[
(p)]) =
(null))) =>
((
(valid)[
(
(ref)[
(p)])]) =
(Truth)))) =>
((NOT ((destroy$r) = (null))) =>
((((valid)[(destroy$r)]) = (Truth)) =>
((((count)[(destroy$r)]) = (0)) =>
(((valid$1) = ((valid) WITH [(destroy$r)] :=
(Falsity))) => (FORALL
(
p: process$type):
(
(NOT
(
(
(ref)[
(p)]) =
(null))) =>
(
(
(valid$1)[
(
(ref)[
(p)])]) =
(Truth))))))))));
CHECKSAT;
|