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

Bug 524 - Simulator breaks when there is an invariant only on the right hand side of the refinement.
Summary: Simulator breaks when there is an invariant only on the right hand side of th...
Status: NEW
Alias: None
Product: UPPAAL TIGA
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P2 normal
Assignee: Alexandre David
URL: http://people.cs.aau.dk/~ulrik/ecdar/...
Depends on:
Blocks:
 
Reported: 2011-08-30 13:07 CEST by Ulrik Nyman
Modified: 2011-08-30 13:07 CEST (History)
0 users

See Also:
Architecture:

Attachments
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 Ulrik Nyman 2011-08-30 13:07:54 CEST 
Properties are found in : http://people.cs.aau.dk/~ulrik/ecdar/bugs/simulatorInvariantBreak.q

A very simple system where two almost identical systems does not refine each other. If the invariant only is present on the right hand side of the refinement then the simulator can reach an inconsistent state after having performed the refinement check.