LTL - wrong answer
Bug #1967251 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Committed
|
Critical
|
Kenneth Yrke Jørgensen | ||
Bug Description
The attached net gives wrong answer for LTL.
The query is E F P=1
and indeed the place can be marked but LTL engine returns false (second query).
If you run it as CTL query (third query) then the answer is correct (true).
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
Revision history for this message
| Jiri Srba (srba) wrote | #2 |
Revision history for this message
| Kenneth Yrke Jørgensen (yrke) wrote | #3 |
| Changed in tapaal: | |
| status: | New → Incomplete |
| status: | Incomplete → In Progress |
| importance: | Undecided → Critical |
| Changed in tapaal: | |
| assignee: | nobody → Kenneth Yrke Jørgensen (yrke) |
| Changed in tapaal: | |
| status: | In Progress → Fix Committed |
To post a comment you must log in.
This is a GUI problem, as the GUI sends to the engine the query
AF P=1
instead of
EF P=1