Incorrectly reported statistics

[Mathias Grund Sørensen]

The following stats are incorrectly reported by the engine (wrt. TAPAAL):

- The number "max tokens" does not always correctly report the maximum number of tokens in any considered marking. See the first attached net+query. With -k 2, the engine reports max tokens: 0, which makes the result conclusive, whereas it should report more than 2 making the result inconclusive.

- With queries containing deadlocks, the stats are all 0 if the query is satisfied by the first marking, making the result undistinguishable from the over-approximation results (see second attached net+query). The initial marking should be counted in the stats as explored as well.

[Jiri Srba (srba)]

The untimed engine should never be called with EG/AF query. Perhaps the engine should report this
and terminate the verification without doing anything.

[Mathias Grund Sørensen (mathias.grund)]

Yes, sorry, my bad.

[Jonas Finnemann Jensen (jopsen)]

I think the max token problem is because we count max-tokens after we restricted the exploration... This is obviously a problem...

Counting the first state for queries that are satisfies initially is probably just adding +1 a few places... Nothing big...

I'll try to take a look at this...

[Jiri Srba (srba)]

The max token problem should return the total maximum number of tokens in any markings that was
ever discovered during the search. In order works a counter should be set to the number of tokens in the initial marking
and everytime a new marking is discovered, the counter should be updated accordingly:
counter = max(counter, number_of_tokens_in_the_discovered_marking)
I hope this makes sense.

Counting the initial state should amount to initialization of the initial values to 1 instead of 0.

Thanks for looking into this.

[Jonas Finnemann Jensen (jopsen)]

For future reference, it's probably best to file separate bugs for separate issues...

I was unable to reproduce the max token issues with other strategies than DFS, which never reported max tokens for any negative, queries.
This have been fixed and DFS will now report max tokens on negative queries too...

With respect to incorrect reporting of statistics when initial state satisfies the query... I think I've fixed it - try it out, and tell me if should be something else :)

Note. before we checked if the initial state satisfied the query ín the OverApprox strategy, we don't do this anymore.
I guess it would give the wrong impression of what over-approx does... so now over-approx just does over-approximation,
it doesn't check if the initial state satisfies the query.

I don't know if you're using the trace option... If but if the query is initially satisfied we'll print an empty trace:
     Trace:
     <trace>
     </trace>
Remark: Traces are always printed to stderr, so the should be easy to get hold of without need to parsing things... Just discard the first line...