Incorrect query dialog for games
Bug #2004467 reported by
Lena Ernstsen
This bug affects 1 person
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Committed
|
Undecided
|
Lena Ernstsen |
Bug Description
Query dialog allows incorrect behaviour for gamed nets.
How to reproduce:
1) Create a coloured game net with a place and transition connected by an arc.
2) Create this query: !(AG TAPN1.P0 = 0) and remove "use query reductions.
3) Save and verify the query.
!) Verification error occurs: Only AF and AG propositions supported for synthesis
4) Edit the query to: AG !(AG TAPN1.P0 = 0)
!) Another Verification error occurs: Only simple synthesis propositions supported (i.e. one
top-most AF or AG and no other nested quantifiers)
For games we should only allow 1 quantification property, either AF or AG. It should not be allowed to negate this quantification.
Changed in tapaal: | |
milestone: | none → cpn |
Changed in tapaal: | |
assignee: | nobody → Lena Ernstsen (lsaid) |
Changed in tapaal: | |
status: | New → In Progress |
Changed in tapaal: | |
status: | In Progress → Fix Committed |
To post a comment you must log in.
Still an issue in CPN branch.