Backup source of First Example (No. 3)

The following program (also called a '''model''') describes a sawtooth function
with the following shape:


 INIT     <=> 0 <= f = 2.
 INCREASE <=> [](f' = 1).
 DROP     <=> [](f- = 2 => f = 0).

The first three lines (often called '''rules''' or '''named constraints''') define three constraints, and the final line combines those rules.

This program defines the trajectory of a variable f (whose value is a function of nonnegative time) in the following way.

The rule INIT defines the value of f at time 0, which takes an uncertain value between 0 and 2.

The rule INCREASE states that the slope of f if always 1.

The rule DROP states that the value of f is reset to 0 whenever the value reaches 2. (The minus sign after f means the left limit of f).

The final line states that
- INIT is enabled,
- DROP is enabled, and
- INCREASE is enabled whenever it is consistent with DROP.

That is, the priority of DROP is higher than INCREASE.

More examples can be found in the [[Examples]] page.