Verificiation results explanation

Bug #1879129 reported by Jiri Srba on 2020-05-17
This bug affects 1 person
Affects Status Importance Assigned to Milestone
Thomas Pedersen

Bug Description

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.

Related branches

Jiri Srba (srba) on 2020-05-17
Changed in tapaal:
assignee: nobody → Thomas Pedersen (tpede16)
Changed in tapaal:
status: New → In Progress
Thomas Pedersen (tpede16) wrote :

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) wrote :

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.

Jiri Srba (srba) on 2020-06-09
Changed in tapaal:
status: In Progress → Fix Committed
To post a comment you must log in.
This report contains Public information  Edit
Everyone can see this information.

Other bug subscribers