plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/FDI/simplified_model.smv

MODULE main

    IVAR
        cmd_to_G1 : {cmd_on, cmd_off, nop};
	cmd_to_G2 : {cmd_on, cmd_off, nop};
	cmd_to_G3 : {cmd_on, cmd_off, nop};
        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};

    VAR
        v_cmd_to_G1 : {cmd_on, cmd_off, nop};
	v_cmd_to_G2 : {cmd_on, cmd_off, nop};
	v_cmd_to_G3 : {cmd_on, cmd_off, nop};
	v_cmd_to_GB1 : {cmd_closed, cmd_open, nop};
	v_cmd_to_GB2 : {cmd_closed, cmd_open, nop};
	v_cmd_to_GB3 : {cmd_closed, cmd_open, nop};
	v_cmd_to_BB1 : {cmd_closed, cmd_open, nop};
	v_cmd_to_BB2 : {cmd_closed, cmd_open, nop};
	v_cmd_to_BB3 : {cmd_closed, cmd_open, nop};

    ASSIGN
      init(v_cmd_to_G1) := nop;
      next(v_cmd_to_G1) := cmd_to_G1;
      init(v_cmd_to_G2) := nop;
      next(v_cmd_to_G2) := cmd_to_G2;
      init(v_cmd_to_G3) := nop;
      next(v_cmd_to_G3) := cmd_to_G3;
      init(v_cmd_to_GB1) := nop;
      next(v_cmd_to_GB1) := cmd_to_GB1;
      init(v_cmd_to_GB2) := nop;
      next(v_cmd_to_GB2) := cmd_to_GB2;
      init(v_cmd_to_GB3) := nop;
      next(v_cmd_to_GB3) := cmd_to_GB3;
      init(v_cmd_to_BB1) := nop;
      next(v_cmd_to_BB1) := cmd_to_BB1;
      init(v_cmd_to_BB2) := nop;
      next(v_cmd_to_BB2) := cmd_to_BB2;
      init(v_cmd_to_BB3) := nop;
      next(v_cmd_to_BB3) := cmd_to_BB3;

    VAR
        SC : System_Configuration(cmd_to_G1, cmd_to_G2, cmd_to_G3, 
				  cmd_to_GB1, cmd_to_GB2, cmd_to_GB3, cmd_to_BB1, cmd_to_BB2, cmd_to_BB3);
        _masterCC : MasterCC#;

    -- Requirements

    -- R1. No bus will be connected to more than 1 power source at any time
    INVAR (SC.B1_poweredby_G1 -> !(SC.B1_poweredby_G2 | SC.B1_poweredby_G3));
    INVAR (SC.B1_poweredby_G2 -> !(SC.B1_poweredby_G1 | SC.B1_poweredby_G3));
    INVAR (SC.B1_poweredby_G3 -> !(SC.B1_poweredby_G1 | SC.B1_poweredby_G2));

    INVAR (SC.B2_poweredby_G1 -> !(SC.B2_poweredby_G2 | SC.B2_poweredby_G3));
    INVAR (SC.B2_poweredby_G2 -> !(SC.B2_poweredby_G1 | SC.B2_poweredby_G3));
    INVAR (SC.B2_poweredby_G3 -> !(SC.B2_poweredby_G1 | SC.B2_poweredby_G2));

    INVAR (SC.B3_poweredby_G1 -> !(SC.B3_poweredby_G2 | SC.B3_poweredby_G3));
    INVAR (SC.B3_poweredby_G2 -> !(SC.B3_poweredby_G1 | SC.B3_poweredby_G3));
    INVAR (SC.B3_poweredby_G3 -> !(SC.B3_poweredby_G1 | SC.B3_poweredby_G2));

    -- R4. If no power source is on, then all buses will be unpowered
    INVARSPEC ((SC.G1.is_off & SC.G2.is_off & SC.G3.is_off) -> (!SC.B1.is_powered & !SC.B2.is_powered & !SC.B3.is_powered));



