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!