| Summary: | The initial state is undefined with invariant using clock initialized other than zero in SMC | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | normal | CC: | adavid |
| Priority: | P5 | ||
| Version: | 4.1.19 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | minimal example | ||
Created attachment 326 [details] minimal example Suppose clock is initialized with value greater than zero: clock A=100.0; And the model has an invariant in the initial location A>=20 which clearly satisfies the initial conditions, yet Uppaal syntax checker complains that "The initial state is undefined".