Model inventory prediction, cache reuse and crafting ownership

src/test/tla/Append.tla

@@ -0,0 +1,66 @@
+------------------------------ MODULE Append ------------------------------
+
+EXTENDS Integers, Words
+CONSTANTS Mode, Clamp, Capacity, Certify
+
+StackMax == 64
+Min(a, b) == IF a < b THEN a ELSE b
+
+VARIABLES size, before, actual, count, reply, finished, result, expected
+appendvars == <<size, before, actual, count, reply, finished, result, expected>>
+
+Sizes   == {1, 63, 64, 65, 127, 128, 129, 2147483646}
+Amounts == {1, 64, 65, 128}
+
+Probe == IF count <= StackMax THEN StackMax + 1 ELSE count
+Large(n) == Capacity > StackMax /\ Add32(n, count) > StackMax
+Limit == IF reply < Probe THEN Add32(actual, reply) ELSE Capacity
+
+Native(n) ==
+    IF n >= Capacity
+    THEN [size |-> n, left |-> count]
+    ELSE
+        LET merged   == Add32(n, count)
+            accepted == IF Large(n) THEN reply ELSE count
+            limit    == IF Large(n) THEN Limit ELSE Capacity
+        IN
+            IF accepted = 0
+            THEN [size |-> n, left |-> count]
+            ELSE IF merged > limit
+            THEN [size |-> limit, left |-> Add32(merged, -limit)]
+            ELSE [size |-> merged, left |-> 0]
+
+Recorded ==
+    IF Native(before).left = 0 /\ Native(before).size >= before /\ before > StackMax
+    THEN Native(before).size - before = count
+    ELSE FALSE
+LineLimit == IF Clamp THEN Min(Capacity, Limit) ELSE Limit
+Fast ==
+    IF Mode = "batch"
+    THEN count <= StackMax /\ size <= Capacity - count /\
+         (~Large(size) \/ ~Certify \/ reply = Probe)
+    ELSE Recorded /\ size >= Native(before).size /\ size > StackMax /\
+         size <= LineLimit - count
+
+AppendInit ==
+    /\ size \in Sizes /\ before \in Sizes /\ actual \in Sizes
+    /\ actual <= Capacity
+    /\ count \in Amounts
+    /\ reply \in {-1, 0, 1, Probe - 1, Probe}
+    /\ finished = FALSE
+    /\ result = [size |-> size, left |-> count] /\ expected = result
+
+AppendNext ==
+    /\ ~finished
+    /\ expected' = Native(size)
+    /\ result' =
+        IF Fast
+        THEN [size |-> size + count, left |-> 0]
+        ELSE Native(size)
+    /\ finished' = TRUE
+    /\ UNCHANGED <<size, before, actual, count, reply>>
+
+AppendSpec == AppendInit /\ [][AppendNext]_appendvars
+AppendParity == finished => result = expected
+
+=============================================================================

src/test/tla/AppendBatch.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION AppendSpec
+CONSTANTS
+    Capacity = 128
+    Mode = "batch"
+    Clamp = TRUE
+    Certify = TRUE
+INVARIANT AppendParity
+CHECK_DEADLOCK FALSE

src/test/tla/AppendMemo.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION AppendSpec
+CONSTANTS
+    Capacity = 128
+    Mode = "memo"
+    Clamp = TRUE
+    Certify = TRUE
+INVARIANT AppendParity
+CHECK_DEADLOCK FALSE

src/test/tla/Blocked.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 128
+    Counts <- FlowCounts
+    Stored <- SmallStored
+    MaxFlows = 1
+    Sorted = TRUE
+    Rollback = TRUE
+    Certify = TRUE
+    Debt = 0
+    Blocked = {2}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE

src/test/tla/Cache.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 4 ExactCount = TRUE Fresh = TRUE
+INVARIANTS Parity
+CHECK_DEADLOCK FALSE

src/test/tla/Cache.tla

@@ -0,0 +1,54 @@
+------------------------------ MODULE Cache ------------------------------
+
+EXTENDS Integers, Sequences, TLC
+CONSTANTS MaxSteps, ExactCount, Fresh
+
+Slots  == {0, 1}
+Items  == {0, 1}
+Counts == {1, 64}
+Keys   == Slots \X Items \X Counts
+Empty  == [key \in Keys |-> -1]
+
+Truth(slot, item, count, epoch) == (slot + item + count + epoch) % (count + 1)
+Key(slot, item, count) == <<slot, item, IF ExactCount THEN count ELSE 1>>
+
+VARIABLES epoch, cache, steps, native, candidate, history
+vars == <<epoch, cache, steps, native, candidate, history>>
+
+Init ==
+    /\ epoch = 0 /\ cache = Empty /\ steps = 0
+    /\ native = <<>> /\ candidate = <<>> /\ history = <<>>
+
+Query(slot, item, count) ==
+    /\ steps < MaxSteps
+    /\ LET key      == Key(slot, item, count)
+           expected == Truth(slot, item, count, epoch)
+           result   == IF cache[key] = -1 THEN expected ELSE cache[key]
+       IN
+           /\ cache' = [cache EXCEPT ![key] = result]
+           /\ native' = Append(native, expected)
+           /\ candidate' = Append(candidate, result)
+           /\ history' = Append(history, <<1, slot, item, count, expected>>)
+    /\ steps' = steps + 1
+    /\ UNCHANGED epoch
+
+Snapshot ==
+    /\ steps < MaxSteps
+    /\ epoch' = 1 - epoch
+    /\ cache' = IF Fresh THEN Empty ELSE cache
+    /\ steps' = steps + 1
+    /\ history' = Append(history, <<0>>)
+    /\ UNCHANGED <<native, candidate>>
+
+Next ==
+    Snapshot \/
+    (\E slot \in Slots, item \in Items, count \in Counts : Query(slot, item, count))
+
+Parity == native = candidate
+
+JavaParity(commands) == Assert(FALSE, "Java binding was not loaded")
+Bound == JavaParity(history)
+
+Spec == Init /\ [][Next]_vars
+
+=============================================================================

