This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

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
Product: UPPAAL TIGA
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC All
: P5 critical
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2018-02-28 11:21 CET by tgunde13
Modified: 2018-02-28 11:22 CET (History)
0 users

See Also:
Architecture:

Attachments
Model used to reproduce (1.52 KB, text/xml)
2018-02-28 11:21 CET, tgunde13 		Details
Add an attachment (proposed patch, testcase, etc.)

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.

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