Raw options compute wrong k-bound
Bug #2051167 reported by
Jiri Srba
This bug affects 1 person
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Committed
|
Undecided
|
Unassigned |
Bug Description
Open the Workflow-complaint example.
Open the strong soundness query and verify. The answer is false as expected.
Then open the strong soundness query again, click on "Use" and verify. The answer is now true (wrong answer).
The problem is that the GUI passes to the engine "-k 2" if you click on "Use" which is wrong, it should pass there "-k 3" which it does correctly when run without "Use". There are two tokens in the net plus one extra token, hence the -k should be 3.
Changed in tapaal: | |
status: | New → Fix Committed |
To post a comment you must log in.