|
| | | The model |
We followed the same scheme as before for combining the LUSTRE controller.
There is however a difference: as LUSTRE is a much more high-level language than our simple AUTOC language, we modelled much of the physical environement in the LUSTRE part, leaving only differential equations/inclusions in the AUTOC part (as well as the scheduler).
The sources are steamboiler.preamble, steamboiler.lus, and steamboiler.environment.m4.
Our model takes into account all the requirement detailed in [1], with 3 pumps (instead of 4). In particular we model
The resulting model is quite big: 63 Boolean or enumerated state variables, and 7 real variables, to which one should add the variables of the environement and of the scheduler linking them.
We detailed below some part of the specification.
The same error protocol is used forall physical devices (pumps, pump controllers, level and steam sensor).
-- **********************************************************************
-- generic 2-states automaton :
-- **********************************************************************
-- switch form false to true if "on" is true
-- switch form true to false if "off" is true
-- remains "init" until the first "on" or the first "off"
node switch(init, on, off : bool) returns (s : bool);
let
s = if(not (init -> pre s)) then (on) else (not off);
tel
-- **********************************************************************
-- 3-state generic automaton
-- **********************************************************************
node switch_on1off12(init,on,off1,off2: bool) returns (state:bool)
var waiting: bool;
let
waiting = switch(false,off1,jafter(off2));
state = switch(init,on, waiting and off2);
tel
-- **********************************************************************
-- Error protocol
-- Special outputs:
-- physical_failure_state: not visible from the controller
-- **********************************************************************
node ErrorProtocol(
FAILURE_DETECTION : bool;
REPAIR_ACK : bool;
iFAILURE : bool;
)
returns (
FAILURE_ACK : bool;
REPAIRED : bool;
physical_failure_state : bool;
)
let
physical_failure_state =
switch_on1off12(false,
iFAILURE,
FAILURE_ACK,iFAILURE);
FAILURE_ACK =
switch(false,
jafter(FAILURE_DETECTION),
jafter(FAILURE_ACK));
REPAIRED =
switch(false,
xedge(not physical_failure_state),
REPAIR_ACK);
tel
-- **********************************************************************
-- A pump and its associated controller
-- Special inputs (simulate non-determinism)
-- iPUMP_FAILURE: first occurence: start of a failure,
-- second: end of the failure
-- iPUMP_CONTROL_FAILURE: idem
-- **********************************************************************
node Pump(
OPEN_PUMP : bool;
CLOSE_PUMP : bool;
PUMP_FAILURE_DETECTION : bool;
PUMP_CONTROL_FAILURE_DETECTION : bool;
PUMP_REPAIR_ACK : bool;
PUMP_CONTROL_REPAIR_ACK : bool;
iPUMP_FAILURE : bool;
iPUMP_CONTROL_FAILURE : bool;
)
returns (
PUMP_STATE : bool;
PUMP_CONTROL_STATE : bool;
PUMP_FAILURE_ACK : bool;
PUMP_CONTROL_FAILURE_ACK: bool;
PUMP_REPAIRED : bool;
PUMP_CONTROL_REPAIRED : bool;
pump_physical_state : bool;
pump_control_physical_state : bool;
pump_physical_failure_state : bool;
pump_control_physical_failure_state : bool
)
let
(PUMP_FAILURE_ACK,PUMP_REPAIRED,pump_physical_failure_state) =
ErrorProtocol( PUMP_FAILURE_DETECTION,
PUMP_REPAIR_ACK,
iPUMP_FAILURE);
(PUMP_CONTROL_FAILURE_ACK,PUMP_CONTROL_REPAIRED,pump_control_physical_failure_state) =
ErrorProtocol( PUMP_CONTROL_FAILURE_DETECTION,
PUMP_CONTROL_REPAIR_ACK,
iPUMP_CONTROL_FAILURE);
pump_physical_state = (false ->
if pump_physical_failure_state then false -- models the effect of the failure: pump_state becomes wrong
else if CLOSE_PUMP then false
else if OPEN_PUMP then true
else pre pump_physical_state);
PUMP_STATE = jafter(pump_physical_state); -- the controller has the knowledge at the next cycle
pump_control_physical_state = (false ->
if pump_physical_failure_state or pump_control_physical_failure_state then false
else if CLOSE_PUMP then false
else if jafter(OPEN_PUMP) then true
else pre pump_control_physical_state);
PUMP_CONTROL_STATE = jafter(pump_control_physical_state);
tel
We display some parts of the node Controller.
-- computed quantities
clevel1 = LEVEL -> pre (alevel1) + apump1*DELTA - 125.0;
clevel2 = LEVEL -> pre (alevel2) + apump2*DELTA;
csteam1 = 0.0;
csteam2 = W;
cpump1 = PumpFlow1(N,PUMP_ERROR,PUMP_CONTROL_STATE);
cpump2 = PumpFlow2(N,PUMP_ERROR,PUMP_CONTROL_STATE);
-- estimated quantities
(alevel1,alevel2) =
if LEVEL<0.0 then (clevel1,clevel2)
else (LEVEL,LEVEL);
(asteam1,asteam2) = if STEAM_ERROR then (csteam1,csteam2) else (STEAM,STEAM);
(apump1,apump2) = (cpump1,cpump2);
-- number of pumps that should be active
shouldbeactive =
if LEVEL<0.0 then -- level failure
if alevel2 < 500.0 then TROIS
else if alevel1 < N1 then DEUX
else ZERO
else
if LEVEL < 500.0 then TROIS
else if LEVEL < N2 then DEUX
else ZERO
;
pfunc = PUMP_CONTROL_STATE and not PUMP_ERROR;
active = if Tall(N, pfunc) then TROIS
else if Tnone(N,pfunc) then ZERO
else if Tone(N,pfunc) then UN
else DEUX
;
open = Inf(active,shouldbeactive); -- should we open a pump ?
close = Sup(active,shouldbeactive); -- should we close a pump ?
OPEN_PUMP = if open then SearchPumpToOpen(Sub(shouldbeactive,active),PUMP_CONTROL_STATE,PUMP_ERROR) else false^N;
CLOSE_PUMP = if close then SearchPumpToClose(Sub(active,shouldbeactive),PUMP_CONTROL_STATE,PUMP_ERROR) else false^N;
The following node choose a number of pumps not in failure state to open.
node SearchPumpToOpen(
nb : Integer;
PUMP_CONTROL_STATE: bool^N;
PUMP_ERROR : bool^N
)
returns(
open : bool^N
)
var nbdone : Integer^N;
done : bool^N;
let
nbdone[0] = if open[0] then Pred(nb) else nb;
nbdone[1..N-1] = if open[1..N-1] then Pred(nbdone[0..N-2]) else nbdone[0..N-2];
done = EgalZero(nbdone);
open[0] = false -> (not PUMP_ERROR[0] and not PUMP_CONTROL_STATE[0]);
open[1..N-1] = false^(N-1) -> (not done[0..N-2] and not PUMP_ERROR[1..N-1] and not PUMP_CONTROL_STATE[1..N-1]);
tel
|
| | | The model |