Add Apalache wrapper for DieHardest

Add APADieHardest.tla, an Apalache-compatible configuration that checks
DieHardest's interleaved composition (Section 4) with --cinit for
constant initialization and [s \in S |-> ...] in place of :> and @@.
Note the Apalache incompatibility of NextParallelGlobalFreeze in
DieHardest.tla (TLCGet takes both Str and Int arguments).

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/DieHard/APADieHardest.tla

@@ -0,0 +1,56 @@
+Apalache configuration for DieHardest (Section 4, interleaved composition).
+
+    $ apalache-mc check \
+        --cinit=ConstInit  --next=NextInterleaved \
+        --inv=NotSolved    --length=13 \
+        APADieHardest.tla
+
+Apalache finds the expected 12-state counterexample in about four hours
+on a 2021 MacBook Pro (Apalache 0.52.2).
+
+----------------------------- MODULE APADieHardest ------------------------------
+(***************************************************************************)
+(* Apalache-compatible model-checking wrapper for DieHardest.              *)
+(*                                                                         *)
+(* DieHardest's Sections 1-3 use TLC-specific operators (TLCGet, TLCSet)   *)
+(* that Apalache does not support.  This module checks only Section 4      *)
+(* (interleaved composition) by selecting NextInterleaved via --next.      *)
+(*                                                                         *)
+(* Adaptations for Apalache:                                               *)
+(*  - Constants are initialized via ConstInit (--cinit) rather than a      *)
+(*    TLC .cfg file.                                                       *)
+(*  - Capacity functions use [s \in S |-> ...] instead of the TLC-module   *)
+(*    operators :> and @@.                                                 *)
+(***************************************************************************)
+
+CONSTANT
+    \* @type: Seq(Str -> Int);
+    Capacities,
+    \* @type: Int;
+    Goal
+
+VARIABLE
+    \* @type: Str -> Int;
+    c1,
+    \* @type: Str -> Int;
+    c2,
+    \* @type: Int;
+    s1,
+    \* @type: Int;
+    s2
+
+INSTANCE DieHardest
+
+MCGoal == 4
+
+MCCapacity1 ==
+    [ s \in {"j1", "j2"} |-> IF s = "j1" THEN 5 ELSE 3 ]
+
+MCCapacity2 ==
+    [ s \in {"j1", "j2", "j3"} |-> IF s = "j1" THEN 5 ELSE 3 ]
+
+ConstInit ==
+    /\ Capacities = <<MCCapacity1, MCCapacity2>>
+    /\ Goal = MCGoal
+
+=============================================================================

specifications/DieHard/DieHardest.tla

@@ -160,6 +160,10 @@ NextParallelFreeze ==
 ASSUME TLCSet(2, 999) /\ TLCSet(3, 999)
 
 NextParallelGlobalFreeze ==
+    \* TLCGet is called with both Str and Int arguments (TLCGet("level")
+    \* vs. TLCGet(2)), so Apalache's type checker cannot assign a single
+    \* type to its parameter.  This operator is therefore incompatible
+    \* with Apalache.  See APADieHardest.tla, which checks Section 4 only.
     /\ IF TLCGet("level") >= TLCGet(2) THEN UNCHANGED c1 ELSE D1!Next
     /\ IF TLCGet("level") >= TLCGet(3) THEN UNCHANGED c2 ELSE D2!Next
     /\ Goal \in Range(c1') /\ TLCGet(2) = 999 => TLCSet(2, TLCGet("level") + 1)

specifications/DieHard/manifest.json

@@ -24,6 +24,11 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/DieHard/APADieHardest.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/DieHard/MCDieHarder.tla",
       "features": [],