From e9a099fc961a84269ef00c16e1a4be5e386eca45 Mon Sep 17 00:00:00 2001
From: Andrey Kuprianov <andrey@informal.systems>
Date: Mon, 10 Aug 2020 23:08:35 +0200
Subject: [PATCH] #414: more TLA+ lite tests

---
 .../support/lite-model-based/LiteTests.tla    | 26 +++++++++++++++++++
 .../support/lite-model-based/MC4_4_faulty.tla |  3 +--
 2 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/tendermint/tests/support/lite-model-based/LiteTests.tla b/tendermint/tests/support/lite-model-based/LiteTests.tla
index 3b3b89132..345cb2eff 100644
--- 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
index 51e23fba0..ec8177e3f 100644
--- 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