#define max(val1, val2) case val1 > val2: val1; val1 <= val2: val2; esac

---------------------------------------------------------------------------
-- POWER DISTRIBUTION SYSTEM CONTROLLER                                  --
---------------------------------------------------------------------------

-- This SMV program models a controller for a power distribution system
-- It includes modules both for the physical system (circuit breakers,
-- switches, lines), and for the controller.

-- Recommended SMV flag: -f

---------------------------------------------------------------------------
-- CIRCUIT BREAKER                                                       --
---------------------------------------------------------------------------

MODULE cbreaker(action)
-- input parameters:
--   action is the action from the controller (open, close, nop)

-- internal state
-- the breaker can be opened or closed
VAR
  status : {opened, closed};
-- the status changes according to the commands of the controller
-- if no command is given by the controller, the status does not change
ASSIGN
  next(status) := case
	action = open  : opened;
	action = close : closed;
	action = nop   : status;
        TRUE : status;
  	esac;

-- output of the circuit breaker
-- output is high if only if the breaker is closed
DEFINE
  out := (status = closed);


---------------------------------------------------------------------------
-- SWITCH                                                                --
---------------------------------------------------------------------------

MODULE switch(left_feed, right_feed, action)
-- input parameters:
--   left_feed  is high if the switch is fed from the left
--   right_feed is high if the switch is fed from the right
--   action is the action from the controller (open, close, nop)

-- internal state
-- the switch can be opened, closed, or broken
-- a closed switch can be in one of these substates: not_feeding,
-- feeding_left, feeding_right
VAR
  status : {opened, not_feeding, feeding_left, feeding_right, broken};

-- the switch gets broken if it is fed simultaneously from the left
-- and from the right; if it is broken, it remains broken forever;
-- otherwise, it opens or closes according to the commands of the controller;
-- an opened switch does not feed the lines it is connected to;
-- a closed switch feeds the opposite line with respect to the one it is
-- fed by (if any)
ASSIGN
  next(status) := case
	status = broken : broken;
	action = open   : opened;
	action = close  : case
		left_feed & right_feed : broken;
		left_feed              : feeding_right;
		right_feed             : feeding_left;
		TRUE                   : not_feeding;
		esac;
	action = nop : case
		status = opened        : opened;
		left_feed & right_feed : broken;
		left_feed              : feeding_right;
		right_feed             : feeding_left;
		TRUE                   : not_feeding;
		esac;
	esac;

-- outputs of the switch:
--   out_left  is high if and only if the switch is feeding the left  line
--   out_right is high if and only if the switch is feeding the right line
DEFINE
  out_left  := (status = feeding_left);
  out_right := (status = feeding_right);


---------------------------------------------------------------------------
-- LINE WITH TWO CONNECTIONS                                             --
---------------------------------------------------------------------------

MODULE line_2(left_feed, right_feed)
-- input parameters:
--   left_feed  is high if the line is fed from the left
--   right_feed is high if the line is fed from the right

-- internal state
-- the line can be closed, broken, or faulty
-- a closed line can be in one of these substates: not_feeding,
-- feeding_left, feeding_right
VAR
  status : {not_feeding, feeding_left, feeding_right, broken, faulty};

IVAR
  fault_event_stuck_at_faulty : boolean;
  nominal_event : boolean;
  
-- the line gets broken if it is fed simultaneously from the left
-- and from the right; broken and faulty states are permanent; a closed line
-- feeds the opposite device with respect to the one it is fed by (if any)
ASSIGN
  next(status) := case
	status = broken        : broken;
	status = faulty        : faulty;
	left_feed & right_feed : broken;
	left_feed              : feeding_right;
	right_feed             : feeding_left;
	TRUE                   : not_feeding;
	esac;

-- outputs of the line:
--   out_left  is high if and only if the line is feeding the left  device
--   out_right is high if and only if the line is feeding the right device
--   operational is true if the line is feeding (left or right)
DEFINE
  out_left  := (status = feeding_left);
  out_right := (status = feeding_right);
DEFINE
  operational := (out_left | out_right);


---------------------------------------------------------------------------
-- LINE WITH THREE CONNECTIONS                                           --
---------------------------------------------------------------------------

MODULE line_3(left_feed, right_feed, up_feed)
-- input parameters:
--   left_feed  is high if the line is fed from the left
--   right_feed is high if the line is fed from the right
--   up_feed    is high if the line is fed from above

-- internal state
-- the line can be closed, broken, or faulty
-- a closed line can be in one of these substates: not_feeding,
-- feeding_left_right, feeding_left_up, feeding_right_up
VAR
  status : {not_feeding, feeding_left_right, feeding_left_up, feeding_right_up,
            broken, faulty};

