TAPAAL

  1. Bug #1031666
  2. Comment #1

Comment 1 for bug 1031666

Revision history for this message
Jiri Srba (srba) wrote :

In fact the answer IS correct (the EG query is satisfied because there is a deadlock right from the start).

When UPPAAL engine is used, we should just add "The answer is conclusive only if the net is bounded for the number of extra tokens. Run the boundedness check in the query dialog."

However, when using the discrete engine, the answer is "The property is NOT satisfied" but add more tokens and try again ...
This is wrong, it should have found the deadlock (as there are no extra tokens).