Export state label to support imed propositions

[Alfons Laarman]

The simplest way to support time in safety / liveness properties, is to allow their propositions to be expressed in the model, and export them as state labels.

For example an invariant "X < 1", where X is a clock, can be implemented in UPPAAL language with a C function:

boolean X_LT_ONE () {
      return model.X < 1;
}

(correct?)

This function can be exported as a state label X_LT_ONE, which can in LTSmin be used in the invariant / LTL property.

[Mads Chr. Olesen (shiyee)]

In general we need the construction of "Model Checking via Reachability Testing for Timed Automata", by Aceto et. al.

If we reduce the scope to just checking invariants, then we could get by with just adding a state label.