Created attachment 321 [details]
Model used to reproduce
Observed: If two edges with:
- Same source location
- Same synchronization property
- Overlapping guards
- Same target location
- Exactly one of them having a clock reset
then they will transition to different states.
However, the engine does not detect this (see attached model).
Expected: The engine should respond with the error "IO determinism violated". This is normally the case with non-deterministic models.
1. Start Ecdar
2. Open the attached system
3. Go to the "Verifier" tab
4. Verify the query "consistency: C2". The result is true. C2 is non-deterministic, so this should be false.
5. Verify the query: "refinement: C2 <= C1". The result is false. This refinement check should give the error "IO determinism violated", and the result should be true.
Ecdar. When opening "About UPPAAL", I see "UPPAAL 4.1.4 (rev. 5264), April 2013 Academic and non-commercial use only".
I tried on Windows 10 and on Linux.
I also tried with the following verifytga version:
(Academic) UPPAAL-TIGA 4.1.12-0.16 (rev. 5145), April 2013
Copyright (c) 1995 - 2013, Uppsala University and Aalborg University.
All rights reserved.
Compiled with i686-w64-mingw32-g++ -Wall -DLIBXML_STATIC -DNDEBUG -O2 -ffloat-store -msse2 -m32 -march=core2 -DENABLE_TIGA -DMULTI_TERMINAL -DENABLE_STORE_MINGRAPH -DTIGA_MERGE_STATES -DTIGA_GREEDY_MERGE -DTIGA_OTF_BUCHI -DBOOST_DISABLE_THREADS -mwindows
Free for academic and non-commercial use only.
I got the same results on verifytga.