Possible bug with parsing big int in queries in verifypn
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
New
|
Undecided
|
Unassigned | ||
Bug Description
We should take a look a this. Citing an email (from last year):
I contact you concerning the examination results for the RC competition of the MCC 2023 edition, for model GPPP.
There have been three queries answered differently by Tapaal and SMPT on instance C0010N1000000000. This is the instance that includes a 'large_marking` warning file, meaning that the initial marking of some places cannot be encoded using int32.
We believe that the answers returned by SMPT are correct in these cases and would like to confirm it with you in order to compile correct oracle values for this competition.
The "easiest" such query is number 13, which is an invariant that can be answered using the "state equation" method
=======
Property GPPP-PT-
AG (and (<= E4P c2) (not (<= 3790526071 R5P)))
=======
Could you tell us what is the answer returned by your tools on this query ? Possibly using 64 bits or arbitrary precision arithmetic versions of your tools.
