Bug 653

Summary: The initial state is undefined with invariant using clock initialized other than zero in SMC
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: normal CC: adavid
Priority: P5    
Version: 4.1.19   
Hardware: All   
OS: All   
Architecture:
Attachments: minimal example

Description Marius Mikučionis 2018-05-02 13:38:50 CEST
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".