// Clocks clock VVI_TIME; clock VVT_TIME; clock AVI_A_TIME; clock AVI_V_TIME; clock HEART_TIME; clock PROGRAMMER_TIME; // Channels encoding Events chan commandedOn; chan commandedOff; chan toIdle; chan toInhibited; chan toTriggered; chan toAVI; chan APace; chan VPace; chan AVI_Refractory_Done; chan AVI_APace; chan AVI_APace_Done; chan AVI_Sense_from_V; urgent chan VentricularChamberSense; //urgent chan AtrialChamberSense; // nobody is listening urgent chan EnablePaceElectronics; urgent chan DisablePaceElectronics; // user interactions: Heart urgent chan stopHeartBeat; urgent chan startHeartBeat; // diagnostic int[0,1] wasSwitchedOff; // ------------------------------ Auxiallry: // anybody listening to VentricularChamberSense? int[0,1] V_listening; int[0,1] A_LISTENING_TO_V; // -- Constant Parameters ------------------------------ const REFRACTORY_TIME 50; const SENSE_TIMEOUT 15; const HEART_DELAY_AFTER_V_CONTRACTION 50; const HEART_DELAY_AFTER_A_CONTRACTION 5; const HEART_ALLOWED_STOP_TIME 135; const MODE_SWITCH_DELAY 66; // ---------------------------------------------------------------------- const ALLOW_SWITCH_OFF 0; // ----- Translation Slack ----- chan xtSglNR4; chan HrtVCtrctENTRYtrhrtsm4; chan HrtACtrctENTRYtrhrtsm4; chan xtSglNR5; chan HrtDtlVCtrctENTRYtrhrtsm4Dtl5; chan HrtDtlACtrctENTRYtrhrtsm4Dtl5; chan xtSglNR3; chan PrgrmmrIdlENTRYtrprgrmmrsm3; chan PrgrmmrRdmENTRYtrprgrmmrsm3; chan PrgrmmrMdswtchENTRYtrprgrmmrsm3; chan xtSglNR2; chan PcAVIENTRYtrpcmkr2; chan PcVVIENTRYtrpcmkr2; chan PcVVTENTRYtrpcmkr2; chan PcIdlENTRYtrpcmkr2; chan PcOffENTRYtrpcmkr2; chan xtSglNR6; chan PcOdfltENTRYtrpcmkr2sbCmpt6; chan PcOIdlENTRYtrpcmkr2sbCmpt6; chan PcOVVIENTRYtrpcmkr2sbCmpt6; chan PcOVVTENTRYtrpcmkr2sbCmpt6; chan PcOAVIENTRYtrpcmkr2sbCmpt6; chan xtSglNR9; chan PcOAVIdfltENTRYtrpcmkr2sbCmpt6AVIMd9; chan PcOAVIdfltEITlvpcmkr2sbCmpt6AVIMd9; chan xtSglNR11; chan PcOAVIVPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9VPrt11; chan xtSglNR10; chan PcOAVIAPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9APrt10; chan xtSglNR8; chan PcOVVTdfltENTRYtrpcmkr2sbCmpt6VVTMd8; chan xtSglNR7; chan PcOVVIdfltENTRYtrpcmkr2sbCmpt6VVIMd7; int triggerVar1; int triggerVar2; int triggerVar3; int triggerVar4; int triggerVar5; int triggerVar7; process heartsim4{ state Detail, L1, L2, IDLE, L15, L16; commit L1, L2, L15, L16; init IDLE; trans L1 -> Detail{sync HrtDtlVCtrctENTRYtrhrtsm4Dtl5!; }, L2 -> Detail{sync HrtDtlACtrctENTRYtrhrtsm4Dtl5!; }, IDLE -> L2{sync HrtACtrctENTRYtrhrtsm4?; assign HEART_TIME := 0; }, IDLE -> L1{sync HrtVCtrctENTRYtrhrtsm4?; assign HEART_TIME := 0; }, Detail -> IDLE{sync xtSglNR4?; }, Detail -> L15{guard triggerVar2 == 1; sync APace?; assign HEART_TIME := 0, HEART_TIME := 0; }, L15 -> L2{sync xtSglNR5!; }, Detail -> L16{guard triggerVar2 == 1; sync VPace?; assign HEART_TIME := 0, HEART_TIME := 0; }, L16 -> L1{sync xtSglNR5!; }; } process heartsim4Detail5{ state VContraction{HEART_TIME <= 0}, AContraction{HEART_TIME <= 0}, AfterVContraction{HEART_TIME <= HEART_DELAY_AFTER_V_CONTRACTION}, AfterAContraction{HEART_TIME <= HEART_DELAY_AFTER_A_CONTRACTION}, Stopped{HEART_TIME <= HEART_ALLOWED_STOP_TIME}, Flatline, IDLE; init IDLE; trans IDLE -> AContraction{sync HrtDtlACtrctENTRYtrhrtsm4Dtl5?; assign triggerVar2 := triggerVar2 + 1 ; }, IDLE -> VContraction{sync HrtDtlVCtrctENTRYtrhrtsm4Dtl5?; assign triggerVar2 := triggerVar2 + 1 ; }, AContraction -> AfterAContraction{}, AfterAContraction -> VContraction{guard HEART_TIME == HEART_DELAY_AFTER_A_CONTRACTION; assign HEART_TIME := 0; }, VContraction -> AfterVContraction{guard V_listening == 0; }, VContraction -> AfterVContraction{guard V_listening == 1; sync VentricularChamberSense!; }, AfterVContraction -> AContraction{guard HEART_TIME == HEART_DELAY_AFTER_V_CONTRACTION; assign HEART_TIME := 0; }, AfterVContraction -> Stopped{assign HEART_TIME := 0; }, Stopped -> Flatline{guard HEART_TIME == HEART_ALLOWED_STOP_TIME; assign HEART_TIME := 0; }, VContraction -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }, AContraction -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }, AfterVContraction -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }, AfterAContraction -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }, Stopped -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }, Flatline -> IDLE{sync xtSglNR5?; assign triggerVar2 := triggerVar2 - 1 ; }; } process programmersim3{ state Idle, Random, Modeswitch, ModeswitchDelay{PROGRAMMER_TIME <= MODE_SWITCH_DELAY}, IDLE; init IDLE; trans IDLE -> Modeswitch{sync PrgrmmrMdswtchENTRYtrprgrmmrsm3?; assign triggerVar1 := triggerVar1 + 1 ; }, IDLE -> Random{sync PrgrmmrRdmENTRYtrprgrmmrsm3?; }, IDLE -> Idle{sync PrgrmmrIdlENTRYtrprgrmmrsm3?; }, Random -> Random{sync commandedOn!; }, Random -> Random{guard ALLOW_SWITCH_OFF == 1; sync commandedOff!; }, Random -> Random{sync toInhibited!; }, Random -> Random{sync toTriggered!; }, Modeswitch -> ModeswitchDelay{sync toInhibited!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, Modeswitch -> ModeswitchDelay{sync toTriggered!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, Modeswitch -> ModeswitchDelay{guard ALLOW_SWITCH_OFF == 1; sync commandedOff!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, Modeswitch -> ModeswitchDelay{sync commandedOn!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, Modeswitch -> ModeswitchDelay{sync toAVI!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, Modeswitch -> ModeswitchDelay{guard ALLOW_SWITCH_OFF == 1; sync toIdle!; assign PROGRAMMER_TIME :=0, triggerVar1 := triggerVar1 - 1 ; }, ModeswitchDelay -> Modeswitch{guard PROGRAMMER_TIME == MODE_SWITCH_DELAY; assign triggerVar1 := triggerVar1 + 1 ; }, Modeswitch -> IDLE{sync xtSglNR3?; assign triggerVar1 := triggerVar1 - 1 ; }; } process pacemaker2{ state Off, subComponent, L3, L4, L5, L6, L7, IDLE, L17, L18, L19, L20, L21, L22, L23, L24, L25, L26, L27, L28, L29, L30, L31, L32, L33, L34, L35, L36, L37, L38, L39, L40, L41, L42, L43, L44, L45, L46, L47, L48, L49, L50, L51, L52, L53, L54, L55, L56, L57, L58, L59, L60, L61; commit L3, L4, L5, L6, L7, L17, L18, L19, L20, L21, L22, L23, L24, L25, L26, L27, L28, L29, L30, L31, L32, L33, L34, L35, L36, L37, L38, L39, L40, L41, L42, L43, L44, L45, L46, L47, L48, L49, L50, L51, L52, L53, L54, L55, L56, L57, L58, L59, L60, L61; init IDLE; trans L3 -> subComponent{sync PcOdfltENTRYtrpcmkr2sbCmpt6!; }, L4 -> subComponent{sync PcOIdlENTRYtrpcmkr2sbCmpt6!; }, L5 -> subComponent{sync PcOVVIENTRYtrpcmkr2sbCmpt6!; }, L6 -> subComponent{sync PcOVVTENTRYtrpcmkr2sbCmpt6!; }, L7 -> subComponent{sync PcOAVIENTRYtrpcmkr2sbCmpt6!; }, IDLE -> Off{sync PcOffENTRYtrpcmkr2?; }, IDLE -> L4{sync PcIdlENTRYtrpcmkr2?; }, IDLE -> L6{sync PcVVTENTRYtrpcmkr2?; assign VVT_TIME := 0; }, IDLE -> L5{sync PcVVIENTRYtrpcmkr2?; assign VVI_TIME := 0; }, IDLE -> L7{sync PcAVIENTRYtrpcmkr2?; assign AVI_A_TIME := 0, AVI_V_TIME := 0; }, Off -> L3{sync commandedOn?; assign VVI_TIME := 0; }, subComponent -> L17{guard triggerVar3 == 1; sync commandedOff?; assign V_listening := 0, wasSwitchedOff := 1; }, L17 -> Off{sync xtSglNR6!; }, subComponent -> L18{guard triggerVar3 == 1; sync toIdle?; assign V_listening := 0, wasSwitchedOff := 1; }, L18 -> L4{sync xtSglNR6!; }, subComponent -> L19{guard triggerVar3 == 1; sync toInhibited?; assign V_listening := 0, VVI_TIME := 0; }, L19 -> L5{sync xtSglNR6!; }, subComponent -> L20{guard triggerVar3 == 1; sync toTriggered?; assign V_listening := 0, VVT_TIME := 0; }, L20 -> L6{sync xtSglNR6!; }, subComponent -> L21{guard triggerVar3 == 1; sync toAVI?; assign V_listening := 0, AVI_A_TIME := 0, AVI_V_TIME := 0; }, L21 -> L7{sync xtSglNR6!; }, subComponent -> L22{guard triggerVar4 == 1; sync commandedOff?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L22 -> L23{sync xtSglNR7!; }, L23 -> Off{sync xtSglNR6!; }, subComponent -> L24{guard triggerVar4 == 1; sync toIdle?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L24 -> L25{sync xtSglNR7!; }, L25 -> L4{sync xtSglNR6!; }, subComponent -> L26{guard triggerVar4 == 1; sync toInhibited?; assign V_listening := 0, V_listening := 0, VVI_TIME := 0; }, L26 -> L27{sync xtSglNR7!; }, L27 -> L5{sync xtSglNR6!; }, subComponent -> L28{guard triggerVar4 == 1; sync toTriggered?; assign V_listening := 0, V_listening := 0, VVT_TIME := 0; }, L28 -> L29{sync xtSglNR7!; }, L29 -> L6{sync xtSglNR6!; }, subComponent -> L30{guard triggerVar4 == 1; sync toAVI?; assign V_listening := 0, V_listening := 0, AVI_A_TIME := 0, AVI_V_TIME := 0; }, L30 -> L31{sync xtSglNR7!; }, L31 -> L7{sync xtSglNR6!; }, subComponent -> L32{guard triggerVar5 == 1; sync commandedOff?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L32 -> L33{sync xtSglNR8!; }, L33 -> Off{sync xtSglNR6!; }, subComponent -> L34{guard triggerVar5 == 1; sync toIdle?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L34 -> L35{sync xtSglNR8!; }, L35 -> L4{sync xtSglNR6!; }, subComponent -> L36{guard triggerVar5 == 1; sync toInhibited?; assign V_listening := 0, V_listening := 0, VVI_TIME := 0; }, L36 -> L37{sync xtSglNR8!; }, L37 -> L5{sync xtSglNR6!; }, subComponent -> L38{guard triggerVar5 == 1; sync toTriggered?; assign V_listening := 0, V_listening := 0, VVT_TIME := 0; }, L38 -> L39{sync xtSglNR8!; }, L39 -> L6{sync xtSglNR6!; }, subComponent -> L40{guard triggerVar5 == 1; sync toAVI?; assign V_listening := 0, V_listening := 0, AVI_A_TIME := 0, AVI_V_TIME := 0; }, L40 -> L41{sync xtSglNR8!; }, L41 -> L7{sync xtSglNR6!; }, subComponent -> L42{guard triggerVar7 == 2; sync commandedOff?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L42 -> L43{sync xtSglNR11!; }, L43 -> L44{sync xtSglNR10!; }, L44 -> L45{sync xtSglNR9!; }, L45 -> Off{sync xtSglNR6!; }, subComponent -> L46{guard triggerVar7 == 2; sync toIdle?; assign V_listening := 0, wasSwitchedOff := 1, V_listening := 0; }, L46 -> L47{sync xtSglNR11!; }, L47 -> L48{sync xtSglNR10!; }, L48 -> L49{sync xtSglNR9!; }, L49 -> L4{sync xtSglNR6!; }, subComponent -> L50{guard triggerVar7 == 2; sync toInhibited?; assign V_listening := 0, V_listening := 0, VVI_TIME := 0; }, L50 -> L51{sync xtSglNR11!; }, L51 -> L52{sync xtSglNR10!; }, L52 -> L53{sync xtSglNR9!; }, L53 -> L5{sync xtSglNR6!; }, subComponent -> L54{guard triggerVar7 == 2; sync toTriggered?; assign V_listening := 0, V_listening := 0, VVT_TIME := 0; }, L54 -> L55{sync xtSglNR11!; }, L55 -> L56{sync xtSglNR10!; }, L56 -> L57{sync xtSglNR9!; }, L57 -> L6{sync xtSglNR6!; }, subComponent -> L58{guard triggerVar7 == 2; sync toAVI?; assign V_listening := 0, V_listening := 0, AVI_A_TIME := 0, AVI_V_TIME := 0; }, L58 -> L59{sync xtSglNR11!; }, L59 -> L60{sync xtSglNR10!; }, L60 -> L61{sync xtSglNR9!; }, L61 -> L7{sync xtSglNR6!; }; } process pacemaker2subComponent6{ state Idle, VVIMode, L8, VVTMode, L9, AVIMode, L10, IDLE; commit L8, L9, L10; init IDLE; trans L8 -> VVIMode{sync PcOVVIdfltENTRYtrpcmkr2sbCmpt6VVIMd7!; }, L9 -> VVTMode{sync PcOVVTdfltENTRYtrpcmkr2sbCmpt6VVTMd8!; }, L10 -> AVIMode{sync PcOAVIdfltENTRYtrpcmkr2sbCmpt6AVIMd9!; }, IDLE -> L10{sync PcOAVIENTRYtrpcmkr2sbCmpt6?; assign AVI_A_TIME := 0, AVI_V_TIME := 0; }, IDLE -> L9{sync PcOVVTENTRYtrpcmkr2sbCmpt6?; assign VVT_TIME := 0; }, IDLE -> L8{sync PcOVVIENTRYtrpcmkr2sbCmpt6?; assign VVI_TIME := 0; }, IDLE -> Idle{sync PcOIdlENTRYtrpcmkr2sbCmpt6?; assign triggerVar3 := triggerVar3 + 1 ; }, IDLE -> L8{sync PcOdfltENTRYtrpcmkr2sbCmpt6?; assign VVI_TIME := 0; }, Idle -> IDLE{sync xtSglNR6?; assign triggerVar3 := triggerVar3 - 1 ; }, VVIMode -> IDLE{sync xtSglNR6?; }, VVTMode -> IDLE{sync xtSglNR6?; }, AVIMode -> IDLE{sync xtSglNR6?; }; } process pacemaker2subComponent6AVIMode9{ state IDLE, ACTIVE, pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork1, pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork2; commit pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork1, pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork2; init IDLE; trans pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork2 -> ACTIVE{sync PcOAVIVPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9VPrt11!; }, pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork1 -> pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork2{sync PcOAVIAPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9APrt10!; }, IDLE -> pacemaker2subComponent6AVIMode9PaceOnAVIdefaultENTRYfork1{sync PcOAVIdfltENTRYtrpcmkr2sbCmpt6AVIMd9?; }, ACTIVE -> IDLE{sync xtSglNR9?; }; } process pacemaker2subComponent6AVIMode9VPart11{ state Refractory, Waiting, WaitingAU{AVI_V_TIME <= 0}, APacing, IDLE; init IDLE; trans IDLE -> Refractory{sync PcOAVIVPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9VPrt11?; assign triggerVar7 := triggerVar7 + 1 ; }, Refractory -> Waiting{sync AVI_Refractory_Done?; assign V_listening := 1; }, Waiting -> WaitingAU{sync VentricularChamberSense?; assign AVI_V_TIME := 0, V_listening := 0; }, WaitingAU -> Waiting{guard A_LISTENING_TO_V == 0; assign V_listening := 1; }, WaitingAU -> Waiting{sync AVI_Sense_from_V!; assign V_listening := 1; }, Waiting -> APacing{sync AVI_APace?; assign V_listening := 0; }, APacing -> Refractory{sync AVI_APace_Done?; }, Refractory -> IDLE{sync xtSglNR11?; assign triggerVar7 := triggerVar7 - 1 ; }, Waiting -> IDLE{sync xtSglNR11?; assign triggerVar7 := triggerVar7 - 1 ; }, WaitingAU -> IDLE{sync xtSglNR11?; assign triggerVar7 := triggerVar7 - 1 ; }, APacing -> IDLE{sync xtSglNR11?; assign triggerVar7 := triggerVar7 - 1 ; }; } process pacemaker2subComponent6AVIMode9APart10{ state Refractory{AVI_A_TIME <= REFRACTORY_TIME}, Waiting{AVI_A_TIME <= SENSE_TIMEOUT}, APacing{AVI_A_TIME <= 0}, APacingAU{AVI_A_TIME <= 0}, IDLE; init IDLE; trans IDLE -> Refractory{sync PcOAVIAPrtdfltENTRYtrpcmkr2sbCmpt6AVIMd9APrt10?; assign triggerVar7 := triggerVar7 + 1 ; }, Refractory -> Waiting{guard AVI_A_TIME == REFRACTORY_TIME; sync AVI_Refractory_Done!; assign A_LISTENING_TO_V := 1, AVI_A_TIME := 0; }, Waiting -> Waiting{sync AVI_Sense_from_V?; assign AVI_A_TIME := 0; }, Waiting -> APacing{guard AVI_A_TIME == SENSE_TIMEOUT; sync APace!; assign A_LISTENING_TO_V := 0, AVI_A_TIME := 0; }, APacing -> APacingAU{sync AVI_APace!; assign AVI_A_TIME := 0; }, APacingAU -> Refractory{sync AVI_APace_Done!; assign AVI_A_TIME := 0; }, Refractory -> IDLE{sync xtSglNR10?; assign triggerVar7 := triggerVar7 - 1 ; }, Waiting -> IDLE{sync xtSglNR10?; assign triggerVar7 := triggerVar7 - 1 ; }, APacing -> IDLE{sync xtSglNR10?; assign triggerVar7 := triggerVar7 - 1 ; }, APacingAU -> IDLE{sync xtSglNR10?; assign triggerVar7 := triggerVar7 - 1 ; }; } process pacemaker2subComponent6VVTMode8{ state Refractory{VVT_TIME <= REFRACTORY_TIME}, WaitingforSense{VVT_TIME <= SENSE_TIMEOUT}, WaitingforSenseAU{VVT_TIME <= 0}, Pacing{VVT_TIME <= 0}, IDLE; init IDLE; trans IDLE -> Refractory{sync PcOVVTdfltENTRYtrpcmkr2sbCmpt6VVTMd8?; assign triggerVar5 := triggerVar5 + 1 ; }, Refractory -> WaitingforSense{guard VVT_TIME == REFRACTORY_TIME; assign VVT_TIME := 0, V_listening := 1; }, WaitingforSense -> WaitingforSenseAU{sync VentricularChamberSense?; assign VVT_TIME := 0,V_listening := 0; }, WaitingforSense -> WaitingforSenseAU{guard VVT_TIME == SENSE_TIMEOUT; assign VVT_TIME := 0, V_listening := 0; }, WaitingforSenseAU -> Pacing{sync VPace!; assign VVT_TIME := 0; }, Pacing -> Refractory{}, Refractory -> IDLE{sync xtSglNR8?; assign triggerVar5 := triggerVar5 - 1 ; }, WaitingforSense -> IDLE{sync xtSglNR8?; assign triggerVar5 := triggerVar5 - 1 ; }, WaitingforSenseAU -> IDLE{sync xtSglNR8?; assign triggerVar5 := triggerVar5 - 1 ; }, Pacing -> IDLE{sync xtSglNR8?; assign triggerVar5 := triggerVar5 - 1 ; }; } process pacemaker2subComponent6VVIMode7{ state Refractory{VVI_TIME <= REFRACTORY_TIME}, WaitingforSense{VVI_TIME <= SENSE_TIMEOUT}, WaitingforSenseAU{VVI_TIME <= 0}, Pacing{VVI_TIME <= 0}, IDLE; init IDLE; trans IDLE -> Refractory{sync PcOVVIdfltENTRYtrpcmkr2sbCmpt6VVIMd7?; assign triggerVar4 := triggerVar4 + 1 ; }, Refractory -> WaitingforSense{guard VVI_TIME == REFRACTORY_TIME; assign VVI_TIME := 0, V_listening := 1; }, WaitingforSense -> WaitingforSense{sync VentricularChamberSense?; assign VVI_TIME := 0; }, WaitingforSense -> WaitingforSenseAU{guard VVI_TIME == SENSE_TIMEOUT; assign VVI_TIME := 0, V_listening := 0; }, WaitingforSenseAU -> Pacing{sync VPace!; assign VVI_TIME := 0; }, Pacing -> Refractory{}, Refractory -> IDLE{sync xtSglNR7?; assign triggerVar4 := triggerVar4 - 1 ; }, WaitingforSense -> IDLE{sync xtSglNR7?; assign triggerVar4 := triggerVar4 - 1 ; }, WaitingforSenseAU -> IDLE{sync xtSglNR7?; assign triggerVar4 := triggerVar4 - 1 ; }, Pacing -> IDLE{sync xtSglNR7?; assign triggerVar4 := triggerVar4 - 1 ; }; } process globalKickoff12{ state start, L11, L12, L13, L14; commit start, L11, L12, L14; init start; trans start -> L11{sync PcAVIENTRYtrpcmkr2!; }, L11 -> L12{sync PrgrmmrMdswtchENTRYtrprgrmmrsm3!; }, L12 -> L13{sync HrtACtrctENTRYtrhrtsm4!; }, L13 -> L14{guard triggerVar1 == 1; }, L14 -> L13{sync xtSglNR3!; }; } system heartsim4, heartsim4Detail5, programmersim3, pacemaker2, pacemaker2subComponent6, pacemaker2subComponent6AVIMode9, pacemaker2subComponent6AVIMode9VPart11, pacemaker2subComponent6AVIMode9APart10, pacemaker2subComponent6VVTMode8, pacemaker2subComponent6VVIMode7, globalKickoff12;