Add Hillel Wayne's two-thread counter as a first refinement example

README.md

@@ -45,6 +45,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [The Coffee Can Bean Problem](specifications/CoffeeCan)                                             | Andrew Helwer                                       |    ✔     |      ✔      |         |     ✔     |    ✔     |
 | [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a)                | Stephan Merz, Leslie Lamport, Markus Kuppe          |    ✔     |      ✔      |   (✔)   |     ✔     |          |
 | [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle)                                           | Florian Schanda                                     |    ✔     |             |         |     ✔     |    ✔     |
+| [Specification Refinement](specifications/SpecificationRefinement)                                  | Hillel Wayne                                        |    ✔     |      ✔      |         |     ✔     |          |
 | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz                        |          |      ✔      |    ✔    |     ✔     |          |
 | [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                                      |          |      ✔      |    ✔    |     ✔     |    ✔     |
 | [Byzantizing Paxos by Refinement](specifications/byzpaxos)                                          | Leslie Lamport                                      |          |      ✔      |    ✔    |     ✔     |          |

specifications/SpecificationRefinement/README.md

@@ -0,0 +1,8 @@
+# Specification Refinement
+
+This example accompanies Hillel Wayne's blog post [*Specification Refinement*](https://www.hillelwayne.com/post/refinement/), which introduces refinement mappings in TLA⁺ using a two-thread counter:
+
+- [`abstract.tla`](abstract.tla) (`abstract.cfg`): The high-level specification where two threads atomically increment a shared `counter` and transition from `"start"` to `"done"`.
+- [`bad.tla`](bad.tla) (`bad.cfg`): A lower-level specification that splits the increment into two non-atomic steps (`GetCounter` and `IncCounter`) using a thread-local variable `tmp` and an intermediate state `"inc"`. Checking `PROPERTY Refinement` with TLC fails with a liveness/temporal property violation, exhibiting the race condition where both threads read `0` and both write `1`.
+- [`good.tla`](good.tla) (`good.cfg`): Adds a `lock` variable to make the read-modify-write critical section mutually exclusive. TLC verifies that `good` refines both `abstract` (`Refinement`) and `bad` (`RefinesBad`).
+- [`good_proof.tla`](good_proof.tla): TLAPS machine-checked proofs that `good` refines both `abstract` (`THEOREM ImplementsAbstract == Spec => Refinement`) and `bad` (`THEOREM ImplementsBad == Spec => RefinesBad`).

specifications/SpecificationRefinement/abstract.cfg

@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+
+CHECK_DEADLOCK FALSE

specifications/SpecificationRefinement/abstract.tla

@@ -0,0 +1,30 @@
+---- MODULE abstract ----
+EXTENDS Integers, Sequences
+
+VARIABLES pc, counter
+vars == <<pc, counter>>
+
+\* Two threads
+Threads == 1..2
+
+\* State transition action
+Trans(thread, from, to) ==
+  /\ pc[thread] = from
+  /\ pc' = [pc EXCEPT ![thread] = to]
+
+\* Both threads start in the `start` state
+Init ==
+  /\ pc = [t \in Threads |-> "start"]
+  /\ counter = 0
+
+Next ==
+  \* Pick one thread
+  \/ \E t \in Threads:
+     \* Move it to `done`
+     /\ Trans(t, "start", "done")
+     \* Increment counter
+     /\ counter' = counter + 1
+
+Spec == Init /\ [][Next]_vars
+
+====

specifications/SpecificationRefinement/bad.cfg

@@ -0,0 +1,5 @@
+SPECIFICATION Spec
+
+PROPERTY Refinement
+
+CHECK_DEADLOCK FALSE

specifications/SpecificationRefinement/bad.tla

@@ -0,0 +1,49 @@
+---- MODULE bad ----
+EXTENDS Integers, Sequences
+
+VARIABLES pc, counter, tmp
+vars == <<pc, counter, tmp>>
+
+Threads == 1..2
+
+States == {"start", "inc", "done"}
+
+Trans(thread, from, to) ==
+  /\ pc[thread] = from
+  /\ pc' = [pc EXCEPT ![thread] = to]
+
+Init ==
+  /\ pc = [t \in Threads |-> "start"]
+  /\ counter = 0
+  /\ tmp = [t \in Threads |-> 0]
+
+GetCounter(t) ==
+  /\ tmp' = [tmp EXCEPT ![t] = counter]
+  /\ UNCHANGED counter
+
+IncCounter(t) ==
+  /\ counter' = tmp[t] + 1
+  /\ UNCHANGED tmp
+
+Next ==
+  \/ \E t \in Threads:
+    \* Step to get the counter value
+    \/ /\ Trans(t, "start", "inc")
+       /\ GetCounter(t)
+    \* Step to increment the counter
+    \/ /\ Trans(t, "inc", "done")
+       /\ IncCounter(t)
+
+Spec == Init /\ [][Next]_vars
+
+Mapping == 
+  INSTANCE abstract WITH
+    counter <- counter,
+    pc <- [t \in Threads |-> 
+      IF pc[t] = "inc" THEN "start"
+      ELSE pc[t]
+      ]
+
+Refinement == Mapping!Spec
+
+====

specifications/SpecificationRefinement/good.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+
+PROPERTIES
+    Refinement
+    RefinesBad
+
+CHECK_DEADLOCK FALSE

specifications/SpecificationRefinement/good.tla

@@ -0,0 +1,63 @@
+---- MODULE good ----
+EXTENDS Integers, Sequences
+
+VARIABLES pc, counter, tmp, lock
+vars == <<pc, counter, tmp, lock>>
+
+Threads == 1..2
+
+States == {"start", "inc", "done"}
+
+Trans(thread, from, to) ==
+  /\ pc[thread] = from
+  /\ pc' = [pc EXCEPT ![thread] = to]
+
+Init ==
+  /\ pc = [t \in Threads |-> "start"]
+  /\ counter = 0
+  /\ tmp = <<0, 0>>
+  /\ lock = 0
+
+AcquireLock(t) ==
+  /\ lock = 0
+  /\ lock' = t
+
+ReleaseLock(t) ==
+  /\ lock = t
+  /\ lock' = 0
+
+GetCounter(t) ==
+  /\ tmp' = [tmp EXCEPT ![t] = counter]
+  /\ UNCHANGED counter
+
+IncCounter(t) ==
+  /\ counter' = tmp[t] + 1
+  /\ UNCHANGED tmp
+
+Next ==
+  \/ \E t \in Threads:
+    \/ /\ Trans(t, "start", "inc")
+       /\ GetCounter(t)
+       /\ AcquireLock(t)
+    \/ /\ Trans(t, "inc", "done")
+       /\ IncCounter(t)
+       /\ ReleaseLock(t)
+
+Spec == Init /\ [][Next]_vars
+
+Mapping == 
+  INSTANCE abstract WITH
+    counter <- counter,
+    pc <- [t \in Threads |-> 
+      IF pc[t] = "inc" THEN "start"
+      ELSE pc[t]
+      ]
+
+Refinement == Mapping!Spec
+
+BadMapping ==
+  INSTANCE bad
+
+RefinesBad == BadMapping!Spec
+
+====

specifications/SpecificationRefinement/good_proof.tla

@@ -0,0 +1,45 @@
+---- MODULE good_proof ----
+EXTENDS good, TLAPS
+
+TypeOK ==
+  /\ pc \in [Threads -> States]
+  /\ counter \in Int
+  /\ tmp \in [Threads -> Int]
+  /\ lock \in Threads \cup {0}
+
+Inv ==
+  /\ TypeOK
+  /\ \A t \in Threads :
+       /\ (pc[t] = "inc") <=> (lock = t)
+       /\ (pc[t] = "inc") => (tmp[t] = counter)
+
+LEMMA TypeAndInv == Spec => []Inv
+<1>1. Init => Inv
+  BY DEF Init, Inv, TypeOK, Threads, States
+<1>2. Inv /\ [Next]_vars => Inv'
+  BY DEF Inv, TypeOK, Next, vars, Threads, States,
+         Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock
+<1>3. QED
+  BY <1>1, <1>2, PTL DEF Spec
+
+THEOREM ImplementsAbstract == Spec => Refinement
+<1>1. Init => Mapping!Init
+  BY DEF Init, Mapping!Init, Threads, Mapping!Threads
+<1>2. Inv /\ [Next]_vars => [Mapping!Next]_Mapping!vars
+  BY DEF Inv, TypeOK, Next, vars, Threads, States,
+         Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock,
+         Mapping!Next, Mapping!vars, Mapping!Trans, Mapping!Threads
+<1>3. QED
+  BY <1>1, <1>2, TypeAndInv, PTL DEF Spec, Refinement, Mapping!Spec
+
+THEOREM ImplementsBad == Spec => RefinesBad
+<1>1. Init => BadMapping!Init
+  BY DEF Init, BadMapping!Init, Threads, BadMapping!Threads
+<1>2. [Next]_vars => [BadMapping!Next]_BadMapping!vars
+  BY DEF Next, vars, Threads, Trans, GetCounter, IncCounter, AcquireLock, ReleaseLock,
+         BadMapping!Next, BadMapping!vars, BadMapping!Threads,
+         BadMapping!Trans, BadMapping!GetCounter, BadMapping!IncCounter
+<1>3. QED
+  BY <1>1, <1>2, PTL DEF Spec, RefinesBad, BadMapping!Spec
+
+====

specifications/SpecificationRefinement/manifest.json

@@ -0,0 +1,63 @@
+{
+  "sources": [
+    "https://www.hillelwayne.com/post/refinement/"
+  ],
+  "authors": [
+    "Hillel Wayne"
+  ],
+  "tags": [
+    "beginner"
+  ],
+  "modules": [
+    {
+      "path": "specifications/SpecificationRefinement/abstract.tla",
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/SpecificationRefinement/abstract.cfg",
+          "runtime": "00:00:01",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 4,
+          "totalStates": 5,
+          "stateDepth": 3
+        }
+      ]
+    },
+    {
+      "path": "specifications/SpecificationRefinement/bad.tla",
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/SpecificationRefinement/bad.cfg",
+          "runtime": "00:00:01",
+          "mode": "exhaustive search",
+          "result": "liveness failure"
+        }
+      ]
+    },
+    {
+      "path": "specifications/SpecificationRefinement/good.tla",
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/SpecificationRefinement/good.cfg",
+          "runtime": "00:00:01",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 9,
+          "totalStates": 9,
+          "stateDepth": 5
+        }
+      ]
+    },
+    {
+      "path": "specifications/SpecificationRefinement/good_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    }
+  ]
+}