Separate the CMP abstraction from the FLASH protocol.

Model checking covers one node count at a time. CMP method of Chou,
Mannava and Park proposed the following workaround: keep a few nodes
concrete, summarize the rest in one abstract node Other, and add rules
that over-approximate what it may do. The abstraction is pushed into
FlashWithMutexCMP.

TLAPS can prove the protocol for every constant value. Thus, a proof
should not have to carry rules that exist to make one node count stand for
all of them, nor should a reader of the protocol -- and both were carrying
them, as ABS_* rules interleaved with the protocol's own, an Env_o
conjunct in every UNCHANGED list, and NodeU widened by Other throughout.

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/FlashProtocol/APFlashWithMutex.cfg

@@ -1,7 +1,6 @@
 CONSTANT
   NODE      <- NodeVal
   DATA      <- DataVal
-  Other     <- OtherVal
   Undefined <- UndefinedVal
 
 INVARIANT

specifications/FlashProtocol/APFlashWithMutex.tla

@@ -19,8 +19,6 @@ CONSTANTS
   \* @type: Set(Str);
   DATA,
   \* @type: Str;
-  Other,
-  \* @type: Str;
   Undefined
 
 VARIABLES
@@ -57,9 +55,7 @@ VARIABLES
   \* @type: Str;
   FwdCmd,
   \* @type: Str;
-  FwdSrc,
-  \* @type: Bool;
-  Env_o
+  FwdSrc
 
 \* Both components of the variable group are strings, which the type checker
 \* cannot tell apart from a two-element sequence.  The group is shadowed here
@@ -77,7 +73,6 @@ INSTANCE FlashWithMutex
 \* Concrete values for the constants used by APFlashWithMutex.cfg.
 NodeVal      == { "n1", "n2" }
 DataVal      == { "d1", "d2" }
-OtherVal     == "Other"
 UndefinedVal == "Undefined"
 
 ==============================================================================

specifications/FlashProtocol/FlashWithMutex.tla

@@ -1,7 +1,6 @@
 CONSTANTS
   NODE = {n1, n2}
   DATA = {d1, d2}
-  Other = Other
   Undefined = Undefined
 
 SYMMETRY Symmetry

specifications/FlashProtocol/FlashWithMutexCMP.tla

@@ -1,8 +1,8 @@
 ------------------------- MODULE MCFlashWithMutex -------------------------
 EXTENDS FlashWithMutex, TLC
 
-\* Nodes and data values are independently interchangeable.  The Other and
-\* Undefined sentinels are fixed because they are outside these sets.
+\* Nodes and data values are independently interchangeable.  The Undefined
+\* sentinel is fixed because it is outside these sets.
 Symmetry == Permutations(NODE) \union Permutations(DATA)
 
 ==============================================================================

specifications/FlashProtocol/MCFlashWithMutex.cfg

@@ -1,7 +1,6 @@
 CONSTANTS
   NODE = {n1, n2}
   DATA = {d1, d2}
-  Other = Other
   Undefined = Undefined
 
 SPECIFICATION FairSpec

specifications/FlashProtocol/MCFlashWithMutex.tla

@@ -14,13 +14,18 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/FlashProtocol/FlashWithMutexCMP.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/FlashProtocol/APFlashWithMutex.tla",
       "features": [],
       "models": [
         {
           "path": "specifications/FlashProtocol/APFlashWithMutex.cfg",
-          "runtime": "00:38:09",
+          "runtime": "00:00:44",
           "mode": "symbolic",
           "result": "success"
         }
@@ -32,12 +37,12 @@
       "models": [
         {
           "path": "specifications/FlashProtocol/MCFlashWithMutex.cfg",
-          "runtime": "00:00:04",
+          "runtime": "00:00:01",
           "mode": "exhaustive search",
           "result": "success",
-          "distinctStates": 32994,
-          "totalStates": 159216,
-          "stateDepth": 34
+          "distinctStates": 2024,
+          "totalStates": 7552,
+          "stateDepth": 21
         }
       ]
     },
@@ -47,12 +52,12 @@
       "models": [
         {
           "path": "specifications/FlashProtocol/MCFlashWithMutexLive.cfg",
-          "runtime": "00:04:44",
+          "runtime": "00:00:15",
           "mode": "exhaustive search",
           "result": "success",
-          "distinctStates": 131976,
-          "totalStates": 636852,
-          "stateDepth": 34,
+          "distinctStates": 8096,
+          "totalStates": 30196,
+          "stateDepth": 21,
           "workers": 4
         }
       ]