File size: 3,632 Bytes
99d3d5f | 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 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 | ------------------------------ MODULE NArrayLogic ------------------------------
EXTENDS Naturals, Sequences, TLC
CONSTANT N
ASSUME N \in Nat /\ N > 0
VARIABLES a, p, c, d, t, comp, r, stage, worm, sealed
Partition(x) ==
LET k == N \div 2 IN
[left |-> [i \in 1..k |-> x[i]],
right |-> [i \in (k+1)..N |-> x[i]]]
Product(pp) ==
LET k == N \div 2 IN
[i \in 1..N |->
IF i <= k THEN pp.left[i] ELSE pp.right[i]]
Difference(x, y) ==
[i \in 1..N |-> IF x[i] >= y[i] THEN x[i] - y[i] ELSE 0]
Transform(x) ==
[i \in 1..N |-> x[i] + 1]
Composition(x) ==
[i \in 1..N |-> x[i] * 2]
Closure(pp) ==
Product(pp)
Invariant(x) ==
\A i \in 1..N-1: x[i] <= x[i+1]
vars == <<a, p, c, d, t, comp, r, stage, worm, sealed>>
Terminal == stage \in {"sealed", "failed"}
Init ==
/\ a = [i \in 1..N |-> 0]
/\ p = Partition(a)
/\ c = Product(p)
/\ d = Difference(a, c)
/\ t = Transform(d)
/\ comp = Composition(t)
/\ r = Closure(p)
/\ stage = "start"
/\ worm = <<>>
/\ sealed = FALSE
RealNext ==
\/ /\ stage = "start"
/\ stage' = "partition"
/\ p' = Partition(a)
/\ UNCHANGED <<a, c, d, t, comp, r, worm, sealed>>
\/ /\ stage = "partition"
/\ stage' = "product"
/\ c' = Product(p)
/\ UNCHANGED <<a, p, d, t, comp, r, worm, sealed>>
\/ /\ stage = "product"
/\ stage' = "difference"
/\ d' = Difference(a, c)
/\ UNCHANGED <<a, p, c, t, comp, r, worm, sealed>>
\/ /\ stage = "difference"
/\ stage' = "transform"
/\ t' = Transform(d)
/\ UNCHANGED <<a, p, c, d, comp, r, worm, sealed>>
\/ /\ stage = "transform"
/\ stage' = "composition"
/\ comp' = Composition(t)
/\ UNCHANGED <<a, p, c, d, t, r, worm, sealed>>
\/ /\ stage = "composition"
/\ stage' = "closure"
/\ r' = Closure(p)
/\ UNCHANGED <<a, p, c, d, t, comp, worm, sealed>>
\/ /\ stage = "closure"
/\ stage' = "invariant"
/\ a' = r
/\ worm' = Append(worm, [op |-> "close", input |-> a, output |-> r])
/\ UNCHANGED <<p, c, d, t, comp, r, sealed>>
\/ /\ stage = "invariant"
/\ Invariant(a)
/\ stage' = "sealed"
/\ sealed' = TRUE
/\ worm' = Append(worm, [op |-> "seal", input |-> a, output |-> a])
/\ UNCHANGED <<a, p, c, d, t, comp, r>>
\/ /\ stage = "invariant"
/\ ~Invariant(a)
/\ stage' = "failed"
/\ worm' = Append(worm, [op |-> "fail", input |-> a, output |-> a])
/\ UNCHANGED <<a, p, c, d, t, comp, r, sealed>>
\* Absorbing self-loop once terminal, so the machine is total: a
\* terminal `stage` is a resting state, not a genuine TLC deadlock.
\* Kept out of `RealNext` (and so out of the `WF_vars(RealNext)`
\* fairness obligation below): a fairness requirement on an action
\* whose own effect is `UNCHANGED vars` can never be honestly
\* satisfied once it is the only action left enabled.
Next ==
\/ RealNext
\/ /\ Terminal
/\ UNCHANGED vars
ArrayType == [1..N -> Nat]
TypeOK ==
/\ a \in ArrayType
/\ p \in [left: [1..(N \div 2) -> Nat], right: [(N \div 2 + 1)..N -> Nat]]
/\ c \in ArrayType
/\ d \in ArrayType
/\ t \in ArrayType
/\ comp \in ArrayType
/\ r \in ArrayType
/\ stage \in
{"start", "partition", "product", "difference", "transform",
"composition", "closure", "invariant", "sealed", "failed"}
/\ sealed \in BOOLEAN
/\ worm \in Seq([op: STRING, input: ArrayType, output: ArrayType])
EventuallyTerminal == <>Terminal
Spec == Init /\ [][Next]_vars /\ WF_vars(RealNext)
=============================================================================
|