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

Bug 524

Summary:	Simulator breaks when there is an invariant only on the right hand side of the refinement.
Product:	UPPAAL TIGA	Reporter:	Ulrik Nyman <ulrik>
Component:	Engine	Assignee:	Alexandre David <adavid>
Status:	NEW ---
Severity:	normal
Priority:	P2
Version:	unspecified
Hardware:	PC
OS:	Linux
URL:	http://people.cs.aau.dk/~ulrik/ecdar/bugs/simulatorInvariantBreak.xml
Architecture:

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.