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".