-- the line gets broken if it is fed simultaneously from two different
-- directions; broken and faulty states are permanent; a closed line feeds
-- the remaining two devices with respect to the one it is fed by (if any)
ASSIGN
  next(status) := case
	status = broken                           : broken;
	status = faulty                           : faulty;
	count(left_feed, right_feed, up_feed) > 1 : broken;
	count(left_feed, right_feed, up_feed) = 0 : not_feeding;
	left_feed                                 : feeding_right_up;
	right_feed                                : feeding_left_up;
        up_feed                                   : feeding_left_right;
        TRUE                                      : status;
	esac;

-- outputs of the line:
--    out_left  is high if and only if the line is feeding the left  device
--    out_right is high if and only if the line is feeding the right device
--    out_up    is high if and only if the line is feeding the upper device
--    operational is true if the line is feeding (left, right, or up)
DEFINE
  out_left  := (status in {feeding_left_up,    feeding_left_right});
  out_right := (status in {feeding_left_right, feeding_right_up  });
  out_up    := (status in {feeding_left_up,    feeding_right_up  });
DEFINE
  operational := (out_left | out_right | out_up);


---------------------------------------------------------------------------
-- CONTROLLER                                                            --
---------------------------------------------------------------------------

MODULE controller(status_CB1,
                  status_CB2,
                  status_CB3,
                  status_SD1,
                  status_SD2,
                  status_SD3,
                  status_SD4,
                  status_SD5,
                  status_SD6,
                  status_SD7,
                  status_L1,
                  status_L2,
                  status_L3,
                  status_L4,
                  status_L5,
                  status_L6,
                  status_L7)

-- inputs of the controller:
-- the status of all the components of the system

-- outputs of the controller are {open, close, nop} commands for
-- the circuit breakers and the switches
VAR
  action_CB1 : {open, close, nop};
  action_CB2 : {open, close, nop};
  action_CB3 : {open, close, nop};
  action_SD1 : {open, close, nop};
  action_SD2 : {open, close, nop};
  action_SD3 : {open, close, nop};
  action_SD4 : {open, close, nop};
  action_SD5 : {open, close, nop};
  action_SD6 : {open, close, nop};
  action_SD7 : {open, close, nop};

-- some useful definitions
-- the controller does not perform any action
DEFINE
  no_actions := (action_CB1 = nop &
                 action_CB2 = nop &
                 action_CB3 = nop &
                 action_SD1 = nop &
                 action_SD2 = nop &
                 action_SD3 = nop &
                 action_SD4 = nop &
                 action_SD5 = nop &
                 action_SD6 = nop &
                 action_SD7 = nop);
-- failures
DEFINE
  failure_L1 := (status_L1 = faulty);
  failure_L2 := (status_L2 = faulty);
  failure_L3 := (status_L3 = faulty);
  failure_L4 := (status_L4 = faulty);
  failure_L5 := (status_L5 = faulty);
  failure_L6 := (status_L6 = faulty);
  failure_L7 := (status_L7 = faulty);
DEFINE
  failure_occurring := (failure_L1 |
                        failure_L2 | 
                        failure_L3 |
                        failure_L4 |
                        failure_L5 |
                        failure_L6 |
                        failure_L7);

-- the delay
-- the controller uses this variable to wait for a fixed delay
-- (see below)
DEFINE
  DELAY := 10;
VAR
  delay : 0..10;
ASSIGN
  init(delay) := DELAY;
  next(delay) := case
	status in {waiting1, waiting2} : max(0, delay - 1);
	TRUE                           : DELAY;
	esac;

-- internal state
-- the controller can be in the following states:
--    monitoring: the controller is monitoring the system waiting for failures
--      to happen
--    waiting1: the controller waits for a fixed delay before initiating any
--      action (this allows the failure to propagate through the network)
--    operating: the controller issues suitable actions to the components
--      after a failure
--    waiting2: the controller waits for a fixed delay before terminating
--      (this allows to observe the effects of the performed operations)
--    finished: the controller terminates
VAR
  status : {monitoring, waiting1, operating, waiting2, finished};

-- logic of the controller
-- a simple controller:
-- it takes into account only single failures
ASSIGN
  init(status) := monitoring;
  next(status) := case
	            status = monitoring : case
		                            failure_occurring : waiting1;
		                            TRUE              : monitoring;
		                          esac;
	            status = waiting1 : case
		                          delay > 0 : waiting1;
		                          TRUE      : operating;
		                        esac;
	            status = operating : waiting2;
	            status = waiting2 : case
		                          delay > 0 : waiting2;
		                          TRUE      : finished;
		                        esac;
	            status = finished : finished;
                    TRUE : status;                    
	          esac;

-- actions are performed while in operating status
TRANS
  (status != operating) -> no_actions
