| #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); |
