state transitions cluster__P P cluster__P_ComboStepMaximality ComboStepMaximality cluster__P_ComboStepMaximality_ComboStepMaximality ComboStepMaximality cluster__P_ComboStepMaximality_MemoryProtocolDeducer MemoryProtocolDeducer cluster__P_ComboStepMaximality_InternalEventDeducer InternalEventDeducer cluster__P_ComboStepMaximality_InputEventDeducer InputEventDeducer cluster__P_Priority Priority cluster__P_Priority_Composite Composite cluster__P_MemoryProtocol MemoryProtocol cluster__P_MemoryProtocol_MemoryProtocol MemoryProtocol cluster__P_MemoryProtocol_RegionAssign RegionAssign cluster__P_InternalEventLifeline InternalEventLifeline cluster__P_InternalEventLifeline_InternalEventLifeline InternalEventLifeline cluster__P_InternalEventLifeline_RegionReceive2 RegionReceive2 cluster__P_InternalEventLifeline_RegionReceive1 RegionReceive1 cluster__P_InternalEventLifeline_RegionBroadcast RegionBroadcast cluster__P_InputEventLifeline InputEventLifeline cluster__P_BigStepMaximality BigStepMaximality __initial __initial->_P _P_ComboStepMaximality_ComboStepMaximality_initial _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps NoComboSteps _P_ComboStepMaximality_ComboStepMaximality_initial->_P_ComboStepMaximality_ComboStepMaximality_NoComboSteps _P_ComboStepMaximality_ComboStepMaximality_TakeMany TakeMany _P_ComboStepMaximality_ComboStepMaximality_Syntactic Syntactic _P_ComboStepMaximality_ComboStepMaximality_TakeOne TakeOne _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeMany ¬input0 [INSTATE(["/P/InputEventLifeline/FirstComboStep","/P/ComboStepMaximality/InputEventDeducer/TakeMany"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeMany ¬internal0 [INSTATE(["/P/InternalEventLifeline/InternalEventLifeline/NextComboStep","/P/ComboStepMaximality/InternalEventDeducer/TakeMany"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeMany [x == 1 and INSTATE(["/P/MemoryProtocol/MemoryProtocol/ComboStep","/P/ComboStepMaximality/MemoryProtocolDeducer/TakeMany"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_Syntactic ¬input0 [INSTATE(["/P/InputEventLifeline/FirstComboStep","/P/ComboStepMaximality/InputEventDeducer/Syntactic"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_Syntactic ¬internal0 [INSTATE(["/P/InternalEventLifeline/InternalEventLifeline/NextComboStep","/P/ComboStepMaximality/InternalEventDeducer/Syntactic"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_Syntactic [x == 1 and INSTATE(["/P/MemoryProtocol/MemoryProtocol/ComboStep","/P/ComboStepMaximality/MemoryProtocolDeducer/Syntactic"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeOne ¬input0 [INSTATE(["/P/InputEventLifeline/FirstComboStep","/P/ComboStepMaximality/InputEventDeducer/TakeOne"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeOne ¬internal0 [INSTATE(["/P/InternalEventLifeline/InternalEventLifeline/NextComboStep","/P/ComboStepMaximality/InternalEventDeducer/TakeOne"])]    _P_ComboStepMaximality_ComboStepMaximality_NoComboSteps->_P_ComboStepMaximality_ComboStepMaximality_TakeOne [x == 1 and INSTATE(["/P/MemoryProtocol/MemoryProtocol/ComboStep","/P/ComboStepMaximality/MemoryProtocolDeducer/TakeOne"])]    _P_ComboStepMaximality_MemoryProtocolDeducer_initial _P_ComboStepMaximality_MemoryProtocolDeducer_Initial Initial _P_ComboStepMaximality_MemoryProtocolDeducer_initial->_P_ComboStepMaximality_MemoryProtocolDeducer_Initial _P_ComboStepMaximality_MemoryProtocolDeducer_TakeMany TakeMany _P_ComboStepMaximality_MemoryProtocolDeducer_Syntactic Syntactic ✓ _P_ComboStepMaximality_MemoryProtocolDeducer_Syntactic->_P_ComboStepMaximality_MemoryProtocolDeducer_TakeMany [x == 0]    _P_ComboStepMaximality_MemoryProtocolDeducer_TakeOne TakeOne _P_ComboStepMaximality_MemoryProtocolDeducer_TakeOne->_P_ComboStepMaximality_MemoryProtocolDeducer_Syntactic [x == 0]    _P_ComboStepMaximality_MemoryProtocolDeducer_Initial->_P_ComboStepMaximality_MemoryProtocolDeducer_TakeOne [x == 0]    _P_ComboStepMaximality_InternalEventDeducer_initial _P_ComboStepMaximality_InternalEventDeducer_Initial Initial _P_ComboStepMaximality_InternalEventDeducer_initial->_P_ComboStepMaximality_InternalEventDeducer_Initial _P_ComboStepMaximality_InternalEventDeducer_TakeMany TakeMany _P_ComboStepMaximality_InternalEventDeducer_Syntactic Syntactic ✓ _P_ComboStepMaximality_InternalEventDeducer_Syntactic->_P_ComboStepMaximality_InternalEventDeducer_TakeMany internal0    _P_ComboStepMaximality_InternalEventDeducer_TakeOne TakeOne _P_ComboStepMaximality_InternalEventDeducer_TakeOne->_P_ComboStepMaximality_InternalEventDeducer_Syntactic internal0    _P_ComboStepMaximality_InternalEventDeducer_Initial->_P_ComboStepMaximality_InternalEventDeducer_TakeOne internal0    _P_ComboStepMaximality_InputEventDeducer_initial _P_ComboStepMaximality_InputEventDeducer_Initial Initial _P_ComboStepMaximality_InputEventDeducer_initial->_P_ComboStepMaximality_InputEventDeducer_Initial _P_ComboStepMaximality_InputEventDeducer_TakeMany TakeMany _P_ComboStepMaximality_InputEventDeducer_Syntactic Syntactic ✓ _P_ComboStepMaximality_InputEventDeducer_Syntactic->_P_ComboStepMaximality_InputEventDeducer_TakeMany input0    _P_ComboStepMaximality_InputEventDeducer_TakeOne TakeOne _P_ComboStepMaximality_InputEventDeducer_TakeOne->_P_ComboStepMaximality_InputEventDeducer_Syntactic input0    _P_ComboStepMaximality_InputEventDeducer_Initial->_P_ComboStepMaximality_InputEventDeducer_TakeOne input0    _P_Priority_initial _P_Priority_initial->_P_Priority_Composite _P_Priority_SourceChild SourceChild _P_Priority_SourceParent SourceParent _P_Priority_Composite->_P_Priority_SourceParent _P_Priority_Composite_initial _P_Priority_Composite_Basic Basic _P_Priority_Composite_initial->_P_Priority_Composite_Basic _P_Priority_Composite_Basic->_P_Priority_SourceChild _P_MemoryProtocol_MemoryProtocol_initial _P_MemoryProtocol_MemoryProtocol_Initial Initial _P_MemoryProtocol_MemoryProtocol_initial->_P_MemoryProtocol_MemoryProtocol_Initial _P_MemoryProtocol_MemoryProtocol_SmallStep SmallStep _P_MemoryProtocol_MemoryProtocol_ComboStep ComboStep _P_MemoryProtocol_MemoryProtocol_BigStep BigStep _P_MemoryProtocol_MemoryProtocol_BigStep->_P_MemoryProtocol_MemoryProtocol_ComboStep [x == 1]    _P_MemoryProtocol_MemoryProtocol_Initial->_P_MemoryProtocol_MemoryProtocol_SmallStep [x == 1]    _P_MemoryProtocol_MemoryProtocol_Initial->_P_MemoryProtocol_MemoryProtocol_BigStep [x == 0]    _P_MemoryProtocol_RegionAssign_initial _P_MemoryProtocol_RegionAssign_Initial Initial _P_MemoryProtocol_RegionAssign_initial->_P_MemoryProtocol_RegionAssign_Initial _P_MemoryProtocol_RegionAssign_Assigned Assigned _P_MemoryProtocol_RegionAssign_Initial->_P_MemoryProtocol_RegionAssign_Assigned /x = 1    _P_InternalEventLifeline_InternalEventLifeline_initial _P_InternalEventLifeline_InternalEventLifeline_Initial Initial _P_InternalEventLifeline_InternalEventLifeline_initial->_P_InternalEventLifeline_InternalEventLifeline_Initial _P_InternalEventLifeline_InternalEventLifeline_Queue Queue _P_InternalEventLifeline_InternalEventLifeline_NextComboStep NextComboStep _P_InternalEventLifeline_InternalEventLifeline_Queue->_P_InternalEventLifeline_InternalEventLifeline_NextComboStep [INSTATE(["/P/InternalEventLifeline/RegionReceive1/GotEvent","/P/InternalEventLifeline/RegionReceive2/GotEvent"])]    _P_InternalEventLifeline_InternalEventLifeline_Remainder Remainder _P_InternalEventLifeline_InternalEventLifeline_NextSmallStep NextSmallStep _P_InternalEventLifeline_InternalEventLifeline_Initial->_P_InternalEventLifeline_InternalEventLifeline_Queue _P_InternalEventLifeline_InternalEventLifeline_Initial->_P_InternalEventLifeline_InternalEventLifeline_Remainder [INSTATE(["/P/InternalEventLifeline/RegionReceive1/GotEvent","/P/InternalEventLifeline/RegionReceive2/GotEvent"])]    _P_InternalEventLifeline_InternalEventLifeline_Initial->_P_InternalEventLifeline_InternalEventLifeline_NextSmallStep [INSTATE(["/P/InternalEventLifeline/RegionReceive1/GotEvent"]) and not INSTATE(["/P/InternalEventLifeline/RegionReceive2/GotEvent"])]    _P_InternalEventLifeline_RegionReceive2_initial _P_InternalEventLifeline_RegionReceive2_Initial Initial _P_InternalEventLifeline_RegionReceive2_initial->_P_InternalEventLifeline_RegionReceive2_Initial _P_InternalEventLifeline_RegionReceive2_GotEvent GotEvent _P_InternalEventLifeline_RegionReceive2_Initial->_P_InternalEventLifeline_RegionReceive2_GotEvent internal0    _P_InternalEventLifeline_RegionReceive1_initial _P_InternalEventLifeline_RegionReceive1_Initial Initial _P_InternalEventLifeline_RegionReceive1_initial->_P_InternalEventLifeline_RegionReceive1_Initial _P_InternalEventLifeline_RegionReceive1_GotEvent GotEvent _P_InternalEventLifeline_RegionReceive1_Initial->_P_InternalEventLifeline_RegionReceive1_GotEvent internal0    _P_InternalEventLifeline_RegionBroadcast_initial _P_InternalEventLifeline_RegionBroadcast_Initial Initial _P_InternalEventLifeline_RegionBroadcast_initial->_P_InternalEventLifeline_RegionBroadcast_Initial _P_InternalEventLifeline_RegionBroadcast_Done Done _P_InternalEventLifeline_RegionBroadcast_Initial->_P_InternalEventLifeline_RegionBroadcast_Done ^internal0    _P_InputEventLifeline_initial _P_InputEventLifeline_FirstSmallStep FirstSmallStep _P_InputEventLifeline_initial->_P_InputEventLifeline_FirstSmallStep _P_InputEventLifeline_FirstComboStep FirstComboStep _P_InputEventLifeline_Whole Whole _P_InputEventLifeline_Whole->_P_InputEventLifeline_FirstComboStep ¬input0    _P_InputEventLifeline_FirstSmallStep->_P_InputEventLifeline_Whole input0    _P_BigStepMaximality_initial _P_BigStepMaximality_Initial Initial _P_BigStepMaximality_initial->_P_BigStepMaximality_Initial _P_BigStepMaximality_TakeMany TakeMany _P_BigStepMaximality_Syntactic Syntactic ✓ _P_BigStepMaximality_Syntactic->_P_BigStepMaximality_TakeMany _P_BigStepMaximality_TakeOne TakeOne _P_BigStepMaximality_TakeOne->_P_BigStepMaximality_Syntactic _P_BigStepMaximality_Initial->_P_BigStepMaximality_TakeOne