src/test/tla/CacheJava.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 4 ExactCount = TRUE Fresh = TRUE
+INVARIANTS Parity Bound
+CHECK_DEADLOCK FALSE

src/test/tla/Compact.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 128
+    Counts <- FlowCounts
+    Stored <- SmallStored
+    MaxFlows = 2
+    Sorted = TRUE
+    Rollback = TRUE
+    Certify = TRUE
+    Debt = 1
+    Blocked = {}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE

src/test/tla/Longs.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    OwnerCount = 2
+    RowCount = 1
+    KeyCount = 1
+    Values <- EdgeValues
+    MaxWrites = 2
+    HeapLimit = 12
+    Detach = TRUE
+    Reverse = FALSE
+    Wrap = TRUE
+INVARIANTS Parity Ownership TypeOK
+CHECK_DEADLOCK FALSE

src/test/tla/NoCert.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 128
+    Counts <- FlowCounts
+    Stored <- SmallStored
+    MaxFlows = 2
+    Sorted = TRUE
+    Rollback = TRUE
+    Certify = FALSE
+    Debt = 1
+    Blocked = {}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE

src/test/tla/NoClamp.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION AppendSpec
+CONSTANTS
+    Capacity = 128
+    Mode = "memo"
+    Clamp = FALSE
+    Certify = TRUE
+INVARIANT AppendParity
+CHECK_DEADLOCK FALSE

src/test/tla/NoCount.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 4 ExactCount = FALSE Fresh = TRUE
+INVARIANTS Parity
+CHECK_DEADLOCK FALSE

src/test/tla/NoDetach.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    OwnerCount = 2
+    RowCount = 2
+    KeyCount = 2
+    Values <- BasicValues
+    MaxWrites = 2
+    HeapLimit = 12
+    Detach = FALSE
+    Reverse = FALSE
+    Wrap = TRUE
+INVARIANTS Parity Ownership TypeOK
+CHECK_DEADLOCK FALSE

src/test/tla/NoFresh.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CONSTANTS MaxSteps = 4 ExactCount = TRUE Fresh = FALSE
+INVARIANTS Parity
+CHECK_DEADLOCK FALSE

src/test/tla/NoOrder.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    OwnerCount = 2
+    RowCount = 2
+    KeyCount = 2
+    Values <- BasicValues
+    MaxWrites = 2
+    HeapLimit = 12
+    Detach = TRUE
+    Reverse = TRUE
+    Wrap = TRUE
+INVARIANTS Parity Ownership TypeOK
+CHECK_DEADLOCK FALSE

src/test/tla/NoProof.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION AppendSpec
+CONSTANTS
+    Capacity = 128
+    Mode = "batch"
+    Clamp = TRUE
+    Certify = FALSE
+INVARIANT AppendParity
+CHECK_DEADLOCK FALSE

src/test/tla/NoRollback.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 128
+    Counts <- FlowCounts
+    Stored <- SmallStored
+    MaxFlows = 2
+    Sorted = TRUE
+    Rollback = FALSE
+    Certify = TRUE
+    Debt = 0
+    Blocked = {}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE

src/test/tla/NoSort.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 128
+    Counts <- FlowCounts
+    Stored <- SmallStored
+    MaxFlows = 2
+    Sorted = FALSE
+    Rollback = TRUE
+    Certify = TRUE
+    Debt = 0
+    Blocked = {}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE

src/test/tla/NoWrap.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    OwnerCount = 2
+    RowCount = 1
+    KeyCount = 1
+    Values <- EdgeValues
+    MaxWrites = 2
+    HeapLimit = 12
+    Detach = TRUE
+    Reverse = FALSE
+    Wrap = FALSE
+INVARIANTS Parity Ownership TypeOK
+CHECK_DEADLOCK FALSE

src/test/tla/Overflow.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+CONSTANTS
+    Capacity = 2147483647
+    Counts <- FlowCounts
+    Stored <- EdgeStored
+    MaxFlows = 2
+    Sorted = TRUE
+    Rollback = TRUE
+    Certify = TRUE
+    Debt = 0
+    Blocked = {}
+INVARIANTS Parity BatchParity
+CHECK_DEADLOCK FALSE