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 --