Strengthen test by adding third invariant.

[Tests][TLC]

tlatools/test-model/suite/test57.cfg

 SPECIFICATION Spec
-INVARIANT Invariant0 Invariant1 Invariant2  
+INVARIANT Invariant0 Invariant2 Invariant3 Invariant1  
 PROPERTY Property
\ No newline at end of file

tlatools/test-model/suite/test57.tla

@@ -12,6 +12,7 @@ Spec == Init /\ [][Next]_x
 Invariant0 == I!B(Next)
 Invariant1 == I!C
 Invariant2 == ~ I!B(I!A)
+Invariant3 == I!D
 Property == [][~I!A]_x
 =============================================================================
 I!C = ENABLED((u'=x) /\ (v' = x+1))

tlatools/test-model/suite/test57a.tla

@@ -5,4 +5,5 @@ VARIABLES u, v
 A == (u'=u) /\ (v'=v+1)
 B(d) == ENABLED d
 C == B(A)
+D == ENABLED A
 =============================================================================
\ No newline at end of file

tlatools/test-model/test57.cfg

 SPECIFICATION Spec
-INVARIANT Invariant0 Invariant1 Invariant2  
+INVARIANT Invariant0 Invariant2 Invariant3 Invariant1
 PROPERTY Property
\ No newline at end of file

tlatools/test-model/test57.tla

@@ -12,6 +12,7 @@ Spec == Init /\ [][Next]_x
 Invariant0 == I!B(Next)
 Invariant1 == I!C
 Invariant2 == ~ I!B(I!A)
+Invariant3 == I!D
 Property == [][~I!A]_x
 =============================================================================
 I!C = ENABLED((u'=x) /\ (v' = x+1))

tlatools/test-model/test57a.tla

@@ -5,4 +5,5 @@ VARIABLES u, v
 A == (u'=u) /\ (v'=v+1)
 B(d) == ENABLED d
 C == B(A)
+D == ENABLED A
 =============================================================================
\ No newline at end of file