Good afternoon, I am doing some experiments with UPPAAL model checker and my understanding is that, when a property is not verified, the verification engine (verifyta) only enables to find one among the following:
- A Trace
- Shortest Trace (Number of Transitions)
- Quickset Trace (Trace with shortest relative time).
This makes a lot of sense, if we consider that model checking focuses on soundness instead of completeness and the fact that at least one trace exists that violates a specific property means that that property is not satisfied.
However, in the context of my application, I would need to find more than one counterexample to analyse their structure etc. To this extent, I was wondering if there exist the possibility of extrapolating ALL the possible traces that violates a particular property defined in TCTL, given a bounded search space (i.e. limiting the depth of the search graph). Furthermore, if UPPAAL doesn't offer this opportunity, could you please point me to other tools that might have implemented it?
Thanks a lot!