| Summary: | Engine does not detect non-determinism, if edges end in the same location | ||
|---|---|---|---|
| Product: | UPPAAL TIGA | Reporter: | tgunde13 |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | critical | ||
| Priority: | P5 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | Model used to reproduce | ||
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. Steps: 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. Build: 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. Frequency: 10/10