close #468

apalache-mc · Jan 25, 2021 · e998886 · e998886
1 parent da5cc41
commit e998886
Show file tree

Hide file tree

Showing 5 changed files with 225 additions and 53 deletions.
diff --git a/test/tla/Config.tla b/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

diff --git a/test/tla/Config4.cfg b/test/tla/Config4.cfg
@@ -0,0 +1,6 @@
+SPECIFICATION
+Spec4
+
+INVARIANT
+Inv2
+
diff --git a/test/tla/Config5.cfg b/test/tla/Config5.cfg
@@ -0,0 +1,6 @@
+SPECIFICATION
+Spec5
+
+INVARIANT
+Inv2
+
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -694,6 +694,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