Comment 6 for bug 948502

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

Now I know what is the problem:

1. The given net is unbounded so the verification is done only up to a given number of tokens.
2. Normal BFS or DFS search in the engine might discover some reachable marking using the given
    number of extra tokens.
3. Discrete inclusion will through away markings with fewer tokens in inclusion places but it might
    end up in a situation where it stores a marking that uses all the available tokens but then it needs to
    make a transition that needs one more token to reach its target marking in the EF query.
    This would be possible from the smaller marking that was removed from PWList but not from
    the maximal marking that already used all tokens.