#414: more TLA+ lite tests

informalsystems · Aug 10, 2020 · e9a099f · e9a099f
1 parent 0df4320
commit e9a099f
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 2 deletions.
diff --git a/tendermint/tests/support/lite-model-based/LiteTests.tla b/tendermint/tests/support/lite-model-based/LiteTests.tla
@@ -15,4 +15,30 @@ TestSuccess ==
 
 TestSuccessInv == ~TestSuccess
 
+\* This test never produces a counterexample; so the model should be corrected
+TestFailedTrustingPeriod ==
+   \E s \in DOMAIN history :
+      history[s].verdict = "FAILED_TRUSTING_PERIOD"
+
+TestFailedTrustingPeriodInv == ~TestFailedTrustingPeriod
+
+Test2CannotVerifySuccess ==
+    /\ state = "finishedSuccess"
+    /\ \E s1, s2 \in DOMAIN history :
+       /\ s1 /= s2
+       /\ history[s1].verdict = "CANNOT_VERIFY"
+       /\ history[s2].verdict = "CANNOT_VERIFY"
+
+Test2CannotVerifySuccessInv == ~Test2CannotVerifySuccess
+
+Test3CannotVerifySuccess ==
+    /\ state = "finishedSuccess"
+    /\ \E s1, s2, s3 \in DOMAIN history :
+       /\ s1 /= s2 /\ s2 /= s3 /\ s1 /= s3
+       /\ history[s1].verdict = "CANNOT_VERIFY"
+       /\ history[s2].verdict = "CANNOT_VERIFY"
+       /\ history[s3].verdict = "CANNOT_VERIFY"
+
+Test3CannotVerifySuccessInv == ~Test3CannotVerifySuccess
+
 ============================================================================
diff --git a/tendermint/tests/support/lite-model-based/MC4_4_faulty.tla b/tendermint/tests/support/lite-model-based/MC4_4_faulty.tla
@@ -8,8 +8,7 @@ IS_PRIMARY_CORRECT == FALSE
 
 VARIABLES
   state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified,
-  prevVerified, prevChecked, prevTime, prevVerdict,
-  nprobes,
+  history, nprobes,
   now, blockchain, Faulty
 
 INSTANCE LiteTests