-- the controller takes into account single failures of the lines
-- L3, L4, L5, L6
-- and issues suitable actions to reconfigurate the network
TRANS
  status = operating -> (
      (failure_L5 -> (action_CB1 = close & 
                      action_CB2 = open  &
                      action_CB3 = nop   &
                      action_SD1 = nop   &
                      action_SD2 = nop   &
                      action_SD3 = nop   &
                      action_SD4 = open  &
                      action_SD5 = close &
                      action_SD6 = nop   &
                      action_SD7 = nop)) &
      (failure_L6 & !failure_L5 ->
                     (action_CB1 = close & 
                      action_CB2 = nop   &
                      action_CB3 = nop   &
                      action_SD1 = nop   &
                      action_SD2 = open  &
                      action_SD3 = nop   &
                      action_SD4 = open  &
                      action_SD5 = close &
                      action_SD6 = nop   &
                      action_SD7 = nop   )) &
      (failure_L4 & !failure_L5 & !failure_L6 ->
                     (action_CB1 = close & 
                      action_CB2 = nop   &
                      action_CB3 = close &
                      action_SD1 = open  &
                      action_SD2 = open  &
                      action_SD3 = nop   &
                      action_SD4 = nop   &
                      action_SD5 = close &
                      action_SD6 = nop   &
                      action_SD7 = nop   )) &
      (failure_L3 & !failure_L5 & !failure_L6 & !failure_L4 ->
                     (action_CB1 = nop   & 
                      action_CB2 = nop   &
                      action_CB3 = close &
                      action_SD1 = open  &
                      action_SD2 = nop   &
                      action_SD3 = nop   &
                      action_SD4 = nop   &
                      action_SD5 = nop   &
                      action_SD6 = nop   &
                      action_SD7 = nop   )) &
      (!failure_L3 & !failure_L5 & !failure_L6 & !failure_L4 ->
                     (action_CB1 = nop   & 
                      action_CB2 = nop   &
                      action_CB3 = nop   &
                      action_SD1 = nop   &
                      action_SD2 = nop   &
                      action_SD3 = nop   &
                      action_SD4 = nop   &
                      action_SD5 = nop   &
                      action_SD6 = nop   &
                      action_SD7 = nop   )))


---------------------------------------------------------------------------
-- MAIN                                                                  --
---------------------------------------------------------------------------

MODULE main

-- the topology

VAR
  CB1  : cbreaker(CTRL.action_CB1);
  CB2  : cbreaker(CTRL.action_CB2);
  CB3  : cbreaker(CTRL.action_CB3);

  SD1  : switch(L3.out_right, L4.out_left,  CTRL.action_SD1);
  SD2  : switch(L6.out_left,  L4.out_up,    CTRL.action_SD2);
  SD3  : switch(L7.out_right, L4.out_right, CTRL.action_SD3);
  SD4  : switch(L5.out_right, L6.out_right, CTRL.action_SD4);
  SD5  : switch(L2.out_right, L3.out_left,  CTRL.action_SD5);
  SD6  : switch(L1.out_right, L2.out_left,  CTRL.action_SD6);
  SD7  : switch(L2.out_up,    L6.out_up,    CTRL.action_SD7);

  L1   : line_2(CB1.out,       SD6.out_left);
  L2   : line_3(SD6.out_right, SD5.out_left,  SD7.out_left);
  L3   : line_2(SD5.out_right, SD1.out_left);
  L4   : line_3(SD1.out_right, SD3.out_right, SD2.out_right);
  L5   : line_2(CB2.out,       SD4.out_left);
  L6   : line_3(SD2.out_left,  SD4.out_right, SD7.out_right);
  L7   : line_2(CB3.out,       SD3.out_left);

  CTRL : controller(CB1.status,
                    CB2.status,
                    CB3.status,
                    SD1.status,
                    SD2.status,
                    SD3.status,
                    SD4.status,
                    SD5.status,
                    SD6.status,
                    SD7.status,
                    L1.status,
                    L2.status,
                    L3.status,
                    L4.status,
                    L5.status,
                    L6.status,
                    L7.status);

-- the initial state
INIT
  CB1.status = opened             &
  CB2.status = closed             &
  CB3.status = opened             &
  SD1.status = feeding_left       &
  SD2.status = feeding_right      &
  SD3.status = opened             &
  SD4.status = feeding_right      &
  SD5.status = opened             &
  SD6.status = not_feeding        &
  SD7.status = opened             &
   L1.status = not_feeding        &
   L2.status = not_feeding        &
   L3.status = feeding_left       &
   L4.status = feeding_left_right &
   L5.status = feeding_right      &
   L6.status = feeding_left_up    &
   L7.status = not_feeding

-- some useful definitions
-- number of operational lines
DEFINE
  NR_OPERATIONAL_LINES :=
	count(L1.operational,
	      L2.operational,
	      L3.operational,
 	      L4.operational,
 	      L5.operational,
 	      L6.operational,
 	      L7.operational);