| MODULE main |
| VAR |
| CN : Controller_Synth(SC.mode_event_Gs, SC.mode_event_CBs, SC.init_state_Gs, SC.init_state_CBs); |
| SC: System_Configuration(CN.cmd_to_Gs, CN.cmd_to_CBs); |
| |
| -- ----------------------------------------------------------- |
| -- Definition of the properties that verify the requirements: |
| |
| -- R1: No bus will be connected to more than 1 power source at any time. |
| -- |
| -- is_broken is true iff the bus is (or was) connected to more than 1 |
| -- power source. |
| INVARSPEC NAME R1_true := !(SC.B1.is_broken | SC.B2.is_broken | SC.B3.is_broken); |
| |
| -- R2: If any power source is on, then all busses will be powered |
| -- |
| -- In R2 we verify that the requirement holds, if there are less than 3 faults |
| INVARSPEC |
| NAME R2_true := |
| ((SC.G1.is_on | SC.G2.is_on | SC.G3.is_on) & (CN.MN.faults_counter < 3)) -> |
| (SC.B1.is_powered & SC.B2.is_powered & SC.B3.is_powered); |
| |
| -- In R2 we verify that there is at least a configuration in which all the |
| -- buses are unpowered. (E.g., the safe configuration where everything is |
| -- off) |
| INVARSPEC |
| NAME R2_false := |
| ((SC.G1.is_on | SC.G2.is_on | SC.G3.is_on)) -> |
| (SC.B1.is_powered & SC.B2.is_powered & SC.B3.is_powered); |
| |
| INVARSPEC NAME R2_fta := (SC.B1.is_powered & SC.B2.is_powered & SC.B3.is_powered); |
| INVARSPEC NAME R2_fta_B1 := (SC.B1.is_powered); |
| INVARSPEC NAME R2_fta_B2 := (SC.B2.is_powered); |
| INVARSPEC NAME R2_fta_B3 := (SC.B3.is_powered); |
| |
| -- R4: If no power source is on, then all buses will be unpowered |
| INVARSPEC |
| NAME R4_true := |
| ((SC.G1.is_off & SC.G2.is_off & SC.G3.is_off) -> |
| (!SC.B1.is_powered & !SC.B2.is_powered & !SC.B3.is_powered)); |
| |
| -- R6: Never more than two generators on unless required in case of failure |
| INVARSPEC |
| NAME R6_true := |
| (CN.MN.faults_counter = 0) -> (SC.G1.is_off | SC.G2.is_off | SC.G3.is_off) |
| |
| -- --------------------------------------------------------------------- |
| -- ---------------------------------------------------------- |
| -- We verify that the monitor correctly knows the state of |
| -- the system at anytime |
| |
| INVARSPEC NAME Monitor_State_Consistency_true := |
| (SC.G1.state = CN.MN.state_est_G1) & |
| (SC.G2.state = CN.MN.state_est_G2) & |
| (SC.G3.state = CN.MN.state_est_G3) & |
| (SC.GB1.state = CN.MN.state_est_GB1) & |
| (SC.GB2.state = CN.MN.state_est_GB2) & |
| (SC.GB3.state = CN.MN.state_est_GB3) & |
| (SC.BB1.state = CN.MN.state_est_BB1) & |
| (SC.BB2.state = CN.MN.state_est_BB2) & |
| (SC.BB3.state = CN.MN.state_est_BB3); |
| |
| -- ------------------------------------------------------------------------- |
| -- From each nominal state it is always possible to end up in a faulty state |
| CTLSPEC |
| NAME system_can_always_fail_true := |
| AG( CN.MN.faults_counter = 0 -> EX (CN.MN.faults_counter >0)) |
| |
| -- We also verify that there is always a path in which there is no fault |
| CTLSPEC |
| NAME system_can_always_work_true := |
| EG (CN.MN.faults_counter = 0); |
| -- ------------------------------------------------------------------------- |
| |
| -- ------------------------------------------------------------------- |
| -- We can verify that each component can always go from a nominal state |
| -- to a faulty state: |
| |
| -- Generators can always go to a faulty state |
| CTLSPEC |
| NAME G1_can_always_fail_true := |
| AG( CN.MN.mode_est_G1 = ok -> EX (CN.MN.mode_est_G1 = ko)) |
| |
| CTLSPEC |
| NAME G2_can_always_fail_true := |
| AG( CN.MN.mode_est_G2 = ok -> EX (CN.MN.mode_est_G2 = ko)) |
| |
| CTLSPEC |
| NAME G3_can_always_fail_true := |
| AG( CN.MN.mode_est_G3 = ok -> EX (CN.MN.mode_est_G3 = ko)) |
| |
| -- and also switches can always become stuck_at_open or stuck_at_close |
| -- GB1, GB2, GB3: |
| CTLSPEC |
| NAME GB1_can_always_fail_true := |
| AG( CN.MN.mode_est_GB1 = ok -> |
| EX (CN.MN.mode_est_GB1 = ko_open) & |
| EX (CN.MN.mode_est_GB1 = ko_closed) ) |
| CTLSPEC |
| NAME GB2_can_always_fail_true := |
| AG( CN.MN.mode_est_GB2 = ok -> |
| EX (CN.MN.mode_est_GB2 = ko_open) & |
| EX (CN.MN.mode_est_GB2 = ko_closed) ) |
| CTLSPEC |
| NAME GB3_can_always_fail_true := |
| AG( CN.MN.mode_est_GB3 = ok -> |
| EX (CN.MN.mode_est_GB3 = ko_open) & |
| EX (CN.MN.mode_est_GB3 = ko_closed) ) |
| -- BB1, BB2, BB3: |
| CTLSPEC |
| NAME BB1_can_always_fail_true := |
| AG( CN.MN.mode_est_BB1 = ok -> |
| EX (CN.MN.mode_est_BB1 = ko_open) & |
| EX (CN.MN.mode_est_BB1 = ko_closed) ) |
| CTLSPEC |
| NAME BB2_can_always_fail_true := |
| AG( CN.MN.mode_est_BB2 = ok -> |
| EX (CN.MN.mode_est_BB2 = ko_open) & |
| EX (CN.MN.mode_est_BB2 = ko_closed) ) |
| CTLSPEC |
| NAME BB3_can_always_fail_true := |
| AG( CN.MN.mode_est_BB3 = ok -> |
| EX (CN.MN.mode_est_BB3 = ko_open) & |
| EX (CN.MN.mode_est_BB3 = ko_closed) ) |
| |
| -- --------------------------------------------------------------- |
| |
| -- --------------------------------------------------------------- |
| -- If there are no faults, the system is in the base configuration |
| DEFINE |
| base_conf := SC.G1.is_on & SC.G2.is_on & SC.G3.is_off & |
| SC.GB1.is_closed & SC.GB2.is_closed & SC.GB3.is_open & |
| SC.BB1.is_open & SC.BB2.is_closed & SC.BB3.is_open; |
| |
| LTLSPEC |
| NAME system_in_base_configuration_until_fault_true := |
| ( base_conf U (CN.MN.faults_counter > 0)) | G base_conf; |
| |
| -- --------------------------------------------------------------- |
| |
| |
| -- END MODULE MAIN -- |
| |
| MODULE System_Configuration(cmd_to_Gs, cmd_to_CBs) |
| |
| DEFINE |
| init_state_G1 := on; |
| init_state_G2 := on; |
| init_state_G3 := off; |
| |
| init_state_GB1 := closed; |
| init_state_GB2 := closed; |
| init_state_GB3 := open; |
| init_state_BB1 := open; |
| init_state_BB2 := closed; |
| init_state_BB3 := open; |
| |
| VAR |
| G1 : Generator(cmd_to_Gs[index_G1], init_state_G1); |
| G2 : Generator(cmd_to_Gs[index_G2], init_state_G2); |
| G3 : Generator(cmd_to_Gs[index_G3], init_state_G3); |
| |
| GB1 : Switch(cmd_to_CBs[index_GB1], init_state_GB1); |
| GB2 : Switch(cmd_to_CBs[index_GB2], init_state_GB2); |
| GB3 : Switch(cmd_to_CBs[index_GB3], init_state_GB3); |
| |
| BB1 : Switch(cmd_to_CBs[index_BB1], init_state_BB1); |
| BB2 : Switch(cmd_to_CBs[index_BB2], init_state_BB2); |
| BB3 : Switch(cmd_to_CBs[index_BB3], init_state_BB3); |
| |
| B1 : Bus(B1_poweredby_G1, B1_poweredby_G2, B1_poweredby_G3); |
| B2 : Bus(B2_poweredby_G1, B2_poweredby_G2, B2_poweredby_G3); |
| B3 : Bus(B3_poweredby_G1, B3_poweredby_G2, B3_poweredby_G3); |
| |
| -- Definition of the signals (in matrix format) used by Controller to know the state of the single components -- |
| |
| DEFINE |
| init_state_Gs := [ |
| init_state_G1, |
| init_state_G2, |
| init_state_G3]; |
| |
| init_state_CBs := [ |
| init_state_GB1, |
| init_state_GB2, |
| init_state_GB3, |
| init_state_BB1, |
| init_state_BB2, |
| init_state_BB3]; |
| |
| DEFINE |
| index_GB1 := 0; |
| index_GB2 := 1; |
| index_GB3 := 2; |
| |
| index_BB1 := 3; |
| index_BB2 := 4; |
| index_BB3 := 5; |
| |
| index_G1 := 0; |
| index_G2 := 1; |
| index_G3 := 2; |
| |
| DEFINE |
| mode_event_Gs := [ |
| fault_event_off_Gs, |
| nominal_event_Gs]; |
| |
| mode_event_CBs := [ |
| fault_event_open_CBs, |
| fault_event_closed_CBs, |
| nominal_event_CBs]; |
| |
| DEFINE |
| fault_event_open_CBs := [ |
| GB1.fault_event_stuck_at_open, |
| GB2.fault_event_stuck_at_open, |
| GB3.fault_event_stuck_at_open, |
| BB1.fault_event_stuck_at_open, |
| BB2.fault_event_stuck_at_open, |
| BB3.fault_event_stuck_at_open]; |
| |
| fault_event_closed_CBs := [ |
| GB1.fault_event_stuck_at_closed, |
| GB2.fault_event_stuck_at_closed, |
| GB3.fault_event_stuck_at_closed, |
| BB1.fault_event_stuck_at_closed, |
| BB2.fault_event_stuck_at_closed, |
| BB3.fault_event_stuck_at_closed]; |
| |
| nominal_event_CBs := [ |
| GB1.nominal_event, |
| GB2.nominal_event, |
| GB3.nominal_event, |
| BB1.nominal_event, |
| BB2.nominal_event, |
| BB3.nominal_event]; |
| |
| DEFINE |
| fault_event_off_Gs := [ |
| G1.fault_event_stuck_at_off, |
| G2.fault_event_stuck_at_off, |
| G3.fault_event_stuck_at_off]; |
| |
| nominal_event_Gs := [ |
| G1.nominal_event, |
| G2.nominal_event, |
| G3.nominal_event]; |
| |
| |
| -- Definition of the possible paths to Bus 1 -- |
| |
| DEFINE |
| B1_poweredby_G1_U := (G1.is_on) & (GB1.is_closed); |
| B1_poweredby_G2_L := B3_poweredby_G2_L & (BB3.is_closed); |
| B1_poweredby_G2_R := B2_poweredby_G2_U & (BB1.is_closed); |
| B1_poweredby_G3_L := B3_poweredby_G3_U & (BB3.is_closed); |
| B1_poweredby_G3_R := B2_poweredby_G3_R & (BB1.is_closed); |
| |
| -- Definition of the possible paths to Bus 2 -- |
| |
| DEFINE |
| B2_poweredby_G1_L := B1_poweredby_G1_U & (BB1.is_closed); |
| B2_poweredby_G1_R := B3_poweredby_G1_R & (BB2.is_closed); |
| B2_poweredby_G2_U := (G2.is_on) & (GB2.is_closed); |
| B2_poweredby_G3_L := B1_poweredby_G3_L & (BB1.is_closed); |
| B2_poweredby_G3_R := B3_poweredby_G3_U & (BB2.is_closed); |
| |
| -- Definition of the possible paths to Bus 3 -- |
| |
| DEFINE |
| B3_poweredby_G1_L := B2_poweredby_G1_L & (BB2.is_closed); |
| B3_poweredby_G1_R := B1_poweredby_G1_U & (BB3.is_closed); |
| B3_poweredby_G2_L := B2_poweredby_G2_U & (BB2.is_closed); |
| B3_poweredby_G2_R := B1_poweredby_G2_R & (BB3.is_closed); |
| B3_poweredby_G3_U := (G3.is_on) & (GB3.is_closed); |
| |
| |
| -- Definition of the possible inputs for Bus 1 -- |
| |
| DEFINE |
| B1_poweredby_G1 := B1_poweredby_G1_U; |
| B1_poweredby_G2 := B1_poweredby_G2_R | B1_poweredby_G2_L; |
| B1_poweredby_G3 := B1_poweredby_G3_R | B1_poweredby_G3_L; |
| |
| -- Definition of the possible inputs for Bus 2 -- |
| |
| DEFINE |
| B2_poweredby_G1 := B2_poweredby_G1_R | B2_poweredby_G1_L; |
| B2_poweredby_G2 := B2_poweredby_G2_U; |
| B2_poweredby_G3 := B2_poweredby_G3_R | B2_poweredby_G3_L; |
| |
| -- Definition of the possible inputs for Bus 3 -- |
| |
| DEFINE |
| B3_poweredby_G1 := B3_poweredby_G1_R | B3_poweredby_G1_L; |
| B3_poweredby_G2 := B3_poweredby_G2_R | B3_poweredby_G2_L; |
| B3_poweredby_G3 := B3_poweredby_G3_U; |
| |
| -- END MODULE SYSTEM CONFIGURATION -- |
| |
| MODULE Generator(cmd, init_state) |
| VAR |
| state : {on, off}; |
| |
| -- Definition of the transition labels between nominal and faulty state -- |
| IVAR |
| fault_event_stuck_at_off : boolean; |
| nominal_event : boolean; |
| TRANS |
| nominal_event = FALSE; |
| |
| DEFINE |
| is_on := (state = on); |
| DEFINE |
| is_off := (state = off); |
| |
| ASSIGN |
| next(state) := |
| case |
| (cmd = cmd_on) : on; |
| (cmd = cmd_off) : off; |
| TRUE : state; |
| esac; |
| |
| ASSIGN |
| init(state) := init_state; |
| |
| -- END MODULE GENERATOR -- |
| |
| |
| MODULE Switch(cmd, init_state) |
| VAR |
| state : {open, closed}; |
| |
| -- Definition of the transition labels between nominal and faulty states -- |
| IVAR |
| fault_event_stuck_at_closed : boolean; |
| fault_event_stuck_at_open : boolean; |
| nominal_event : boolean; |
| |
| DEFINE |
| is_closed := (state = closed); |
| |
| DEFINE |
| is_open := (state = open); |
| |
| ASSIGN |
| next(state) := |
| case |
| (cmd = cmd_open) : open; |
| (cmd = cmd_closed) : closed; |
| TRUE : state; |
| esac; |
| |
| ASSIGN |
| init(state) := init_state; |
| |
| -- END MODULE SWITCH -- |
| |
| MODULE Bus(in1, in2, in3) |
| VAR |
| state : {working, broken}; |
| |
| DEFINE |
| is_broken := (state = broken); |
| DEFINE |
| is_powered := (state = working) & (count((in1), (in2), (in3)) = 1); |
| |
| -- When the bus is overpowered it becomes broken and unfixable -- |
| ASSIGN |
| init(state) := |
| case |
| (count((in1), (in2), (in3)) > 1) : broken; |
| TRUE : working; |
| esac; |
| |
| next(state) := |
| case |
| next((count((in1), (in2), (in3)) > 1)) : broken; |
| TRUE : state; |
| esac; |
| |
| -- END MODULE BUS -- |
| -- The Synthesized controller is built by defining the constraints that |
| -- we want our system to satisfy. When a fault occurs, the controller |
| -- will try to find a configuration for the system that satisfies all |
| -- the requirements. |
| -- As opposed to the Explicit Faults controller, this strategy results |
| -- in a much simpler (and compact) controller. |
| -- |
| -- In order to work, the Synthesized controller uses a Monitor. The |
| -- Monitor has two goals: |
| -- 1. keep track of the modes of each component |
| -- 2. predict the behaviour of a command |
| -- With these information, the controller can reason on what would |
| -- happen if he issues a certain command. E.g., if G1 is faulty |
| -- (stuck_at_off) then the controller can issue the command do_on |
| -- but this will have no effect since the generator is faulty. |
| -- The monitor will, therefore, estimate that this command will |
| -- not be useful and say that the component will stay |
| |
| -- The module takes as parameter the mode events and the initial states |
| -- of the components. The mode events are the signals that denote a |
| -- transition from healthy to faulty (or viceversa). |
| MODULE Controller_Synth(mode_event_Gs, mode_event_CBs, init_state_Gs, init_state_CBs) |
| |
| -- The controller uses a Monitor. This monitor takes as parameter |
| -- the mode signals (mode_event_*) the command signals (cmd_to_*) |
| -- and the initial configuration of each component (init_state_*) |
| VAR |
| MN : Monitor(mode_event_Gs, mode_event_CBs, cmd_to_Gs, cmd_to_CBs, init_state_Gs, init_state_CBs); |
| |
| -- We define the possible commands for each component. |
| -- Apart from the commands to bring the system into |
| -- a particular state, we have also the nop command. |
| -- This command is useful if we know that a component |
| -- is already in a particular state and we do not want |
| -- to modify it. |
| IVAR |
| cmd_to_GB1 : {cmd_closed, cmd_open, nop}; |
| cmd_to_GB2 : {cmd_closed, cmd_open, nop}; |
| cmd_to_GB3 : {cmd_closed, cmd_open, nop}; |
| |
| cmd_to_BB1 : {cmd_closed, cmd_open, nop}; |
| cmd_to_BB2 : {cmd_closed, cmd_open, nop}; |
| cmd_to_BB3 : {cmd_closed, cmd_open, nop}; |
| |
| cmd_to_G1 : {cmd_on, cmd_off, nop}; |
| cmd_to_G2 : {cmd_on, cmd_off, nop}; |
| cmd_to_G3 : {cmd_on, cmd_off, nop}; |
| |
| -- We now group the commands by component's type: |
| -- cmd_to_Gs and cmd_to_CBs |
| DEFINE |
| cmd_to_Gs := [ |
| cmd_to_G1, |
| cmd_to_G2, |
| cmd_to_G3]; |
| |
| cmd_to_CBs := [ |
| cmd_to_GB1, |
| cmd_to_GB2, |
| cmd_to_GB3, |
| cmd_to_BB1, |
| cmd_to_BB2, |
| cmd_to_BB3]; |
| |
| -- In general, there are two ways of disable the block |
| -- G1+GB1: 1) turn off G1 or 2) open GB1 (or both). |
| -- To avoid this non-determinism we add the following |
| -- assumption: When GBn is open the Gn must be off. |
| TRANS |
| (next(MN.state_est_GB1) = open) -> (cmd_to_G1 = cmd_off); |
| |
| TRANS |
| (next(MN.state_est_GB2) = open) -> (cmd_to_G2 = cmd_off); |
| |
| TRANS |
| (next(MN.state_est_GB3) = open) -> (cmd_to_G3 = cmd_off); |
| |
| |
| -- Similarly to what we did in the System model, we need |
| -- to keep track of the information of which Bus is powered |
| -- by which generator and how. |
| -- Note, however, that in this case we are not interested in |
| -- the current state of the system, but in the future state |
| -- (i.e., next( ) ). |
| -- This means that, e.g., B1_poweredby_G1_U should be read |
| -- as follows: the bus B1 will be powered by G1 from above. |
| -- Remember that Up,Left and Right indicate where the power |
| -- comes from from the point of view of the Bus. E.g., |
| -- B1_poweredby_G2_L identify the path BB2+BB3 from G2 to B1 |
| |
| -- Definition of the possible paths to Bus 1 -- |
| DEFINE |
| B1_poweredby_G1_U := (next(MN.state_est_G1) = on) & (next(MN.state_est_GB1) = closed); |
| B1_poweredby_G2_L := B3_poweredby_G2_L & (next(MN.state_est_BB3) = closed); |
| B1_poweredby_G2_R := B2_poweredby_G2_U & (next(MN.state_est_BB1) = closed); |
| B1_poweredby_G3_L := B3_poweredby_G3_U & (next(MN.state_est_BB3) = closed); |
| B1_poweredby_G3_R := B2_poweredby_G3_R & (next(MN.state_est_BB1) = closed); |
| |
| -- Definition of the possible paths to Bus 2 -- |
| DEFINE |
| B2_poweredby_G1_L := B1_poweredby_G1_U & (next(MN.state_est_BB1) = closed); |
| B2_poweredby_G1_R := B3_poweredby_G1_R & (next(MN.state_est_BB2) = closed); |
| B2_poweredby_G2_U := (next(MN.state_est_G2) = on) & (next(MN.state_est_GB2) = closed); |
| B2_poweredby_G3_L := B1_poweredby_G3_L & (next(MN.state_est_BB1) = closed); |
| B2_poweredby_G3_R := B3_poweredby_G3_U & (next(MN.state_est_BB2) = closed); |
| |
| -- Definition of the possible paths to Bus 3 -- |
| DEFINE |
| B3_poweredby_G1_L := B2_poweredby_G1_L & (next(MN.state_est_BB2) = closed); |
| B3_poweredby_G1_R := B1_poweredby_G1_U & (next(MN.state_est_BB3) = closed); |
| B3_poweredby_G2_L := B2_poweredby_G2_U & (next(MN.state_est_BB2) = closed); |
| B3_poweredby_G2_R := B1_poweredby_G2_R & (next(MN.state_est_BB3) = closed); |
| B3_poweredby_G3_U := (next(MN.state_est_G3) = on) & (next(MN.state_est_GB3) = closed); |
| |
| -- We now abstract from the particular path used to power |
| -- the bus, and simply say which generator will power |
| -- the bus. |
| DEFINE |
| B1_poweredby_G1 := B1_poweredby_G1_U; |
| B1_poweredby_G2 := B1_poweredby_G2_R | B1_poweredby_G2_L; |
| B1_poweredby_G3 := B1_poweredby_G3_R | B1_poweredby_G3_L; |
| |
| DEFINE |
| B2_poweredby_G1 := B2_poweredby_G1_R | B2_poweredby_G1_L; |
| B2_poweredby_G2 := B2_poweredby_G2_U; |
| B2_poweredby_G3 := B2_poweredby_G3_R | B2_poweredby_G3_L; |
| |
| DEFINE |
| B3_poweredby_G1 := B3_poweredby_G1_R | B3_poweredby_G1_L; |
| B3_poweredby_G2 := B3_poweredby_G2_R | B3_poweredby_G2_L; |
| B3_poweredby_G3 := B3_poweredby_G3_U; |
| |
| |
| -- We can now encode the logic of the controller. |
| -- In order to do so, we define the constraints that represent |
| -- our requirements. |
| |
| -- Requirement R1 -- |
| -- R1: No bus will be connected to more than 1 power source at any time. |
| -- |
| -- This requirement is formalized in two steps: |
| -- 1. We explicit that a Bus is working if and only if |
| -- it is not powered by more than two generators |
| -- 2. We force all the Buses to be working. |
| DEFINE |
| B1_is_working := |
| (B1_poweredby_G1 -> !B1_poweredby_G2) & |
| (B1_poweredby_G2 -> !B1_poweredby_G3) & |
| (B1_poweredby_G3 -> !B1_poweredby_G1); |
| |
| DEFINE |
| B2_is_working := |
| (B2_poweredby_G1 -> !B2_poweredby_G2) & |
| (B2_poweredby_G2 -> !B2_poweredby_G3) & |
| (B2_poweredby_G3 -> !B2_poweredby_G1); |
| |
| DEFINE |
| B3_is_working := |
| (B3_poweredby_G1 -> !B3_poweredby_G2) & |
| (B3_poweredby_G2 -> !B3_poweredby_G3) & |
| (B3_poweredby_G3 -> !B3_poweredby_G1); |
| |
| -- This TRANS forces all the buses to be working. |
| TRANS |
| B1_is_working & |
| B2_is_working & |
| B3_is_working; |
| |
| |
| -- In order to encode R3, we need to define the commands |
| -- that will bring our system into a configuration |
| -- in which a bus will be powered by a particular generator |
| -- through a particular path. |
| -- E.g., cmd_B1_poweredby_G1_U is the command that requires |
| -- G1 to go in the state on and GB1 in the state closed. |
| |
| DEFINE |
| cmd_B1_poweredby_G1_U := (cmd_to_G1 = cmd_on) & (cmd_to_GB1 = cmd_closed); |
| cmd_B1_poweredby_G2_R := cmd_B2_poweredby_G2_U & (cmd_to_BB1 = cmd_closed); |
| cmd_B1_poweredby_G2_L := cmd_B3_poweredby_G2_L & (cmd_to_BB3 = cmd_closed); |
| cmd_B1_poweredby_G3_L := cmd_B3_poweredby_G3_U & (cmd_to_BB3 = cmd_closed); |
| cmd_B1_poweredby_G3_R := cmd_B2_poweredby_G3_R & (cmd_to_BB1 = cmd_closed); |
| |
| DEFINE |
| cmd_B2_poweredby_G2_U := (cmd_to_G2 = cmd_on) & (cmd_to_GB2 = cmd_closed); |
| cmd_B2_poweredby_G1_L := cmd_B1_poweredby_G1_U & (cmd_to_BB1 = cmd_closed); |
| cmd_B2_poweredby_G1_R := cmd_B3_poweredby_G1_R & (cmd_to_BB2 = cmd_closed); |
| cmd_B2_poweredby_G3_R := cmd_B3_poweredby_G3_U & (cmd_to_BB2 = cmd_closed); |
| cmd_B2_poweredby_G3_L := cmd_B1_poweredby_G3_L & (cmd_to_BB1 = cmd_closed); |
| |
| DEFINE |
| cmd_B3_poweredby_G2_L := cmd_B2_poweredby_G2_U & (cmd_to_BB2 = cmd_closed); |
| cmd_B3_poweredby_G2_R := cmd_B1_poweredby_G2_R & (cmd_to_BB3 = cmd_closed); |
| cmd_B3_poweredby_G1_R := cmd_B1_poweredby_G1_U & (cmd_to_BB3 = cmd_closed); |
| cmd_B3_poweredby_G1_L := cmd_B2_poweredby_G1_L & (cmd_to_BB2 = cmd_closed); |
| cmd_B3_poweredby_G3_U := (cmd_to_G3 = cmd_on) & (cmd_to_GB3 = cmd_closed); |
| |
| -- Since there could be faults in the system, we need to check whether it is |
| -- possible to go into a particular configuration. For example, if a |
| -- switch is stuck_at_open, we cannot go into a configuration that requires |
| -- the switch to be closed. We identify with these can_do_* DEFINEs. |
| DEFINE |
| can_do_B1_poweredby_G1_U := (next(MN.mode_est_G1) = ok) & (next(MN.mode_est_GB1) in {ok, ko_closed}); |
| can_do_B1_poweredby_G2_R := can_do_B2_poweredby_G2_U & (next(MN.mode_est_BB1) in {ok, ko_closed}); |
| can_do_B1_poweredby_G2_L := can_do_B3_poweredby_G2_L & (next(MN.mode_est_BB3) in {ok, ko_closed}); |
| can_do_B1_poweredby_G3_L := can_do_B3_poweredby_G3_U & (next(MN.mode_est_BB3) in {ok, ko_closed}); |
| can_do_B1_poweredby_G3_R := can_do_B2_poweredby_G3_R & (next(MN.mode_est_BB1) in {ok, ko_closed}); |
| |
| DEFINE |
| can_do_B2_poweredby_G2_U := (next(MN.mode_est_G2) = ok) & (next(MN.mode_est_GB2) in {ok, ko_closed}); |
| can_do_B2_poweredby_G1_L := can_do_B1_poweredby_G1_U & (next(MN.mode_est_BB1) in {ok, ko_closed}); |
| can_do_B2_poweredby_G1_R := can_do_B3_poweredby_G1_R & (next(MN.mode_est_BB2) in {ok, ko_closed}); |
| can_do_B2_poweredby_G3_R := can_do_B3_poweredby_G3_U & (next(MN.mode_est_BB2) in {ok, ko_closed}); |
| can_do_B2_poweredby_G3_L := can_do_B1_poweredby_G3_L & (next(MN.mode_est_BB1) in {ok, ko_closed}); |
| |
| |
| DEFINE |
| can_do_B3_poweredby_G2_L := can_do_B2_poweredby_G2_U & (next(MN.mode_est_BB2) in {ok, ko_closed}); |
| can_do_B3_poweredby_G2_R := can_do_B1_poweredby_G2_R & (next(MN.mode_est_BB3) in {ok, ko_closed}); |
| can_do_B3_poweredby_G1_R := can_do_B1_poweredby_G1_U & (next(MN.mode_est_BB3) in {ok, ko_closed}); |
| can_do_B3_poweredby_G1_L := can_do_B2_poweredby_G1_L & (next(MN.mode_est_BB2) in {ok, ko_closed}); |
| can_do_B3_poweredby_G3_U := (next(MN.mode_est_G3) = ok) & (next(MN.mode_est_GB3) in {ok, ko_closed}); |
| |
| |
| -- Requirement R3 -- |
| -- R3: Path and Generator priority |
| -- |
| -- R3 is formalized by specifying the priority of the |
| -- different configurations. In particular, we use a |
| -- case statement in order to prioritize the choices |
| -- for each bus. |
| -- E.g., for B1 we specify that the best configuration |
| -- is being powered by G1 from above (G1_U), |
| -- followed by being powered by G2 from the right |
| -- (G2_R) etc. |
| |
| -- B1 preferences |
| TRANS |
| case |
| can_do_B1_poweredby_G1_U : cmd_B1_poweredby_G1_U; |
| can_do_B1_poweredby_G2_R : cmd_B1_poweredby_G2_R; |
| can_do_B1_poweredby_G2_L : cmd_B1_poweredby_G2_L; |
| can_do_B1_poweredby_G3_L : cmd_B1_poweredby_G3_L; |
| can_do_B1_poweredby_G3_R : cmd_B1_poweredby_G3_R; |
| TRUE : TRUE; |
| esac; |
| |
| -- B2 preferences |
| TRANS |
| case |
| can_do_B2_poweredby_G2_U : cmd_B2_poweredby_G2_U; |
| can_do_B2_poweredby_G1_L : cmd_B2_poweredby_G1_L; |
| can_do_B2_poweredby_G1_R : cmd_B2_poweredby_G1_R; |
| can_do_B2_poweredby_G3_R : cmd_B2_poweredby_G3_R; |
| can_do_B2_poweredby_G3_L : cmd_B2_poweredby_G3_L; |
| TRUE : TRUE; |
| esac; |
| |
| -- B3 preferences |
| TRANS |
| case |
| can_do_B3_poweredby_G2_L : cmd_B3_poweredby_G2_L; |
| can_do_B3_poweredby_G2_R : cmd_B3_poweredby_G2_R; |
| can_do_B3_poweredby_G1_R : cmd_B3_poweredby_G1_R; |
| can_do_B3_poweredby_G1_L : cmd_B3_poweredby_G1_L; |
| can_do_B3_poweredby_G3_U : cmd_B3_poweredby_G3_U; |
| TRUE : TRUE; |
| esac; |
| |
| -- END MODULE CONTROLLER -- |
| MODULE Monitor(mode_event_Gs, mode_event_CBs, cmd_to_Gs, cmd_to_CBs, init_state_Gs, init_state_CBs) |
| |
| -- Definition of the monitors for the circuit components -- |
| VAR |
| mode_est_GB1 : {ok, ko_open, ko_closed}; |
| mode_est_GB2 : {ok, ko_open, ko_closed}; |
| mode_est_GB3 : {ok, ko_open, ko_closed}; |
| |
| mode_est_BB1 : {ok, ko_open, ko_closed}; |
| mode_est_BB2 : {ok, ko_open, ko_closed}; |
| mode_est_BB3 : {ok, ko_open, ko_closed}; |
| |
| mode_est_G1 : {ok, ko}; |
| mode_est_G2 : {ok, ko}; |
| mode_est_G3 : {ok, ko}; |
| |
| VAR |
| state_est_G1 : {on, off}; |
| state_est_G2 : {on, off}; |
| state_est_G3 : {on, off}; |
| |
| state_est_GB1 : {closed, open}; |
| state_est_GB2 : {closed, open}; |
| state_est_GB3 : {closed, open}; |
| |
| state_est_BB1 : {closed, open}; |
| state_est_BB2 : {closed, open}; |
| state_est_BB3 : {closed, open}; |
| |
| DEFINE |
| faults_counter := count( |
| (mode_est_GB1 != ok), |
| (mode_est_GB2 != ok), |
| (mode_est_GB3 != ok), |
| (mode_est_BB1 != ok), |
| (mode_est_BB2 != ok), |
| (mode_est_BB3 != ok), |
| (mode_est_G1 != ok), |
| (mode_est_G2 != ok), |
| (mode_est_G3 != ok)); |
| |
| |
| -- Definition of the components signals used to monitor their funtionality -- |
| DEFINE |
| fault_event_open_CBs := mode_event_CBs[0]; |
| fault_event_closed_CBs := mode_event_CBs[1]; |
| nominal_event_CBs := mode_event_CBs[2]; |
| |
| fault_event_off_Gs := mode_event_Gs[0]; |
| nominal_event_Gs := mode_event_Gs[1]; |
| |
| index_GB1 := 0; |
| index_GB2 := 1; |
| index_GB3 := 2; |
| |
| index_BB1 := 3; |
| index_BB2 := 4; |
| index_BB3 := 5; |
| |
| index_G1 := 0; |
| index_G2 := 1; |
| index_G3 := 2; |
| |
| ASSIGN |
| init(mode_est_GB1) := ok; |
| next(mode_est_GB1) := |
| case |
| fault_event_open_CBs[index_GB1] : ko_open; |
| fault_event_closed_CBs[index_GB1] : ko_closed; |
| nominal_event_CBs[index_GB1] : ok; |
| TRUE : mode_est_GB1; |
| esac; |
| |
| ASSIGN |
| init(mode_est_GB2) := ok; |
| next(mode_est_GB2) := |
| case |
| fault_event_open_CBs[index_GB2] : ko_open; |
| fault_event_closed_CBs[index_GB2] : ko_closed; |
| nominal_event_CBs[index_GB2] : ok; |
| TRUE : mode_est_GB2; |
| esac; |
| |
| ASSIGN |
| init(mode_est_GB3) := ok; |
| next(mode_est_GB3) := |
| case |
| fault_event_open_CBs[index_GB3] : ko_open; |
| fault_event_closed_CBs[index_GB3] : ko_closed; |
| nominal_event_CBs[index_GB3] : ok; |
| TRUE : mode_est_GB3; |
| esac; |
| |
| ASSIGN |
| init(mode_est_BB1) := ok; |
| next(mode_est_BB1) := |
| case |
| fault_event_open_CBs[index_BB1] : ko_open; |
| fault_event_closed_CBs[index_BB1] : ko_closed; |
| nominal_event_CBs[index_BB1] : ok; |
| TRUE : mode_est_BB1; |
| esac; |
| |
| ASSIGN |
| init(mode_est_BB2) := ok; |
| next(mode_est_BB2) := |
| case |
| fault_event_open_CBs[index_BB2] : ko_open; |
| fault_event_closed_CBs[index_BB2] : ko_closed; |
| nominal_event_CBs[index_BB2] : ok; |
| TRUE : mode_est_BB2; |
| esac; |
| |
| |
| init(mode_est_BB3) := ok; |
| next(mode_est_BB3) := |
| case |
| fault_event_open_CBs[index_BB3] : ko_open; |
| fault_event_closed_CBs[index_BB3] : ko_closed; |
| nominal_event_CBs[index_BB3] : ok; |
| TRUE : mode_est_BB3; |
| esac; |
| |
| ASSIGN |
| init(mode_est_G1) := ok; |
| next(mode_est_G1) := |
| case |
| fault_event_off_Gs[index_G1] : ko; |
| nominal_event_Gs[index_G1] : ok; |
| TRUE : mode_est_G1; |
| esac; |
| |
| ASSIGN |
| init(mode_est_G2) := ok; |
| next(mode_est_G2) := |
| case |
| fault_event_off_Gs[index_G2] : ko; |
| nominal_event_Gs[index_G2] : ok; |
| TRUE : mode_est_G2; |
| esac; |
| |
| ASSIGN |
| init(mode_est_G3) := ok; |
| next(mode_est_G3) := |
| case |
| fault_event_off_Gs[index_G3] : ko; |
| nominal_event_Gs[index_G3] : ok; |
| TRUE : mode_est_G3; |
| esac; |
| |
| ASSIGN |
| init(state_est_G1) := init_state_Gs[index_G1]; |
| next(state_est_G1) := |
| case |
| fault_event_off_Gs[index_G1] : off; |
| (next(mode_est_G1) = ok) & (cmd_to_Gs[index_G1] = cmd_on) : on; |
| (next(mode_est_G1) = ok) & (cmd_to_Gs[index_G1] = cmd_off) : off; |
| TRUE : state_est_G1; |
| esac; |
| |
| ASSIGN |
| init(state_est_G2) := init_state_Gs[index_G2]; |
| next(state_est_G2) := |
| case |
| fault_event_off_Gs[index_G2] : off; |
| (next(mode_est_G2) = ok) & (cmd_to_Gs[index_G2] = cmd_on) : on; |
| (next(mode_est_G2) = ok) & (cmd_to_Gs[index_G2] = cmd_off) : off; |
| TRUE : state_est_G2; |
| esac; |
| |
| ASSIGN |
| init(state_est_G3) := init_state_Gs[index_G3]; |
| next(state_est_G3) := |
| case |
| fault_event_off_Gs[index_G3] : off; |
| (next(mode_est_G3) = ok) & (cmd_to_Gs[index_G3] = cmd_on) : on; |
| (next(mode_est_G3) = ok) & (cmd_to_Gs[index_G3] = cmd_off) : off; |
| TRUE : state_est_G3; |
| esac; |
| |
| ASSIGN |
| init(state_est_GB1) := init_state_CBs[index_GB1]; |
| next(state_est_GB1) := |
| case |
| fault_event_open_CBs[index_GB1] : open; |
| fault_event_closed_CBs[index_GB1] : closed; |
| (next(mode_est_GB1) = ok) & (cmd_to_CBs[index_GB1] = cmd_open) : open; |
| (next(mode_est_GB1) = ok) & (cmd_to_CBs[index_GB1] = cmd_closed) : closed; |
| TRUE : state_est_GB1; |
| esac; |
| |
| ASSIGN |
| init(state_est_GB2) := init_state_CBs[index_GB2]; |
| next(state_est_GB2) := |
| case |
| fault_event_open_CBs[index_GB2] : open; |
| fault_event_closed_CBs[index_GB2] : closed; |
| (next(mode_est_GB2) = ok) & (cmd_to_CBs[index_GB2] = cmd_open) : open; |
| (next(mode_est_GB2) = ok) & (cmd_to_CBs[index_GB2] = cmd_closed) : closed; |
| TRUE : state_est_GB2; |
| esac; |
| |
| ASSIGN |
| init(state_est_GB3) := init_state_CBs[index_GB3]; |
| next(state_est_GB3) := |
| case |
| fault_event_open_CBs[index_GB3] : open; |
| fault_event_closed_CBs[index_GB3] : closed; |
| (next(mode_est_GB3) = ok) & (cmd_to_CBs[index_GB3] = cmd_open) : open; |
| (next(mode_est_GB3) = ok) & (cmd_to_CBs[index_GB3] = cmd_closed) : closed; |
| TRUE : state_est_GB3; |
| esac; |
| |
| ASSIGN |
| init(state_est_BB1) := init_state_CBs[index_BB1]; |
| next(state_est_BB1) := |
| case |
| fault_event_open_CBs[index_BB1] : open; |
| fault_event_closed_CBs[index_BB1] : closed; |
| (next(mode_est_BB1) = ok) & (cmd_to_CBs[index_BB1] = cmd_open) : open; |
| (next(mode_est_BB1) = ok) & (cmd_to_CBs[index_BB1] = cmd_closed) : closed; |
| TRUE : state_est_BB1; |
| esac; |
| |
| ASSIGN |
| init(state_est_BB2) := init_state_CBs[index_BB2]; |
| next(state_est_BB2) := |
| case |
| fault_event_open_CBs[index_BB2] : open; |
| fault_event_closed_CBs[index_BB2] : closed; |
| (next(mode_est_BB2) = ok) & (cmd_to_CBs[index_BB2] = cmd_open) : open; |
| (next(mode_est_BB2) = ok) & (cmd_to_CBs[index_BB2] = cmd_closed) : closed; |
| TRUE : state_est_BB2; |
| esac; |
| |
| ASSIGN |
| init(state_est_BB3) := init_state_CBs[index_BB3]; |
| next(state_est_BB3) := |
| case |
| fault_event_open_CBs[index_BB3] : open; |
| fault_event_closed_CBs[index_BB3] : closed; |
| (next(mode_est_BB3) = ok) & (cmd_to_CBs[index_BB3] = cmd_open) : open; |
| (next(mode_est_BB3) = ok) & (cmd_to_CBs[index_BB3] = cmd_closed) : closed; |
| TRUE : state_est_BB3; |
| esac; |
| |
| -- END MODULE MONITOR -- |
