Exhaustive search via transition enumeration

[andrey-kuprianov]

The ability to enumere counterexamples is crucial in such usage scenarios as model-based testing, where counterexamples are used as test cases. As the first step towards #79, we need to implement the simplest exhaustive search for counterexamples: via enumerating sequences of transitions.

• the tool should support --continue option;
• every new counterexample returned with -continue should use a different sequence of transitions leading to an invariant violation.

In case of a lot of non-determinism this can of course blow up, because it means enumerating the tree branches. But exhaustiveness on the base of transition sequences is the simplest to implement, and offers an intuitive mental picture for the end user. This strategy can later be complemented in the scope of #79 with different ones (based on the values of state variables for example).

[konnov]

@Kukovec do you like to give it a try? The new transition executor is documented in ADR003, which is used by SeqModelChecker.

[konnov]

I would de-prioritize this one in favor of #730

[konnov]

Last time we have decided to prioritize this approach, at least as a provisional solution. I think there is a nice way to implement enumeration of counterexamples and make it useful in various scenarios. See a detailed description in the discussion #827.