Skip to content

Instantly share code, notes, and snippets.

@p-offtermatt

p-offtermatt/informative_counterexample.tla

Created May 25, 2022 15:29
Show Gist options
  • Save p-offtermatt/03f62963715887af33420d580af85940 to your computer and use it in GitHub Desktop.
Save p-offtermatt/03f62963715887af33420d580af85940 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
informative_counterexample.tla
---------------------------- MODULE counterexample ----------------------------
EXTENDS ManyBoxes
(* Constant initialization state *)
(* ConstInit == TRUE *)
ConstInit == TRUE
(* Initial state *)
(* State0 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = FALSE
/\ __loop_☐☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐♢(x = 2) = FALSE
/\ __loop_☐♢(x = 2) = FALSE
/\ __loop_♢(x = 2) = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ ☐☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐☐♢(x = 2)_globally = TRUE
/\ ☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐♢(x = 2)_globally = TRUE
/\ ☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐♢(x = 2)_globally = TRUE
/\ ☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐♢(x = 2)_globally = TRUE
/\ ☐☐♢(x = 2) = FALSE
/\ ☐☐♢(x = 2)_globally = TRUE
/\ ☐♢(x = 2) = FALSE
/\ ☐♢(x = 2)_globally = TRUE
/\ ♢(x = 2) = FALSE
/\ ♢(x = 2)_eventually = FALSE
/\ x = 0
/\ y = 1 *)
State0 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = FALSE
/\ __loop___temporal_t_1 = FALSE
/\ __loop___temporal_t_2 = FALSE
/\ __loop___temporal_t_3 = FALSE
/\ __loop___temporal_t_4 = FALSE
/\ __loop___temporal_t_5 = FALSE
/\ __loop___temporal_t_6 = FALSE
/\ __loop___temporal_t_7 = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ __temporal_t_1 = FALSE
/\ __temporal_t_1_globally = TRUE
/\ __temporal_t_2 = FALSE
/\ __temporal_t_2_globally = TRUE
/\ __temporal_t_3 = FALSE
/\ __temporal_t_3_globally = TRUE
/\ __temporal_t_4 = FALSE
/\ __temporal_t_4_globally = TRUE
/\ __temporal_t_5 = FALSE
/\ __temporal_t_5_globally = TRUE
/\ __temporal_t_6 = FALSE
/\ __temporal_t_6_globally = TRUE
/\ __temporal_t_7 = FALSE
/\ __temporal_t_7_eventually = FALSE
/\ x = 0
/\ y = 1
(* Transition 0 to State1 *)
(* State1 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = TRUE
/\ __loop_☐☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐♢(x = 2) = FALSE
/\ __loop_☐♢(x = 2) = FALSE
/\ __loop_♢(x = 2) = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ ☐☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐♢(x = 2) = FALSE
/\ ☐☐♢(x = 2)_globally = FALSE
/\ ☐♢(x = 2) = FALSE
/\ ☐♢(x = 2)_globally = FALSE
/\ ♢(x = 2) = FALSE
/\ ♢(x = 2)_eventually = FALSE
/\ x = 1
/\ y = 0 *)
State1 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = TRUE
/\ __loop___temporal_t_1 = FALSE
/\ __loop___temporal_t_2 = FALSE
/\ __loop___temporal_t_3 = FALSE
/\ __loop___temporal_t_4 = FALSE
/\ __loop___temporal_t_5 = FALSE
/\ __loop___temporal_t_6 = FALSE
/\ __loop___temporal_t_7 = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ __temporal_t_1 = FALSE
/\ __temporal_t_1_globally = FALSE
/\ __temporal_t_2 = FALSE
/\ __temporal_t_2_globally = FALSE
/\ __temporal_t_3 = FALSE
/\ __temporal_t_3_globally = FALSE
/\ __temporal_t_4 = FALSE
/\ __temporal_t_4_globally = FALSE
/\ __temporal_t_5 = FALSE
/\ __temporal_t_5_globally = FALSE
/\ __temporal_t_6 = FALSE
/\ __temporal_t_6_globally = FALSE
/\ __temporal_t_7 = FALSE
/\ __temporal_t_7_eventually = FALSE
/\ x = 1
/\ y = 0
(* Transition 0 to State2 *)
(* State2 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = TRUE
/\ __loop_☐☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐☐♢(x = 2) = FALSE
/\ __loop_☐☐♢(x = 2) = FALSE
/\ __loop_☐♢(x = 2) = FALSE
/\ __loop_♢(x = 2) = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ ☐☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐☐♢(x = 2) = FALSE
/\ ☐☐☐♢(x = 2)_globally = FALSE
/\ ☐☐♢(x = 2) = FALSE
/\ ☐☐♢(x = 2)_globally = FALSE
/\ ☐♢(x = 2) = FALSE
/\ ☐♢(x = 2)_globally = FALSE
/\ ♢(x = 2) = FALSE
/\ ♢(x = 2)_eventually = FALSE
/\ x = 0
/\ y = 1 *)
State2 ==
FalseLiveness_init = FALSE
/\ __loop_InLoop = TRUE
/\ __loop___temporal_t_1 = FALSE
/\ __loop___temporal_t_2 = FALSE
/\ __loop___temporal_t_3 = FALSE
/\ __loop___temporal_t_4 = FALSE
/\ __loop___temporal_t_5 = FALSE
/\ __loop___temporal_t_6 = FALSE
/\ __loop___temporal_t_7 = FALSE
/\ __loop_x = 0
/\ __loop_y = 1
/\ __temporal_t_1 = FALSE
/\ __temporal_t_1_globally = FALSE
/\ __temporal_t_2 = FALSE
/\ __temporal_t_2_globally = FALSE
/\ __temporal_t_3 = FALSE
/\ __temporal_t_3_globally = FALSE
/\ __temporal_t_4 = FALSE
/\ __temporal_t_4_globally = FALSE
/\ __temporal_t_5 = FALSE
/\ __temporal_t_5_globally = FALSE
/\ __temporal_t_6 = FALSE
/\ __temporal_t_6_globally = FALSE
/\ __temporal_t_7 = FALSE
/\ __temporal_t_7_eventually = FALSE
/\ x = 0
/\ y = 1
(* The following formula holds true in the last state and violates the invariant *)
(* InvariantViolation ==
(__loop_InLoop
/\ x = __loop_x
/\ y = __loop_y
/\ ☐☐☐☐☐☐♢(x = 2) = __loop_☐☐☐☐☐☐♢(x = 2)
/\ ☐☐☐☐☐♢(x = 2) = __loop_☐☐☐☐☐♢(x = 2)
/\ ☐☐☐☐♢(x = 2) = __loop_☐☐☐☐♢(x = 2)
/\ ☐☐☐♢(x = 2) = __loop_☐☐☐♢(x = 2)
/\ ☐☐♢(x = 2) = __loop_☐☐♢(x = 2)
/\ ☐♢(x = 2) = __loop_☐♢(x = 2)
/\ ♢(x = 2) = __loop_♢(x = 2)
/\ (~♢(x = 2) \/ ♢(x = 2)_eventually)
/\ (~☐♢(x = 2)_globally \/ ☐♢(x = 2))
/\ (~☐☐♢(x = 2)_globally \/ ☐☐♢(x = 2))
/\ (~☐☐☐♢(x = 2)_globally \/ ☐☐☐♢(x = 2))
/\ (~☐☐☐☐♢(x = 2)_globally \/ ☐☐☐☐♢(x = 2))
/\ (~☐☐☐☐☐♢(x = 2)_globally \/ ☐☐☐☐☐♢(x = 2))
/\ (~☐☐☐☐☐☐♢(x = 2)_globally \/ ☐☐☐☐☐☐♢(x = 2)))
/\ ~FalseLiveness_init *)
InvariantViolation ==
(__loop_InLoop
/\ x = __loop_x
/\ y = __loop_y
/\ __temporal_t_1 = __loop___temporal_t_1
/\ __temporal_t_2 = __loop___temporal_t_2
/\ __temporal_t_3 = __loop___temporal_t_3
/\ __temporal_t_4 = __loop___temporal_t_4
/\ __temporal_t_5 = __loop___temporal_t_5
/\ __temporal_t_6 = __loop___temporal_t_6
/\ __temporal_t_7 = __loop___temporal_t_7
/\ (~__temporal_t_7 \/ __temporal_t_7_eventually)
/\ (~__temporal_t_6_globally \/ __temporal_t_6)
/\ (~__temporal_t_5_globally \/ __temporal_t_5)
/\ (~__temporal_t_4_globally \/ __temporal_t_4)
/\ (~__temporal_t_3_globally \/ __temporal_t_3)
/\ (~__temporal_t_2_globally \/ __temporal_t_2)
/\ (~__temporal_t_1_globally \/ __temporal_t_1))
/\ ~FalseLiveness_init
================================================================================
(* Created by Apalache on Wed May 25 17:26:11 CEST 2022 *)
(* https://github.com/informalsystems/apalache *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment