Bug 648 - Engine does not detect non-determinism, if edges end in the same location
Summary: Engine does not detect non-determinism, if edges end in the same location
Status: NEW
Alias: None
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC All
: P5 critical
Assignee: Alexandre David
Depends on:
Reported: 2018-02-28 11:21 CET by tgunde13
Modified: 2018-02-28 11:22 CET (History)
0 users

See Also:

Model used to reproduce (1.52 KB, text/xml)
2018-02-28 11:21 CET, tgunde13

Note You need to log in before you can comment on or make changes to this bug.
Description tgunde13 2018-02-28 11:21:35 CET
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.
Free for academic and non-commercial use only.

I got the same results on verifytga.

Frequency: 10/10