Maude-help mailing list

[mina ana <touta8 AT live.fr>]

hey every body i wanna sk about the difference between strat & owise & it's utilisability then i have 
fmod SERVICE is         


 sorts Service Services . 


 subsort Service < Services .


 op nils : -> Service [ctor] . 


 op __ : Services Services -> Services [ctor assoc comm id: nils prec 25 ] .


 op _BelongsTo_ : Service Services -> Bool .


 var Ss : Services .


 vars S1 : Service .


 eq  S1 BelongsTo S1 Ss = true .


 eq  S1 BelongsTo Ss = false [owise] .


 endfm 


 


 fmod COMPONENT is                    


 sorts Component Components .


 subsort Component < Components .


 op nilc : -> Component [ctor] . 


 op __ : Components Components -> Components [ctor assoc comm id: nilc  prec 25 ] .


 op _BelongsTo_ : Component Components -> Bool .


 ops C1 CA C-SM POSTFIX  : -> Component [ctor] .


 var Cs : Components .


 vars c1 : Component .


 eq  c1 BelongsTo c1 Cs = true .


 eq  c1 BelongsTo Cs = false [owise] .


 endfm


 ***


 fmod SIMPLE-PREDICATE is


 protecting FLOAT . 


 protecting SERVICE . 


 protecting COMPONENT .


 sorts EnvProp SimplPredicate ComparOper Val .


 subsort Float < Val .


 subsort  Service < SimplPredicate .


 op nilsp : -> SimplPredicate [ctor] .


 op _\/_ : SimplPredicate SimplPredicate -> SimplPredicate [ctor assoc comm id: nilsp prec 27 ] .    


 op `[___`] : EnvProp ComparOper Val -> SimplPredicate [ctor prec 26 ] .


 op notS_ : Service ->  SimplPredicate [ctor prec 26 ] .


 op notC_ : Component ->  SimplPredicate [ctor prec 26 ] .


 op _._ : Component Service ->  SimplPredicate [ctor prec 26 ] .


 ops = : -> ComparOper [ctor] .


 endfm 


  ***


 fmod PREDICATES is 


 protecting SIMPLE-PREDICATE .


 sorts Predicate Predicates  .  


 subsorts SimplPredicate < Predicate .


 subsort Predicate < Predicates .


 op nilpr : -> Predicate [ctor] .


 op True : -> Predicate [ctor] .


 op _/\_ : Predicates Predicates -> Predicates [ctor assoc comm id: nilpr prec 28 ] .


 op FS : Predicates -> Services .


 op FC : Predicates -> Components .


 vars Pdcts1  Pdcts2 : Predicates .


 var s : Service .


 var c : Component .


 var ev : EnvProp .


 var spd1 spd2 : SimplPredicate .


 var co : ComparOper .


 var v : Val .


 eq FS(notS s \/ spd1 /\ Pdcts2  ) = s FS( spd1 /\ Pdcts2) .


 eq FS(Pdcts2) = nils [owise] .


 eq FC(notC c \/ spd1 /\ Pdcts2  ) = c FC( spd1 /\ Pdcts2) .


 eq FC(Pdcts2) = nilc [owise] . 


 endfm


 ***


 fmod INTRA-DEPEND-LANGAGE is


 protecting PREDICATES .


 sorts Dependency Dependencies .


 subsort Dependency < Dependencies .


 op _=>_ : Predicates  Service -> Dependency [ctor prec 29] .


 op _andD_  : Dependencies Dependencies -> Dependencies [ctor comm assoc  prec 30 ] .


 op _orD_ : Dependencies Dependencies -> Dependencies [ctor  comm assoc  prec 30] .


 op  ?_  : Dependencies -> Dependencies [ctor prec 30] .


 endfm


 ***


 fmod ENV-VARS is          


 protecting SIMPLE-PREDICATE .         


 sort EnvVar EnvVars .


 subsort EnvVar < EnvVars . 


 op nilev : -> EnvVar [ctor] .  


 op `(___`) : EnvProp ComparOper Val -> EnvVar [ctor prec 26 ] .


 op __ : EnvVars EnvVars -> EnvVars [ctor assoc comm id: nilev prec 27 ] .


 endfm 


 ***


 fmod INSTALLED-COMPONENTS is         


 protecting INTRA-DEPEND-LANGAGE .


 sorts InstalledC InstalledCs . 


 subsort InstalledC < InstalledCs .


 op <_`,_`,_`,_> : Component Services Services Components -> InstalledC [ctor prec 26] .


 op nilic : ->  InstalledC [ctor] . 


 op __ : InstalledCs InstalledCs -> InstalledCs [ctor assoc comm id: nilic prec 27 ] .


 op ProvidedS : InstalledCs -> Services .


 op InstC : InstalledCs -> Components .


 op ForbiddenS : InstalledCs ->  Services .


 op ForbiddenC : InstalledCs -> Components .


 var C : Component .


 var S : Service .


 var P : Services .


 var F : Services .


 var Cs : Components .


 var I : InstalledCs .


 ***  provided services by intalled components


 eq ProvidedS(nilic) = nils . 


 eq ProvidedS(< C , P , F , Cs > I) =  P ProvidedS(I) . 


 ***   identifiers list of all installed components


 eq InstC(nilic) = nilc .


 eq InstC(< C , P , F , Cs > I) = C InstC(I) .


 *** Forbidden services by intalled components


 eq ForbiddenS(nilic) = nils .


 eq ForbiddenS(< C , P , F , Cs > I) = F ForbiddenS(I) .


 ***  Forbidden components by installed components


 eq ForbiddenC(nilic) = nilc .


 eq ForbiddenC(< C , P , F , Cs > I) = Cs ForbiddenC(I) .


 endfm 


 ***


 fmod DEP-GRAPH is                     


 protecting  COMPONENT .  


 protecting  SERVICE .   


 sorts Label Node Nodes Edge Edges Graph .    


 subsort Node < Nodes .


 subsort Edge < Edges .


 ops M O : -> Label [ctor] .


 op niln : -> Node [ctor] .


 op `(_._`) : Component Service -> Node [ctor prec 25 ] .  


 op __ : Nodes Nodes -> Nodes [ctor assoc comm id: niln prec 26 ] .


 op _in_ : Node Nodes -> Bool .


 op link`(_._._`) : Node Node Label -> Edge [ctor prec 26 ] .


 op nile : -> Edge [ctor] .


 op __ : Edges Edges -> Edges [assoc comm id: nile prec 27 ] . 


 op _in_ : Edge Edges -> Bool .  


 op |_`,_| : Nodes Edges -> Graph [ctor prec 28 ] .


 ops source target : Edge -> Node .    


 op label : Edge -> Label .


 op addN : Graph Nodes -> Graph .


 op addE : Graph Edges -> Graph .


 op allLinks : Node Nodes Label -> Edges .


 vars  e1 e2 : Edge .


 vars n1 n2 : Node .


 vars Ns Ns’ : Nodes .


 vars Es Es’ : Edges .


 var l : Label .


 eq n1 in n1 Ns = true .


 eq n1 in Ns = false [owise] .


 eq e1 in e1 Es = true .


 eq e1 in Es = false [owise] .


 eq source(link( n1 . n2 . l )) = n1 .


 eq target(link( n1 . n2 . l )) = n2 .


 eq label(link( n1 . n2 . l )) = l .


 eq addN(| Ns , Es | , niln) = | Ns , Es | .


 eq addN(| Ns , Es | , n1 Ns’ ) = if not ( n1 in Ns ) then addN(| n1 Ns , Es | , Ns’ ) else addN(| Ns , Es | , Ns’ ) fi .


 eq addE(| Ns , Es | , nile ) = | Ns , Es | .


 eq addE(| Ns , Es | , e1 Es’ ) = if not (e1 in Es) then addE( addN(| Ns , e1 Es | , source(e1) target(e1)), Es’) else addE(| Ns , Es | , Es’ ) fi . 


 eq allLinks( n1, niln, l) = nile .


 eq allLinks( n1, n2 Ns, l) = link( n1 . n2 . l ) allLinks (n1 , Ns, l ) .


 endfm


 fmod CONTEXT is          


 protecting ENV-VARS .   


 protecting INSTALLED-COMPONENTS .         


 protecting DEP-GRAPH .         


 sort Context .


 op ctx`(_`,_`,_`) :  EnvVars InstalledCs Graph -> Context [ctor prec 30 ] .


 op evalDep : Dependencies Context -> Bool .


 op eval : Predicates Context -> Bool .


 vars D1 D2 : Dependencies .


 var S : Service .


 vars CO CO2 : Component .


 var X : Context .


 vars SP1 SP2 : SimplPredicate .


 vars P1 P2 : Predicates .


 vars PS FS : Services .


 var FC : Components .


 var ev : EnvProp .


 var co : ComparOper .


 vars v v’ : Val .


 var E1 : EnvVar .


 var E : EnvVars .


 var IC : InstalledCs .


 var G : Graph .


 eq eval(S , ctx( E , IC , G ))= not ( S BelongsTo ProvidedS(IC) ) .


 eq eval( True , X ) = true .


 eq eval( [ ev = v ] , ctx( ( ev = v’ ) E , IC , G ))= if v == v’ then  true else v < v’ fi .


 eq eval( notS S, ctx(E , IC , G ))=  not( S BelongsTo ProvidedS(IC) ) .


 eq eval( notC CO, ctx(E , IC , G ))=  not( CO BelongsTo InstC(IC) ) .


 eq eval( CO . S , ctx(E , < CO , PS , FS , FC > IC , G ))= S BelongsTo PS .


 eq eval( CO . S , ctx(E , IC , G ))= false [owise] .


 eq eval( SP1 \/ SP2 , X) = eval( SP1 , X ) or eval( SP2 , X ) .


 eq eval( P1 /\ P2 , X) = eval( P1 , X ) and eval( P2 , X ) .


 eq evalDep(P1 => S , X) = eval(P1,X) .

 eq evalDep (? D1 , X ) = true .


 eq evalDep( D1 andD D2 , X) = evalDep( D1 , X) and evalDep(D2 , X) .


 eq evalDep(D1 orD D2 , X) =  evalDep( D1 , X ) or evalDep( D2 , X) .


 endfm


 


 mod CONFIG is          


 protecting CONTEXT .


 sort Declaration .


 sort Configuration .


 subsort Context Declaration < Configuration .


 op _:_ : Component Dependencies -> Declaration [ctor prec 31 ] .


 op nilcnf : -> Configuration [ctor] .


 op __ : Configuration Configuration -> Configuration [ assoc comm id: nilcnf prec 32 ] .


 op PSDep : Dependencies Configuration -> Services .


 op FSDep : Dependencies Context -> Services .


 op FCDep : Dependencies Context -> Components .


 op RSDep : Dependencies Service -> Nodes .


 op modify : Graph Component Dependencies Services -> Graph .


 var C : Component .


 vars D D1 D2 : Dependencies .


 var E : EnvVars .


 var I : InstalledCs .


 var G : Graph .


 var spd1 :  SimplPredicate . 


 vars SS S : Service .


 var Ss : Services .


 vars Q P : Predicates .


 var X : Context .


  *** (Forbidden services by component)


 eq FSDep(P => S, X) = FS(P) .


 eq FSDep(D1 andD D2,X) = FSDep(D1,X) FSDep(D2,X) . 


 eq FSDep(D1 orD D2,X) =  if evalDep(D1,X) then FSDep(D1,X) else  FSDep(D2 , X) fi . 


 eq FSDep(? D1 , X) = nils . *** (Forbidden components by component C) 


 eq FCDep(P => S, X) = FC(P) .


 eq FCDep(D1 andD D2,X) = FCDep(D1, X) FCDep(D2, X) .


 eq FCDep(D1 orD D2, X) = if evalDep(D1, X) then FCDep(D1, X) else FCDep(D2, X) fi  .


 eq FCDep(? D1, X) = nilc .


 *** (provided services of component C)


 eq PSDep(P => S , X) = S .


 eq PSDep(D1 andD D2, X) = PSDep(D1,X) PSDep(D2,X) .


 eq PSDep(D1 orD D2,X) = if  evalDep(D1,X) then PSDep(D1,X) else PSDep(D2,X) fi . 


 eq PSDep(? D1, X) = PSDep(D1 , X) .


 eq RSDep( C . S \/ spd1 /\ P => S , S) = ( C . S ) RSDep( spd1 /\ P => S , S ) .


 eq RSDep( P => S , SS ) = niln [owise] .


 eq RSDep(D1 andD D2, S) = RSDep(D1, S) RSDep(D2,S) .


 eq RSDep(D1 orD D2,S) = RSDep(D1,S) .


 eq RSDep(? D1,S) = RSDep(D1,S) .


 eq modify(G, C, D, nils ) = G . 


 eq modify(G, C, D, S Ss ) =  modify(addE(addN( G , ( C . S ) ), allLinks(( C . S ), RSDep( D , S ) , M )), C, D, Ss ) [owise] .


 rl [install] : ctx( E , I , G ) C : D => if  ( not ( C BelongsTo ForbiddenC(I)) and  evalDep( D , ctx( E , I , G ) )) then ctx( E , < C , PSDep( D , ctx( E , I , G )), FSDep( D , ctx( E , I , G )), FCDep( D , ctx( E , I , G ))>  I, modify(G , C , D , PSDep(D, ctx( E , I , G )))) else ctx( E , I , G ) fi .  


 endm


 


 mod TEST-INSTALL is 


 including CONFIG .


 ops S-lib S-Amavis Smta Sav  : -> Service [ctor] .


 ops FDS OS RAM : -> EnvProp [ctor] .


 ops LINUX : -> Val [ctor] .


 op my-conf : -> Configuration [ctor] .


 eq my-conf = ctx( ( FDS = 5000000.0 ) ( OS = LINUX ) ( RAM = 128.0 )  , < C1 , S-lib , nils , nilc > < CA , S-Amavis , nils , nilc > , | ( C1 . S-lib ) ( CA . S-Amavis ) , nile | ) POSTFIX : [ FDS = 5000000.0 ] /\ notC C-SM  => Smta andD  ? S-Amavis => Sav .


 endm 


mod SUCCESS-INSTALL-CHECKER is
protecting TEST-INSTALL .
including MODEL-CHECKER .
including SATISFACTION . 
subsort Configuration < State .  
vars C : Component .
var P : Prop .
var cnf :  Configuration .
var E : EnvVars .
var I : InstalledCs .
var G : Graph . 
op IsSuccessfullyInstalled : Component -> Prop .
ops initial-conf : -> Configuration .
eq initial-conf = my-conf .
eq ctx(E,I,G) cnf |= IsSuccessfullyInstalled(C) = not(C BelongsTo InstC(I) and C BelongsTo ForbiddenC(I)) .
eq cnf |= P = false [owise] . 
endm

mod SAFETY-INSTALL-CHECKER is
protecting TEST-INSTALL .
including MODEL-CHECKER .
including SATISFACTION . 
 subsort Configuration < State .  
 vars C CC : Component . 
 var S : Service . 
 vars P P1 : Services . 
 vars F F1 : Services .
 vars Cs Css : Components . 
 var I : InstalledCs . 
 var PP : Prop .
 var cnf :  Configuration .
 var E : EnvVars .
 var G : Graph .
 op safety : -> Prop .
ops initial-conf : -> Configuration .
eq initial-conf = my-conf .
 eq ctx( E , < C , P , F , C Cs > I , G ) cnf |= safety = false .
 eq ctx(E , < C , P  , F , Cs > < CC , P1  , F1 , C Css > I , G) cnf |= safety = false .
 eq cnf |= PP = true [owise] .
endm

i wanna write strategy well just for try strategy language on rl [install] : ctx( E , I , G ) C : D => if  ( not ( C BelongsTo 
ForbiddenC(I)) and  evalDep( D , ctx( E , I , G ) )) then ctx( E , < C
 , PSDep( D , ctx( E , I , G )), FSDep( D , ctx( E , I , G )), FCDep( D ,
 ctx( E , I , G ))>  I, modify(G , C , D , PSDep(D, ctx( E , I , G 
)))) else ctx( E , I , G ) fi .

it's about how to instal an component & there's some conditions to install it can you help me to write an simple strategy