-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE System_Configuration(cmd_to_G1, cmd_to_G2, cmd_to_G3,
			    cmd_to_GB1, cmd_to_GB2, cmd_to_GB3, cmd_to_BB1, cmd_to_BB2, cmd_to_BB3)
    VAR
        G1 : Generator_#Extended(cmd_to_G1, init_state_G1);
        G2 : Generator_#Extended(cmd_to_G2, init_state_G2);
        G3 : Generator_#Extended(cmd_to_G3, init_state_G3);
        GB1 : Switch_#Extended(cmd_to_GB1, init_state_GB1);
        GB2 : Switch_#Extended(cmd_to_GB2, init_state_GB2);
        GB3 : Switch_#Extended(cmd_to_GB3, init_state_GB3);
        BB1 : Switch_#Extended(cmd_to_BB1, init_state_BB1);
        BB2 : Switch_#Extended(cmd_to_BB2, init_state_BB2);
        BB3 : Switch_#Extended(cmd_to_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);
    DEFINE
        init_state_BB3 := open;
        init_state_BB2 := closed;
        init_state_BB1 := open;
        init_state_GB3 := open;
        init_state_GB2 := closed;
        init_state_GB1 := closed;
        init_state_G3 := off;
        init_state_G2 := on;
        init_state_G1 := on;
        B1_poweredby_G3_R := (B2_poweredby_G3_R & BB1.is_closed);
        B1_poweredby_G3_L := (B3_poweredby_G3_U & BB3.is_closed);
        B1_poweredby_G2_R := (B2_poweredby_G2_U & BB1.is_closed);
        B1_poweredby_G2_L := (B3_poweredby_G2_L & BB3.is_closed);
        B1_poweredby_G1_U := (G1.is_on & GB1.is_closed);
        B2_poweredby_G3_R := (B3_poweredby_G3_U & BB2.is_closed);
        B2_poweredby_G3_L := (B1_poweredby_G3_L & BB1.is_closed);
        B2_poweredby_G2_U := (G2.is_on & GB2.is_closed);
        B2_poweredby_G1_R := (B3_poweredby_G1_R & BB2.is_closed);
        B2_poweredby_G1_L := (B1_poweredby_G1_U & BB1.is_closed);
        B3_poweredby_G3_U := (G3.is_on & GB3.is_closed);
        B3_poweredby_G2_R := (B1_poweredby_G2_R & BB3.is_closed);
        B3_poweredby_G2_L := (B2_poweredby_G2_U & BB2.is_closed);
        B3_poweredby_G1_R := (B1_poweredby_G1_U & BB3.is_closed);
        B3_poweredby_G1_L := (B2_poweredby_G1_L & BB2.is_closed);
        B1_poweredby_G3 := (B1_poweredby_G3_R | B1_poweredby_G3_L);
        B1_poweredby_G2 := (B1_poweredby_G2_R | B1_poweredby_G2_L);
        B1_poweredby_G1 := B1_poweredby_G1_U;
        B2_poweredby_G3 := (B2_poweredby_G3_R | B2_poweredby_G3_L);
        B2_poweredby_G2 := B2_poweredby_G2_U;
        B2_poweredby_G1 := (B2_poweredby_G1_R | B2_poweredby_G1_L);
        B3_poweredby_G3 := B3_poweredby_G3_U;
        B3_poweredby_G2 := (B3_poweredby_G2_R | B3_poweredby_G2_L);
        B3_poweredby_G1 := (B3_poweredby_G1_R | B3_poweredby_G1_L);


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Generator_#Extended(cmd, init_state)
    VAR
        Gen_StuckOff : Gen_StuckOff_FM_Mod(state_#nominal, off, fault_event_stuck_at_off);
    VAR
        state_#nominal : {on, off};

    IVAR
        fault_event_stuck_at_off : boolean;
        nominal_event : boolean;

    DEFINE
        is_on := state = on;
        is_off := state = off;
        state := Gen_StuckOff.state_#fault;

    -- Synthesis does not accept DEFINEs as observables
    VAR v_state : {on, off};
    ASSIGN v_state := state;

    ASSIGN
        init(state_#nominal) := init_state;
        next(state_#nominal) := case
cmd = cmd_on : on;
cmd = cmd_off : off;
TRUE : state;
esac;

    TRANS nominal_event = FALSE;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Gen_StuckOff_FM_Mod(state__#read, term_#1, fault_event_stuck_at_off#event)
    VAR
        stuckAt_Off : stuckAt_Off_fm_Mod(mode = NOMINAL, mode_is_stuckAt_Off, term_#1, state__#read, state__#write, event = stuckAt_Off#failure, event = _#NoEvent);
    VAR
        mode : {NOMINAL, stuckAt_Off#FAULT};
        state__#write : {on, off};

    IVAR
        event : {_#NoEvent, stuckAt_Off#failure};

    DEFINE
        NoEvent := event = _#NoEvent;
        cando_stuckAt_Off#FAULT := ((mode = NOMINAL & stuckAt_Off.trans_trig_guard_#0) | (mode = stuckAt_Off#FAULT & stuckAt_Off.trans_trig_guard_#1));
        state_#fault := case
mode = NOMINAL : state__#read;
mode_is_stuckAt_Off : state__#write;
TRUE : state__#read;
esac;
        mode_is_stuckAt_Off := mode = stuckAt_Off#FAULT;

    INIT mode = NOMINAL;

    TRANS (event in stuckAt_Off#failure <-> fault_event_stuck_at_off#event);

    TRANS case
((mode = stuckAt_Off#FAULT & stuckAt_Off.trans_trig_guard_#1) | (mode = NOMINAL & stuckAt_Off.trans_trig_guard_#0)) : next(mode) = stuckAt_Off#FAULT;
TRUE : (next(mode) = mode & NoEvent);
esac;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Off_fm_Mod(is_nominal, is_fault, term, input, varout, _failure, ev_#NoEvent)
    VAR
        stuckAt_OffEM : stuckAt_Off_fm_EM_Mod(is_nominal, is_fault, term, input, varout);
    DEFINE
        failure := _failure;
        NoEvent := ev_#NoEvent;
        trans_trig_guard_#0 := failure;
        trans_trig_guard_#1 := NoEvent;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Off_fm_EM_Mod(is_nominal, is_fault, term, input, varout)
    TRANS (!(!is_fault & next(is_fault)) | next(varout) = term);

    TRANS (!(is_fault & next(is_fault)) | next(varout) = varout);

    TRANS (!(is_nominal & next(is_nominal)) | next(varout) = varout);


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Switch_#Extended(cmd, init_state)
    VAR
        Switch_StuckClosed_StuckOpen : Switch_StuckClosed_StuckOpen_FM_Mod(state_#nominal, closed, open, fault_event_stuck_at_closed, nominal_event, fault_event_stuck_at_open);
    VAR
        state_#nominal : {open, closed};

    IVAR
        fault_event_stuck_at_closed : boolean;
        fault_event_stuck_at_open : boolean;
        nominal_event : boolean;

    DEFINE
        is_closed := state = closed;
        is_open := state = open;
        state := Switch_StuckClosed_StuckOpen.state_#fault;

    VAR v_state : {open, closed};
    ASSIGN v_state := state;

    ASSIGN
        init(state_#nominal) := init_state;
        next(state_#nominal) := case
cmd = cmd_open : open;
cmd = cmd_closed : closed;
TRUE : state;
esac;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Switch_StuckClosed_StuckOpen_FM_Mod(state__#read, term_#1, term_#2, fault_event_stuck_at_closed#event, nominal_event#event, fault_event_stuck_at_open#event)
    VAR
        stuckAt_Closed : stuckAt_Closed_fm_Mod(mode = NOMINAL, mode_is_stuckAt_Closed, term_#1, state__#read, state__#write, event = stuckAt_Closed#failure, event = stuckAt_Closed#self_fixed, event = _#NoEvent);
        stuckAt_Open : stuckAt_Open_fm_Mod(mode = NOMINAL, mode_is_stuckAt_Open, term_#2, state__#read, state__#write, event = stuckAt_Open#failure, event = stuckAt_Open#self_fixed, event = _#NoEvent);
    VAR
        mode : {NOMINAL, stuckAt_Closed#FAULT, stuckAt_Open#FAULT};
        state__#write : {open, closed};

    IVAR
        event : {_#NoEvent, stuckAt_Closed#failure, stuckAt_Closed#self_fixed, stuckAt_Open#failure, stuckAt_Open#self_fixed};

    DEFINE
        NoEvent := event = _#NoEvent;
        cando_stuckAt_Closed#FAULT := ((mode = NOMINAL & stuckAt_Closed.trans_trig_guard_#0) | (mode = stuckAt_Closed#FAULT & stuckAt_Closed.trans_trig_guard_#1));
        cando_stuckAt_Open#FAULT := ((mode = NOMINAL & stuckAt_Open.trans_trig_guard_#0) | (mode = stuckAt_Open#FAULT & stuckAt_Open.trans_trig_guard_#1));
        state_#fault := case
mode = NOMINAL : state__#read;
(mode_is_stuckAt_Open | mode_is_stuckAt_Closed) : state__#write;
TRUE : state__#read;
esac;
        mode_is_stuckAt_Closed := mode = stuckAt_Closed#FAULT;
        mode_is_stuckAt_Open := mode = stuckAt_Open#FAULT;

    INIT mode = NOMINAL;

    TRANS (event in stuckAt_Closed#failure <-> fault_event_stuck_at_closed#event);

    TRANS (event in stuckAt_Open#self_fixed union stuckAt_Closed#self_fixed <-> nominal_event#event);

    TRANS (event in stuckAt_Open#failure <-> fault_event_stuck_at_open#event);

    TRANS case
(mode = stuckAt_Open#FAULT & stuckAt_Open.trans_trig_guard_#2) : next(mode) = NOMINAL;
((mode = stuckAt_Open#FAULT & stuckAt_Open.trans_trig_guard_#1) | (mode = NOMINAL & stuckAt_Open.trans_trig_guard_#0)) : next(mode) = stuckAt_Open#FAULT;
(mode = stuckAt_Closed#FAULT & stuckAt_Closed.trans_trig_guard_#2) : next(mode) = NOMINAL;
((mode = stuckAt_Closed#FAULT & stuckAt_Closed.trans_trig_guard_#1) | (mode = NOMINAL & stuckAt_Closed.trans_trig_guard_#0)) : next(mode) = stuckAt_Closed#FAULT;
TRUE : (next(mode) = mode & NoEvent);
esac;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Closed_fm_Mod(is_nominal, is_fault, term, input, varout, _failure, _self_fixed, ev_#NoEvent)
    VAR
        stuckAt_ClosedEM : stuckAt_Closed_fm_EM_Mod(is_nominal, is_fault, term, input, varout);
    DEFINE
        failure := _failure;
        self_fixed := _self_fixed;
        NoEvent := ev_#NoEvent;
        trans_trig_guard_#0 := failure;
        trans_trig_guard_#1 := (NoEvent & !self_fixed);
        trans_trig_guard_#2 := self_fixed;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Closed_fm_EM_Mod(is_nominal, is_fault, term, input, varout)
    TRANS (!(!is_fault & next(is_fault)) | next(varout) = term);

    TRANS (!(is_fault & next(is_fault)) | next(varout) = varout);

    TRANS (!(is_nominal & next(is_nominal)) | next(varout) = varout);


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Open_fm_Mod(is_nominal, is_fault, term, input, varout, _failure, _self_fixed, ev_#NoEvent)
    VAR
        stuckAt_OpenEM : stuckAt_Open_fm_EM_Mod(is_nominal, is_fault, term, input, varout);
    DEFINE
        failure := _failure;
        self_fixed := _self_fixed;
        NoEvent := ev_#NoEvent;
        trans_trig_guard_#0 := failure;
        trans_trig_guard_#1 := (NoEvent & !self_fixed);
        trans_trig_guard_#2 := self_fixed;


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE stuckAt_Open_fm_EM_Mod(is_nominal, is_fault, term, input, varout)
    TRANS (!(!is_fault & next(is_fault)) | next(varout) = term);

    TRANS (!(is_fault & next(is_fault)) | next(varout) = varout);

    TRANS (!(is_nominal & next(is_nominal)) | next(varout) = varout);


-- ===============================================================================
--                               End of module
-- ===============================================================================

-- ===============================================================================
MODULE Bus(in1, in2, in3)
    VAR
        state : {working, broken};

    DEFINE
        is_broken := state = broken;
        is_powered := (state = working & count(in1, in2, in3) = 1);

    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 of module
-- ===============================================================================

-- ===============================================================================
MODULE MasterCC#

-- ===============================================================================
--                               End of module
-- ===============================================================================