You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
37 lines
942 B
37 lines
942 B
------------------ MODULE TendermintAccTrace_004_draft -------------------------
|
|
(*
|
|
When Apalache is running too slow and we have an idea of a counterexample,
|
|
we use this module to restrict the behaviors only to certain actions.
|
|
Once the whole trace is replayed, the system deadlocks.
|
|
|
|
Version 1.
|
|
|
|
Igor Konnov, 2020.
|
|
*)
|
|
|
|
EXTENDS Sequences, Apalache, TendermintAcc_004_draft
|
|
|
|
\* a sequence of action names that should appear in the given order,
|
|
\* excluding "Init"
|
|
CONSTANT
|
|
\* @type: TRACE;
|
|
Trace
|
|
|
|
VARIABLE
|
|
\* @type: TRACE;
|
|
toReplay
|
|
|
|
TraceInit ==
|
|
/\ toReplay = Trace
|
|
/\ action' := "Init"
|
|
/\ Init
|
|
|
|
TraceNext ==
|
|
/\ Len(toReplay) > 0
|
|
/\ toReplay' = Tail(toReplay)
|
|
\* Here is the trick. We restrict the action to the expected one,
|
|
\* so the other actions will be pruned
|
|
/\ action' := Head(toReplay)
|
|
/\ Next
|
|
|
|
================================================================================
|