%% file DiningPhilosophers.mcrl2 %% October 2011 %% %% This specification corresponds to a Paradigm model of the migration %% for a system with three philosophers %% %% NOTE. There are slight differences with the model in the journal %% paper since here three rather than five philosophers are %% modeled. In particular, there are for McPal in state Delegated only %% four possible ways for the migration to continue. Therefore rules %% (29)-(32) do not appear in this specification. sort %% Phil PID = struct P1 | P2 | P3 ; PState = struct Thinking | AskingForks | Eating ; PPhase = struct Disallowed | Allowed ; %% Fork FID = struct F1 | F2 | F3 ; FState = struct RHq | LHq | AtRH | AtLH ; FPhase = struct Freed | Claimed ; %% McPhil MID = struct M1 | M2 | M3 ; MState = struct NonExisting | Awake | JoiningIn | ToL | ToR | ToBeL | ToBeR | Dozing ; MPhase = struct Passive | Active | EndAsL| EndAsR | Retreating ; %% McPal LState = struct Observing | JITting | StartMigr | Delegated | Gathering | Content ; LPhase = struct Hibernating | Migrating ; %% Global Protocol Rules GRuleSet = struct Hib | Start | Halfway | End ; %% Individual Protocol Rules IRuleSet = struct IAsIs | McPhilHasTakenOver | McPhilChoseL | McPhilChoseR | ToBeLSet | ToBeRSet ; %% subprotocols ProtID = struct Prot1 | Prot2 | Prot3 ; map Phil2Prot : PID -> ProtID ; eqn Phil2Prot(P1) = Prot1 ; Phil2Prot(P2) = Prot2 ; Phil2Prot(P3) = Prot3 ; map LFork2Prot : FID -> ProtID ; eqn LFork2Prot(F1) = Prot1 ; LFork2Prot(F2) = Prot2 ; LFork2Prot(F3) = Prot3 ; map RFork2Prot : FID -> ProtID ; eqn RFork2Prot(F1) = Prot3 ; RFork2Prot(F2) = Prot1 ; RFork2Prot(F3) = Prot2 ; map MPhil2Prot : MID -> ProtID ; eqn MPhil2Prot(M1) = Prot1 ; MPhil2Prot(M2) = Prot2 ; MPhil2Prot(M3) = Prot3 ; act %% Phil local transitions getHungry, take, layDown : PID ; %% Phil phase transfers %% phase transfers in as-is rule17DisallowedRequest, rule19DisallowedRequest, rule20AllowedDone : ProtID ; %%phase transfers during migration rule38DisallowedRequest, rule40DisallowedRequest, rule41AllowedDone, rule42DisallowedRequest, rule43DisallowedRequest, rule45DisallowedRequest, rule46AllowedDone, rule47DisallowedRequest, rule49DisallowedRequest, rule50AllowedDone : ProtID ; rule51DisallowedRequest, rule53DisallowedRequest, rule54AllowedDone, rule55DisallowedRequest, rule57DisallowedTriv, rule58DisallowedRequest, rule59AllowedDone, rule60DisallowedRequest, rule62DisallowedRequest, rule63AllowedDone, rule64DisallowedRequest, rule66DisallowedTriv, rule67DisallowedRequest, rule68AllowedDone : ProtID ; %%phase transfers in to-be as left-oriented rule69DisallowedRequest, rule71DisallowedRequest, rule72AllowedDone, %%phase transfers in to-be as right-oriented rule73DisallowedRequest, rule75DisallowedRequest, rule76AllowedDone : ProtID ; %% Fork local transitions toRH, toLH, tryRH, tryLH, return : FID ; %% Fork phase transfers %%phase transfers actions in as-is rule17FreedGone, rule18ClaimedGot, rule18FreedGone, rule19ClaimedGot, rule20ClaimedGot : ProtID ; %%phase transfers during migration rule38FreedGone, rule39ClaimedGot, rule39FreedGone, rule40ClaimedGot, rule41ClaimedGot, rule42ClaimedGot, rule42ClaimedTriv, rule43FreedGone, rule44ClaimedGot, rule44FreedGone, rule45ClaimedGot, rule46ClaimedGot, rule47FreedGone, rule48ClaimedGot, rule48FreedGone, rule49ClaimedGot, rule50ClaimedGot : ProtID ; rule51FreedGone, rule52ClaimedGot, rule52FreedGone, rule53ClaimedGot, rule54ClaimedGot, rule55FreedTriv, rule55FreedGone, rule56ClaimedTriv, rule56FreedGone, rule57ClaimedTriv, rule58ClaimedGot, rule59ClaimedGot : ProtID ; rule60FreedGone, rule61ClaimedGot, rule61FreedGone, rule62ClaimedGot, rule63ClaimedGot, rule64FreedTriv, rule64FreedGone, rule65ClaimedTriv, rule65FreedGone, rule66ClaimedTriv, rule67ClaimedGot, rule68ClaimedGot : ProtID ; %%phase transfers in to-be rule69FreedGone, rule70ClaimedGot, rule70FreedGone, rule71ClaimedGot, rule72ClaimedGot, rule73FreedGone, rule74ClaimedGot, rule74FreedGone, rule75ClaimedGot, rule76ClaimedGot : ProtID ; %% McPhil local transitions stir, takeOver37 : ProtID; %% conducting transitions during migration conductToL38, conductToL39, conductToL47, conductToL48, conductToL49, conductToL50 : ProtID; conductToR40, conductToR41, conductToR42, conductToR43, conductToR44, conductToR45, conductToR46 : ProtID; choreofyToL51, choreofyToL52, choreofyToL53, choreofyToL54, choreofyToR55, choreofyToR56, choreofyToR57, choreofyToR58, choreofyToR59, choreofyToR60, choreofyToR61, choreofyToR62, choreofyToR63, choreofyToR64, choreofyToR65, choreofyToR66, choreofyToR67, choreofyToR68, %% McPhil local transitions after migration yawn, immobilize : ProtID ; %% McPhil phase transfers rule24PassiveTriv ; rule25ActiveHalfwayR, rule26ActiveHalfwayL ; rule27ActiveHalfwayR, rule27ActiveHalfwayL ; rule28ActiveHalfwayR, rule28ActiveHalfwayL ; rule33EndAsRDone, rule34EndAsLDone : ProtID; rule35RetreatingAway ; rule38JoiningInConductToL, rule39JoiningInConductToL, rule40JoiningInConductToR, rule41JoiningInConductToR, rule42JoiningInConductToR : ProtID; rule43ToRConductToR, rule44ToRConductToR, rule45ToRConductToR, rule46ToRConductToR, rule47ToLConductToL, rule48ToLConductToL, rule49ToLConductToL, rule50ToLConductToL : ProtID; %% McPal local transitions wantChange, giveOut21, cleanUp22, delegate24, rule23HibernatingPrepared, stub25, stub26, stub27, stub28; collect33, collect34 : ProtID ; close35 ; rule36MigratingDone ; %% Global Protocol dynamics rule21ok, rule22ok, rule23ok, rule24ok, rule25ok, rule26ok, rule27ok, rule28ok; rule33ok, rule34ok : ProtID ; rule35ok, rule36ok ; %% Indinvidual Protocol Dynamics %% Individual Protocol dynamics in as-is rule17ok, rule18ok, rule19ok, rule20ok : ProtID ; %% Individual Protocol dynamics during migration rule37ok, rule38ok, rule39ok, rule40ok, rule41ok, rule42ok, rule43ok, rule44ok, rule45ok, rule46ok, rule47ok, rule48ok, rule49ok, rule50ok, %% Individual Protocol dynamics towards to-be left-oriented rule51ok, rule52ok, rule53ok, rule54ok, %% Individual Protocol dynamics towards to-be right-oriented rule55ok, rule56ok, rule57ok, rule58ok, rule59ok, rule60ok, rule61ok, rule62ok, rule63ok, rule64ok, rule65ok, rule66ok, rule67ok, rule68ok, %% Individual Protocol dynamics in to-be left-oriented rule69ok, rule70ok, rule71ok, rule72ok, %% Individual Protocol dynamics in to-be right-oriented rule73ok, rule74ok, rule75ok, rule76ok : ProtID ; %% communicating actions rule17, rule18, rule19, rule20 : ProtID ; rule21, rule22, rule23, rule24, rule25, rule26, rule27, rule28; rule33, rule34 : ProtID ; rule35, rule36 ; rule37, rule38, rule39, rule40, rule41, rule42 : ProtID ; rule43, rule44, rule45, rule46, rule47, rule48, rule49, rule50 : ProtID ; rule51, rule52, rule53, rule54, rule55, rule56, rule57, rule58, rule59 : ProtID ; rule60, rule61, rule62, rule63, rule64, rule65, rule66, rule67, rule68 : ProtID ; rule69, rule70, rule71, rule72, rule73, rule74, rule75, rule76 : ProtID ; %% Process defintions %% Every process specification consists of two parts. The first part %% describes the local transitions the process can perform given the %% current local state and the current phases. The second part %% specifies the phase transfer possibilities given the current phase %% of the process and the subset of states that form the trap allowing %% the phase transfer. proc Phil(i:PID,s:PState,p:PPhase) = %% local transitions from Phil STD in Figure 1a ( ( s == Thinking ) && ( p == Disallowed ) ) -> getHungry(i) . Phil(i,AskingForks,p) + ( ( s == AskingForks ) && ( p == Allowed ) ) -> take(i) . Phil(i,Eating,p) + ( ( s == Eating ) && ( p == Allowed ) ) -> layDown(i) . Phil(i,Thinking,p) + %% phase transfers %% phase transfer in as-is left-oriented %% corresponding to role Eater in Figure 1b %% and the corresponding traps in Figure 1c ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule17DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule19DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule20AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% phase transfer during migration -- orchestration rules %% rules (38)-(42) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule38DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule40DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule41AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule42DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> %% rules (43)-(50) rule43DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule45DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule46AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule47DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule49DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule50AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% rules (51)-(54) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule51DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule53DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule54AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% rules (55)-(59) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule55DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) ) -> rule57DisallowedTriv(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule58DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule59AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% rules (60)-(63) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule60DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule62DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule63AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% rules (64)-(67) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule64DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) ) -> rule66DisallowedTriv(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule67DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule68AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% phase transfers in to-be left-order, %% rules (69)-(72) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule69DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule71DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule72AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) + %% phase transfers in to-be right-order, %% rules (73)-(76) ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule73DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Disallowed) + ( ( p == Disallowed ) && ( s == AskingForks ) ) -> rule75DisallowedRequest(Phil2Prot(i)) . Phil(i,s,Allowed) + ( ( p == Allowed ) && ( s == Thinking ) ) -> rule76AllowedDone(Phil2Prot(i)) . Phil(i,s,Disallowed) ; proc Fork(i:FID,s:FState,pl:FPhase,pr:FPhase) = %% local transitions from Fork STD in Figure 2a %% transition tryLH ( ( s == RHq ) && ( pl == Freed ) && ( pr == Freed ) ) -> tryLH(i) . Fork(i,LHq,Freed,Freed) + ( ( s == RHq ) && ( pl == Freed ) && ( pr == Claimed ) ) -> delta + ( ( s == RHq ) && ( pl == Claimed ) && ( pr == Freed ) ) -> tryLH(i) . Fork(i,LHq,Claimed,Freed) + ( ( s == RHq ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> delta + %% transition tryRH ( ( s == LHq ) && ( pl == Freed ) && ( pr == Freed ) ) -> tryRH(i) . Fork(i,RHq,Freed,Freed) + ( ( s == LHq ) && ( pl == Freed ) && ( pr == Claimed ) ) -> tryRH(i) . Fork(i,RHq,Freed,Claimed) + ( ( s == LHq ) && ( pl == Claimed ) && ( pr == Freed ) ) -> delta + ( ( s == LHq ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> delta + %% transition toLH ( ( s == LHq ) && ( pl == Freed ) && ( pr == Freed ) ) -> delta + ( ( s == LHq ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> toLH(i) . Fork(i,AtLH,Claimed,Claimed) + ( ( s == LHq ) && ( pl == Claimed ) && ( pr == Freed ) ) -> toLH(i) . Fork(i,AtLH,Claimed,Freed) + ( ( s == LHq ) && ( pl == Freed ) && ( pr == Claimed ) ) -> delta + %% transition toRH ( ( s == RHq ) && ( pl == Freed ) && ( pr == Freed ) ) -> delta + ( ( s == RHq ) && ( pl == Freed ) && ( pr == Claimed ) ) -> toRH(i) . Fork(i,AtRH,Freed,Claimed) + ( ( s == RHq ) && ( pl == Claimed ) && ( pr == Freed ) ) -> delta + ( ( s == RHq ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> toRH(i) . Fork(i,AtRH,Claimed,Claimed) + %% transition return from AtRH ( ( s == AtRH ) && ( pl == Freed ) && ( pr == Freed ) ) -> return(i) . Fork(i,LHq,Freed,Freed) + ( ( s == AtRH ) && ( pl == Freed ) && ( pr == Claimed ) ) -> delta + ( ( s == AtRH ) && ( pl == Claimed ) && ( pr == Freed ) ) -> return(i) . Fork(i,LHq,Claimed,Freed) + ( ( s == AtRH ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> delta + %% transition return from AtLH ( ( s == AtLH ) && ( pl == Freed ) && ( pr == Freed ) ) -> return(i) . Fork(i,RHq,Freed,Freed) + ( ( s == AtLH ) && ( pl == Freed ) && ( pr == Claimed ) ) -> return(i) . Fork(i,RHq,Freed,Claimed) + ( ( s == AtLH ) && ( pl == Claimed ) && ( pr == Freed ) ) -> delta + ( ( s == AtLH ) && ( pl == Claimed ) && ( pr == Claimed ) ) -> delta + %% phase transfers %% phase transfers in as-is left-oriented %% corresponding to role ForLH in Figure 2c %% and the corresponing traps in Figure 2b %% rules (17)-(20) ( ( pl == Freed ) && ( ( s != AtLH ) ) ) -> rule17FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule18ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Freed ) && ( ( s != AtRH ) ) ) -> rule18FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule19ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule20ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule20ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% phase transfers during migration - left-right order %% rules (38)-(39) ( ( pl == Freed ) && ( s != AtLH ) ) -> rule38FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule39ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Freed ) && ( ( s != AtRH ) ) ) -> rule39FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + %% phase transfers during migration - right-left order %% rules (40)-(41) ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule40ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule41ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule41ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% switch rule from left-oriented to right oriented, rule (42) ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule42ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) ) -> rule42ClaimedTriv(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + %% right-order decided and moved to ToR, rules (43)-(46) ( ( pr == Freed ) && ( s != AtRH ) ) -> rule43FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule44ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Freed ) && ( ( s != AtLH ) ) ) -> rule44FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule45ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule46ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule46ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% left-right decided and moved to ToL, rules (47)-(50) ( ( pl == Freed ) && ( s != AtLH ) ) -> rule47FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule48ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Freed ) && ( s != AtRH ) ) -> rule48FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule49ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule50ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule50ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% at ToL, sticking to left, rules (51)-(54) ( ( pl == Freed ) && ( s != AtLH ) ) -> rule51FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule52ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Freed ) && ( s != AtRH ) ) -> rule52FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule53ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule54ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule54ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% at ToL, moving to right, rules (55)-(58) ( ( pl == Freed ) ) -> rule55FreedTriv(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Freed ) && ( s != AtRH ) ) -> rule55FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) ) -> rule56ClaimedTriv(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Freed ) && ( s != AtRH ) ) -> rule56FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) ) -> rule57ClaimedTriv(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) ) -> rule57ClaimedTriv(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule58ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule59ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule59ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% at ToL, sticking to left, rules (60)-(63) ( ( pr == Freed ) && ( s != AtRH ) ) -> rule60FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule61ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Freed ) && ( s != AtLH ) ) -> rule61FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule62ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule63ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule63ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + %% at ToR, moving to left, rules (64)-(68) ( ( pr == Freed ) ) -> rule64FreedTriv(RFork2Prot(i)) . Fork(i,s,pl,Freed) + ( ( pl == Freed ) && ( s != AtLH ) ) -> rule64FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Claimed ) ) -> rule65ClaimedTriv(RFork2Prot(i)) . Fork(i,s,pl,Freed) + ( ( pl == Freed ) && ( s != AtLH ) ) -> rule65FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Claimed ) ) -> rule66ClaimedTriv(RFork2Prot(i)) . Fork(i,s,pl,Freed) + ( ( pl == Claimed ) ) -> rule66ClaimedTriv(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule67ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule68ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule68ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% phase transfers in to-be, left oriented, %% rules (69)-(72) ( ( pl == Freed ) && ( ( s == RHq ) || ( s == LHq ) || ( s == AtRH ) ) ) -> rule69FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule70ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pr == Freed ) && ( ( s != AtRH ) ) ) -> rule70FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule71ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule72ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule72ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) + %% phase transfers in to-be, right oriented, %% rules (73)-(76) ( ( pr == Freed ) && ( s != AtRH ) ) -> rule73FreedGone(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule74ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Claimed) + ( ( pl == Freed ) && ( ( s != AtLH ) ) ) -> rule74FreedGone(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule75ClaimedGot(LFork2Prot(i)) . Fork(i,s,Claimed,pr) + ( ( pl == Claimed ) && ( s == AtLH ) ) -> rule76ClaimedGot(LFork2Prot(i)) . Fork(i,s,Freed,pr) + ( ( pr == Claimed ) && ( s == AtRH ) ) -> rule76ClaimedGot(RFork2Prot(i)) . Fork(i,s,pl,Freed) ; proc McPhil(i:MID, s:MState, p:MPhase) = %% local transitions from McPhil STD in Figure 7a %% allowed in phase Active ( ( s == NonExisting ) && ( p == Active ) ) -> stir(MPhil2Prot(i)) . McPhil(i,Awake,p) + ( ( s == Awake ) && ( p == Active ) ) -> takeOver37(MPhil2Prot(i)) . McPhil(i,JoiningIn,Active) + ( ( s == JoiningIn ) && ( p == Active ) ) -> conductToL38(MPhil2Prot(i)) . McPhil(i,ToL,Active) + ( ( s == JoiningIn ) && ( p == Active ) ) -> conductToL39(MPhil2Prot(i)) . McPhil(i,ToL,Active) + ( ( s == JoiningIn ) && ( p == Active ) ) -> conductToR40(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == JoiningIn ) && ( p == Active ) ) -> conductToR41(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == JoiningIn ) && ( p == Active ) ) -> conductToR42(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == ToR ) && ( p == Active ) ) -> conductToR43(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == ToR ) && ( p == Active ) ) -> conductToR44(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == ToR ) && ( p == Active ) ) -> conductToR45(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == ToR ) && ( p == Active ) ) -> conductToR46(MPhil2Prot(i)) . McPhil(i,ToR,Active) + ( ( s == ToL ) && ( p == Active ) ) -> conductToL47(MPhil2Prot(i)) . McPhil(i,ToL,Active) + ( ( s == ToL ) && ( p == Active ) ) -> conductToL48(MPhil2Prot(i)) . McPhil(i,ToL,Active) + ( ( s == ToL ) && ( p == Active ) ) -> conductToL49(MPhil2Prot(i)) . McPhil(i,ToL,Active) + ( ( s == ToL ) && ( p == Active ) ) -> conductToL50(MPhil2Prot(i)) . McPhil(i,ToL,Active) + %% allowed in phase EndAsL ( ( s == ToL ) && ( p == EndAsL ) ) -> choreofyToL51(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToL ) && ( p == EndAsL ) ) -> choreofyToL52(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToL ) && ( p == EndAsL ) ) -> choreofyToL53(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToL ) && ( p == EndAsL ) ) -> choreofyToL54(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToR ) && ( p == EndAsL ) ) -> choreofyToR64(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToR ) && ( p == EndAsL ) ) -> choreofyToR65(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToR ) && ( p == EndAsL ) ) -> choreofyToR66(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToR ) && ( p == EndAsL ) ) -> choreofyToR67(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToR ) && ( p == EndAsL ) ) -> choreofyToR68(MPhil2Prot(i)) . McPhil(i,ToBeL,EndAsL) + ( ( s == ToBeL ) && ( p == EndAsL ) ) -> yawn(MPhil2Prot(i)) . McPhil(i,Dozing,EndAsL) + ( ( s == Dozing ) && ( p == EndAsL ) ) -> immobilize(MPhil2Prot(i)) . McPhil(i,NonExisting,EndAsL) + %% allowed in phase EndAsR ( ( s == ToL ) && ( p == EndAsR ) ) -> choreofyToR55(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToL ) && ( p == EndAsR ) ) -> choreofyToR56(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToL ) && ( p == EndAsR ) ) -> choreofyToR57(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToL ) && ( p == EndAsR ) ) -> choreofyToR58(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToL ) && ( p == EndAsR ) ) -> choreofyToR59(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToR ) && ( p == EndAsR ) ) -> choreofyToR60(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToR ) && ( p == EndAsR ) ) -> choreofyToR61(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToR ) && ( p == EndAsR ) ) -> choreofyToR62(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToR ) && ( p == EndAsR ) ) -> choreofyToR63(MPhil2Prot(i)) . McPhil(i,ToBeR,EndAsR) + ( ( s == ToBeR ) && ( p == EndAsR ) ) -> yawn(MPhil2Prot(i)) . McPhil(i,Dozing,EndAsR) + ( ( s == Dozing ) && ( p == EndAsR ) ) -> immobilize(MPhil2Prot(i)) . McPhil(i,NonExisting,EndAsR) + %% allowed in phase Retreating ( ( s == ToBeL ) && ( p == Retreating ) ) -> yawn(MPhil2Prot(i)) . McPhil(i,Dozing,Retreating) + ( ( s == ToBeR ) && ( p == Retreating ) ) -> yawn(MPhil2Prot(i)) . McPhil(i,Dozing,Retreating) + ( ( s == Dozing ) && ( p == Retreating ) ) -> immobilize(MPhil2Prot(i)) . McPhil(i,NonExisting,Retreating) + %% phase transfers %% corresponding to role Evol in Figure 7c %% and the corresponing traps in Figure 7b %% Note the way the consistency rules (25)-(28) resolve %% the existing non-determinism in the role Evol %% in the phase Active ( ( p == Passive ) && ( s == NonExisting ) ) -> rule24PassiveTriv . McPhil(i,s,Active) + %% rule25 for three phils: if all R, change fork1 to L ( ( p == Active ) && ( s == ToR ) ) -> ( ( i == M1 ) -> rule25ActiveHalfwayR . McPhil(i,s,EndAsL) + ( i != M1 ) -> rule25ActiveHalfwayR . McPhil(i,s,EndAsR) ) + %% rule 26 for three phils: if all L, change fork2 to R ( ( p == Active ) && ( s == ToL ) ) -> ( ( i == M2 ) -> rule26ActiveHalfwayL . McPhil(i,s,EndAsR) + ( i != M2 ) -> rule26ActiveHalfwayL . McPhil(i,s,EndAsL) ) + %% rule 27 for three phils: if two L and one R, fine ( ( p == Active ) && ( s == ToL ) ) -> rule27ActiveHalfwayL . McPhil(i,s,EndAsL) + ( ( p == Active ) && ( s == ToR ) ) -> rule27ActiveHalfwayR . McPhil(i,s,EndAsR) + %% rule 28 for three phils: if two R and one L, fine ( ( p == Active ) && ( s == ToL ) ) -> rule28ActiveHalfwayL . McPhil(i,s,EndAsL) + ( ( p == Active ) && ( s == ToR ) ) -> rule28ActiveHalfwayR . McPhil(i,s,EndAsR) + %% finishing phase transfers ( ( p == EndAsR ) && ( s != ToL ) && ( s != ToR ) ) -> rule33EndAsRDone(MPhil2Prot(i)) . McPhil(i,s,Retreating) + ( ( p == EndAsL ) && ( s != ToL ) && ( s != ToR ) ) -> rule34EndAsLDone(MPhil2Prot(i)) . McPhil(i,s,Retreating) + ( ( p == Retreating ) && ( s == NonExisting ) ) -> rule35RetreatingAway . McPhil(i,s,Passive) ; proc McPal(s:LState,p:LPhase) = %% local transitions from McPal STD in Figure 6a ( ( s == Observing ) && ( p == Hibernating ) ) -> wantChange . McPal(JITting,Hibernating) + ( ( s == JITting ) && ( p == Hibernating ) ) -> giveOut21 . McPal(StartMigr,Hibernating) + ( ( s == Content ) && ( p == Hibernating ) ) -> cleanUp22 . McPal(Observing,Hibernating) + %% local transitions of McPal that %% prescribe the continuation of the migration %% rules (25)- (28). %% Note the way these local transitions %% navigate the migration to different migration scenarios, %% but do not influence the transition taken by a particular McPhil %% reflecting as such the distributed character of the migration %% test case for rule 25 ( ( s == Delegated ) && ( p == Migrating ) ) -> stub25 . McPal(Gathering,Migrating) + %% test case for rule 26 ( ( s == Delegated ) && ( p == Migrating ) ) -> stub26 . McPal(Gathering,Migrating) + %% test case for rule 27 ( ( s == Delegated ) && ( p == Migrating ) ) -> stub27 . McPal(Gathering,Migrating) + %% test case for rule 28 ( ( s == Delegated ) && ( p == Migrating ) ) -> stub28 . McPal(Gathering,Migrating) + %% local transitions towards finishing the migration %% rules (33)-(35) ( ( s == Gathering ) && ( p == Migrating ) ) -> ( sum protid:ProtID . collect33(protid) . McPal(Gathering,Migrating) ) + ( ( s == Gathering ) && ( p == Migrating ) ) -> ( sum protid:ProtID . collect34(protid) . McPal(Gathering,Migrating) ) + ( ( s == Gathering ) && ( p == Migrating ) ) -> close35 . McPal(Content,Migrating) + %% phase transfers of McPal %% corresponding to role Evol in Figure 6c %% and the corresponding traps in Figure 6b %% consistency rule (23) ( ( p == Hibernating ) && ( s == StartMigr ) ) -> rule23HibernatingPrepared . McPal(s,Migrating) + %% conducting rule (24) ( ( s == StartMigr ) && ( p == Migrating ) ) -> delegate24 . McPal(Delegated,Migrating) + %% consistency rule (36) ( ( p == Migrating ) && ( s == Content ) ) -> rule36MigratingDone . McPal(s,Hibernating) ; %% This is the specification of the General Protocol Rule Process. %% This process is a counterpart to the change clauses orchestrated by %% McPal in the Paradigm model. proc GProtRules(grs:GRuleSet) = ( grs == Hib ) -> ( rule21ok . GProtRules(Start) ) + ( grs == Start ) -> ( rule23ok . GProtRules() + rule24ok . GProtRules(Halfway) ) + ( grs == Halfway ) -> ( rule25ok . GProtRules() + rule26ok . GProtRules() + rule27ok . GProtRules() + rule28ok . GProtRules() + ( sum protid:ProtID . rule33ok(protid) . GProtRules() ) + ( sum protid:ProtID . rule34ok(protid) . GProtRules() ) + rule35ok . GProtRules() + rule36ok . GProtRules() + rule22ok . GProtRules(End) ) + ( grs == End ) -> ( delta ) ; %% These are the specifications of the three Individual Protocol Rule %% Processes. They are counterparts to change clauses orchestrated by %% the three McPhil's. proc IProtRules(protid:ProtID,irs:IRuleSet) = ( irs == IAsIs ) -> ( rule17ok(protid) . IProtRules() + rule18ok(protid) . IProtRules() + rule19ok(protid) . IProtRules() + rule20ok(protid) . IProtRules() + rule37ok(protid) . IProtRules(protid,McPhilHasTakenOver) ) + ( irs == McPhilHasTakenOver ) -> ( rule38ok(protid) . IProtRules(protid,McPhilChoseL) + rule39ok(protid) . IProtRules(protid,McPhilChoseL) + rule40ok(protid) . IProtRules(protid,McPhilChoseR) + rule41ok(protid) . IProtRules(protid,McPhilChoseR) + rule42ok(protid) . IProtRules(protid,McPhilChoseR) ) + ( irs == McPhilChoseL ) -> ( rule47ok(protid) . IProtRules() + rule48ok(protid) . IProtRules() + rule49ok(protid) . IProtRules() + rule50ok(protid) . IProtRules() + rule51ok(protid) . IProtRules(protid,ToBeLSet) + rule52ok(protid) . IProtRules(protid,ToBeLSet) + rule53ok(protid) . IProtRules(protid,ToBeLSet) + rule54ok(protid) . IProtRules(protid,ToBeLSet) + rule55ok(protid) . IProtRules(protid,ToBeRSet) + rule56ok(protid) . IProtRules(protid,ToBeRSet) + rule57ok(protid) . IProtRules(protid,ToBeRSet) + rule58ok(protid) . IProtRules(protid,ToBeRSet) + rule59ok(protid) . IProtRules(protid,ToBeRSet) ) + ( irs == McPhilChoseR ) -> ( rule43ok(protid) . IProtRules() + rule44ok(protid) . IProtRules() + rule45ok(protid) . IProtRules() + rule46ok(protid) . IProtRules() + rule60ok(protid) . IProtRules(protid,ToBeRSet) + rule61ok(protid) . IProtRules(protid,ToBeRSet) + rule62ok(protid) . IProtRules(protid,ToBeRSet) + rule63ok(protid) . IProtRules(protid,ToBeRSet) + rule64ok(protid) . IProtRules(protid,ToBeLSet) + rule65ok(protid) . IProtRules(protid,ToBeLSet) + rule66ok(protid) . IProtRules(protid,ToBeLSet) + rule67ok(protid) . IProtRules(protid,ToBeLSet) + rule68ok(protid) . IProtRules(protid,ToBeLSet) ) + ( irs == ToBeLSet ) -> ( rule69ok(protid) . IProtRules() + rule70ok(protid) . IProtRules() + rule71ok(protid) . IProtRules() + rule72ok(protid) . IProtRules() ) + ( irs == ToBeRSet ) -> ( rule73ok(protid) . IProtRules() + rule74ok(protid) . IProtRules() + rule75ok(protid) . IProtRules() + rule76ok(protid) . IProtRules() ) ; init hide ( { %% Phil getHungry, take, layDown, %% Fork tryRH, tryLH, toRH, toLH, return, %% %% rule17, rule18, rule19, rule20, %% rule21, rule22, %% rule23, rule24, %% rule25, rule26, rule27, rule28, %% rules for more phils %% rule29, rule30, rule31, rule32, %% rule33, rule34, rule35, rule36, rule37, %% rule38, rule39, rule40, rule41, rule42, %% rule43, rule44, rule45, rule46, %% rule47, rule48, rule49, rule50, %% rule51, rule52, rule53, rule54, %% rule55, rule56, rule57, rule58, rule59, %% rule60, rule61, rule62, rule63, %% rule64, rule65, rule66, rule67, rule68, %% rule69, rule70, rule71, rule72, %% rule73, rule74, rule75, rule76 wantChange, stir, yawn, immobilize }, allow ( { %% Phil getHungry, take, layDown, %% Fork toRH, toLH, return, tryRH, tryLH, %% McPal wantChange, %% McPhil stir, yawn, immobilize, %% consistency rules rule17, rule18, rule19, rule20, rule21, rule22, rule23, rule24, rule25, rule26, rule27, rule28, rule33, rule34, rule35, rule36, rule37, rule38, rule39, rule40, rule41, rule42, rule43, rule44, rule45, rule46, rule47, rule48, rule49, rule50, rule51, rule52, rule53, rule54, rule55, rule56, rule57, rule58, rule59, rule60, rule61, rule62, rule63, rule64, rule65, rule66, rule67, rule68, rule69, rule70, rule71, rule72, rule73, rule74, rule75, rule76 }, comm( { %% as-is rule17DisallowedRequest | rule17FreedGone | rule17ok -> rule17, rule18ClaimedGot | rule18FreedGone | rule18ok-> rule18, rule19DisallowedRequest | rule19ClaimedGot | rule19ok -> rule19, rule20AllowedDone | rule20ClaimedGot | rule20ClaimedGot | rule20ok -> rule20, giveOut21 | rule21ok -> rule21, cleanUp22 | rule22ok -> rule22, %% rule23HibernatingPrepared | rule23ok -> rule23, delegate24 | rule24PassiveTriv | rule24PassiveTriv | rule24PassiveTriv | rule24ok -> rule24, %% stub25 | rule25ActiveHalfwayR | rule25ActiveHalfwayR | rule25ActiveHalfwayR | rule25ok -> rule25, stub26 | rule26ActiveHalfwayL | rule26ActiveHalfwayL | rule26ActiveHalfwayL | rule26ok -> rule26, stub27 | rule27ActiveHalfwayL | rule27ActiveHalfwayL | rule27ActiveHalfwayR | rule27ok -> rule27, stub28 | rule28ActiveHalfwayR | rule28ActiveHalfwayR | rule28ActiveHalfwayL | rule28ok -> rule28, %% collect33 | rule33EndAsRDone | rule33ok -> rule33, collect34 | rule34EndAsLDone | rule34ok -> rule34, close35 | rule35RetreatingAway | rule35RetreatingAway | rule35RetreatingAway | rule35ok -> rule35, rule36MigratingDone | rule36ok -> rule36, %% McPhil makes its choice takeOver37 | rule37ok -> rule37, conductToL38 | rule38DisallowedRequest | rule38FreedGone | rule38ok -> rule38, conductToL39 | rule39ClaimedGot | rule39FreedGone | rule39ok -> rule39, conductToR40 | rule40DisallowedRequest | rule40ClaimedGot | rule40ok -> rule40, conductToR41 | rule41AllowedDone | rule41ClaimedGot | rule41ClaimedGot | rule41ok -> rule41, conductToR42 | rule42DisallowedRequest | rule42ClaimedGot | rule42ClaimedTriv | rule42ok -> rule42, %% McPhil chose right-orientation conductToR43 | rule43DisallowedRequest | rule43FreedGone | rule43ok -> rule43, conductToR44 | rule44ClaimedGot | rule44FreedGone | rule44ok -> rule44, conductToR45 | rule45DisallowedRequest | rule45ClaimedGot | rule45ok -> rule45, conductToR46 | rule46AllowedDone | rule46ClaimedGot | rule46ClaimedGot | rule46ok -> rule46, %% McPhil chose left orientation conductToL47 | rule47DisallowedRequest | rule47FreedGone | rule47ok -> rule47, conductToL48 | rule48ClaimedGot | rule48FreedGone | rule48ok -> rule48, conductToL49 | rule49DisallowedRequest | rule49ClaimedGot | rule49ok -> rule49, conductToL50 | rule50AllowedDone | rule50ClaimedGot | rule50ClaimedGot | rule50ok -> rule50, %% McPhil's left choice confirmed choreofyToL51 | rule51DisallowedRequest | rule51FreedGone | rule51ok -> rule51, choreofyToL52 | rule52ClaimedGot | rule52FreedGone | rule52ok -> rule52, choreofyToL53 | rule53DisallowedRequest | rule53ClaimedGot | rule53ok -> rule53, choreofyToL54 | rule54AllowedDone | rule54ClaimedGot | rule54ClaimedGot | rule54ok -> rule54, %% McPhil's left choice overruled choreofyToR55 | rule55DisallowedRequest | rule55FreedTriv | rule55FreedGone | rule55ok -> rule55, choreofyToR56 | rule56ClaimedTriv | rule56FreedGone | rule56ok -> rule56, choreofyToR57 | rule57DisallowedTriv | rule57ClaimedTriv | rule57ClaimedTriv | rule57ok -> rule57, choreofyToR58 | rule58DisallowedRequest | rule58ClaimedGot | rule58ok -> rule58, choreofyToR59 | rule59AllowedDone | rule59ClaimedGot | rule59ClaimedGot | rule59ok -> rule59, %% McPhil's right choice confirmed choreofyToR60 | rule60DisallowedRequest | rule60FreedGone | rule60ok -> rule60, choreofyToR61 | rule61ClaimedGot | rule61FreedGone | rule61ok -> rule61, choreofyToR62 | rule62DisallowedRequest | rule62ClaimedGot | rule62ok -> rule62, choreofyToR63 | rule63AllowedDone | rule63ClaimedGot | rule63ClaimedGot | rule63ok -> rule63, %% McPhil's right choice overruled choreofyToR64 | rule64DisallowedRequest | rule64FreedTriv | rule64FreedGone | rule64ok -> rule64, choreofyToR65 | rule65ClaimedTriv | rule65FreedGone | rule65ok -> rule65, choreofyToR66 | rule66DisallowedTriv | rule66ClaimedTriv | rule66ClaimedTriv | rule66ok -> rule66, choreofyToR67 | rule67DisallowedRequest | rule67ClaimedGot | rule67ok -> rule67, choreofyToR68 | rule68AllowedDone | rule68ClaimedGot | rule68ClaimedGot | rule68ok -> rule68, %% to-be left oriented rule69DisallowedRequest | rule69FreedGone | rule69ok -> rule69, rule70ClaimedGot | rule70FreedGone | rule70ok-> rule70, rule71DisallowedRequest | rule71ClaimedGot | rule71ok -> rule71, rule72AllowedDone | rule72ClaimedGot | rule72ClaimedGot | rule72ok -> rule72, %% to-be right oriented rule73DisallowedRequest | rule73FreedGone | rule73ok -> rule73, rule74ClaimedGot | rule74FreedGone | rule74ok-> rule74, rule75DisallowedRequest | rule75ClaimedGot | rule75ok -> rule75, rule76AllowedDone | rule76ClaimedGot | rule76ClaimedGot | rule76ok -> rule76 }, Phil(P1,Thinking,Disallowed) || Phil(P2,AskingForks,Disallowed) || Phil(P3,Thinking,Disallowed) || Fork(F1,RHq,Freed,Freed) || Fork(F2,RHq,Freed,Freed) || Fork(F3,RHq,Freed,Freed) || McPhil(M1,NonExisting,Passive) || McPhil(M2,NonExisting,Passive) || McPhil(M3,NonExisting,Passive) || McPal(Observing,Hibernating) || IProtRules(Prot1,IAsIs) || IProtRules(Prot2,IAsIs) || IProtRules(Prot3,IAsIs) || GProtRules(Hib) ) ));