Add liveness page

FedericoPonzi · Jul 16, 2024 · f67e5c9 · f67e5c9
1 parent 9630127
commit f67e5c9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
@@ -25,6 +25,7 @@
     - [TLC Model Checker](./using/tlc.md)
         - [How TLC works](./using/tlc/how-tlc-works.md)
         - [Trace Validation](./using/tlc/trace-validation.md)
+        - [Liveness](./using/tlc/liveness.md)
     - [Standard Library](./using/standard-lib.md)
     - [Community Modules](./using/community-modules.md)
     - [Debugger](./using/debugger.md)

diff --git a/src/using/tlc/liveness.md b/src/using/tlc/liveness.md
@@ -0,0 +1,5 @@
+# Liveness checks
+if TLC is configured to check three temporal formulas A,B,C;
+TLC does *not* check if A, B or C are identical formulas. If TLC is set to
+check A, A, A (it will still create three OrderOfSolutions). It is up to the
+user to prevent this.