Bug 523

Summary: SMC throws exception: State does not satisfy invariant
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Alexandre David <adavid>
Status: ASSIGNED ---    
Severity: major    
Priority: P2    
Version: 4.1.4   
Hardware: PC   
OS: Linux   
Attachments: model.xml

Description Marius Mikučionis 2011-08-30 12:46:46 CEST
I've come up with a model which triggers the following in the ConcreteDelay Filter:

 throw Bug("State does not satisfy invariant")

Sadly it does not say anything about the state or invariant concerned, so it is uninformative and needs some debugging to investigate.
Comment 1 Marius Mikučionis 2011-08-30 12:48:08 CEST
Created attachment 243 [details]
Comment 2 Marius Mikučionis 2011-08-30 12:48:34 CEST
Created attachment 244 [details]