Discrete inclusion provides wrong answer

[Jiri Srba]

Open the attached net verification-problem and verify, TAPAAL returns wrong verification answer
(even if the query is upward closed). This was a problem already at 2.0.0, so this has nothing to do
with the relaxation of the upward closed queries. The problem is in the engine and I attach also the
exported files 1.xml 1.q that show the problem:

./verifytapn64 -k 4 -f 1 ~/1.xml ~/1.q

is NOT satisfied, and

./verifytapn64 -k 4 -f 0 ~/1.xml ~/1.q

is satisfied (the same for 32 version of the engine).

The reason seems the place on the receiver side where there is the token in the initial marking.
If this is not including in the inclusion places, all is fine. The same is, of course, if in the query we
ask about equality to 1 for this place.

[Jiri Srba (srba)]

One more information, the problem is here with DFS and CoverMost search, for BFS it returns the correct answer.

[Jiri Srba (srba)]

Here is a simpler net having the same problematic behaviour. Note that only two places are
included into inclusion check.

[Jiri Srba (srba)]

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.

[Jiri Srba (srba)]

The bug is fixed as follows. Both in query verification and batch processing:

1. unsatisfeid EF query for unbounded net with discrete inclusion is reported as "Inconclusive answer"
2. satisfied AG query for unbounded net with discrete inclusion is also reported as "Inconclusive answer"