Simple control system maintaining the level of liquid in a tank.
| define min = 5.                                                   | 
| define max = 10. | 
| define closed = 0.                                                 | 
| define open = 1. | 
| define example() = {                        | 
|   exists V 1,V 2,I,O,L : {                    | 
|    initialise(V 1,V 2,L) and                                        | 
|    keep{                              | 
|     pipe(V 1,I,0,3) and                                          | 
|     pipe(V 2,O,1,1) and                                          | 
|     tank(I,O,L) and                                             | 
|     controller(V 1,V 2,L) and                                     | 
|     format("V 1=%d,V 2=%d,I =%d,O=%d,L=%d∖n", | 
|                 V 1,V 2,I,O,L)                                        | 
|    } and len(50)                                                          | 
|   }                                  | 
| }.                                                                    | 
| /* Initial state. Note valves closed imply that the flows are also zero. */   | 
| define initialise(V 1,V 2,L) = {                          | 
|    V 1 = closed and                                                               | 
|    V 2 = closed and | 
|    L = 0                                                                                      | 
| }.                                                                                  | 
| /* Defines a flow rate F between minf and maxf, or zero if V is closed. */  | 
| define pipe(V,F,minf,maxf) = {                         | 
|    if(V = open) then                                                           | 
|      F = (Random mod (maxf −minf + 1)) + minf                            | 
|     else F = 0                                                                               | 
| }.                                                                                  | 
| /* The level of liquid in a unit interval. */                       | 
| define tank(I,O,L) = {                      | 
|    L := L + I − O                                               | 
| }.                                                                  | 
| /* The state of each valve in a unit interval */                  | 
| define controller(V 1,V 2,L) = {                 | 
|    if L < max then {V 1 := open} else {V 1 := closed} and | 
|    if L > min then {V 2 := open} else {V 2 := closed}    | 
| }.                                                                  | 
Run of the controller:
State 0: V1=0, V2=0, I=0, O=0, L=0 ... State 13: V1=1, V2=1, I=2, O=1, L=10 State 14: V1=0, V2=1, I=0, O=1, L=11 State 15: V1=0, V2=1, I=0, O=1, L=10 ... State 27: V1=1, V2=1, I=0, O=1, L=7 State 28: V1=1, V2=1, I=2, O=1, L=6 State 29: V1=1, V2=1, I=0, O=1, L=7 ... State 42: V1=1, V2=1, I=2, O=1, L=10 State 43: V1=0, V2=1, I=0, O=1, L=11 State 44: V1=0, V2=1, I=0, O=1, L=10 ...
So L does not stay between 5 and 10!
| define min = 5.                                          | 
| define max = 10. | 
| define closed = 0.                                        | 
| define open = 1. | 
| define example() = {                    | 
|   exists V 1,V 2,I1,I,O1,O,L : {            | 
|    initialise(L) and                                        | 
|    keep{                         | 
|     pipe(V 1,I1,I,0,3) and                             | 
|     pipe(V 2,O1,O,1,1) and                            | 
|     tank(I,O,L) and                                    | 
|     controller(V 1,V 2,L,I1,O1) and                   | 
|     format("V 1=%d,I1=%d,I =%d,               | 
|                V 2=%d,O1=%d,O=%d,L=%d∖n", | 
|                 V 1,I1,I,V 2,O1,O,L)                    | 
|    } and len(50)                                               | 
|   }                              | 
| }.                                                           | 
| /* Initial state. Note initial tank level is min. */                     | 
| define initialise(L) = {                         | 
|    L = min                                                                      | 
| }.                                                                       | 
| /* Defines a flow rate F between minf and maxf,                      | 
|  Fw represents the willing flow while                                      | 
|  Fa represents the actually flow which is either the willing flow if | 
|  the valve is open and zero when valve V is closed. */                | 
| define pipe(V,Fw,Fa,minf,maxf) = {                | 
|    Fw = (Random mod (maxf −minf + 1)) + minf and         | 
|    if(V = open) then Fa = Fw else Fa = 0                          | 
| }.                                                                       | 
| /* The level of liquid in a unit interval. */                                      | 
| define tank(I,O,L) = {                            | 
|    L := L + I − O                                                           | 
| }.                                                                               | 
| /* The state of each valve in a unit interval */                                 | 
| define controller(V 1,V 2,I1,O1,L) = {                   | 
|    if L + I1 − O1 <= max then {V 1 = open} else {V 1 = closed} and | 
|    if L + I1 − O1 >= min then {V 2 = open} else {V 2 = closed}    | 
| }.                                                                               | 
Run of the controller:
State 0: V1=1, I1=2, I=2, V2=1, O1=1, O=1, L=5 State 1: V1=1, I1=2, I=2, V2=1, O1=1, O=1, L=6 State 2: V1=1, I1=2, I=2, V2=1, O1=1, O=1, L=7 State 3: V1=1, I1=3, I=3, V2=1, O1=1, O=1, L=8 State 4: V1=1, I1=0, I=0, V2=1, O1=1, O=1, L=10 State 5: V1=1, I1=1, I=1, V2=1, O1=1, O=1, L=9 ... ... State 44: V1=0, I1=3, I=0, V2=1, O1=1, O=1, L=10 State 45: V1=0, I1=3, I=0, V2=1, O1=1, O=1, L=9 State 46: V1=1, I1=0, I=0, V2=1, O1=1, O=1, L=8 State 47: V1=1, I1=1, I=1, V2=1, O1=1, O=1, L=7 State 48: V1=1, I1=2, I=2, V2=1, O1=1, O=1, L=7 State 49: V1=1, I1=1, I=1, V2=1, O1=1, O=1, L=8
Now L does stay between 5 and 10!