-
Notifications
You must be signed in to change notification settings - Fork 1
/
XfromNAND.tla
74 lines (58 loc) · 1.77 KB
/
XfromNAND.tla
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
-------------------------- MODULE XfromNAND --------------------------
EXTENDS TLC, Naturals, Integers, FiniteSets
(* --algorithm fromNAND
variables S = { << 0, 0, 1, 1 >>, << 0, 1, 0, 1 >> };
Goal = {<<0, 1, 1, 0>>, <<0, 0, 0, 1>>};
define
nand_elem(bit1, bit2) == 1 - bit1 * bit2
nand(row1, row2) == <<
nand_elem(row1[1], row2[1]),
nand_elem(row1[2], row2[2]),
nand_elem(row1[3], row2[3]),
nand_elem(row1[4], row2[4])
>>
end define;
begin
while TRUE do
assert ~( Goal \subseteq S /\ S \subseteq Goal);
with x \in S do
with y \in S do
either
S := S \union {nand(x, y)};
or
S := S \ {x};
or
S := S \ {y};
end either;
end with;
end with;
end while;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES S, Goal
(* define statement *)
nand_elem(bit1, bit2) == 1 - bit1 * bit2
nand(row1, row2) == <<
nand_elem(row1[1], row2[1]),
nand_elem(row1[2], row2[2]),
nand_elem(row1[3], row2[3]),
nand_elem(row1[4], row2[4])
>>
vars == << S, Goal >>
Init == (* Global variables *)
/\ S = { << 0, 0, 1, 1 >>, << 0, 1, 0, 1 >> }
/\ Goal = {<<0, 1, 1, 0>>, <<0, 0, 0, 1>>}
Next == /\ Assert(~( Goal \subseteq S /\ S \subseteq Goal),
"Failure of assertion at line 22, column 5.")
/\ \E x \in S:
\E y \in S:
\/ /\ S' = (S \union {nand(x, y)})
\/ /\ S' = S \ {x}
\/ /\ S' = S \ {y}
/\ Goal' = Goal
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
=============================================================================
\* Modification History
\* Last modified Mon Jun 25 16:46:04 EDT 2018 by adampalay
\* Created Mon Jun 11 15:52:06 EDT 2018 by adampalay