Can UPPAAL get all the counterexamples?
29 views
Skip to first unread message
刘乔森
Sep 12, 2023, 11:22:57 PM9/12/23
to UPPAAL
Hi.
When I enter A[] not Automata.locationA in the validation screen for reachability analysis, I can get a symbolic trace (counterexample) when the model doesn't satisfy the property, sometimes there is more than one counterexample, is there a way for me to get all similar counterexamples?
Here "Automata" means template and "locationA" means a specified location.
When I enter A[] not Automata.locationA in the validation screen for reachability analysis, I can get a symbolic trace (counterexample) when the model doesn't satisfy the property, sometimes there is more than one counterexample, is there a way for me to get all similar counterexamples?
Here "Automata" means template and "locationA" means a specified location.
Reply all
Reply to author
Forward
0 new messages