close apalache-mc#468 (apalache-mc#491)

Co-authored-by: Shon Feder <shon@informal.systems>

UNRELEASED.md

@@ -13,6 +13,7 @@
 ### Bug fixes
 
  * handling big integers, see #450
+ * better parsing of SPECIFICATION in TLC configs, see #468
  * expanding tuples in quantifiers, see #476
  * unfolding UNCHANGED for arbitrary expressions, see #471
  * unfolding UNCHANGED <<>>, see #475
@@ -22,4 +23,3 @@
  * constant simplification over strings, see #197
  * propagation of primes inside expressions,
    e.g., (f[i])' becomes f'[i'] if both f and i are state variables
-

test/tla/Config.tla

@@ -34,6 +34,12 @@ Spec ==
 Spec2 ==
     Init2 /\ [][Next2]_x
 
+Spec4 ==
+    (Init2 /\ [][Next2]_x) /\ WF_x(Next2)
+
+Spec5 ==
+    Init2 /\ ([][Next2]_x /\ SF_x(Next2))
+
 \* the default invariant
 Inv ==
     x < 1

test/tla/Config4.cfg

@@ -0,0 +1,6 @@
+SPECIFICATION
+Spec4
+
+INVARIANT
+Inv2
+

test/tla/Config5.cfg

@@ -0,0 +1,6 @@
+SPECIFICATION
+Spec5
+
+INVARIANT
+Inv2
+

test/tla/cli-integration-tests.md

@@ -712,6 +712,40 @@ The outcome is: NoError
 ...
 ```
 
+### configure via TLC config with SPECIFICATION and fairness
+
+```sh
+$ apalache-mc check --config=Config4.cfg Config.tla | sed 's/[IEW]@.*//'
+...
+  > Config4.cfg: Loading TLC configuration
+...
+  > Config4.cfg: Using SPECIFICATION Spec4
+...
+  > Set the initialization predicate to Init2
+  > Set the transition predicate to Next2
+  > Set an invariant to Inv2
+...
+The outcome is: NoError
+...
+```
+
+### configure via TLC config with SPECIFICATION and fairness
+
+```sh
+$ apalache-mc check --config=Config5.cfg Config.tla | sed 's/[IEW]@.*//'
+...
+  > Config5.cfg: Loading TLC configuration
+...
+  > Config5.cfg: Using SPECIFICATION Spec5
+...
+  > Set the initialization predicate to Init2
+  > Set the transition predicate to Next2
+  > Set an invariant to Inv2
+...
+The outcome is: NoError
+...
+```
+
 ### configure complains about circular dependencies
 
 ```sh