-
Notifications
You must be signed in to change notification settings - Fork 1
/
XfromNAND2.tla
84 lines (60 loc) · 2.06 KB
/
XfromNAND2.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
75
76
77
78
79
80
81
82
83
84
----------------------------- MODULE XfromNAND2 -----------------------------
EXTENDS TLC, Naturals, Integers, Sequences
(* --algorithm nand
variables
CircuitState = << >>;
Wires = { << "input", << 0, 0, 1, 1 >> >>, << "input", << 0, 1, 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])
>>
RECURSIVE compute(_)
compute(state) ==
IF state[1] = "input"
THEN state[2]
ELSE nand(compute(state[2]), compute(state[3]))
end define;
begin
while TRUE do
with wirePair \in (Wires \X Wires) do
CircuitState := << "nand" >> \o wirePair;
print CircuitState;
Wires := Wires \union { CircuitState };
end with;
end while;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES CircuitState, Wires
(* 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])
>>
RECURSIVE compute(_)
compute(state) ==
IF state[1] = "input"
THEN state[2]
ELSE nand(compute(state[2]), compute(state[3]))
vars == << CircuitState, Wires >>
Init == (* Global variables *)
/\ CircuitState = << >>
/\ Wires = { << "input", << 0, 0, 1, 1 >> >>, << "input", << 0, 1, 0, 1 >> >> }
Next == \E wirePair \in (Wires \X Wires):
/\ CircuitState' = << "nand" >> \o wirePair
/\ PrintT(CircuitState')
/\ Wires' = (Wires \union { CircuitState' })
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
Invariant == (Len(CircuitState) = 0) \/ (compute(CircuitState) /= << 0, 1, 1, 0 >>)
=============================================================================
\* Modification History
\* Last modified Wed Jun 27 16:43:40 EDT 2018 by adampalay
\* Last modified Thu Jun 21 17:18:46 EDT 2018 by emanuel
\* Created Wed Jun 20 15:31:47 EDT 2018 by adampalay