--- blue, red, pink top-down separately mod PSYSTEM is inc PSCONFIGURATION . inc INT . sorts Priority PrioritySet . subsort Priority < Qid . subsort Priority < PrioritySet . op noprty : -> Priority . op __ : PrioritySet PrioritySet -> PrioritySet [assoc comm id: noprty] . sort PriorityPair PriorityPairSet . subsort PriorityPair < PriorityPairSet . op empty : -> PriorityPairSet . op _>_ : Priority Priority -> PriorityPair . op _`,_ : PriorityPairSet PriorityPairSet -> PriorityPairSet . sorts MRule MRuleSet . subsort MRule < MRuleSet . op _->_ : Soup MsgDissSoup -> MRule . op _:_->_ : Priority Soup MsgDissSoup -> MRule . op none : -> MRule . op _`,_ : MRuleSet MRuleSet -> MRuleSet [assoc comm id: none] . op maxSize : -> Int . op idle : -> Configuration . vars L L1 L2 : Label . vars O O' : Obj . vars S S1 S2 : Soup . var Mb : Membrane . vars M M1 M2 M3 M4 : MembraneSet . vars DM DM1 DM2 : DMembraneSet . vars M+ M1+ M2+ : MembraneSet+ . vars M' M1' M2' : MembraneSet? . vars neM neM1 neM2 neM3 neM4 : NeMembraneSet . vars neDM neDM1 neDM2 : NeDMembraneSet . vars neM+ neM1+ neM2+ : NeMembraneSet+ . vars neM' neM1' neM2' : NeMembraneSet? . vars S? S1? S' S1' S2' : Soup? . vars Sd Sd1 Sd2 : DissSoup . var Sod : OutDissSoup . var So : OutSoup . vars Smd Smd1 Smd2 : MsgDissSoup . var B : Bool . var PPair : PriorityPair . var PPS PPS1 : PriorityPairSet . vars R R1 R2 : MRule . vars RS RS1 RS2 RS3 : MRuleSet . vars P P1 P2 : Priority . vars PS PS1 PS2 : PrioritySet . op lhs : MRule -> Soup . eq lhs(S -> Smd) = S . eq lhs(P : S -> Smd) = S . op rhs : MRule -> MsgDissSoup . eq rhs(S -> Smd) = Smd . eq rhs(P : S -> Smd) = Smd . op prty : MRule -> Priority . eq prty(S -> Smd) = noprty . eq prty(P : S -> Smd) = P . eq prty(none) = noprty . op priorities : MRuleSet -> PrioritySet . ceq priorities(RS) = prty(R1) prty(R2) priorities(RS1) if R1, R2, RS1 := RS /\ R1 =/= none /\ R2 =/= none . eq priorities(R) = prty(R) . eq priorities(none) = noprty . op rules : Label -> MRuleSet . op freeDeltaRules : Label -> MRuleSet . op rho : Label -> PriorityPairSet . op lower : Label Priority -> PrioritySet . op lower : Priority PriorityPairSet -> PrioritySet . eq lower(L, P) = lower(P, rho(L)) . ceq lower(P, PPS) = lower(P, PPair) lower(P, PPS1) if PPair, PPS1 := PPS . eq lower(P, (P1 > P2)) = if P == P1 then P2 else noprty fi . --- eq lower(P, PPair) = noprty [owise] . op _in_ : Priority PrioritySet -> Bool . ceq P in PS = true if P PS1 := PS . eq P in PS = false [owise] . op rules2 : Label Bool -> MRuleSet . eq rules2(L, B) = if B then freeDeltaRules(L) else rules(L) fi . ---- --- multiset inclusion ---- op isIn : Soup Soup -> Bool . ceq isIn(S1, S2) = true if S1 S := S2 . eq isIn(S1, S2) = false [owise] . op hasDelta : MsgDissSoup -> Bool . ceq hasDelta(Smd) = true if Smd1 delta := Smd . eq hasDelta(Smd) = false [owise] . ---- --- removes from PS the lower priorities than P ---- op rmLower : Label Priority PrioritySet -> PrioritySet . ceq rmLower(L, P, PS) = rmLower(L, P, rmLower(L, P1, PS2)) if P =/= noprty /\ P1 PS1 := lower(L, P) /\ P1 PS2 := PS /\ P1 =/= noprty . ceq rmLower(L, P, PS) = PS if P == noprty . eq rmLower(L, P, PS) = PS [owise] . ---- --- tests if a matching rule is allowed to be applied wrt priorities ---- op allowed : Label Soup MRule MRuleSet PrioritySet -> Bool . --- [1] ceq allowed(L, S, R, RS, PS) = allowed(L, S, R, R1, PS) and allowed(L, S, R, RS1, PS) if R1, RS1 := RS /\ R1 =/= none /\ RS1 =/= none . --- [2] R1 has prty over R, but R1 does not match ceq allowed(L, S, R, R1, PS) = (not isIn(lhs(R1), S)) if prty(R1) =/= noprty /\ prty(R) =/= noprty /\ prty(R) in PS /\ prty(R) in lower(L, prty(R1)) . --- [3] ceq allowed(L, S, R, R1, PS) = true if prty(R1) =/= noprty /\ prty(R) =/= noprty /\ prty(R) in PS /\ not(prty(R) in lower(L, prty(R1))) . --- [4] ceq allowed(L, S, R, R1, PS) = true if prty(R1) == noprty /\ prty(R) =/= noprty /\ prty(R) in PS . --- [5] ceq allowed(L, S, R, R1, PS) = false if prty(R) =/= noprty /\ not (prty(R) in PS) . --- [6] ceq allowed(L, S, R, R1, PS) = true if prty(R) == noprty . eq allowed(L, S, R, R1, PS) = false [owise] . ---- --- verifies for every membrane L if there are no more rules --- that can be applied in a maximal parallel step ---- op irreducible : Label Soup MRuleSet -> Bool . op irreducible : Label PrioritySet Soup MRuleSet -> Bool . eq irreducible(L, empty, RS) = true . ceq irreducible(L, S, RS) = (not isIn(lhs(R), S)) and irreducible(L, S, RS1) if R, RS1 := RS /\ R =/= none /\ S =/= empty . ceq irreducible(L, S, R) = (not isIn(lhs(R), S)) if S =/= empty . eq irreducible(L, S, none) = true . *** first PS == remaining priorities eq irreducible(L, PS, empty, RS) = true . eq irreducible(L, PS, S, none) = true . ceq irreducible(L, PS, S, RS) = if prty(R) == noprty then (not isIn(lhs(R), S)) and irreducible(L, PS, S, RS1) else ((not isIn(lhs(R), S)) or (not (prty(R) in PS))) and irreducible(L, PS, S, RS1) fi if S =/= empty /\ R, RS1 := RS /\ R =/= none . ceq irreducible(L, PS, S, R) = if prty(R) == noprty then (not isIn(lhs(R), S)) else ((not isIn(lhs(R), S)) or (not (prty(R) in PS))) fi if S =/= empty . ---- --- counting the objects ---- op # : Configuration -> Int . op # : Soup -> Int . op # : NeMembraneSet -> Int . eq #({ X:Membrane }) = #(X:Membrane) . eq #(O S) = 1 + #(S) . eq #((empty).Soup) = 0 . eq #(delta) = 0 . eq #(< L | S >) = #(S) . eq #(< L | S ; neM >) = #(S) + #(neM) . eq #((neM1, neM2)) = #(neM1) + #(neM2) . eq #(idle) = 0 . ---- --- counting an object ---- op # : Configuration Obj -> Int . op # : Soup Obj -> Int . op # : NeMembraneSet Obj -> Int . eq #( { < L | S ; neM > }, O ) = #(S, O) + #(neM, O) . eq #( { < L | S > }, O ) = #(S, O) . eq #(idle, O) = 0 . eq #(O S, O') = if O == O' then 1 + #(S, O') else #(S, O') fi . eq #((empty).Soup, O) = 0 . eq #(delta S, O) = #(S, O) . eq #(< L | S >, O) = #(S, O) . eq #(< L | S ; neM >, O) = #(S, O) + #(neM, O) . eq #((neM1, neM2), O) = #(neM1, O) + #(neM2, O) . --- --- defs --- op blue : Membrane -> Membrane? [format (b! o)] . op blue : NeMembraneSet -> NeMembraneSet? [format (b! o)] . op blue : Label Soup Bool -> Soup? [format (b! o)] . op blue : Label PrioritySet Soup Bool -> Soup? [format (b! o)] . op blue : Label Soup -> Soup? [format (b! o)] . op blue : Label PrioritySet Soup -> Soup? [format (b! o)] . op green : Membrane+ -> Membrane? [format (y! o)] . op green : NeMembraneSet+ -> NeMembraneSet? [format (y! o)] . op green : MsgDissSoup -> Soup? [format (y! o)] . op red : Membrane+ -> Membrane? [format (m! o)] . op red : NeMembraneSet+ -> NeMembraneSet? [format (m! o)] . op red : MsgDissSoup -> Soup? [format (m! o)] . op pink : DMembrane -> Membrane? [format (r! o)] . op pink : NeDMembraneSet -> NeMembraneSet? [format (r! o)] . op pink : DissSoup -> Soup? [format (r! o)] . ---- --- firing a transition step ---- crl [1] : { X:Membrane } => { blue(X:Membrane) } if maxSize =/= 0 /\ (#(X:Membrane) < maxSize) . crl [1''] : { X:Membrane } => idle if maxSize =/= 0 /\ (#(X:Membrane) >= maxSize) . crl [1'] : { X:Membrane } => { blue(X:Membrane) } if maxSize == 0 . rl { green(X:Membrane+) } => { red(X:Membrane+) } . rl { green(X:DMembrane) } => { pink(X:DMembrane) } . rl { green(X:Membrane) } => { X:Membrane } . ---- --- applying the evolution rules ---- crl [3] : blue(< L | S ; neM >) => if PS == noprty then (if (freeDeltaRules(L) == none) then < L | blue(L, S) ; blue(neM) > else < L | blue(L, S, false) ; blue(neM) > fi) else (if (freeDeltaRules(L) == none) then < L | blue(L, PS, S) ; blue(neM) > else < L | blue(L, PS, S, false) ; blue(neM) > fi) fi if PS := priorities(rules(L)) . crl [4] : blue(< L | S >) => if PS == noprty then (if (freeDeltaRules(L) == none) then < L | blue(L, S) > else < L | blue(L, S, false) > fi) else (if (freeDeltaRules(L) == none) then < L | blue(L, PS, S) > else < L | blue(L, PS, S, false) > fi) fi if PS := priorities(rules(L)) . crl [5] : blue(neM) => blue(neM1), blue(neM2) if neM1, neM2 := neM . ---- --- if already a delta occured during the first stage a second rule with --- delta in the rhs cannot be applied during the same stage --- we start with false and when a delta occurs it turns intro true --- rules(L, false) == rules(L) --- rules(L, true) == rules(L) \ dissolving rules ---- crl [6'] : blue(L, S, B) => green(rhs(R)) blue(L, S1, B or hasDelta(rhs(R))) if R, RS := rules2(L, B) /\ S2 := lhs(R) /\ S2 S1 := S . crl [6] : blue(L, S) => green(rhs(R)) blue(L, S1) if R, RS := rules(L) /\ S2 := lhs(R) /\ S2 S1 := S . crl [7'] : blue(L, S, B) => green(S) if irreducible(L, S, rules2(L, B)) . crl [7] : blue(L, S) => green(S) if irreducible(L, S, rules(L)) . crl [8'] : blue(L, PS, S, B) => green(rhs(R)) blue(L, rmLower(L, prty(R), PS), S1, B or hasDelta(rhs(R))) if R, RS1 := rules2(L, B) /\ S2 := lhs(R) /\ S2 S1 := S /\ allowed(L, S, R, RS1, PS) . crl [8] : blue(L, PS, S) => green(rhs(R)) blue(L, rmLower(L, prty(R), PS), S1) if R, RS1 := rules(L) /\ S2 := lhs(R) /\ S2 S1 := S /\ allowed(L, S, R, RS1, PS) . crl [9'] : blue(L, PS, S, B) => green(S) if irreducible(L, PS, S, rules2(L, B)) . crl [9] : blue(L, PS, S) => green(S) if irreducible(L, PS, S, rules(L)) . eq < L | green(Smd) >, neM' = green(< L | Smd >), neM' . eq < L1 | S' ; < L | green(Smd) > > = < L1 | S' ; green(< L | Smd >) > . eq { < L | green(Sd) > } = { < L | Sd > } . eq < L | green(Smd) ; green(neM+) > = green(< L | Smd ; neM+ >) . eq green(Smd) green(Smd1) = green(Smd Smd1) . eq green(neM1+), green(neM2+) = green((neM1+, neM2+)) . ---- --- target solving ---- vars neM? neM1? neM2? : NeMembraneSet? . rl red(< L | Smd ; neM+ >) => < L | red(Smd) ; red(neM+) > . rl red(< L | Smd >) => < L | red(Smd) > . rl red(neM1+, neM2+) => red(neM1+), red(neM2+) . --- in-messages crl < L | red(Smd) S? ; neM? > => < L | red(Smd1) S? ; < L1 | green(S) S1? > , neM1? > if Smd1 (S, in(L1)) := Smd /\ < L1 | S1? > , neM1? := neM? . crl < L | red(Smd) S? ; neM? > => < L | red(Smd1) S? ; < L1 | green(S) S1? ; neM1? > , neM2? > if Smd1 (S, in(L1)) := Smd /\ < L1 | S1? ; neM1? > , neM2? := neM? . crl < L | red(Smd) S? ; neM? > => < L | red(Smd1) S? ; < L1 | green(S) S1? > > if Smd1 (S, in(L1)) := Smd /\ < L1 | S1? > := neM? . crl < L | red(Smd) S? ; neM? > => < L | red(Smd1) S? ; < L1 | green(S) S1? ; neM1? > > if Smd1 (S, in(L1)) := Smd /\ < L1 | S1? ; neM1? > := neM? . --- out-messages crl < L | S? ; neM? > => < L | S? green(S) ; < L1 | red(Smd) S1? > , neM1? > if < L1 | red(Smd (S, out)) S1? > , neM1? := neM? . crl < L | S? ; neM? > => < L | S? green(S) ; < L1 | red(Smd) S1? ; neM1? > , neM2? > if < L1 | red(Smd (S, out)) S1? ; neM1? > , neM2? := neM? . crl < L | S? ; neM? > => < L | S? green(S) ; < L1 | red(Smd) S1? > > if < L1 | red(Smd (S, out)) S1? > := neM? . crl < L | S? ; neM? > => < L | S? green(S) ; < L1 | red(Smd) S1? ; neM1? > > if < L1 | red(Smd (S, out)) S1? ; neM1? > := neM? . --- out-messages in the skin membrane crl { < L | red(Smd) S? ; neM? > } => { < L | red(Smd1) S? ; neM? > } if Smd1 (S, out) := Smd . rl red(Sd) => green(Sd) . ---- --- dissolving ---- rl pink(< L | S ; neDM >) => < L | S ; pink(neDM) > . rl pink(neDM1 , neDM2) => pink(neDM1) , pink(neDM2) . rl pink(M) => M . crl < L | S ; neM? > => < L | S S1 ; pink(neDM1) , neM2? > if pink(< L1 | S1 delta ; neDM1 >) , neM2? := neM? . crl < L | S ; neM? > => < L | S S1 ; neM1? > if pink(< L1 | S1 delta >) , neM1? := neM? . crl < L | S ; neM? > => < L | S S1 > if pink(< L1 | S1 delta >) := neM? . crl < L | S ; neM? > => < L | S S1 ; pink(neDM) > if pink(< L1 | S1 delta ; neDM >) := neM? . endm