| Summary: | SMC throws exception: State does not satisfy invariant | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | ASSIGNED --- | ||
| Severity: | major | ||
| Priority: | P2 | ||
| Version: | 4.1.4 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: |
model.xml
query.q |
||
Created attachment 243 [details]
model.xml
Created attachment 244 [details]
query.q
|
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.