********************************************************************* *** Prototyping SOS in Maude *** *** Send comments and report bugs to: *** m.r.mousavi @ tue.nl *** *** The paper about this implementation is available at: *** http://www.win.tue.nl/~mousavi/sos05-meta-theory.pdf ********************************************************************** ********************************************************************** *** Changes log: *** CONS-Chk now takes 3 parameters *** CONS-Chk ( ExtendedTSS:TSS , *** ExtendingTSSModule:Qid , *** ExtendingTSS: TSS ) *** For compatibility reasons the version with 4 parameters is kept and *** the first two parameters are disregarded ********************************************************************** ************************* *** Abstract Terms * ************************* fmod States is pr NAT . sorts CT T . sorts FV FVSet . subsorts CT FV < T . ops X-_ Y-_ : Nat -> FV [ctor prec 1] . subsort FV < FVSet . op emFV : -> FVSet [ctor] . op _ , _ : FVSet FVSet -> FVSet [ctor comm assoc id: emFV] . op vars ( _ ) : T -> FVSet . op _ disjoint _ : FVSet FVSet -> Bool . op redundant ( _ ) : FVSet -> Bool . op toSet ( _ ) : FVSet -> FVSet . op _ subset _ : FVSet FVSet -> Bool . var v : FV . var vset vsetp : FVSet . eq vars ( v ) = v . eq ( v , vset ) disjoint ( v , vsetp ) = false . eq vset disjoint vsetp = true [owise] . eq redundant ( v , v , vset ) = true . eq redundant ( vset ) = false [owise] . eq toSet ( v , v , vset ) = toSet ( v , vset ) . eq toSet ( vset ) = vset [owise] . eq vset subset ( vset , vsetp ) = true . eq vset subset vsetp = false [owise] . endfm ************************* *** Substitutions * ************************* fmod Substitutions is inc States . sorts NESbst Sbst SbstErr . subsort NESbst < Sbst < SbstErr . op emSbst : -> Sbst [ctor] . op errSbst : -> SbstErr [ctor] . op _ |-> _ : FV T -> NESbst [ctor] . op _ , _ : [Sbst] [Sbst] -> [Sbst] [comm assoc id: emSbst] . op _ ( _ ) : Sbst T -> T . var s t sp : T . var sigma sigmap : Sbst . var nesigma : NESbst . var v vp : FV . eq ( errSbst, nesigma ) = errSbst . eq ( (v |-> s) , (v |-> s) ) = (v |-> s) . ceq ( (v |-> s) , (v |-> sp) ) = errSbst if ( s =/= sp ) . cmb ( ( v |-> s ) , nesigma ) : Sbst if nesigma :: Sbst . eq ( emSbst ( s ) ) = s . eq ( ( ( v |-> s ) , sigma ) ( v ) ) = s . eq ( ( ( v |-> s ) , sigma ) ( vp ) ) = vp [owise] . endfm ****************************** *** Abstract Term Matching * ****************************** fmod Term-Match is inc Substitutions . var s t sp tp : T . var v : FV . op match ( _ , _ ) : T T -> [Sbst] . eq match ( v , s ) = ( v |-> s ) . eq match ( s , s ) = emSbst [owise] . endfm ************************************************ *** Transition System Specifications (TSS's) * ************************************************ fmod TSS-Definition is inc States . sorts Labels LabelSet . subsort Labels < LabelSet . sorts Fr NFr PFr IPFr FrSet . sorts Rl TSS . subsorts NFr PFr IPFr < Fr < FrSet . subsorts Rl < TSS . op emLabel : -> LabelSet [ctor] . op _ , _ : LabelSet LabelSet -> LabelSet [ctor comm assoc id: emLabel ] . op _ ==_==> _ : T Labels T -> PFr [prec 97]. op _ ==_==> : T Labels -> IPFr [prec 97]. op _ ==_=/=> : T Labels -> NFr [prec 97]. op source ( _ ) : Fr -> T . op target ( _ ) : PFr -> T . op _ subset _ : TSS TSS -> Bool . op emFr : -> FrSet [ctor] . op _ , _ : FrSet FrSet -> FrSet [ctor comm assoc id: emFr prec 99] . op _ === _ : FrSet PFr -> Rl [ctor prec 100 ] . op === _ : PFr -> Rl [ prec 101 ] . op posLabels ( _ ) : FrSet -> LabelSet . op targetVars ( _ ) : FrSet -> FVSet . op sourceVars ( _ ) : PFr -> FVSet . op prem(_) : Rl -> FrSet . op conc(_) : Rl -> PFr . op _ , _ : TSS TSS -> TSS [ctor comm assoc prec 101] . op source _ : Rl -> T . var frset : FrSet . var pfr : PFr . var fr : Fr . var s sp t tp : T . var l : Labels . var lset : LabelSet . var tss tssp : TSS . eq prem(frset === pfr) = frset . eq conc(frset === pfr) = pfr . eq posLabels ( emFr ) = emLabel . eq posLabels ( s == l ==> sp ) = l . eq posLabels ( s == l =/=> ) = emLabel . eq posLabels ( s == l ==> ) = emLabel . ceq posLabels ( fr , frset ) = ( posLabels ( fr ) , posLabels ( frset ) ) if frset =/= emFr . eq targetVars ( emFr ) = emFV . eq targetVars ( s == l ==> t ) = vars ( t ) . eq targetVars ( s == l =/=> ) = emFV . eq targetVars ( s == l ==> ) = emFV . ceq targetVars ( fr , frset ) = ( targetVars ( fr ) , targetVars ( frset ) ) if frset =/= emFr . eq sourceVars ( s == l ==> t ) = vars ( s ) . eq source ( s == l ==> sp ) = s . eq target ( s == l ==> sp ) = sp . eq ( === pfr ) = ( emFr === pfr ) . eq source ( frset === pfr ) = source ( pfr ) . eq tss subset ( tss , tssp ) = true . eq tss subset tssp = false [owise] . endfm ****************************** *** Minimal Process Algebra * ****************************** fmod MPA-TSS is inc Term-Match . inc TSS-Definition . sort BAct . subsort BAct < Labels . *** MPA Signature ops delta : -> T [ctor] . op ft ( _ ) : T -> T [ctor] . op _ ; _ : BAct T -> T [ctor prec 2]. op _ + _ : T T -> T [ctor prec 3] . *** Substitutions and Matching ops a b : -> BAct [ctor] . var act : BAct . var sigma : Sbst . vars s t sp tp : T . eq sigma ( delta ) = delta . eq sigma ( act ; s ) = act ; ( sigma ( s ) ) . eq sigma ( s + t ) = ( ( sigma ( s ) ) + ( sigma ( t ) ) ) . eq match ( ( s + t ) , ( sp + tp ) ) = ( match ( s, sp ) , match ( t, tp ) ) . eq match ( ( act ; s ) , ( act ; t ) ) = match ( s, t ) . eq vars ( delta ) = emFV . eq vars ( act ; s ) = vars ( s ) . eq vars ( s + t ) = ( vars ( s ) , vars ( t ) ) . ops MPA : -> TSS . eq MPA = ( === a ; X- 0 == a ==> X- 0 ) , ( X- 0 == a ==> Y- 0 === X- 0 + X- 1 == a ==> Y- 0 ) , ( X- 1 == a ==> Y- 1 === X- 0 + X- 1 == a ==> Y- 1 ) . op Test : -> TSS . eq Test = ( === ( ft ( delta ) ) == a ==> delta ) . endfm **************************************** *** Minimal Process Algebra with Time * **************************************** fmod MPAT-TSS is inc MPA-TSS . op tick : -> Labels [ctor] . *** MPA Signature op delay ; _ : T -> T [ctor prec 2] . *** Substitutions and Matching var sigma : Sbst . var s : T . eq sigma ( delay ; s ) = delay ; ( sigma ( s ) ) . op MPAT : -> TSS . eq MPAT = ( MPA , ( === delay ; X- 0 == tick ==> X- 0 ) , ( ( X- 0 == tick ==> Y- 0 , X- 1 == tick ==> Y- 1 ) === X- 0 + X- 1 == tick ==> Y- 0 + Y- 1 ) , ( ( X- 0 == tick ==> Y- 1 , X- 1 == tick =/=> ) === X- 0 + X- 1 == tick ==> Y- 0 ) , ( ( X- 0 == tick ==> Y- 0 , X- 1 == tick ==> Y- 1 ) === X- 1 + X- 0 == tick ==> Y- 0 + Y- 1 ) ) . endfm ************************* *** Formula Matching * ************************* fmod Formula-Match is pr MPAT-TSS . op _ (_) : Sbst Fr -> Fr . op _ (_) : Sbst FrSet -> FrSet . op match( _, _ ) : Fr Fr -> [Sbst] . var s sp t tp : T . var l : Labels . var sigma : Sbst . var frst : FrSet . var fr : Fr . eq sigma ( s == l ==> ) = ( ( sigma ( s ) ) == l ==> ) . eq sigma ( s == l ==> sp ) = ( ( sigma ( s ) ) == l ==> ( sigma ( sp ) ) ) . eq sigma ( s == l =/=> ) = ( ( sigma ( s ) ) == l =/=> ) . eq sigma ( emFr ) = emFr . eq sigma ( fr , frst ) = ( sigma ( fr ) , sigma ( frst ) ) . eq match ( ( s == l ==> sp ) , ( t == l ==> tp ) ) = ( match ( s, t ) , match ( t, tp ) ) . eq match ( ( s == l =/=> ) , ( t == l =/=> ) ) = match ( s, t ) . eq match ( ( s == l ==> ) , ( t == l ==> ) ) = match ( s, t ) . eq match ( ( s == l ==> sp ) , ( t == l ==> ) ) = match ( s, t ) . endfm fmod QID-Set is pr QID . sort QidSet . subsort Qid < QidSet . op emQid : -> QidSet [ctor] . op _ comma _ : QidSet QidSet -> QidSet [ctor comm assoc id: emQid] . op _ setminus _ : QidSet QidSet -> QidSet . op _ in _ : Qid QidSet -> Bool . var qid qidp : Qid . var qidset qidsetp : QidSet . eq qid comma qid = qid . eq qid in ( qid comma qidset ) = true . eq qid in qidset = false [owise] . eq (qid comma qidset) setminus (qid comma qidsetp) = (qidset setminus qidsetp) . eq qidset setminus qidsetp = qidset [owise] . endfm ************************************ *** Operations on Metalevel Terms * ************************************ fmod OP-Ext is pr NAT . pr QID-Set . inc META-LEVEL . ********************************************************************* **** extractOpNames ( module sort bool ) extracts **** operator names in module with the target sort **** depending on bool, it would extract the operations in the included **** modules or not ********************************************************************* op extractOpNames ( _ _ _ ) : Qid Qid Bool -> QidSet . ********************************************************************* **** opsToNames ( ops sort ) takes the list of operator declarations **** with target sort **** and converts it into a set of Qid's ********************************************************************* op opsToNames ( _ _ ) : OpDeclSet Qid -> QidSet . ********************************************************************* *** trmToQidList ( term ) extracts the list of Qid's in a term ********************************************************************* op trmToQidList(_) : Term -> QidList . ********************************************************************* **** trmToQidList ( qidlist qidset ) **** counts the number of elements from qidset appearing in qidlist ********************************************************************* op countCommonOps ( _ , _ ) : QidList QidSet -> Nat . var opdecl : OpDecl . var opdeclst : OpDeclSet . var opnames qidset : QidSet . var modname opname sortname : Qid . var qid qidp : Qid . var qidlist : QidList . var bool : Bool . var trm : Term . var trmlist trmlistp : TermList . var xvar : Variable . var xconst : Constant . eq extractOpNames ( modname sortname bool ) = opsToNames ( getOps ( upModule ( modname , bool ) ) sortname ) . eq opsToNames ( none sortname ) = emQid . ceq opsToNames ( opdecl sortname ) = opname if op opname : (typlist:TypeList) -> sortname [attrst:AttrSet]. := opdecl . eq opsToNames ( opdecl sortname ) = emQid [owise] . eq opsToNames ( ( opdecl opdeclst ) sortname ) = ( opsToNames ( opdecl sortname ) comma opsToNames ( opdeclst sortname ) ) [owise] . eq trmToQidList(xvar) = xvar . eq trmToQidList(xconst) = getName(xconst) . eq trmToQidList(opname [ trmlist ]) = ( opname trmToQidList(trmlist) ) . eq trmToQidList( trmlist , trmlistp) = ( trmToQidList(trmlist) trmToQidList(trmlistp) ) . eq countCommonOps ( ( qid qidlist ) , ( qid comma qidset ) ) = ( 1 + countCommonOps ( qidlist , ( qid comma qidset ) ) ) . ceq countCommonOps ( ( qid qidlist ) , qidset ) = ( countCommonOps ( qidlist , qidset ) ) if ( not ( qid in qidset ) ) . eq countCommonOps ( nil , qidset ) = 0 . endfm ********************************** *** Error and Success Messages *** ********************************** fmod MESSAGES is pr STRING . pr Formula-Match . sort Message . op successmsg ( _ ) : String -> Message [ctor format (d n gi o n)]. op errormsg ( _ , _ , _ ) : String Rl String -> Message [ctor format (d d n d nr o n d o) ] . op errormsg ( _ ) : String -> Message [ctor format (d d nir d o)]. endfm *************************************** *** Checking Congruence Meta-Theorem * *************************************** fmod GSOS-Check is pr OP-Ext . pr MESSAGES . op GSOS-Chk ( _ , _ ) : Qid TSS -> Message . op fsource ( _ _ , _ ) : Qid Rl QidSet -> Bool . op disjointVars ( _ ) : Rl -> Bool . var modname : Qid . var rl : Rl . var qidset : QidSet . var tss : TSS . eq fsource ( modname rl , qidset ) = ( countCommonOps ( trmToQidList ( getTerm ( metaReduce ( upModule ( modname , false ) , upTerm ( ( source ( rl ) ) ) ) ) ) , qidset ) <= 1 ) . eq disjointVars ( rl ) = ( targetVars ( prem ( rl ) ) disjoint sourceVars ( conc ( rl ) ) ) . ceq GSOS-Chk ( modname , rl ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has more than one operator in its source of conclusion.") if ( not ( fsource ( modname rl, extractOpNames ( modname 'T false ) ) ) ) . ceq GSOS-Chk ( modname , rl ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has a source variable in the target of premises." ) if ( not ( disjointVars ( rl ) ) ) . ceq GSOS-Chk ( modname , ( rl, tss ) ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has a source variable in the target of premises." ) if ( not ( disjointVars ( rl ) ) ) . ceq GSOS-Chk ( modname , ( rl, tss ) ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has more than one operator in its source of conclusion.") if not ( fsource ( modname rl, extractOpNames ( modname 'T false ) ) ) . ceq GSOS-Chk ( modname , ( rl, tss ) ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has non distinct variables as the target of premises.") if redundant ( targetVars ( prem ( rl ) ) ) . ceq GSOS-Chk ( modname , ( rl, tss ) ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has non distinct variables as the source of conclusion.") if redundant ( sourceVars ( conc ( rl ) ) ) . ceq GSOS-Chk ( modname , rl ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has non distinct variables as the target of premises.") if redundant ( targetVars ( prem ( rl ) ) ) . ceq GSOS-Chk ( modname , rl ) = errormsg ( "GSOS-Check: Error, the following rule:" , rl, "has non distinct variables as the source of conclusion.") if redundant ( sourceVars ( conc ( rl ) ) ) . eq GSOS-Chk ( modname , tss ) = successmsg ( "GSOS-Check: TSS conforms to GSOS." ) [owise] . endfm ******************************************************* *** Checking Operational Conservativity Meta-Theorem * ******************************************************* fmod CONSV-Check is pr OP-Ext . pr MESSAGES . op Cons-Chk ( _ , _ , _ , _ ) : Qid TSS Qid TSS -> Message . op Cons-Chk ( _ , _ , _ ) : TSS Qid TSS -> Message . op freshRule ( _ , _ ) : Qid Rl -> Bool . var modname modnamep : Qid . var tss tssp : TSS . var rl rlp : Rl . var l : Labels . var lset : LabelSet . eq Cons-Chk ( modname , tss , modnamep, tssp ) = Cons-Chk ( tss , modnamep , tssp ) . ceq freshRule ( modname , rl ) = true if ( l , lset ) := posLabels ( prem ( rl ) ) /\ ( countCommonOps ( trmToQidList ( upTerm ( l ) ) , extractOpNames ( modname 'Labels false ) ) >= 1 ) . ceq freshRule ( modname , rl ) = true if ( countCommonOps ( trmToQidList ( getTerm ( metaReduce ( upModule ( modname , false ) , upTerm ( ( source ( rl ) ) ) ) ) ) , extractOpNames ( modname 'T false ) ) >= 1 ) . eq freshRule ( modname , rl ) = false [owise] . ceq Cons-Chk ( tss , modname , rl ) = errormsg ( "CONS-Check: Error, the following rule:" , rl, "does not have fresh label or function symbol. " ) if ( not ( freshRule ( modname , rl ) ) ) . ceq Cons-Chk ( tss , modname , ( rl , tss ) ) = errormsg ( "CONS-Check: Error, the following rule:" , rl, "does not have fresh label or function symbol. " ) if ( not ( freshRule ( modname , rl ) ) ) . ceq Cons-Chk ( tss , modname , tssp ) = errormsg ( "CONS-Check: The extended TSS is not a subset of the extending one.") if ( not ( tss subset tssp ) ) . ceq Cons-Chk ( tss , modname , tssp ) = errormsg ( "CONS-Check: The extended TSS is not source preserving.") if ( not ( tss subset tssp ) ) . eq Cons-Chk ( tss , modname , tssp ) = successmsg ( "CONS-Check: Operational conservativity theorem checked successfully." ) [owise] . endfm ********************* *** Animating TSS's * ********************* mod TSS-Animation is pr Formula-Match . sorts TransConfs TransConf . subsorts Sbst < TransConfs . subsorts T < TransConf . op _ |- _ : TSS IPFr -> TransConf [prec 110]. op _ ||- _ : TSS FrSet -> TransConfs [prec 110]. var frst frstp : FrSet . var s sp : T . var tss tssp : TSS . var sigma rho : Sbst . var l : Labels . var fr : Fr . var rule : Rl . var y : FV . crl ( tss |- ( s == l ==> ) ) => ( ( sigma, rho ) ( target ( conc ( rule ) ) ) ) if ( rule , tssp ) := tss /\ sigma := match ( conc ( rule ) , ( s == l ==> ) ) /\ ( tss ||- ( sigma ( prem( rule ) ) ) ) => rho /\ ( ( sigma , rho ) :: Sbst ) . crl ( tss ||- frst ) => ( rho, sigma ) if ( fr, frstp ) := frst /\ ( frstp =/= emFr ) /\ ( tss ||- fr ) => rho /\ ( tss ||- frstp ) => sigma . rl (tss ||- emFr) => emSbst . crl ( tss ||- ( s == l ==> y ) ) => (y |-> sp) if ( tss |- ( s == l ==> ) ) => sp . crl ( tss ||- (s == l ==> ) ) => (emSbst) if ( tss |- ( s == l ==> ) ) => sp . inc META-LEVEL . var possible? : ResultPair? . crl ( tss ||- (s == l =/=> ) ) => ( emSbst ) if possible? := metaRewrite( ['TSS-Animation], upTerm( ( tss |- ( s == l ==> ) ) ) , 1 ) /\ (possible? :: ResultPair ) . endm