Verificiation results explanation

[Jiri Srba]

The "Verification result" dialog shows a button called explanation.
I would suggest to remove the button and instead show the explanation for
Discovered/Explored/Stored markings as tool tips.
Test it both for timed and untimed nets.

[Thomas Pedersen (tpede16)]

I can see in the code that there is a specific verification result explanation for when a CTL query is solved without using state equations. However, I am having trouble creating a CTL query, which is not solved by state equations, to test it.

Is there some option to disable state equations I am missing? Otherwise, how do I go about creating a CTL query which cannot be solved by state equations?

[Jiri Srba (srba)]

Yes, in the CTL query dialog open the advanced mode (right upper corner button) and then deselect all techniques (in particular query simplifiaction). Then e.g.the query EF P1=1 on the net P0 -> T0 -> P1 will run the actual verification and show the number of reachable markings etc.