*** *** rafqq 05-20-2003 Maude alpha80 *** *** in Maude alpha80: *** load rafall *** rew qraf . mod QQ is inc ALLBP . inc SIMPLE . subsort Dish < State . op qraf : -> Dish . eq qraf = PD( empty {CM | PS PA [Pak1 - act] [PKCz - act] [Src - act] [H-Ras - GTP] { Raf1.domains 14-3-3a 14-3-3b PP2A {NM | empty { empty }}}} ) . op test : -> Enclosure . eq test = {CM | PA {Raf1.domains Src}} . ********************************************************************** *** praf1 is a set of edges which should be true *** these edges first appear after rules 3 when Raf has stuck to *** the cell membrane op praf1 : -> Prop . eq PD( out:Soup {CM | cm:Soup e((Raf1, (S 621)), (14-3-3a,SBD)) e(b(PS),(Raf1, C1 )) e(b(PA),(Raf1, PABM )) e((14-3-3a,DMD ), (14-3-3b,DMD)) {cyto:Soup {NM | nm:Soup {nuc:Soup }}}} ) |= praf1 = true . ***( Maude> red findPath(qraf, praf1) . reduce in QQ : findPath(qraf, praf1) . rewrites: 31 in 0ms cpu (0ms real) (~ rewrites/second) result SimplePath: spath('Raf1#1.PKCz 'Raf#2.PP2A 'Raf#3.PS.PA, PD({CM | PA PS [Pak1 - act] [PKCz - act] [H-Ras - GTP] [Src - act] e(Raf1,C1, b(PS)) e( Raf1,PABM, b(PA)) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [ Raf1 | RBD,(Y 341),(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(S 621 - phos - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A {NM | empty{empty}}}})) ) ********************************************************************** *** praf2 is a set of edges which should not be true *** the first four edges occur when raf is stuck to the CM *** the last edge occurs when raf is bound to 14-3-3 in the cyto op praf2 : -> Prop . eq PD( out:Soup {CM | cm:Soup [H-Ras - GTP] e((Raf1, (S 621)), (14-3-3a,SBD)) e(b(PS),(Raf1, C1 )) e(b(PA),(Raf1, PABM )) e((14-3-3a,DMD ), (14-3-3b,DMD)) e((Raf1, (S 259)), (14-3-3b,SBD)) {cyto:Soup {NM | nm:Soup {nuc:Soup }}}} ) |= praf2 = true . ***( Maude> red findPath(qraf, praf2) . reduce in QQ : findPath(qraf, praf2) . rewrites: 19 in 0ms cpu (0ms real) (~ rewrites/second) result SimplePath: (noPath).SimplePath ) *** praf0 is the property that Raf1 becomse activated at the membrane op praf0 : -> Prop . eq PD( out:Soup {CM | cm:Soup [Raf1 - act] {cyto:Soup}} ) |= praf0 = true . ***( Maude> red findPath(qraf,praf0) . reduce in QQ : findPath(qraf, praf0) . rewrites: 44 in 10ms cpu (10ms real) (4400 rewrites/second) result SimplePath: spath('Raf1#1.PKCz 'Raf1#2.PP2A 'Raf1#3.PS.PA 'Raf1#4.Ras 'Raf1#5.S338phos 'Raf1#6.Y341phos 'Raf1#7.Raf1.is.act, PD({CM | PA PS [Pak1 - act] [PKCz - act] [Raf1 - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}})) ) *** That Raf1 can be activated can also be discovered by simply rewriting *** but this doesn't tell you how. ***( Maude> rew [9] qraf . rewrite [9] in QQ : qraf . rewrites: 9 in 0ms cpu (0ms real) (~ rewrites/second) result Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Raf1 - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) ) *** There are two ways to get to the activated state ***( search qraf =>! D:Dish . Solution 1 (state 8) states: 9 rewrites: 11 in 0ms cpu (0ms real) (~ rewrites/second) D:Dish --> PD({CM | PA PS [Pak1 - act] [PKCz - act] [Raf1 - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) *** There are two transitions from state 4 leading to states 5,6 *** which both have single transitions back to state 7. Maude> show search graph . state 0, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b e(Raf1,S 259, 14-3-3b,SBD) e(Raf1,S 621, 14-3-3a, SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | C1,PABM,RBD,(Y 341),(S 43),(S 338),(S 259 - phos - bound),(S 621 - phos - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | (T 141),(DMD - bound),(SBD - bound)] {NM | empty{empty}}}}) arc 0 ===> state 1 (rl {CM | cm:Soup [PKCz - act]{cyto:Soup e(Raf1,S 259, 14-3-3b,SBD) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | raf1:Atts,(Y 341),(S 43),(S 338),(S 259 - phos - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | (T 141), (DMD - bound),(SBD - bound)]}} => {CM | cm:Soup [PKCz - act]{cyto:Soup ((( e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259 - phos),(S 338),(Y 341),raf1:Atts,(S 621 - phos - bound)]}} [label Raf1#1.PKCz] .) state 1, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | C1,PABM,RBD,(Y 341),(S 43),(S 338),(S 259 - phos),(S 621 - phos - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] {NM | empty{empty}}}}) arc 0 ===> state 2 (rl {CM | cm:Soup{PP2A cyto:Soup e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | raf1:Atts,(Y 341),(S 43),(S 338),(S 259 - phos),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]}} => {CM | cm:Soup{ cyto:Soup PP2A (((e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD)) [ 14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound), 1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(S 338),(Y 341),raf1:Atts,(S 621 - phos - bound)]}} [label Raf1#2.PP2A] .) state 2, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | C1,PABM,RBD,(Y 341),(S 43),(S 259),(S 338),(S 621 - phos - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] {NM | empty{empty}}}}) arc 0 ===> state 3 (rl {CM | PA PS cm:Soup{cyto:Soup e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | C1,PABM,raf1:Atts,(Y 341),(S 43),(S 259),(S 338),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]}} => {CM | cm:Soup PS PA (((((e(b(PA), Raf1,PABM) e(14-3-3a,DMD, 14-3-3b,DMD)) e(b(PS), Raf1, C1)) e(Raf1,S 621, 14-3-3a,SBD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(S 338),(Y 341),(S 621 - phos - bound),(C1 - bound),raf1:Atts,(PABM - bound)]{cyto:Soup}} [label Raf1#3.PS.PA] .) state 3, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [H-Ras - GTP] [Src - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e( 14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | RBD,(Y 341),(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(S 621 - phos - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) arc 0 ===> state 4 (rl {CM | PA PS cm:Soup [?Ras:Ras - GTP] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) [ Raf1 | RBD,raf1:Atts,(Y 341),(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{cyto:Soup}} => {CM | cm:Soup PS PA (((((((e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1, RBD)) e(b(PA), Raf1,PABM)) e(b(PS), Raf1,C1)) e(Raf1,S 621, 14-3-3a,SBD)) [ 14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound), 1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(S 338),(Y 341),(S 621 - phos - bound),(C1 - bound),(PABM - bound),raf1:Atts,(RBD - bound)]) [ ?Ras:Ras | GTPbound,(RafBD - bound)]{cyto:Soup}} [label Raf1#4.Ras] .) state 4, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Src - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(H-Ras,RafBD, Raf1,RBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | (Y 341),(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(RBD - bound),(S 621 - phos - bound)] [ H-Ras | GTPbound,(RafBD - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [ 14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) arc 0 ===> state 5 (rl {CM | PA PS cm:Soup [?Pak:Pak - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) e( ?Ras:Ras,RafBD, Raf1,RBD) [Raf1 | raf1:Atts,(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(RBD - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] [?Ras:Ras | GTPbound,(RafBD - bound)]{cyto:Soup}} => {CM | cm:Soup PS PA ((((((((e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1,RBD)) e(b( PA), Raf1,PABM)) e(b(PS), Raf1,C1)) e(Raf1,S 621, 14-3-3a,SBD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(S 338 - phos),(S 621 - phos - bound),(C1 - bound),(PABM - bound),raf1:Atts,(RBD - bound)]) [?Ras:Ras | GTPbound,(RafBD - bound)]) [?Pak:Pak - act]{cyto:Soup}} [label Raf1#5.S338phos] .) arc 1 ===> state 6 (rl {CM | PA PS cm:Soup [?Slk:Slk - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) e( ?Ras:Ras,RafBD, Raf1,RBD) [Raf1 | raf1:Atts,(Y 341),(S 43),(S 259),(C1 - bound),(PABM - bound),(RBD - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] [?Ras:Ras | GTPbound,(RafBD - bound)]{cyto:Soup}} => {CM | cm:Soup PS PA ((((((((e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1,RBD)) e(b( PA), Raf1,PABM)) e(b(PS), Raf1,C1)) e(Raf1,S 621, 14-3-3a,SBD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(Y 341 - phos),(S 621 - phos - bound),(C1 - bound),(PABM - bound),raf1:Atts,(RBD - bound)]) [?Ras:Ras | GTPbound,(RafBD - bound)]) [?Slk:Slk - act]{cyto:Soup}} [label Raf1#6.Y341phos] .) state 5, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Src - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(H-Ras,RafBD, Raf1,RBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | (Y 341),(S 43),(S 259),(C1 - bound),(PABM - bound),(RBD - bound),(S 338 - phos),(S 621 - phos - bound)] [H-Ras | GTPbound,(RafBD - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) arc 0 ===> state 7 (rl {CM | PA PS cm:Soup [?Slk:Slk - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) e( ?Ras:Ras,RafBD, Raf1,RBD) [Raf1 | raf1:Atts,(Y 341),(S 43),(S 259),(C1 - bound),(PABM - bound),(RBD - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] [?Ras:Ras | GTPbound,(RafBD - bound)]{cyto:Soup}} => {CM | cm:Soup PS PA ((((((((e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1,RBD)) e(b( PA), Raf1,PABM)) e(b(PS), Raf1,C1)) e(Raf1,S 621, 14-3-3a,SBD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(Y 341 - phos),(S 621 - phos - bound),(C1 - bound),(PABM - bound),raf1:Atts,(RBD - bound)]) [?Ras:Ras | GTPbound,(RafBD - bound)]) [?Slk:Slk - act]{cyto:Soup}} [label Raf1#6.Y341phos] .) state 6, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Src - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(H-Ras,RafBD, Raf1,RBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | (S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(RBD - bound),(Y 341 - phos),(S 621 - phos - bound)] [H-Ras | GTPbound,(RafBD - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) arc 0 ===> state 7 (rl {CM | PA PS cm:Soup [?Pak:Pak - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) e( ?Ras:Ras,RafBD, Raf1,RBD) [Raf1 | raf1:Atts,(S 43),(S 259),(S 338),(C1 - bound),(PABM - bound),(RBD - bound),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] [?Ras:Ras | GTPbound,(RafBD - bound)]{cyto:Soup}} => {CM | cm:Soup PS PA ((((((((e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1,RBD)) e(b( PA), Raf1,PABM)) e(b(PS), Raf1,C1)) e(Raf1,S 621, 14-3-3a,SBD)) [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]) [14-3-3a | (SBD - bound),1a:Atts,(DMD - bound)]) [Raf1 | (S 43),(S 259),(S 338 - phos),(S 621 - phos - bound),(C1 - bound),(PABM - bound),raf1:Atts,(RBD - bound)]) [?Ras:Ras | GTPbound,(RafBD - bound)]) [?Pak:Pak - act]{cyto:Soup}} [label Raf1#5.S338phos] .) state 7, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Src - act] e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(H-Ras,RafBD, Raf1,RBD) e(14-3-3a,DMD, 14-3-3b,DMD) [Raf1 | (S 43),(S 259),(C1 - bound),( PABM - bound),(RBD - bound),(Y 341 - phos),(S 338 - phos),(S 621 - phos - bound)] [H-Ras | GTPbound,(RafBD - bound)] [14-3-3a | (DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)]{PP2A 14-3-3a 14-3-3b { NM | empty{empty}}}}) arc 0 ===> state 8 (rl e(b(PA), Raf1,PABM) e(b(PS), Raf1,C1) e(Raf1,S 621, 14-3-3a,SBD) e(14-3-3a,DMD, 14-3-3b,DMD) e(?Ras:Ras,RafBD, Raf1,RBD) [Raf1 | (S 43),(S 259),(C1 - bound),(PABM - bound),(RBD - bound),(Y 341 - phos),( S 338 - phos),(S 621 - phos - bound)] [14-3-3a | 1a:Atts,(DMD - bound),(SBD - bound)] [14-3-3b | SBD,(DMD - bound),(T 141 - phos)] [?Ras:Ras | GTPbound,(RafBD - bound)] => [Raf1 - act] [?Ras:Ras - GTP] [label Raf1#7.Raf1.is.act] .) state 8, Dish: PD({CM | PA PS [Pak1 - act] [PKCz - act] [Raf1 - act] [H-Ras - GTP] [Src - act]{PP2A 14-3-3a 14-3-3b {NM | empty{empty}}}}) ) ********************************************************************** endm