Created attachment 279 [details] A simple model that illustrates the problem The verification results are incorrect, when the queries are run as a batch (all selected) in the verifier tab in UPPAAL. For the attached example, all queries (Q1 - Q4) pass when run as a batch. However, this is incorrect: We know that Q4 should fail! When we run the queries individually, we get the correct results. I have previously seen a similar problem (which is probably caused by the same problem): Changing one query may affect the results of other queries (and care has been taken to ensure that the queries are side-effect-free). I have marked the problem as critical because a formal verifier should never present wrong results. PS: How do we get a newer version than 4.19? Best regards, Allan Munck
Also, the external verifier "verifyta" produces different results than shown in the verifier tab in UPPAAL.
Dear Alan Munck, Thanks for the report. I am trying to reproduce it and I observe the strange behavior (not satisfied in individual checks and erroneously satisfied in batch) with the first query: A[] APP.ShowingList imply APP.listSize() == MaxRftListLength The other 3 queries are satisfied (correctly). There is no newer public release, but there's a beta snapshot: http://people.cs.aau.dk/~marius/beta/uppaal-4.1.20-beta7.zip (it seems that this particular issue is fixed over there) Marius
Fixed in the 4.1.20 release