***************************************************************************************
***State:   A translator for OTS specifications to Maude at meta-level
***Author:  Min Zhang
***Version: 1.2
***Date:    2009/04/05
***Place:   JAIST
***************************************************************************************
***(
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 inclof the License, or
  (at your option) any later version.
		
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNSS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.
		
You should have received a copy of the GNU General Public Leicense
along with this program; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
		
		
******************************************************
***predefined modules 
******************************************************
***for HS
fmod STATE is 
	sort OTSState .
		
endfm
		
***for ES
fmod STATE-ES is
	sorts OValue OTSState .
	subsort OValue < OTSState .
	
	op nil : -> OTSState .
	op __ : OTSState OTSState -> OTSState [assoc comm id: nil format(o nt o)] .
		
endfm 
		
*****************************************************
***for translation
*****************************************************

fmod OTS-BUBBLES is
  including QID-LIST .
***  sorts @HiddenSortToken@ @VisibleSortToken@ .
  sorts @OTSBubble@ @OTSToken@ @NeOTSTokenList@ @OTSSortToken@ .

  op otsBubble : QidList -> @OTSBubble@ [special (id-hook Bubble (1 -1 `( `)) 
                                                  op-hook qidListSymbol (__ : QidList QidList ~> QidList)
                                                  op-hook qidSymbol (<Qids> : ~> Qid))] .
  
  op neOTSTokenList : QidList -> @NeOTSTokenList@ [special (id-hook Bubble (1 -1) 
                                                            op-hook qidListSymbol (__ : QidList QidList ~> QidList)
                                                            op-hook qidSymbol (<Qids> : ~> Qid)
                                                            id-hook Exclude(. { } ))] .  

  op otsToken : Qid -> @OTSToken@ [special (id-hook Bubble (1 1) 
                                            op-hook qidSymbol (<Qids> : ~> Qid)
                                            id-hook Exclude(. < { } ( )))] . 
                                
endfm


fmod OTS-COMMANDS is
  including COMMANDS .
  
      op conv2maude`. : -> @Command@ .
endfm

fmod OTS-OP-ATTRIBUTES is
   protecting OTS-BUBBLES .
   sorts @CafeAttr@ @CafeAttrList@ .
   subsorts @CafeAttr@ < @CafeAttrList@ .
  
   op __ : @CafeAttrList@ @CafeAttrList@ -> @CafeAttrList@ [assoc] .
   ops assoc comm constr  : -> @CafeAttr@ .
   op id:_ : @OTSBubble@ -> @CafeAttr@ .
 
endfm


fmod OTS-META-SIGN is
     *** including F&S-MODS&THS .
     *** including OTS-BUBBLES .
     including OTS-COMMANDS .
     including FULL-MAUDE-SIGN .
     including OTS-OP-ATTRIBUTES .

     sorts @OTS-MODULE@ @OTSDecl@ @HiddenSortDecl@ @VisibleSortList@ @VisibleSortDecl@ @OTSOpDecl@ @OTSImportDecl@ @OTSType@ @OTSTypeList@  @OTSSortList@ @OTSSort@ @InitialDecl@ @BehaviorEquationDecl@ @OTSDeclList@ @OTSEqDecl@ @OTSVarDecl@ @OTSSubSortRel@ @OTSLDeclList@  .

     subsort @OTSToken@ < @OTSSort@ < @OTSType@ .
     subsort @OTSSort@ < @OTSSortList@ .
     subsort @OTSType@ < @OTSTypeList@ .
     subsorts @OTSImportDecl@ @OTSVarDecl@ @OTSEqDecl@  @VisibleSortDecl@ @OTSOpDecl@ < @OTSLDeclList@ .
     subsorts  @OTSDecl@  @HiddenSortDecl@ @BehaviorEquationDecl@ @OTSLDeclList@ < @OTSDeclList@ .

     op __ : @OTSDeclList@ @OTSDeclList@ -> @OTSDeclList@ [assoc] .
     op __ : @OTSLDeclList@ @OTSLDeclList@ -> @OTSLDeclList@ [assoc] .
     op __ : @VisibleSortList@ @VisibleSortList@ -> @VisibleSortList@ [assoc] .
     op __ : @OTSTypeList@ @OTSTypeList@ -> @OTSTypeList@ [assoc] .
          
     *** hidden sort declaration
     op *`[_`]* : @OTSToken@ -> @HiddenSortDecl@ .
     op pr`(_`) : @OTSToken@ -> @OTSImportDecl@ [ctor] .
     op inc`(_`) : @OTSToken@ -> @OTSImportDecl@ [ctor] .
     
     op `[_`] : @OTSSortList@ -> @VisibleSortDecl@ .
     op `[_`] : @OTSSubSortRel@ -> @VisibleSortDecl@ .
     
     op _<_ : @OTSSortList@ @OTSSortList@ -> @OTSSubSortRel@ .
     op _<_ : @OTSSortList@ @OTSSubSortRel@ -> @OTSSubSortRel@ .

     op var_:_. : @NeOTSTokenList@ @OTSType@ -> @OTSVarDecl@ .
     op vars_:_. : @NeOTSTokenList@ @OTSType@ -> @OTSVarDecl@ .
     
     op eq_=_. : @OTSBubble@ @OTSBubble@ -> @OTSEqDecl@ .
     op ceq_=_if_. : @OTSBubble@ @OTSBubble@ @OTSBubble@ -> @OTSEqDecl@ .
 
     *** 4.3
     op op_:`->_`{_`}. : @OTSToken@ @OTSType@ @CafeAttrList@ -> @OTSOpDecl@ .
     op op_:_->_`{_`}. : @OTSToken@ @OTSTypeList@ @OTSSort@ @CafeAttrList@  -> @OTSOpDecl@ .     
     op op_:`->_. : @OTSToken@ @OTSType@ -> @OTSOpDecl@ .
     op op_:_->_. : @OTSToken@ @OTSTypeList@ @OTSType@ -> @OTSOpDecl@ .     
     op ops_:`->_`{_`}. : @NeOTSTokenList@ @OTSType@ @CafeAttrList@ -> @OTSOpDecl@ .
     op ops_:_->_`{_`}. : @NeOTSTokenList@ @OTSTypeList@ @OTSType@ @CafeAttrList@  -> @OTSOpDecl@ .     
     op ops_:`->_. : @NeOTSTokenList@ @OTSType@ -> @OTSOpDecl@ .
     op ops_:_->_. : @NeOTSTokenList@ @OTSTypeList@ @OTSType@  -> @OTSOpDecl@ .     
     
     ***observer declaration
     op bop_:_->_. : @OTSToken@ @OTSTypeList@ @OTSSort@  -> @OTSOpDecl@  .
     op bops_:_->_. : @NeOTSTokenList@ @OTSTypeList@ @OTSSort@ -> @OTSOpDecl@ .
     op bop_:_->_`{_`}. : @OTSToken@ @OTSTypeList@ @OTSSort@ @CafeAttrList@  -> @OTSOpDecl@ .     
     op bops_:_->_`{_`}. : @NeOTSTokenList@ @OTSTypeList@ @OTSType@ @CafeAttrList@  -> @OTSOpDecl@ .
     op bceq_=_if_. : @OTSBubble@ @OTSBubble@ @OTSBubble@ -> @BehaviorEquationDecl@  .


     op mod*_`{_`} : @OTSToken@ @OTSDeclList@ -> @OTS-MODULE@ .
     op mod!_`{_`} : @OTSToken@ @OTSLDeclList@ -> @OTS-MODULE@ .

     subsort @OTS-MODULE@ < @Input@ .     
endfm


fmod OTS-SIGN is
  including EXT-SORT .
  
  sorts HiddenSortDecl OTSDecl OTSDeclSet BehaviorEquation OTSEquation OTSEquationSet OTSOpDecl OTSOpDeclSet .

  subsort BehaviorEquation OTSEquation < OTSEquationSet .
  subsort OTSOpDecl < OTSOpDeclSet .
  subsort OTSDecl < OTSDeclSet .
  sort OTSModule .
   
  op *`[_`]* : Sort -> HiddenSortDecl .
  op (bop_:_->_) : Qid TypeList Type -> OTSDecl [ctor format(g o g o g o o )] .
  op (bops_:_->_) : QidList TypeList Type -> OTSDecl [ctor format(g o g o g o o )] .
  op none : -> OTSDeclSet [ctor] .
  op __ : OTSDeclSet OTSDeclSet -> OTSDeclSet [ctor assoc comm id: none format(d ni d)] .
  op none : -> OTSEquationSet [ctor] .
  op __ : OTSEquationSet OTSEquationSet -> OTSEquationSet [ctor assoc comm id: none format(d ni d)] .
   op none : -> OTSOpDeclSet [ctor] .
  op __ : OTSOpDeclSet OTSOpDeclSet -> OTSOpDeclSet [ctor assoc comm id: none format(d ni d)] .
  
  op op_:_->_ : Qid TypeList Type -> OTSOpDecl [ctor format(g o g o g o o )] .
  op eq_=_. : Term Term -> OTSEquation [ctor format(g o g o g o )] .
  op ceq_=_if_. : Term Term EqCondition -> OTSEquation [ctor format(g o g o g o o o )] .
  op bceq_=_if_. : Term Term EqCondition -> BehaviorEquation [ctor format(g o g o g o o o)] .
  op pr`(_`) : ModuleExpression -> Import [ctor] .
  op inc`(_`) : ModuleExpression -> Import [ctor] .
  op none : -> HiddenSortDecl [ctor] .
  op mod*_`{_____`} : Header ImportList HiddenSortDecl OTSOpDeclSet OTSDeclSet OTSEquationSet -> OTSModule 
                       [ctor gather(& & & & & &) format(d d s n++i ni d d ni n--i d)] .
  op emptyOTSModule : -> OTSModule .
endfm


fmod OPERATOR-OTS is
  including OTS-SIGN .
  including UNIT .
  including META-LEVEL .
  
  sorts Bop2op .
  sorts Bop2opList .
  sorts DoubleResultPair .
  sorts TypeConstants TypeConstantsList .
  sorts Combine4TupleResult RuleConditionPair .
  sorts MetaTermTriple .
  sorts MetaTermTripleSet .
  subsorts Bop2op < Bop2opList .
  subsorts TypeConstants < TypeConstantsList .
  subsorts MetaTermTriple < MetaTermTripleSet .
  
  op `[_;_`] : OTSDecl OpDecl -> Bop2op [ctor format (o o r o o o)] .
  op nil : -> Bop2opList [ctor] .
  op __ : Bop2opList Bop2opList -> Bop2opList [assoc comm id: nil ctor prec 121 gather (e E)] .
  op <_;_> : Bop2opList SModule -> DoubleResultPair [ctor] .
  op getBOP2OP : [Bop2opList] [Qid] -> [Bop2op] .
  op getBOP : Bop2op -> Qid .
  op getOP : Bop2op -> Qid .
  op getObvdType : Bop2op -> Type .
  op getTransitions : OTSDeclSet -> OTSDeclSet .
  op getHiddenSortDecl : OTSModule -> HiddenSortDecl .
  op getOTSDeclSet : OTSModule -> OTSDeclSet .
  op getSort : HiddenSortDecl -> Sort .
  op getName : OTSModule -> Header .
  op getImports : OTSModule -> ImportList .
  op getSorts : OTSModule -> SortSet .
  op getEqs : OTSModule -> OTSEquationSet .
  op getPars : OTSModule -> ParameterDeclList .
  op getOps : OTSModule -> OTSOpDeclSet .
  op getInitialState : OTSModule -> Constant .
  op getConditionOps : OTSModule -> QidList .
  op getConditionOpsAux : OTSOpDeclSet Type -> QidList .
  op setHiddenSortDecl : OTSModule HiddenSortDecl -> OTSModule .
  op setOTSDeclSet : OTSModule OTSDeclSet -> OTSModule .
  op setName : OTSModule Header -> OTSModule .
  op setImports : OTSModule ImportList -> OTSModule .
  op setOps : OTSModule OTSOpDeclSet -> OTSModule .
  op setEqs : OTSModule OTSEquationSet -> OTSModule .
  op setPars : OTSModule ParameterDeclList -> OTSModule .
  op setSubsorts : OTSModule SubsortDeclSet -> OTSModule .
  op setSorts : OTSModule SortSet -> OTSModule .
  op addHiddenSortDecl : HiddenSortDecl OTSModule -> OTSModule .
  op addOTSDeclSet : OTSDeclSet OTSModule -> OTSModule .
  op addImports : ImportList OTSModule -> OTSModule .
  op addEqs : OTSEquationSet OTSModule -> OTSModule .
  op addSorts : SortSet OTSModule -> OTSModule .
  op addOps : OTSOpDeclSet OTSModule -> OTSModule .
  op empty : OTSModule -> OTSModule .
  
  vars H H' 						: Header .
  vars IL IL' 						: ImportList .
  vars HSD HSD' 				: HiddenSortDecl .
  vars OTSOPDS OTSOPDS' 			: OTSOpDeclSet .
  vars OPDS OPDS' 			: OpDeclSet .
  vars OTSDS OTSDS' 		: OTSDeclSet .
  vars EqS EqS' EqCS 		: EquationSet .
  vars OTSEqS	OTSEqS'	: OTSEquationSet .
  var SS 							: SortSet .
  vars S HS 						: Sort .
  var RIS? 							: [RuleSet] .
  vars U OTSM 					: OTSModule .
  vars U' U'' M			 		: Module .
  var ME' 							: ModuleExpression .
  var PDL 							: ParameterDeclList .
  var MAS 							: MembAxSet .
  var SSDS 						: SubsortDeclSet .
  var FM 							: FModule .
  vars OPS QL CS CS' 		: QidList .
  vars TCL TCL' 					: TypeConstantsList .
  var GTL 							: GroundTermList .
  vars TL TL' TL'' 				: TermList .
  vars T T' T'' T3 				: Term .
  vars Attr AttrS AttrS' 		: AttrSet .
  vars V V' 						: Variable .
  vars EqC EqC' 				: EqCondition .
  var CON 						: Constant .
  var RlC 							: Condition .
  var Rl 							: Rule .
  var RlS 							: RuleSet .
  var RP 							: ResultPair .
  var Eq 							: Equation .
  vars MTTS MTTS' 			: MetaTermTripleSet .
  var BOP2OP 					: Bop2op .
  vars MTT MTT' 				: MetaTermTriple .
  vars Ty Ty' Ty'' 				: Type .
  vars TyL TyL' 					: TypeList .
  vars OP OP' OP'' C C' 		: Qid .
  var BOPL 						: Bop2opList .
  vars OT BV SV OT' BV' SV' : Term .

  op nil : -> TypeConstants .
  op __ : TypeConstantsList TypeConstantsList -> TypeConstantsList [assoc comm id: nil] .
  op `[_;_`] : Type QidList -> TypeConstants [ctor format (o o r o o o)] .
  op add2TypeConstants : Qid TypeConstants -> TypeConstants .
  op getConstants : Type TypeConstantsList -> QidList .
  op <_;_;_> : TermList TermList AttrSet -> Combine4TupleResult .
  op <_;_> : EqCondition RuleSet -> RuleConditionPair .
  op none : -> RuleConditionPair .
  op getVariables : Term -> TermList .
  op getVariables : TermList -> TermList .
  op getVariables : Equation -> TermList .
  op getVariables : EqCondition -> TermList .
  op combineVariables : TermList TermList -> TermList .
  op inVars : Variable TermList -> Bool .
  op substitute : Qid Variable Equation -> Equation .
  op substitute : Qid Variable Term -> Term .
  op substitute : Qid Variable TermList -> TermList .
  op substitute : Qid Variable EqCondition -> EqCondition .
  op getEquations : Constant EquationSet -> EquationSet .
  op getEquations : Term EquationSet -> EquationSet .
  op contains : Term Constant -> Bool .
  op contains : TermList Constant -> Bool .
  op removeConditionEqs : EquationSet EquationSet -> EquationSet .
  op removeConditionEqC : EquationSet EqCondition -> EqCondition .
  op replaceConditionParts : EquationSet FModule -> EquationSet .

  op getConditionEqs : QidList EquationSet -> EquationSet .
  op combineRules : RuleConditionPair -> Rule .
  op combineLRA : RuleSet -> Combine4TupleResult .
  op replaceTerm : Term Term Term -> Term .
  op replaceTermList : TermList Term Term -> TermList .
  op replaceCondition : EqCondition Term Term -> EqCondition .
  op buildVar : Type TermList -> Qid .
  op buildVarAux : TermList -> Qid .
  op <_`,_`,_`,_> : Term Qid Term Term -> MetaTermTriple [ctor] .
  op empty : -> MetaTermTripleSet [ctor] .
  op __ : MetaTermTripleSet MetaTermTripleSet -> MetaTermTripleSet [assoc comm id: empty] .
  op getOTSTerm : MetaTermTriple -> Term .
  op getObsOP : MetaTermTriple -> Qid .
  op getObsVal : MetaTermTriple -> Term .
  op getSuccVal : MetaTermTriple -> Term .
  op hasOTSTerm : MetaTermTripleSet Term -> Bool .
  op getMTT : MetaTermTripleSet Term -> MetaTermTriple .
  op setOTSTerm : MetaTermTriple Term -> MetaTermTriple .
  op setObsOP : MetaTermTriple Qid -> MetaTermTriple .
  op setObsVal : MetaTermTriple Term -> MetaTermTriple .
  op setSuccVal : MetaTermTriple Term -> MetaTermTriple .
  op term2string : TermList -> String .
  op getConstantsList : Module TypeList -> TypeConstantsList .
  op getConstantsListAux1 : OpDeclSet TypeList -> TypeConstantsList .
  op getConstantsListAux2 : OpDeclSet Type -> TypeConstants .
  op add2TypeList : TypeList TypeList -> TypeList .
  op getNewOTSTerm : Bop2opList TermList Type MetaTermTripleSet -> TermList .
  op getNewOTSTermAux : Bop2opList Term MetaTermTripleSet -> TermList .
  op initialObsSuccValue : Term MetaTermTripleSet -> Term .
  op initialObsSuccValueAux : TermList MetaTermTripleSet -> TermList .
  op buildLHS : MetaTermTripleSet -> Term .
  op buildLHSAux : MetaTermTripleSet -> TermList .
  op buildRHS : MetaTermTripleSet -> Term .
  op buildRHSAux : MetaTermTripleSet -> TermList .
  op buildObsSuccValue : MetaTermTripleSet -> MetaTermTripleSet .
  op buildObsSuccValueAux : MetaTermTripleSet MetaTermTripleSet -> MetaTermTripleSet .
  op isSetExp : Type -> Bool .
  op isOccurs : Type TypeList -> Bool .

  eq getBOP2OP (([(bop OP : TyL -> Ty ) ; (op OP' : TyL' -> Ty' [Attr] .)] BOPL), OP) = 
  	   [(bop OP : TyL -> Ty ) ; (op OP' : TyL' -> Ty' [Attr] .)] .
  eq getBOP ([(bop OP : TyL -> Ty ) ; (op OP' : TyL' -> Ty' [Attr] .)]) = OP .
  eq getOP ([(bop OP : TyL -> Ty ) ; (op OP' : TyL' -> Ty' [Attr] .)]) = OP' .
  eq getObvdType ([(bop OP : TyL -> Ty ) ; (op OP' : TyL' -> Ty' [Attr] .)]) = Ty .
  eq getBOP2OP (BOPL, OP) = nil [owise] .
  
  eq getConditionOps (OTSM) = 
  	   getConditionOpsAux (getOps (OTSM), getSort (getHiddenSortDecl (OTSM))) .
  eq getConditionOpsAux ((op OP : S TyL -> 'Bool ) OTSOPDS, S) = OP getConditionOpsAux (OTSOPDS, S) .
  eq getConditionOpsAux (OTSOPDS, S) = nil [owise] .
  
  eq emptyOTSModule = mod* nullHeader {nil none none none none} .
  eq getInitialState (mod* H {IL * [S] * OTSOPDS OTSDS OTSEqS}) = qid ("init." + string (S)) .
  eq getSort ((* [S] *)) = S .
  eq getHiddenSortDecl (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = HSD .
  eq getOTSDeclSet (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = OTSDS .
  eq getName (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = H .
  eq getImports (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = IL .
  eq getSorts (mod* H {IL * [S] * OTSOPDS OTSDS OTSEqS}) = S .
  eq getOps (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = OTSOPDS .
  eq getEqs (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = OTSEqS .
  eq getPars (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}) = nil .
  eq getTransitions ((bop OP : Ty TyL -> Ty ) OTSDS) = (bop OP : Ty TyL -> Ty ) getTransitions (OTSDS) .
  eq getTransitions (none) = none .
  ceq getTransitions ((bop OP : Ty TyL -> Ty' ) OTSDS) = getTransitions (OTSDS) if Ty =/= Ty' .
  
  eq setHiddenSortDecl (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, HSD') = mod* H {IL HSD' OTSOPDS OTSDS OTSEqS} .
  eq setName (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, ME') = mod* ME' {IL HSD OTSOPDS OTSDS OTSEqS} .
  eq setOTSDeclSet (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, OTSDS') = mod* H {IL HSD OTSOPDS OTSDS' OTSEqS} .
  eq setImports (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, IL') = mod* H {IL' HSD OTSOPDS OTSDS OTSEqS} .
  eq setSorts (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, SS) = mod* H {IL HSD OTSOPDS OTSDS OTSEqS} .
  eq setOps (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, OTSOPDS') = mod* H {IL HSD OTSOPDS' OTSDS OTSEqS} .
  eq setEqs (mod* H {IL HSD OTSOPDS OTSDS OTSEqS}, OTSEqS') = mod* H {IL HSD OTSOPDS OTSDS OTSEqS'} .
  eq setPars (OTSM, PDL) = OTSM .
  
  eq empty (OTSM) = emptyOTSModule .
  eq setSubsorts (OTSM, SSDS) = OTSM .
  
  eq addHiddenSortDecl (HSD, OTSM) = setHiddenSortDecl (OTSM, HSD) .
  eq addOTSDeclSet (OTSDS, OTSM) = setOTSDeclSet (OTSM, (OTSDS getOTSDeclSet (OTSM))) .
  eq addEqs (OTSEqS, OTSM) = setEqs (OTSM, OTSEqS getEqs (OTSM)) .
  eq addImports (IL, OTSM) = setImports (OTSM, IL getImports (OTSM)) .
  eq addOps (OTSOPDS, OTSM) = setOps (OTSM, OTSOPDS getOps (OTSM)) .
  eq addSorts (SS, OTSM) = setSorts (OTSM, SS getSorts (OTSM)) .
  eq add2TypeConstants (OP, [Ty ; OPS]) = [Ty ; OP OPS] .
  
  eq getConstants (Ty, [Ty ; OPS] TCL) = OPS .
  eq getConstants (Ty, TCL) = nil [owise] .
  
  eq replaceCondition ((T = T'), T'', T3) = (replaceTerm (T, T'', T3) = replaceTerm (T', T'', T3)) .
  eq replaceCondition ((T : Ty), T', T'') = (replaceTerm (T, T', T'') : Ty) .
  eq replaceCondition ((T := T'), T'', T3) = (replaceTerm (T, T'', T3) := replaceTerm (T', T'', T3)) .
  eq replaceCondition ((EqC /\ EqC'), T, T') = (replaceCondition (EqC, T, T') /\ replaceCondition (EqC', T, T')) .
  eq replaceCondition (nil, T, T') = nil .
  
  eq buildVar (Ty, TL) = if TL =/= empty then qid (string (Ty) + string (buildVarAux (TL))) else qid (string (Ty) + "@") fi .
  ceq buildVarAux ((T, TL)) = qid (string (getName (T)) + string (buildVarAux (TL))) if TL =/= empty .
  eq buildVarAux (T) = getName (T) .
  eq buildVarAux (empty) = nil .
  
  eq replaceTerm (T, T, T'') = T'' .
  ceq replaceTerm (T, T', T'') = OP [replaceTermList (TL, T', T'')] if OP [TL] := T .
  eq replaceTerm (T, T', T'') = T [owise] .
  eq replaceTermList ((T, TL), T', T'') = (replaceTerm (T, T', T''), replaceTermList (TL, T', T'')) .
  eq replaceTermList (empty, T, T') = empty .
  
  ceq combineRules (< EqC ; RlS >) = if TL'' :: NeTermList then (crl '__ [TL] => '__ [TL'] if EqC [AttrS] .) else (crl TL => TL' if EqC [AttrS] .) fi
    if < TL ; TL' ; AttrS > := combineLRA (RlS) /\ (T, TL'') := TL .
  eq combineRules (none) = none .
  ceq combineLRA ((rl T => T' [AttrS] .) RlS) = < (T, TL) ; (T', TL') ; (AttrS AttrS') > if < TL ; TL' ; AttrS' > := combineLRA (RlS) .
  eq combineLRA (none) = < empty ; empty ; none > .
  
  ceq getConditionEqs (OP QL, EqS) = getConditionEqs (OP, EqS) getConditionEqs (QL, EqS) if QL =/= (nil) .TypeList .
  eq getConditionEqs (OP, (eq OP [TL] = T' [AttrS] .) EqS) = (eq OP [TL] = T' [AttrS] .) getConditionEqs (OP, EqS) .
  eq getConditionEqs (OP, none) = none .
  eq getConditionEqs (OP, EqS) = none [owise] .
  eq getConditionEqs (nil, EqS) = none .
  
  eq removeConditionEqs (EqCS, (ceq T = T' if EqC [AttrS] .) EqS) = 
  	   (ceq T = T' if removeConditionEqC (EqCS, EqC) [AttrS] .) removeConditionEqs (EqCS, EqS) .
  eq removeConditionEqs (EqCS, none) = none .
  eq removeConditionEqs (EqCS, EqS) = EqS [owise] .
  eq removeConditionEqC (((eq T = T'' [AttrS] .) EqCS), (T = T')) = (T'' = T') .
  eq removeConditionEqC (((eq T = T'' [AttrS] .) EqCS), (T := T')) = (T'' := T') .
  eq removeConditionEqC (((eq T = T'' [AttrS] .) EqCS), (T : S)) = (T'' : S) .
  eq removeConditionEqC (EqCS, (EqC /\ EqC')) = removeConditionEqC (EqCS, EqC) /\ removeConditionEqC (EqCS, EqC) .
  eq removeConditionEqC (EqCS, EqC) = EqC [owise] .
 
  ceq replaceConditionParts (((ceq T = T' if T'' = 'true.Bool [AttrS] .) EqS), FM) = 
  		((ceq T = T' if getTerm (RP) = 'true.Bool [AttrS] .) replaceConditionParts (EqS, FM)) 
  	if RP := metaReduce (FM, T'') /\ RP :: ResultPair .
  eq replaceConditionParts (none, FM) = none .
  eq replaceConditionParts (EqS, FM) = EqS [owise] .
  
  eq contains (OP [TL], CON) = contains (TL, CON) .
  eq contains (CON, CON) = true .
  eq contains (T, CON) = false [owise] .
  ceq contains ((T, TL), CON) = contains (T, CON) or contains (TL, CON) if TL =/= (empty) .EmptyCommaList .
  eq contains (empty, CON) = false .
  
  eq getEquations (CON, (eq T = T' [AttrS] .) EqS) = 
  	   if contains (T, CON) then ((eq T = T' [AttrS] .) getEquations (CON, EqS)) else getEquations (CON, EqS) fi .
  eq getEquations (CON, EqS) = none [owise] .
  
  eq substitute (C, V, (eq T = T' [AttrS] .)) = (eq substitute (C, V, T) = substitute (C, V, T') [AttrS] .) .
  eq substitute (C, V, (ceq T = T' if EqC [AttrS] .)) = (ceq substitute (C, V, T) = substitute (C, V, T') if substitute (C, V, EqC) [AttrS] .) .
  eq substitute (C, V, OP [TL]) = if TL :: GroundTermList then OP [TL] else OP [substitute (C, V, TL)] fi .
  eq substitute (C, V, T) = if T == V then qid (string (C) + "." + string (getType (V))) else T fi .
  eq substitute (C, V, (T, TL)) = (substitute (C, V, T), substitute (C, V, TL)) .
  eq substitute (C, V, empty) = empty .
  ceq substitute (C, V, (EqC /\ EqC')) = 
  		(substitute (C, V, EqC) /\ substitute (C, V, EqC')) 
  	if EqC' =/= (nil) .EqCondition and EqC =/= (nil).EqCondition .
  eq substitute (C, V, (T := T')) = (substitute (C, V, T) := substitute (C, V, T')) .
  eq substitute (C, V, (T = T')) = (substitute (C, V, T) = substitute (C, V, T')) .
  eq substitute (C, V, (T : S)) = (substitute (C, V, T) := S) .
  eq substitute (C, V, (nil) .EqCondition) = (nil) .EqCondition .
  
  ceq getVariables ((EqC /\ EqC')) = 
  		combineVariables (getVariables (EqC), getVariables (EqC')) 
  	if EqC' =/= (nil) .EqCondition and EqC =/= (nil).EqCondition .
  eq getVariables ((T := T')) = getVariables (T) .
  eq getVariables ((T = T')) = getVariables (T) .
  eq getVariables ((T : S)) = getVariables (T) .
  eq getVariables ((nil) .EqCondition) = empty .
  
  eq inVars (V, (V', TL)) = if V == V' then true else inVars (V, TL) fi .
  eq inVars (V, empty) = false .
  
  eq combineVariables ((V, TL), TL') = 
  	   if inVars (V, TL') then combineVariables (TL, TL') else combineVariables (TL, (V, TL')) fi .
  eq combineVariables (empty, TL) = TL .
  
  eq getVariables (OP [TL]) = if TL :: GroundTermList then empty else getVariables (TL) fi .
  eq getVariables (T) = if T :: Variable then T else empty fi .
  eq getVariables ((T, TL)) = combineVariables (getVariables (T), getVariables (TL)) .
  eq getVariables (empty) = empty .
  eq getVariables (eq T = T' [AttrS] .) = getVariables (T) .
  eq getVariables (ceq T = T' if EqC [AttrS] .) = combineVariables (getVariables (T), getVariables (EqC)) .
    
  eq isOccurs (Ty, (Ty' TyL)) = if Ty == Ty' then true else isOccurs (Ty, TyL) fi .
  eq isOccurs (Ty, nil) = false .
  
  ceq add2TypeList ((Ty TyL), TyL') = 
  			if not isOccurs (Ty, TyL') then add2TypeList (TyL, (Ty TyL')) else add2TypeList (TyL, TyL') fi 
  		if TyL =/= nil .
  eq add2TypeList (Ty, TyL) = if not isOccurs (Ty, TyL) then (Ty TyL) else TyL fi .
  eq add2TypeList (nil, TyL) = TyL .
  
  eq isSetExp (Ty) = false [owise] .
  ceq isSetExp (Ty) = true if length (string (Ty)) > 3 and substr (string (Ty), sd (length (string (Ty)), 3), length (string (Ty))) == "Set" .
  
  eq getConstantsList (M, TyL) = getConstantsListAux1 (getOps(M), TyL) .
  eq getConstantsListAux1 (OPDS, Ty TyL) = (getConstantsListAux2 (OPDS, Ty)) getConstantsListAux1 (OPDS, TyL) .
  eq getConstantsListAux1 (OPDS, nil) = nil .
  ceq getConstantsListAux2 ((op OP : TyL' -> Ty [Attr] .) OPDS, Ty') = 
  		if Ty == Ty' and TyL' == nil then 
  			add2TypeConstants (OP, getConstantsListAux2(OPDS, Ty')) else getConstantsListAux2 (OPDS, Ty') fi 
  	if not isSetExp (Ty') .
  ceq getConstantsListAux2 ((op OP : TyL' -> Ty  [Attr] .) OPDS, Ty') = 
  		if Ty == Ty'' and TyL' == nil then 
  			add2TypeConstants (OP, getConstantsListAux2 (OPDS, Ty')) else 
  			getConstantsListAux2 (OPDS, Ty') fi 
  		if isSetExp (Ty') /\ Ty'' := qid (substr (string (Ty'), 0, sd (length (string (Ty')), 3))) .
  eq getConstantsListAux2 (none, Ty) = [Ty ; nil] .
  
  ceq term2string ((T, TL)) = string (getName (T)) + term2string (TL) if TL =/= empty /\ T :: Variable .
  eq term2string (empty) = "" .
  ceq term2string (T) = string (getName (T)) if T :: Variable .
  eq term2string ((T, TL)) = term2string (TL) [owise] .
  
  eq buildObsSuccValue (MTTS) = buildObsSuccValueAux (MTTS, empty) .
  eq buildObsSuccValueAux (empty, MTTS) = MTTS .
  eq buildObsSuccValueAux (MTT, MTTS) = (setSuccVal (MTT, initialObsSuccValue (getSuccVal (MTT), (MTT MTTS))) MTTS) .
  ceq buildObsSuccValueAux ((MTT MTTS), MTTS') = 
  		buildObsSuccValueAux (MTTS, (MTT' MTTS')) 
  		if MTTS =/= empty /\ 
  			MTT' := setSuccVal (MTT, initialObsSuccValue (getSuccVal (MTT), (MTT MTTS MTTS'))) /\ 
  			MTT' :: MetaTermTriple .
  eq buildObsSuccValueAux (MTTS, MTTS') = MTTS' [owise] .
  
  eq buildRHS (< OP [T, TL], OP', BV, SV >) = (OP' [TL, SV]) .
  ceq buildRHS (< OP [T, TL], OP', BV, SV > MTTS) = '__ [OP' [TL, SV], buildRHSAux (MTTS)] if MTTS =/= empty .
  eq buildRHSAux (MTT MTTS) = (buildRHS (MTT), buildRHSAux (MTTS)) .
  eq buildRHSAux (empty) = empty .
  
  eq buildLHS (< OP [T, TL], OP', BV, SV >) = (OP' [TL, BV]) .
  ceq buildLHS (< OP [T, TL], OP', BV, SV > MTTS) = '__ [OP' [TL, BV], buildLHSAux (MTTS)] if MTTS =/= empty .
  eq buildLHSAux (MTT MTTS) = (buildLHS (MTT), buildLHSAux (MTTS)) .
  eq buildLHSAux (empty) = empty .
  
  ceq initialObsSuccValue (T, MTTS) = getObsVal (MTT) if MTT := getMTT (MTTS, T) /\ MTT =/= empty .
  ceq initialObsSuccValue (OP [TL], MTTS) = (OP [initialObsSuccValueAux (TL, MTTS)]) if not hasOTSTerm (MTTS, OP [TL]) .
  eq initialObsSuccValue (T, MTTS) = T [owise] .
  eq initialObsSuccValueAux (empty, MTTS) = empty .
  eq initialObsSuccValueAux ((T, TL), MTTS) = (initialObsSuccValue (T, MTTS), initialObsSuccValueAux (TL, MTTS)) .
  
  eq getMTT ((< OT, OP, BV, SV > MTTS), OT) = < OT, OP, BV, SV > .
  eq getMTT (MTTS, OT) = empty [owise] .
  
  ceq getNewOTSTerm (BOPL, (T, TL), Ty, MTTS) = 
  		(getNewOTSTerm (BOPL, T, Ty, MTTS), getNewOTSTerm (BOPL, TL, Ty, MTTS)) if TL =/= empty .
  eq getNewOTSTerm (BOPL, empty, Ty, MTTS) = empty .
  ceq getNewOTSTerm (BOPL, OP [T, TL], Ty, MTTS) = 
  		getNewOTSTermAux (BOPL, OP [T, TL], MTTS) if (T :: Constant or T :: Variable) /\ getType (T) == Ty .
  ceq getNewOTSTermAux (BOPL, OP [T, TL], MTTS) = empty if hasOTSTerm (MTTS, OP [T, TL]) .
  ceq getNewOTSTermAux (BOPL, OP [T, TL], MTTS) = 
  		(OP [T, TL]) if not hasOTSTerm (MTTS, OP [T, TL]) /\ BOP2OP := getBOP2OP (BOPL, OP) /\ BOP2OP =/= nil .
  eq getNewOTSTermAux (BOPL, T, MTTS) = empty [owise] .
  ceq getNewOTSTerm (BOPL, T, Ty, MTTS) = empty if T :: Constant or T :: Variable .
  eq getNewOTSTerm (BOPL, OP [T, TL], Ty, MTTS) = 
  		(getNewOTSTerm (BOPL, T, Ty, MTTS), getNewOTSTerm (BOPL, TL, Ty, MTTS)) [owise] .
  		
  eq getOTSTerm (< OT, OP, BV, SV >) = OT .
  eq getObsOP (< OT, OP, BV, SV >) = OP .
  eq getObsVal (< OT, OP, BV, SV >) = BV .
  eq getSuccVal (< OT, OP, BV, SV >) = SV .
  eq setOTSTerm (< OT, OP, BV, SV >, OT') = < OT', OP, BV, SV > .
  eq setObsOP (< OT, OP, BV, SV >, OP') = < OT, OP', BV, SV > .
  eq setObsVal (< OT, OP, BV, SV >, BV') = < OT, OP, BV', SV > .
  eq setSuccVal (< OT, OP, BV, SV >, SV') = < OT, OP, BV, SV' > .
  eq hasOTSTerm ((< OT, OP, BV, SV > MTTS), OT) = true .
  eq hasOTSTerm (MTTS, OT) = false [owise] .
endfm
    
    
fmod OTS-DECL-PARSING is
	including UNIT-DECL-PARSING .
	including OPERATOR-OTS .
	
	op convert2OValue : Term -> Term .
	op convert2NOValue : Term -> Term .
	op parseOTSDecl : Term OTSModule -> OTSModule .
	op parseOTSDecl : Term Module Module OpDeclSet -> ParseDeclResult .
	op getObservers : Module -> OpDeclSet .
	op isObserver : Qid OpDeclSet -> Bool .
	op parseHiddenSort : Term ~> Sort .
	op unfoldOTS : QidList TypeList Sort -> OTSDeclSet .
	op addSortToken : Term -> Term .
	op sub2sort : Term -> Term .
	op combine2sort : Term Term -> Term .
	op unfoldOTSOpDecl : QidList TypeList Sort -> OTSOpDeclSet .
	op map2MaudeAttr : TermList -> TermList .

	vars T T' T'' T''' T4 : Term .
	vars S S' S'' : Term .
	vars TL TL' : TermList .
	vars OTSM : OTSModule .
	vars VDS VDS' : OpDeclSet .
	var PDR : ParseDeclResult .
	vars F O : Qid .
	vars H : Header .
	vars SSDS : SubsortDeclSet .
	vars OPDS : OpDeclSet . 
	vars MAS : MembAxSet .
	vars EqS : EquationSet .
	vars RIS : RuleSet .
	vars IL : ImportList .
	vars SS : SortSet .
	vars QL QL' QL'' : QidList .
	vars PU U PU' U' : Module .
	var HS : Sort .
	var OTSDS : OTSDeclSet .
	var OTSD  : OTSDecl .
	var TyL : TypeList .
	var Ty 	: Type .
	var QI 	: Qid .
	var QIL 	: QidList .
	vars M M'  : Module .
	var DB    : Database .
	var RP    : [ResultPair] .
	
    eq map2MaudeAttr('__[TL]) = '__[map2MaudeAttr(TL)] .
    eq map2MaudeAttr(('constr.@CafeAttr@, TL)) = ('ctor.@Attr@, map2MaudeAttr(TL)) .
    eq map2MaudeAttr(('assoc.@CafeAttr@, TL)) = ('assoc.@Attr@, map2MaudeAttr(TL)) .
    eq map2MaudeAttr(('comm.@CafeAttr@, TL)) = ('comm.@Attr@, map2MaudeAttr(TL)) .
    eq map2MaudeAttr(('id:_['otsBubble[T]], TL)) = ('id:_['bubble[T]], map2MaudeAttr(TL)) .
	eq map2MaudeAttr(empty) = empty .
	*** eq map2MaudeAttr(TL) = empty [owise] .


	eq unfoldOTSOpDecl((QI QIL), TyL, Ty) = ((op QI : TyL -> Ty) unfoldOTSOpDecl(QIL, TyL, Ty)) .
	eq unfoldOTSOpDecl(nil, TyL, Ty) = none .
	***parse imported expression
	eq  parseOTSDecl('pr`(_`)['otsToken[T]], OTSM) = addImports((protecting parseModExp('token[T]) .), OTSM) .
	eq  parseOTSDecl('inc`(_`)['otsToken[T]], OTSM) = addImports((including parseModExp('token[T]) .), OTSM) .
	
	*** parse hiddensort and sort
	ceq parseOTSDecl('*`[_`]*[T], OTSM) = addHiddenSortDecl((*[ HS ]*), OTSM) if HS := parseHiddenSort(T) .
	eq parseOTSDecl('`[_`]['neOTSTokenList[T]], OTSM) = addSorts(parseSortSet(addSortToken(T)), OTSM) .
	eq parseOTSDecl('`[_`]['otsToken[T]], OTSM) = addSorts(parseSortSet('sortToken[T]), OTSM) .
	eq  parseOTSDecl('op_:`->_`{_`}.['otsToken[T], 'otsToken[T'], T''],  OTSM) = 
		addOps((op downQid(T) : nil -> parseType('sortToken[T'])), OTSM) .               
	***  eq parseOTSDecl('`[_`]['_<_[T, T'']], OTSM) = 
	
	***parse normal operators
	eq parseOTSDecl('op_:`->_.['otsToken[T], 'otsToken[T']], OTSM) = addOps((op downQid(T) : nil -> parseType('sortToken[T']) ), OTSM) .
	
	eq parseOTSDecl('ops_:`->_.['neOTSTokenList[T], 'otsToken[T']], OTSM) = 
		addOps(unfoldOTSOpDecl(downTypes(T), nil, parseType('sortToken[T'])), OTSM) .
	
	ceq parseOTSDecl('op_:_->_.['otsToken[T], T', 'otsToken[T'']], OTSM ) = 
		addOps((op downQid(T) : parseTypeList(T4) -> parseType('sortToken[T''])), OTSM) if T4 := addSortToken(T') .
	
	ceq parseOTSDecl('ops_:_->_.['neOTSTokenList[T], T', 'otsToken[T'']], OTSM) = 
		addOps(unfoldOTSOpDecl(downTypes(T), parseTypeList(T4), parseType('sortToken[T''])), OTSM) if T4 := addSortToken(T') .
	  
	  ***ceq parseOTSDecl('op_:_->_`{_`}.['otsToken[T], T', 'otsToken[T''], T'''], OTSM) = 
	  ***    addOps((op downQid(T) : parseTypeList(T4) -> parseType('sortToken[T'']) 
	  ***    [parsePreAttrs(T''', size(parseTypeList(T4)))] .), OTSM) if T4 := addSortToken(T') .                             
      
	  ***parse behavioral operations
	eq  parseOTSDecl('bop_:_->_.['otsToken[T], T', T''], OTSM) = 
		parseOTSDecl('bops_:_->_.['neOTSTokenList[T], T', T''], OTSM) .
	eq  parseOTSDecl('bop_:_->_`{_`}.['otsToken[T], T', T'', T'''], OTSM) = 
		parseOTSDecl('bops_:_->_.['neOTSTokenList[T], T', T''], OTSM) .
	ceq  parseOTSDecl('bops_:_->_.['neOTSTokenList[T], T', 'otsToken[T'']], OTSM) = 
        addOTSDeclSet(unfoldOTS(downTypes(T), parseTypeList(T4), parseType('sortToken[T''])), OTSM) 
	  if T4 := addSortToken(T') . 
	ceq  parseOTSDecl('bops_:_->_`{_`}.['neOTSTokenList[T], T', 'otsToken[T''], T'''], OTSM) = 
        addOTSDeclSet(unfoldOTS(downTypes(T), parseTypeList(T4), parseType('sortToken[T''])), OTSM) 
	  if T4 := addSortToken(T') . 

	  ***parse equations at meta-level
	eq parseOTSDecl('eq_=_.['otsBubble[T], 'otsBubble[T']], OTSM) = OTSM . ***addEqs((eq 'T = T' [none] .), OTSM) .
	eq parseOTSDecl('ceq_=_if_.['otsBubble[T], 'otsBubble[T'], 'otsBubble[T'']], OTSM) = OTSM .
	  *** addEqs((ceq T = T' if T'' = ''true.Bool [none] .), OTSM) .
	  ***to be handled
	  ***eq parseOTSDecl('bceq_=_if_.['bubble[T], 'bubble[T'], 'bubble[T'']], OTSM) = addEqs((bceq T = T' if T'' = 'true [none] .), OTSM) .
	
	eq parseOTSDecl('var_:_.['neOTSTokenList[T], T'], OTSM) = OTSM .
	eq parseOTSDecl('vars_:_.['neOTSTokenList[T], T'], OTSM) = OTSM .
	
	
	**************************************
	***convert to Funtion Module
	************************************** 
	
	eq parseOTSDecl('pr`(_`)['otsToken[T]], PU, U, VDS) = parseDecl('protecting_.['token[T]], PU, U, VDS) .
	eq parseOTSDecl('inc`(_`)['otsToken[T]], PU, U, VDS) = parseDecl('including_.['token[T]], PU, U, VDS) .
	eq parseOTSDecl('*`[_`]*['otsToken[T]], PU, U, VDS) = parseDecl('sort_.['sortToken[T]], PU, U, VDS) .
	ceq parseOTSDecl('`[_`]['otsToken[T]], PU, U, VDS) = parseDecl('sorts_.[T'], PU, U, VDS) if T' := addSortToken('otsToken[T]) .
	ceq parseOTSDecl('`[_`]['__[T, T']], PU, U, VDS) = parseDecl('sorts_.['__[T'', T''']], PU, U, VDS) 
      if T'' := addSortToken(T) /\ T''' := addSortToken(T') . 
	ceq parseOTSDecl('`[_`]['_<_[T, T']], PU, U, VDS) = parseDecl('subsorts_.['_<_[T'', T''']], PU', U', VDS') 
      if T'' := addSortToken(T) /\ 
          T''' := addSortToken(T') /\
          < PU' ; U' ;  VDS' > := parseDecl('sorts_.[sub2sort('_<_[T, T'])], PU, U, VDS) . 
    
	eq parseOTSDecl('eq_=_.['otsBubble[T], 'otsBubble[T']], PU, U, VDS) = parseDecl('eq_=_.['bubble[T], 'bubble[T']], PU, U, VDS) .
	eq parseOTSDecl('ceq_=_if_.['otsBubble[T], 'otsBubble[T'], 'otsBubble[T'']], PU, U, VDS) = 
		  parseDecl('ceq_=_if_.['bubble[T], 'bubble[T'], 'bubble[T'']], PU, U, VDS) .
	eq parseOTSDecl('var_:_.['neOTSTokenList[T], T'], PU, U, VDS) = parseOTSDecl('vars_:_.['neOTSTokenList[T], T'], PU, U, VDS) .
	eq parseOTSDecl('vars_:_.['neOTSTokenList[T], 'otsToken[T']], PU, U, VDS) = 
		< PU ; U ; VDS parseVars(downQidList(T), parseType('sortToken[T'])) > .
    
	***  eq parseDecl('vars_:_.['neOTSTokenList[''I.Qid],'sortToken[''Pid.Qid]]
	
	ceq parseOTSDecl('op_:_->_`{_`}.['otsToken[T], T', 'otsToken[T''], T'''],  PU, U, VDS) = 
		parseDecl('op_:_->_`[_`].['token[T], T4, 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS) if T4 := addSortToken(T') .            
	
	ceq parseOTSDecl('op_:_->_.['otsToken[T], T', 'otsToken[T'']],  PU, U, VDS) = 
		parseDecl('op_:_->_.['token[T], T4, 'sortToken[T'']], PU, U, VDS) if T4 := addSortToken(T') .            
	
	eq  parseOTSDecl('op_:`->_`{_`}.['otsToken[T], 'otsToken[T''], T'''],  PU, U, VDS) = 
		parseDecl('op_:`->_`[_`].['token[T], 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS) .               

  eq  parseOTSDecl('op_:`->_.['otsToken[T], 'otsToken[T'']],  PU, U, VDS) = 
      parseDecl('op_:`->_.['token[T], 'sortToken[T'']], PU, U, VDS) .     
  
  ceq parseOTSDecl('ops_:_->_`{_`}.['neOTSTokenList[T], T', 'otsToken[T''], T'''],  PU, U, VDS) = 
      parseDecl('ops_:_->_`[_`].['neTokenList[T], T4, 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS)  if  T4 := addSortToken(T') .            

  ceq parseOTSDecl('ops_:_->_.['neOTSTokenList[T], T', 'otsToken[T'']],  PU, U, VDS) = 
      parseDecl('ops_:_->_.['neTokenList[T], T4, 'sortToken[T'']], PU, U, VDS) if T4 := addSortToken(T') .            

  eq  parseOTSDecl('ops_:`->_`{_`}.['neOTSTokenList[T], 'otsToken[T''], T'''],  PU, U, VDS) = 
      parseDecl('ops_:`->_`[_`].['neTokenList[T], 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS) .               

  eq  parseOTSDecl('ops_:`->_.['neOTSTokenList[T], 'otsToken[T'']],  PU, U, VDS) = 
      parseDecl('ops_:`->_.['neTokenList[T], 'sortToken[T'']], PU, U, VDS) .           
  
  ceq parseOTSDecl('bop_:_->_.['otsToken[T], T', 'otsToken[T'']],  PU, U, VDS) = 
      parseDecl('op_:_->_.['token[T], T4, 'sortToken[T'']], PU, U, VDS) if  T4 := addSortToken(T') .   

  ceq parseOTSDecl('bop_:_->_`{_`}.['otsToken[T], T', 'otsToken[T''], T'''],  PU, U, VDS) = 
      parseDecl('op_:_->_`[_`].['token[T], T4, 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS) if T4 := addSortToken(T') .            
 
  ceq parseOTSDecl('bops_:_->_.['neOTSTokenList[T], T', 'otsToken[T'']],  PU, U, VDS) = 
      parseDecl('ops_:_->_.['neTokenList[T], T4, 'sortToken[T'']], PU, U, VDS) if T4 := addSortToken(T') .             
 
  ceq parseOTSDecl('ops_:_->_`{_`}.['neOTSTokenList[T], T', 'otsToken[T''], T'''],  PU, U, VDS) = 
      parseDecl('ops_:_->_`[_`].['neTokenList[T], T4, 'sortToken[T''], map2MaudeAttr(T''')], PU, U, VDS)  if  T4 := addSortToken(T') .            

      
  eq parseHiddenSort('otsToken[T]) = 
     if downQid(T) :: Type
     then downQid(T) 
     else qidError('\y 'Warning: '\o downQid(T) 'is 'not 'a 'valid 'sort. '\n) 
     fi .
  eq parseHiddenSort(T)
     = qidError('\y 'Warning: '\o 'invalid 'sort. '\n) [owise] .

  ceq unfoldOTS((QL QIL), TyL , Ty) = OTSD unfoldOTS(QIL, TyL, Ty)
      if OTSD := (bop QL : TyL -> Ty ) 	  . 
  eq unfoldOTS(nil, TyL, Ty) = none . 
  
  eq combine2sort('sortToken[T], T') = '__['sortToken[T], T'] .
  eq combine2sort('__[T, T''], T''') = combine2sort(T'', '__[T, T''']) .
  eq combine2sort(nil, T) = T .
  eq combine2sort(T, nil) = T .
  
  eq sub2sort('_<_[T, T']) = combine2sort(sub2sort(T), sub2sort(T')) .
  eq sub2sort('__['otsToken[T], T']) = ('__['sortToken[T], sub2sort(T')]) .
  eq sub2sort(nil) = nil .
  eq sub2sort('otsToken[T]) = ('sortToken[T]) .
  
  eq addSortToken('__['otsToken[T], T']) = ('__['sortToken[T], addSortToken(T')]) .
  eq addSortToken('_<_['otsToken[T], T']) = ('_<_['sortToken[T], addSortToken(T')]) .
  eq addSortToken(nil) = nil .
  eq addSortToken('otsToken[T]) = ('sortToken[T]) [owise] .

endfm


mod OTS-PARSER is
     protecting DATABASE-HANDLING .
     protecting OTS-DECL-PARSING .
     
     op parseOTS : Term -> OTSModule .
     op parseOTS2 : Term Term OTSModule -> OTSModule .
     op parseOTS3 : Term Term Term OTSModule -> OTSModule .
     op parseOTS4 : Term Term OTSModule -> OTSModule .
     
     op procOTSModule : Term Database -> Database .
     op procOTSModule2 : Term Term Database -> Database .
     op procOTSModule3 : Term Term Term Module Database -> Database .
     op procOTSModule4 : Term Term Module Module  OpDeclSet Database -> Database .

     vars T T' T'' : Term .
     var  DB : Database .
     vars F QI : Qid .
     vars OTSM OTSM' : OTSModule .
     var  VDS : OpDeclSet .
     vars PDR PDR'  : ParseDeclResult .
     var  TL : TermList .
     vars PU PU' U U' : Module .

     eq  parseOTS(T) = parseOTS2(T, T, emptyOTSModule) .
     eq parseOTS2(T, 'mod*_`{_`}[T', T''], OTSM) = parseOTS3(T, T', T'', OTSM) .
     eq parseOTS3(T, 'otsToken[T'], T'', OTSM) = parseOTS4(T, T'', setName(OTSM, downQid(T'))) . 
     ceq parseOTS4(T, '__[T', T''], OTSM) = parseOTS4(T, T'', OTSM') if OTSM' := parseOTSDecl(T', OTSM) .
     ceq parseOTS4(T, F[TL], OTSM) = OTSM' if F =/= '__ /\ OTSM' := parseOTSDecl(F[TL], OTSM) .



     *******************************************************************************************************
     ***extend procModule so that OTS module can be converted into a function module in Maude 
     *******************************************************************************************************
     eq procOTSModule(T, DB) = procOTSModule2(T, T, DB) .
     eq procOTSModule2(T, 'mod!_`{_`}[T', T''], DB)  = procOTSModule3(T, T', T'', emptyFModule, DB) .
     eq procOTSModule2(T, 'mod*_`{_`}[T', T''], DB)  = procOTSModule3(T, T', T'', emptyFModule, DB) .
     ceq procOTSModule3(T, 'otsToken[T'], T'', U, DB) = 
         procOTSModule4(T, T'', setName(U, QI), setName(U, QI), none, DB) 
        if QI := downQid(T') .
        
     ceq procOTSModule4(T, '__[T', T''], PU, U, VDS, DB) 
         = procOTSModule4(T, T'', preModule(PDR), unit(PDR), vars(PDR), DB)
           if PDR := parseOTSDecl(T', PU, U, VDS) .
     ceq procOTSModule4(T, F[TL], PU, U, VDS, DB) = 
         evalPreModule(preModule(PDR), unit(PDR), vars(PDR), insTermModule(getName(U), T, DB))
         if F =/= '__ /\ PDR := parseOTSDecl(F[TL], PU, U, VDS) .
   
endm

fmod CONVERT-SIGNAURE is
	including OPERATOR-OTS .
	
	sorts Para ParaList .
	subsort Para < ParaList .

	op p : TermList -> Para [ctor] .
	op nil : -> Para [ctor] .
    op __ : ParaList ParaList -> ParaList [assoc comm id: nil] .
	op convertHiddenSort     : HiddenSortDecl SModule -> SModule .
	op convertOps		 : OTSOpDeclSet Sort SModule -> SModule .
	op convertBOP		 : OTSDeclSet DoubleResultPair -> DoubleResultPair .
	op buildOperator    : Nat -> Qid . 
  	op buildOperatorAux : Nat -> String .
  	op buildOperator     : Qid TypeList -> Qid .
   	

	var OPDS : OpDeclSet .
	var OTSOPDS : OTSOpDeclSet .
	var OTSDS : OTSDeclSet .
	var SM : SModule .
	vars S HS : Sort .
	vars OP OP' OP'' : Qid .
    vars Ty Ty' Ty'' : Type .
    vars TyL TyL' : TypeList .
    var Attr : AttrSet .
    var BOPL : Bop2opList .
    
	eq convertHiddenSort( (*[ S ]*), SM) = addSorts(S, SM) .
	eq convertHiddenSort(none, SM) = SM .
	
	eq convertOps((op 'init : nil -> Ty ) OTSOPDS, HS, SM) = 
		   	if Ty == HS then
	 			addOps((op 'init : nil -> 'OTSState [none] .), convertOps(OTSOPDS, HS, SM))
			else 
		 		addOps((op 'init : nil -> Ty [none] .), convertOps(OTSOPDS, HS, SM)) 
			fi .

	ceq convertOps((op OP : nil -> Ty ) OTSOPDS, HS, SM) = 
		addOps((op OP : nil -> Ty [none] .), convertOps(OTSOPDS, HS, SM)) if OP =/= 'init .

	eq 	convertOps((op OP : Ty TyL -> Ty' ) OTSOPDS, HS, SM) = 
		if Ty == HS and Ty' == Ty then 
			convertOps(OTSOPDS, HS, SM) 
		else
			addOps((op OP : Ty TyL -> Ty' [none] .), convertOps(OTSOPDS, HS, SM)) 
		fi .

	eq convertOps(none, HS, SM) = SM .

    eq convertBOP((bop OP : Ty TyL -> Ty' ) OTSDS, < BOPL ; SM > ) = 
	if Ty =/= Ty' then
	  convertBOP(OTSDS, < [(bop OP : Ty TyL -> Ty' );(op buildOperator(OP, TyL) : TyL Ty' -> 'OValue [none] .)] BOPL ;
			 addOps((op buildOperator(OP, TyL) : TyL Ty' -> 'OValue [none] .), SM) > )
		else
		   convertBOP(OTSDS, < BOPL ; addOps((op OP : Ty TyL -> Ty' [none] .), SM) > )
		fi .
	eq convertBOP(none, < BOPL ; SM >) = < BOPL ; SM > .

	eq buildOperator(OP, Ty TyL) = buildOperator(qid(string(OP) + "_"), TyL) .
	eq buildOperator(OP, nil) = qid(string(OP) + " :_") .

endfm

***OMG-RWMODULE-STRATEGY IS USED TO GENERATE A GENERAL SYSTEM MODULE THAT
***SPECIFIES AN OTS EXPLICITELY WITH LESS REWRITING RULES.
***ADDITIONAL OBSERVERS MAY BE NEEDED TO PROVIDE NECESSARY INFORMATION
***TO MAKE REWRITING RULES EXECUTABLE
***THE FUNCTION OF ERROR-HANDING IS ALSO ADDED 
		
fmod OMG-RWMODULE-STRATEGY is

	protecting CONVERT-SIGNAURE .
    including DATABASE .
	protecting DECL-META-PRETTY-PRINT .

	sort Pair{RuleSet,ExtSub} .
	sort Pair{TermList,TermList} .
	sort Pair{Qid,ExtSub} .
	sort Pair{Qid,Type} .
	subsort Pair{Qid,Type} < ResultPair < Pair{TermList,TermList} .
	sort ExtSubstitution .
	subsort Substitution < ExtSubstitution .
    
    op _<-_ : Term Term -> ExtSubstitution [ditto] .
	op none : -> ExtSubstitution [ctor] .
    op _;_ : ExtSubstitution ExtSubstitution -> ExtSubstitution [ditto] .
    op substitutionError : QidList QidList ~> ExtSubstitution [format(r o)] .
	op {_,_} : Qid Type -> Pair{Qid,Type} [ctor] .
	op {_,_} : Qid ExtSubstitution -> Pair{Qid,ExtSub} [ctor] .
	op {_,_} : TermList TermList -> Pair{TermList,TermList} [ctor] .
	op {_,_} : RuleSet ExtSubstitution -> Pair{RuleSet,ExtSub} [ctor] .
	op singleRuleError : QidList QidList ~> Pair{RuleSet,ExtSub} .
	op termError : QidList QidList ~> Pair{TermList,TermList} .

	op convert2sysm  : OTSModule ->  DoubleResultPair .
	  
    op buildRewMod : Bop2opList OTSModule SModule Header Database ~> Module .
    op buildRewModAux1 : Bop2opList OTSModule SModule FModule FModule ~> Module .
	op buildRewModAux2 : Bop2opList OTSModule SModule FModule FModule OpDeclSet ~> Module .
    op buildSetSorts : TypeList SortSet -> SortSet .
	op buildSubsortDeclSet : SortSet -> SubsortDeclSet .
    ***op buildSortSetListAux : TypeList SortSet -> TypeList .
	op buildAuxObservers : TypeList -> OpDeclSet .
	op buildAuxObserversAux : Type OpDeclSet Nat -> OpDeclSet .
	op existsOB : Qid OpDeclSet -> Bool .
	op buildCatenationOps : SortSet -> OpDeclSet .
	op remove : OpDeclSet OpDeclSet -> OpDeclSet .
	op getUsedOPDS : RuleSet OpDeclSet -> OpDeclSet .
	op getUsedOPDSAux : TermList OpDeclSet -> OpDeclSet .
	op buildTypeList   : OTSDeclSet -> TypeList .
	op combineTypeList : TypeList TypeList -> TypeList .
	op filter          : TypeList TypeList -> TypeList .
	op cover           : TypeList TypeList -> TypeList .
	op removeType      : TypeList Type     -> TypeList .
    op convError : QidList QidList -> [Module] [ctor format(r o)] .

    var BOPL : Bop2opList .
    var OTSM : OTSModule .
	var OTSDS : OTSDeclSet .
	var SM : SModule .
	var H  : Header .
	var DB : Database .
	vars S HS : Sort .
	vars FM FM' : FModule .
	vars SS SS' : SortSet .
	vars OPDS OPDS' : OpDeclSet .
	vars OTSOPDS : OTSOpDeclSet .
	vars TyL TyL'' : TypeList .
	vars Ty Ty' Ty'' : Type .
    vars SSDS : SubsortDeclSet .
	vars OP : Qid .
	vars N : Nat .
	vars Rls Rls' : RuleSet .
	vars QIL QIL' : QidList .
	vars OPD : OpDecl .
	vars M : Module .
	vars IL : ImportList .
	vars HSD : HiddenSortDecl .
	vars OTSEqS : OTSEquationSet .

	ceq convert2sysm(mod* H { IL HSD OTSOPDS OTSDS OTSEqS }) = 
	   < BOPL ; addImports(((including 'STATE-ES .) IL), 
				  convertHiddenSort(HSD,
					convertOps(OTSOPDS,  getSort(HSD), SM))) >
	   if < BOPL ; SM > := convertBOP(OTSDS, < nil ; setName(emptySModule, qid(string(H) + "-MAUDE")) > ) .

	
	eq buildTypeList(none) = nil .
	eq buildTypeList((bop OP : Ty TyL -> Ty' ) OTSDS) = combineTypeList(TyL, buildTypeList(OTSDS)) . 
	eq combineTypeList(TyL, TyL') = (filter(TyL, TyL')) (cover(TyL, TyL')) .
	
	eq combineTypeList(TyL, TyL') = (filter(TyL, TyL')) (cover(TyL, TyL')) .

	eq cover(nil, nil) = nil .
	eq cover(nil, TyL) = TyL .
	eq cover(TyL, nil) = TyL .
	eq cover(Ty TyL, TyL') = if occurs(Ty, TyL') then cover(TyL, removeType(TyL', Ty)) else (Ty cover(TyL, TyL')) fi . 
  	eq filter(nil, nil) = nil .
	eq filter(nil, TyL) = nil .
	eq filter(TyL, nil) = nil .
	eq filter(Ty TyL, TyL') = if occurs(Ty, TyL') then (Ty filter(TyL, removeType(TyL', Ty))) else  filter(TyL, TyL') fi .  
	ceq removeType(TyL, Ty) = TyL'' TyL' if occurs(Ty, TyL) /\ (TyL'' Ty TyL') := TyL .
	eq removeType(TyL, Ty) = TyL [owise] .

	

	eq existsOB(OP, ((op OP : Ty -> 'OValue [ctor] .) OPDS)) = true .
	eq existsOB(OP, OPDS) = false [owise] .

	ceq buildSetSorts((Ty TyL), SS) = (Ty' ; SS')
		if TyL =/= nil /\
		   Ty' := qid(string(Ty) + "Set") /\
		   SS' := buildSetSorts(TyL, SS) /\
		   not ((Ty' in SS) or (Ty' in SS')) .

	ceq buildSetSorts(Ty, SS) = 
	  if not (Ty' in SS) then Ty' else none fi
	  if Ty' := qid(string(Ty) + "Set") .
	
	eq buildSetSorts(nil, SS) = none .

	eq buildSetSorts((Ty TyL), SS) = buildSetSorts(TyL, SS) [owise] .


	ceq buildSubsortDeclSet((Ty ; SS)) = 
		((subsort qid(substr(string(Ty), 0, sd(length(string(Ty)), 3))) < Ty .) 
		  buildSubsortDeclSet(SS))
	  if SS =/= none .

	eq buildSubsortDeclSet(Ty) = 
		(subsort qid(substr(string(Ty), 0, sd(length(string(Ty)), 3))) < Ty .) .

	eq buildSubsortDeclSet(none) = none .

	eq buildAuxObservers(Ty TyL) = 
		buildAuxObserversAux(Ty, buildAuxObservers(TyL), 1) .
	eq buildAuxObservers(nil) = none .
	
	eq buildCatenationOps(Ty ; SS) = 
		( (op 'nil : nil -> Ty [ctor] . ) 
		  (op '__ : Ty Ty -> Ty [assoc comm id(qid("nil." + string(Ty)))] .)
		  buildCatenationOps(SS)) .
	eq buildCatenationOps(none) = none .

	ceq buildAuxObserversAux(Ty, OPDS, N) = 
	  if not existsOB(OP, OPDS) then 
		  ((op OP : qid(string(Ty) + "Set") -> 'OValue [ctor] .) OPDS)
		else buildAuxObserversAux(Ty, OPDS, (N + 1)) fi
	  if OP := qid("O" + string(Ty) + string(N, 10) + " :_") .

	ceq buildRewModAux1(BOPL, OTSM, SM, FM, FM') = 
	    buildRewModAux2(BOPL, OTSM, addOps(OPDS', addSubsorts(SSDS, addSorts(SS, SM))), FM, FM', OPDS) 
      if OTSDS := getOTSDeclSet(OTSM) /\ 
		  TyL := buildTypeList(getTransitions(OTSDS)) /\
		  SS := buildSetSorts(TyL, getSorts(FM')) /\
		  SSDS := buildSubsortDeclSet(SS) /\
		  OPDS' := buildCatenationOps(SS) /\
		  OPDS := buildAuxObservers(TyL) .
	
	****LAST STEP****
	***INITIATE the initial state***********
	ceq buildRewModAux2(BOPL, OTSM, SM, FM, FM', OPDS) = 
		addRls(Rls, 
			addEqs(Eq,
				addOps(OPDS', SM)))
	  if Rls := buildRewritingRules(BOPL, OPDS, getTransitions(getOTSDeclSet(OTSM)), FM, FM') /\
	     OPDS' := getUsedOPDS(Rls, OPDS) /\
	     Eq := initialStateEq(BOPL, OPDS', FM') .

	ceq buildRewModAux2(BOPL, OTSM, SM, FM, FM', OPDS) = 
		convError(QIL, ('buildRewModAux2 QIL'))
	  if Rls := buildRewritingRules(BOPL, OPDS, getTransitions(getOTSDeclSet(OTSM)), FM, FM') /\
	     OPDS' := getUsedOPDS(Rls, OPDS) /\
	     eqError(QIL, QIL') := initialStateEq(BOPL, OPDS', FM') .	  
	
	ceq buildRewModAux2(BOPL, OTSM, SM, FM, FM', OPDS) = 
		convError(QIL, ('buildRewModAux2 QIL'))
	  if ruleError(QIL, QIL') := buildRewritingRules(BOPL, OPDS, getTransitions(getOTSDeclSet(OTSM)), FM, FM') .

	eq getUsedOPDS((rl T => T' [Ats] .), OPDS) 
		= getUsedOPDSAux(T, OPDS) .	
	eq getUsedOPDS((crl T => T' if EqC [Ats] .), OPDS) 
		= getUsedOPDSAux(T, OPDS) .
	eq getUsedOPDSAux('__[TL], OPDS) = getUsedOPDSAux(TL, OPDS) .
	
	ceq getUsedOPDSAux((T, TL), OPDS) = 
		(OPDS' getUsedOPDSAux(TL, remove(OPDS', OPDS))) 
		if TL =/= empty /\ OPDS' := getUsedOPDSAux(T, OPDS) .
	ceq getUsedOPDSAux(OP[TL], (op OP : TyL -> Ty [Ats] .) OPDS) = 
		(op OP : TyL -> Ty [Ats] .) if OP =/= '__ .
	eq getUsedOPDSAux(T, OPDS) = none [owise] .
	
	ceq remove((OPD OPDS), OPDS') = 
		remove(OPD, remove(OPDS', OPDS))
		if OPDS =/= none .
	eq remove(OPD, (OPD OPDS)) = OPDS .
	eq remove(none, OPDS) = OPDS .
	eq remove(OPD, OPDS) = OPDS [owise] .
		
	ceq getUsedOPDS((Rl Rls), OPDS) = 
		(OPDS' getUsedOPDS(Rls, remove(OPDS', OPDS)))
	if Rls =/= none /\
		OPDS' := getUsedOPDS(Rl, OPDS) .
		
	  ***Aux1 : For all transitions
	  ***Aux2 : For one transition
	  ***Aux3 : For one transition with effective condition
	  ***Aux4 : For one transition without effective condition

	op initialStateEq : Bop2opList OpDeclSet FModule ~> Equation .
	op initialStateEqAux1 : Bop2opList OpDeclSet TypeList FModule ~> Equation .
	op initialStateEqAux2 : Bop2opList OpDeclSet TypeConstantsList FModule ~> Equation .
	op initialStateEqAux3 : Bop2opList TypeConstantsList FModule ~> TermList .
	op initialStateEqAux4 : OpDeclSet TypeConstantsList ~> TermList .
	op initialStateEqAux5 : TermList Qid FModule ~> TermList .
	op constructParameters : Qid TypeList TypeConstantsList -> TermList .
	op buildList : Type QidList -> TermList .
	op constructParametersAux1 : Qid ParaList -> TermList .
	op constructParametersAux2 : TypeList TypeConstantsList -> ParaList .
	op constructParametersAux3 : QidList Type ParaList -> ParaList .
	op consError : QidList QidList ~> Term .

	op eqError : QidList QidList ~> Equation .

	op buildRewritingRules : Bop2opList OpDeclSet OTSDeclSet FModule FModule ~> RuleSet .
	op buildRewritingRulesAux1 : Bop2opList OpDeclSet OTSDeclSet FModule FModule ~> RuleSet .
	op buildRewritingRulesAux2 : Bop2opList OpDeclSet Qid FModule FModule ~> RuleSet .
	op buildRewritingRulesAux3 : Bop2opList OpDeclSet Qid Equation EquationSet FModule ~> RuleSet .
	op buildRewritingRulesAux4 : Bop2opList OpDeclSet Qid EquationSet FModule ~> Rule .
	op buildRewritingRulesAux6 : Bop2opList OpDeclSet Qid Equation EquationSet FModule ExtSubstitution ~> Rule .
	op buildRewritingRulesAux5 : Bop2opList OpDeclSet Qid EquationSet EquationSet FModule ~> RuleSet .
	
	
	op buildSingleRewritingRules : Bop2opList EquationSet FModule ExtSubstitution ~> Pair{RuleSet,ExtSub} .
	op buildSingleRewritingRules : Bop2opList EquationSet Equation FModule ExtSubstitution ~> Pair{RuleSet,ExtSub} .
	
	op buildSingleRewritingRulesAux1 : 
		Bop2opList Qid Qid Term TermList TermList FModule ExtSubstitution ~> Pair{RuleSet,ExtSub} .
	
	op  buildSingleRewritingRulesAux2 :
		Bop2opList Equation Term FModule  ExtSubstitution ~> Pair{RuleSet, ExtSub} .
	
	op  buildSingleRewritingRulesAux3 :
		Bop2opList Term Term FModule  ExtSubstitution ~> Pair{RuleSet, ExtSub} .
	
	
	op getEffectiveCondEq : Qid EquationSet ~> Equation .
	op getRelatedEqsWRTObs : Qid EquationSet -> EquationSet .

	op evaluateCondEq : Bop2opList Equation -> ExtSubstitution .
	op evaluateCondEqAux1 : Qid Qid Type Term ExtSubstitution ~> ExtSubstitution .
	op evaluateCondEqAux2 : Qid TermList Type Term ExtSubstitution -> ExtSubstitution .
	op evaluateCondEqAux3 : Qid TermList Type Term ExtSubstitution ~> ExtSubstitution .
	op evaluateCondEqAux4 : Qid TermList Term ExtSubstitution ~> ExtSubstitution .
	
	op rmEffectiveConds : OTSDeclSet FModule -> FModule .
	op rmEffectiveCondEqs : OTSDeclSet EquationSet -> EquationSet .
	op rmEffectiveCondEqsAux : Qid EquationSet -> EquationSet .
	op ruleError : QidList QidList ~> Rule [ctor format(r o)] .
	op getObsOp : Bop2opList Qid -> Pair{Qid,Type} .
	op opError : QidList QidList ~> Pair{Qid,Type} [ctor format(r o)] .
	op introVariable : Qid Term Type ExtSubstitution -> Pair{Qid,ExtSub} .
	op getRedResult : FModule Term -> Term .
	op redError : QidList QidList ~> Term [ctor format(r o)] .
	
	op combineRwRules : RuleSet ExtSubstitution Qid ~> Rule .
	op substitute : RuleSet ExtSubstitution ~> Rule .
	op substituteAux : TermList ExtSubstitution -> Term .
	op combineRwRulesAux : RuleSet Qid -> Rule .
	op combineRwRulesAux1 : RuleSet -> Pair{TermList,TermList} .
	op addAuxiliaryOps : Rule OpDeclSet Qid ~> Rule .
	op getBadVariables : Term Term -> TermList .
	op buildAuxiliaryOps : TermList Term Term OpDeclSet Qid ~> Pair{TermList,TermList} .
	op filterVariable : TermList TermList -> TermList .
	op getAuxOps : OpDeclSet Term Type -> Qid .
	op getAuxOpsAux1 : OpDeclSet Term Type -> Qid .
	op isAlreadyExisted : Qid Term -> Bool .
	op isAlreadyExistedAux : Qid TermList -> Bool .
	op addConditionPart : Rule Equation OpDeclSet ExtSubstitution FModule Qid ~> Rule .
	op splitConditionEq : Equation -> EquationSet .
	op getTypeList : Bop2opList OpDeclSet -> TypeList .


	vars EqS : EquationSet .
	vars T T' T'' T1 T2 T3 : Term .
	vars TL TL' TL'' : TermList .
	vars Ats Ats' : AttrSet .
	vars FM'' : FModule .
	vars Rl Rl' Rl'' : Rule .
	vars Eq : Equation .
	vars Eq' : Equation .
	vars EqS' : EquationSet .
	vars F OP' OP'' : Qid .
	vars EqC : EqCondition .
	***vars Eq : Equation .
	vars BOP : Bop2op .
	vars BOP' : [Bop2op] .
	vars EQ : [Equation] .
	vars EST EST' EST'' : ExtSubstitution .
	vars TyL' : TypeList .
	vars V : Variable .
	var RP : [ResultPair] .
	var TCL : TypeConstantsList .
	var TLL : ParaList .
	
	
	ceq constructParametersAux3((OP QIL), Ty, TLL) = 
		(constructParametersAux3(OP, Ty, TLL)
		  constructParametersAux3(QIL, Ty, TLL))
	  if QIL =/= nil .
	
	ceq constructParametersAux3(OP, Ty, (p(TL) TLL)) = 
		(p((qid(string(OP) + "." + string(Ty)), TL)) constructParametersAux3(OP, Ty, TLL))
	  if TLL =/= nil .
	
	eq constructParametersAux3(OP, Ty, nil) = 
		p(qid(string(OP) + "." + string(Ty))) .
	
	eq constructParametersAux3(nil, Ty, nil) = nil .
	
	ceq constructParametersAux2((Ty TyL), TCL) = 
		constructParametersAux3(getConstants(Ty, TCL), Ty, 
		  constructParametersAux2(TyL, TCL)) 
	if TyL =/= nil .
	
	eq constructParametersAux2(Ty, TCL) = 
		constructParametersAux3(getConstants(Ty, TCL), Ty, nil) .
	
	eq constructParametersAux2(nil, TCL) = 
		nil .

	ceq constructParameters(OP, TyL, TCL) = 
		constructParametersAux1(OP, TLL) 
	  if TLL := constructParametersAux2(TyL, TCL) .
	
	ceq constructParametersAux1(OP, (p(T) TLL)) = 
		(OP['init.Sys, T], constructParametersAux1(OP, TLL))
	  if TLL =/= nil .
	
	eq constructParametersAux1(OP, p(T)) = 
		OP['init.Sys, T] .
	eq constructParametersAux1(OP, nil) = 
		OP['init.Sys] .
	****************************************************************************
	
	ceq initialStateEqAux4((OPD OPDS), TCL) =
		(T, TL')
	if OPDS =/= none /\
		T := initialStateEqAux4(OPD, TCL) /\
		TL' := initialStateEqAux4(OPDS, TCL) .

	ceq initialStateEqAux4((OPD OPDS), TCL) =
		consError(QIL, ('initialStateEqAux4, QIL'))
	if OPDS =/= none /\
		consError(QIL, QIL') := initialStateEqAux4(OPD, TCL) .

	ceq initialStateEqAux4((OPD OPDS), TCL) =
		consError(QIL, ('initialStateEqAux4, QIL'))
	if OPDS =/= none /\
		consError(QIL, QIL') := initialStateEqAux4(OPDS, TCL) .

	ceq initialStateEqAux4((op OP : Ty -> Ty' [Ats] .), TCL) =
		if TL :: Term then OP[TL] else OP['__[TL]] fi
		if QIL := getConstants(Ty, TCL) /\
			TL := buildList(Ty, QIL) .

	eq initialStateEqAux4(none, TCL) = empty .

	eq initialStateEqAux4(OPDS, TCL) = 
		consError('unkown 'error, 'initialStateEqAux4) [owise] .
	****************************************
	ceq buildList(Ty, (OP QIL)) = 
		(qid(string(OP) + "." + string(Ty)), buildList(Ty, QIL)) 
	if QIL =/= nil .
	eq buildList(Ty, OP) = 
		qid(string(OP) + "." + string(Ty)) .
	eq buildList(Ty, nil) = qid("nil." + string(Ty)) .
	****************************************************
	ceq initialStateEqAux3((BOP BOPL), TCL, FM) =
		(TL, TL') 
	  if BOPL =/= nil /\
		  TL := initialStateEqAux3(BOP, TCL, FM) /\
		  TL' := initialStateEqAux3(BOPL, TCL, FM) .

	ceq initialStateEqAux3((BOP BOPL), TCL, FM) =
		 consError(QIL, ('initialStateEqAux3, QIL'))
	  if BOPL =/= nil /\
		  consError(QIL, QIL') := initialStateEqAux3(BOPL, TCL, FM) .
	
	ceq initialStateEqAux3((BOP BOPL), TCL, FM) =
		 consError(QIL, ('initialStateEqAux3, QIL'))
	  if BOPL =/= nil /\
		  consError(QIL, QIL') := initialStateEqAux3(BOP, TCL, FM) .
	
	ceq initialStateEqAux3(([(bop OP : Ty TyL -> Ty' ); (op OP' : TyL' -> 'OValue [none] .)]), TCL, FM) = 
		initialStateEqAux5(TL, OP', FM) 
	  if TL := constructParameters(OP, TyL, TCL) .

	eq initialStateEqAux3(nil, TCL, FM) = empty .

	eq initialStateEqAux3(BOPL, TCL, FM) = 
		consError('unkown 'error, 'initialStateEqAux3) [owise] .
	************************************************************
	ceq initialStateEqAux5((T, TL), OP, FM) = 
		(T', TL')
	if TL =/= empty /\
		T' := initialStateEqAux5(T, OP, FM) /\
		TL' := initialStateEqAux5(TL, OP, FM) .

	ceq initialStateEqAux5((T, TL), OP, FM) = 
		consError(QIL, ('initialStateEqAux5 QIL'))
	if TL =/= empty /\
		consError(QIL, QIL') := initialStateEqAux5(T, OP, FM) .

	ceq initialStateEqAux5((T, TL), OP, FM) = 
		consError(QIL, ('initialStateEqAux5 QIL'))
	if TL =/= empty /\
		consError(QIL, QIL') := initialStateEqAux5(TL, OP, FM) .
		
	ceq initialStateEqAux5((OP[T, TL]), OP', FM) = 
	  if RP :: ResultPair then
		  (OP'[TL, getTerm(RP)])
		else
		  consError('cannot 'get 'initial 'value 'for '\g OP, 'initialStateEqAux5) 
		fi
	  if RP := metaReduce(FM, OP[T, TL]) .
		
	eq initialStateEqAux5(empty, OP', FM) = 
		empty .
	
	eq initialStateEqAux5(T, OP, FM) = 
		consError('unkown 'error, 'initialStateEqAux5) [owise] .

*****************************************************
	ceq initialStateEqAux2(BOPL, OPDS, TCL, FM) =
		eqError(QIL, ('initialStateEqAux2 QIL'))
	  if consError(QIL, QIL') := initialStateEqAux3(BOPL, TCL, FM) .
	
	ceq initialStateEqAux2(BOPL, OPDS, TCL, FM) =
		eqError(QIL, ('initialStateEqAux2 QIL'))
	  if	TL :=  initialStateEqAux3(BOPL, TCL, FM) /\
	  	consError(QIL, QIL') := initialStateEqAux4(OPDS, TCL) .
		  
	ceq initialStateEqAux2(BOPL, OPDS, TCL, FM) =
	  if TL =/= empty or TL' =/= empty  then
		  (eq 'init.OTSState = '__[TL, TL'] [none] .)
		else
		  eqError('no 'observed 'valued 'found, 'initialStateEqAux2) 
		fi
	  if TL := initialStateEqAux3(BOPL, TCL, FM) /\
		  TL' := initialStateEqAux4(OPDS, TCL) .

	eq initialStateEqAux2(BOPL, OPDS, TCL, FM) =
		  eqError('unkown 'error, 'initialStateEqAux2) [owise] .

******************************************************

	ceq getTypeList(nil, (op OP : Ty -> Ty' [Ats] .) OPDS) = 
		(Ty getTypeList(nil, OPDS)) 
	  if OPDS =/= none .

	eq getTypeList(nil, (op OP : Ty -> Ty' [Ats] .)) = 
		Ty . 

	eq getTypeList(([(bop OP : Ty TyL -> Ty' ); (op OP' : TyL' -> 'OValue [none] .)]), OPDS) = 
		add2TypeList(TyL, getTypeList(nil, OPDS)) .

	ceq getTypeList((BOP BOPL), OPDS) = 
		add2TypeList(getTypeList(BOP, OPDS), getTypeList(BOPL, OPDS)) 
	  if BOPL =/= nil .
	
	eq getTypeList(nil, none) = nil .
	
	ceq initialStateEqAux1(BOPL, OPDS, TyL, FM) = 
		initialStateEqAux2(BOPL, OPDS, TCL, FM) 
	  if TCL := getConstantsList(FM, TyL) .
	
	ceq initialStateEq(BOPL, OPDS, FM) = 
		initialStateEqAux1(BOPL, OPDS, TyL, FM) 
	  if TyL := getTypeList(BOPL, OPDS) /\
		  TyL =/= none .

	eq initialStateEq(BOPL, OPDS, FM) = eqError('Failed 'to 'initialize 'initial 'state, 'initialStateEq) [owise] .
	***************************************************************************************************
	ceq getRedResult(FM, T) = 
		getTerm(RP) 
	  if RP := metaReduce(FM, T) /\
		  RP :: ResultPair .
	eq getRedResult(FM, T) = redError('Failed 'to 'evaluate 'term '\r '\n eMetaPrettyPrint(FM, T), 'getRedResult) .

	eq getObsOp(([(bop OP : TyL -> Ty' ); (op OP' : TyL' -> 'OValue [none] .)] BOPL), OP) = 
		{OP', Ty'} .
	eq getObsOp(BOPL, OP) = opError('no 'corresponding 'observer 'for '\g OP '\o, 'getObsOp) [owise] .
	
	eq introVariable(OP, TL, Ty, ((OP[TL] <- T); EST)) = {T, ((OP[TL] <- T) ; EST)} .
	ceq introVariable(OP, TL, Ty, EST) = {V, ((OP[TL] <- V); EST)}
	  if V := qid("v" + string(OP) + term2string(TL) + ":" + string(Ty)) [owise] .
	

	ceq buildSingleRewritingRulesAux1(BOPL, OP, OP', T, TL, TL', FM, EST) = 
		{(rl OP''[TL', T'] => OP''[TL', T''] [none] .), EST'}
	  if {OP'', Ty} := getObsOp(BOPL, OP) /\
		  {T', EST'} := introVariable(OP, (T, TL'), Ty, EST) /\
		  T'' := getRedResult(FM, OP[OP'[T, TL], TL']) .

	ceq buildSingleRewritingRulesAux2(BOPL, (eq T = T' [Ats] .), T'', FM, EST) = 
		{Rls, EST'}
		if {Rls, EST'} := buildSingleRewritingRulesAux3(BOPL, T', T'', FM, EST) .

	eq buildSingleRewritingRulesAux2(BOPL, Eq, T'', FM, EST) = 
		singleRuleError(('unkown 'error),  ('\g 'buildSingleRewritingRulesAux2)) [owise] .

	ceq buildSingleRewritingRulesAux3(BOPL, OP[(T, TL)], OP'[T, TL'], FM, EST) =
		if BOP' :: Bop2op and T :: Variable then
			buildSingleRewritingRulesAux1(BOPL, OP, OP', T, TL', TL, FM, EST)
		else 
			singleRuleError('no 'observation 'for '\g OP, 'buildSingleRewritingRulesAux3) 
		fi
	  if BOP' := getBOP2OP(BOPL, OP) .

	****For termlist
 	ceq buildSingleRewritingRulesAux3(BOPL, (T', TL), T'', FM, EST) =
	    {(Rls Rls'), EST''} 
	  if TL =/= empty /\ 
	  	{Rls, EST'} := buildSingleRewritingRulesAux3(BOPL, T', T'', FM, EST) /\
		{Rls', EST''} := buildSingleRewritingRulesAux3(BOPL, TL, T'', FM, EST') .
		
	ceq buildSingleRewritingRulesAux3(BOPL, (T', TL), T'', FM, EST) =
	    singleRuleError(QIL, ('buildSingleRewritingRulesAux3 QIL'))
	  if TL =/= empty /\ 
	  	singleRuleError(QIL, QIL') := buildSingleRewritingRulesAux3(BOPL, T', T'', FM, EST) .
	
	ceq buildSingleRewritingRulesAux3(BOPL, (T', TL), T'', FM, EST) =
	    singleRuleError(QIL, ('buildSingleRewritingRulesAux3 QIL'))
	  if TL =/= empty /\ 
	  	{Rls, EST'} := buildSingleRewritingRulesAux3(BOPL, T', T'', FM, EST) /\
		singleRuleError(QIL, QIL') := buildSingleRewritingRulesAux3(BOPL, TL, T'', FM, EST') .
	
	***for a single term
	eq buildSingleRewritingRulesAux3(BOPL, OP[TL], T'', FM, EST) =
		buildSingleRewritingRulesAux3(BOPL, TL, T'', FM, EST) [owise] .

	ceq buildSingleRewritingRulesAux3(BOPL, T, T', FM, EST) =  
		{none, EST} 
	   if T :: Variable or T :: Constant .
	   
    eq buildSingleRewritingRulesAux3(BOPL, T, T', FM, EST) =  
	   singleRuleError('unkown 'error,  '\g 'buildSingleRewritingRulesAux3)	[owise] .


*************************************************************************
	***BUILDING REWRITING RULE FOR EACH EQUATION WITHOUT CONDITION
		
		***KEY Equation to construct a rewrite rule for an observer
		***OP' : Observer
		***OP : Transition
	***ceq buildSingleRewritingRules(BOPL, (ceq T = T' if EqC [Ats] . ), FM, EST) = 
	***	  buildSingleRewritingRulesAux1(BOPL, OP', OP, T'', TL, TL', FM, EST)
	***	if OP'[OP[T'', TL], TL'] := T .

	ceq buildSingleRewritingRules(BOPL, (eq T = T' [Ats] . ), FM, EST) = 
		  buildSingleRewritingRulesAux1(BOPL, OP', OP, T'', TL, TL', FM, EST)
		if OP'[OP[T'', TL], TL'] := T .

	ceq buildSingleRewritingRules(BOPL, (Eq EqS), FM, EST) = 
		{Rl Rls, EST''}
	  if  EqS =/= none /\
		  {Rl , EST'} := buildSingleRewritingRules(BOPL, Eq, FM, EST) /\
		  {Rls, EST''} := buildSingleRewritingRules(BOPL, EqS, FM, EST') .
	
	ceq buildSingleRewritingRules(BOPL, (Eq EqS), FM, EST) = 
		singleRuleError(QIL, 'buildSingleRewritingRules QIL')
	  if  EqS =/= none /\
		  {Rl , EST'} := buildSingleRewritingRules(BOPL, Eq, FM, EST) /\
		  singleRuleError(QIL, QIL') := buildSingleRewritingRules(BOPL, EqS, FM, EST') .	
	
	ceq buildSingleRewritingRules(BOPL, (Eq EqS), FM, EST) = 
		singleRuleError(QIL, 'buildSingleRewritingRules QIL')
	  if EqS =/= none /\
		  singleRuleError(QIL, QIL') := buildSingleRewritingRules(BOPL, Eq, FM, EST) .
	
	eq buildSingleRewritingRules(BOPL, none, FM, EST) = 
		{none, EST} .
	
	eq buildSingleRewritingRules(BOPL, EqS, FM, EST) = 
		singleRuleError('unrecognized 'equation 'found! eMetaPrettyPrint(FM, EqS), 'buildSingleRewritingRules) [owise] .
		
	***BUILDING REWRITING RULE FOR EACH EQUATION WITH CONDITIONS
	****************************************************************************************************
		***KEY Equation to construct a rewrite rule for an observer
		***OP' : Observer
		***OP : Transition
		
	***Rls is not used after being assigned
	***buildSingleRewritingRulesAux is used for???

	ceq buildSingleRewritingRules(BOPL, (ceq T = T' if EqC [Ats] . ), Eq, FM, EST) = 
		  {(Rls Rls'), EST''}
		if OP'[OP[T'', TL], TL'] := T /\ 
		{Rls, EST'} := buildSingleRewritingRulesAux1(BOPL, OP', OP, T'', TL, TL', FM, EST) /\
		{Rls', EST''} := buildSingleRewritingRulesAux2(BOPL, Eq, OP[T'', TL], FM, EST') .

	ceq buildSingleRewritingRules(BOPL, (ceq T = T' if EqC [Ats] . ), Eq, FM, EST) = 
		  singleRuleError(QIL, 'buildSingleRewritingRules QIL')
		if OP'[OP[T'', TL], TL'] := T /\ 
		{Rls, EST'} := buildSingleRewritingRulesAux1(BOPL, OP', OP, T'', TL, TL', FM, EST) /\
		singleRuleError(QIL, QIL') := buildSingleRewritingRulesAux2(BOPL, Eq, OP[T'', TL], FM, EST') .

	ceq buildSingleRewritingRules(BOPL, (Eq EqS), Eq', FM, EST) = 
		{Rls' Rls, EST''}
	  if  EqS =/= none /\
		  {Rls' , EST'} := buildSingleRewritingRules(BOPL, Eq, Eq', FM, EST) /\
		  {Rls, EST''} := buildSingleRewritingRules(BOPL, EqS, Eq', FM, EST') .
		  
	ceq buildSingleRewritingRules(BOPL, (Eq EqS), Eq', FM, EST) = 
		singleRuleError(QIL, 'buildSingleRewritingRules QIL')
	  if  EqS =/= none /\
		  singleRuleError(QIL, QIL') := buildSingleRewritingRules(BOPL, Eq, Eq', FM, EST) .
		  
	ceq buildSingleRewritingRules(BOPL, (Eq EqS), Eq', FM, EST) = 
		singleRuleError(QIL, 'buildSingleRewritingRules QIL')
	  if  EqS =/= none /\
		  {Rl , EST'} := buildSingleRewritingRules(BOPL, Eq, Eq', FM, EST) /\
		  singleRuleError(QIL, QIL')  := buildSingleRewritingRules(BOPL, EqS, Eq', FM, EST') .
		  
	eq buildSingleRewritingRules(BOPL, none, Eq', FM, EST) = 
		{none, EST} .

	eq buildSingleRewritingRules(BOPL, EqS, Eq', FM, EST) = 
		singleRuleError('unrecognized 'equation 'found!  eMetaPrettyPrint(FM, (Eq' EqS)), 'buildSingleRewritingRules) [owise] .	

	****************************************************************************************************
	ceq substitute((Rl Rls), EST) = 
		substitute(Rl, EST) substitute(Rls, EST)
	  if Rls =/= none .

	eq substitute((rl T => T' [Ats] .), EST) =
		(rl substituteAux(T, EST) => substituteAux(T', EST) [Ats] .) . 
	
	eq substitute(none, EST) = ruleError('none 'related 'equations 'defined, 'substitute) .

	ceq substituteAux((T, TL), EST) = 
		(substituteAux(T, EST), substituteAux(TL, EST)) 
	  if TL =/= empty . 
	
	eq substituteAux(empty, EST) = empty .

	ceq substituteAux(T, EST) = T if T :: Constant or T :: Variable .
	***eq substituteAux(T, EST) = T [owise] .

	eq substituteAux(OP[TL], ((OP[TL] <- T); EST)) = T . 
	eq substituteAux(OP[TL], EST) = OP[substituteAux(TL, EST)] [owise] .

	
	ceq combineRwRules(Rls, EST, OP) = 
		combineRwRulesAux(Rls', OP)
	  if Rls' := substitute(Rls, EST) .
	

	eq combineRwRules(Rls, EST, OP) = ruleError('Failed 'to 'combine 'rules, 'combineRwRules) [owise] .
	
	eq combineRwRulesAux((rl T => T' [Ats] .), OP) = (rl T => T' [Ats label(OP)] .) .
	ceq combineRwRulesAux(Rls, OP) = 
		(rl '__[TL] => '__[TL'] [label(OP)] .) 
	  if not (Rls :: Rule) /\
		  {TL, TL'} := combineRwRulesAux1(Rls) .
	ceq combineRwRulesAux1(((rl T => T' [Ats] .) Rls)) = 
		{(T, TL), (T', TL')}
	  if Rls =/= none /\
	  {TL, TL'} := combineRwRulesAux1(Rls) .
	eq combineRwRulesAux1(rl T => T' [Ats] .) =
		{T, T'} .
		
		
	**********************************************************************************
	***split condition
	eq splitConditionEq((eq T = '_or_[T', T''] [Ats] .)) = 
		((eq T = T' [Ats] .) splitConditionEq((eq T = T'' [Ats] .))) .
	eq splitConditionEq(eq T = T' [Ats] .) = (eq T = T' [Ats] .) .
	**********************************************************************************
	***evaluate effective conditions
	ceq evaluateCondEq((BOP BOPL), Eq) = (evaluateCondEq(BOP, Eq) ; evaluateCondEq(BOPL, Eq)) if BOPL =/= nil .
	eq evaluateCondEq([(bop OP : Ty TyL -> Ty' ) ; (op OP' : TyL' -> 'OValue [none] .)], (eq T = T' [Ats] .)) =
		evaluateCondEqAux1(OP, OP', Ty', T', none) .
	
	ceq evaluateCondEqAux1(OP, OP', Ty', F[T, T'], EST) = 
		evaluateCondEqAux1(OP, OP', Ty', T', EST') 
	  if F == '_/\_ /\ EST' := evaluateCondEqAux1(OP, OP', Ty', T, EST) .

	ceq evaluateCondEqAux1(OP, OP', Ty', F[T, T'], EST) = 
		substitutionError(QIL, 'evaluateCondEqAux1 QIL')
	  if F == '_/\_ /\ 
	  substitutionError(QIL, QIL') := evaluateCondEqAux1(OP, OP', Ty', T, EST) .

	
	ceq evaluateCondEqAux1(OP, OP', Ty', F[T, T'], EST) = 
		evaluateCondEqAux1(OP, OP', Ty', T', EST') 
	  if F == '_and_ /\ EST' := evaluateCondEqAux1(OP, OP', Ty', T, EST) .

	ceq evaluateCondEqAux1(OP, OP', Ty', F[T, T'], EST) = 
		substitutionError(QIL, 'evaluateCondEqAux1 QIL')
	  if F == '_and_ /\ 
	  substitutionError(QIL, QIL') := evaluateCondEqAux1(OP, OP', Ty', T, EST) .
	
	ceq evaluateCondEqAux1(OP, OP', Ty, F[T, T'], EST) = 
		evaluateCondEqAux2(OP, TL, Ty, T, EST) 
	  if (F == '_\in_ or F == '_in_)  /\
	    OP[TL] := T' .
	
	ceq evaluateCondEqAux1(OP, OP', Ty, F[T, T'], EST) = 
		evaluateCondEqAux4(OP, TL, T', EST) 
	  if (F == '_==_ or F == '_=_)   /\
	    OP[TL] := T .

	ceq evaluateCondEqAux1(OP, OP', Ty, F[T, T'], EST) = 
		substitutionError('Cannot 'support 'disjunction 'now!, 'evaluateCondEqAux1)
	  if F == '_\/_ .
	
	eq evaluateCondEqAux1(OP, OP', Ty, T, EST) = EST [owise] .

	eq evaluateCondEqAux4(OP, TL, T, ((OP[TL] <- T') ; EST)) = 
		(OP[TL] <- T ; EST) .
	eq evaluateCondEqAux4(OP, TL, T, EST) = 
		(OP[TL] <- T ; EST) [owise] .

	ceq evaluateCondEqAux2(OP, TL, Ty', T, ((OP[TL] <- T') ; EST)) = 
		((OP[TL] <- '__[TL', T]) ; EST)
	  if '__[TL'] := T' .

	eq evaluateCondEqAux3(OP, TL, Ty', T, ((OP[TL] <- T') ; EST)) = 
		substitutionError('Condition 'conflict 'for 'operator '\g OP '\o, 'evaluateCondEqAux3) .
	
	eq evaluateCondEqAux3(OP, TL, Ty', T, EST) = 
		((OP[TL] <- T); EST) [owise] .
	
	eq evaluateCondEqAux2(OP, TL, Ty', T, EST) = 
		((OP[TL] <- '__[T, qid("v" + string(Ty') + ":" + string(Ty'))]); EST) [owise] .

	**************************************************************************************

	ceq addConditionPart((rl T2 => T3 [Ats'] .), (eq T = T' [Ats] .), OPDS, EST', FM, OP) = 
	  if T1 == 'true.Bool then
		(rl T2 => T3 [Ats'] .)
	  else 
		(crl T2 => T3 if T'' = 'true.Bool [Ats'] .)
		fi
	  if T'' := substituteAux(T', EST') /\
		  RP := metaReduce(FM, T'') /\
		  RP :: ResultPair /\
		  T1 := getTerm(RP) .
		  
	eq addConditionPart(Rl, Eq, OPDS, EST', FM, OP) = 
		ruleError('Failed 'to 'add 'condition 'part 'for '\g OP '\o, 'addConditionPart) [owise] .


	*****************************************************************************************
		
	ceq filterVariable(TL, (T, TL')) =
	  if not inVars(T, TL) then (T, filterVariable(TL, TL')) else filterVariable(TL, TL') fi 
	if TL' =/= none .
	
	eq filterVariable(TL, empty) = empty .	
	
	ceq getBadVariables(T, T') = 
		filterVariable(TL, TL') 
	  if TL := getVariables(T) /\
		  TL' := getVariables(T') .

	***726**********************************************************************************
	***what about if TL is not empty
	ceq addAuxiliaryOps((crl T => T' if EqC [Ats] .), OPDS, OP) = 
		(crl T => T' if EqC [Ats] .)
	  if TL := getBadVariables(T, T') /\
		  TL == empty  .

	ceq addAuxiliaryOps((crl T => T' if EqC [Ats] .), OPDS, OP) = 
		(crl T1 => T2 if EqC [Ats] .)
	  if TL := getBadVariables(T, T') /\
		  TL =/= empty /\
		  {T1, T2} := buildAuxiliaryOps(TL, T, T', OPDS, OP) .

	ceq addAuxiliaryOps((crl T => T' if EqC [Ats] .), OPDS, OP) = 
		ruleError(QIL, 'addAuxiliaryOps QIL')
	  if TL := getBadVariables(T, T') /\
		  TL =/= empty /\
		  termError(QIL, QIL') := buildAuxiliaryOps(TL, T, T', OPDS, OP) .

	ceq addAuxiliaryOps((rl T => T' [Ats] .), OPDS, OP) = 
		(rl T1 => T2 [Ats] .)
	  if TL := getBadVariables(T, T') /\
		  TL =/= empty /\
		  {T1, T2} := buildAuxiliaryOps(TL, T, T', OPDS, OP) .
	
	ceq addAuxiliaryOps((rl T => T' [Ats] .), OPDS, OP) = 
		ruleError(QIL, 'addAuxiliaryOps QIL')
	  if TL := getBadVariables(T, T') /\
		  TL =/= empty /\
		  termError(QIL, QIL') := buildAuxiliaryOps(TL, T, T', OPDS, OP) .

	ceq addAuxiliaryOps((rl T => T' [Ats] .), OPDS, OP) = 
		(rl T => T' [Ats] .)
	  if TL := getBadVariables(T, T') /\
		  TL == empty .
	
	eq addAuxiliaryOps(Rl, OPDS, OP) = 
		ruleError('Failed 'to 'add 'Auxiliary 'observors 'for '\g OP '\o, 'addAuxiliaryOps) [owise] .

		 
	eq isAlreadyExisted(OP, '__[TL]) = isAlreadyExistedAux(OP, TL) . 
	eq isAlreadyExisted(OP, (OP[TL])) = true .
	eq isAlreadyExisted(OP, T) = false [owise] .
	eq isAlreadyExistedAux(OP, (T, TL)) = 
		if isAlreadyExisted(OP, T) then true else isAlreadyExistedAux(OP, TL) fi .
	eq isAlreadyExistedAux(OP, empty) = false .

	eq getAuxOps(OPDS, T, Ty) = getAuxOpsAux1(OPDS, T, qid(string(Ty) + "Set")) .
	eq getAuxOpsAux1(((op OP : Ty -> 'OValue [ctor] .) OPDS), T, Ty) = 
	  if not isAlreadyExisted(OP, T) then OP else getAuxOpsAux1(OPDS, T, Ty) fi .
	
	ceq buildAuxiliaryOps((T, TL), T1, T2, OPDS, OP) = 
		buildAuxiliaryOps(TL, ('__[TL', T'']), ('__[TL'', T'']), OPDS, OP)
	  if T :: Variable /\
		  Ty := getType(T) /\
		OP' := getAuxOps(OPDS, T1, Ty) /\
		T'' := OP'['__[T, qid("vs" + string(getName(T)) + ":" + string(Ty) + "Set")]] /\
		  '__[TL'] := T1 /\
		  '__[TL''] := T2 .
	
	eq buildAuxiliaryOps(empty, T, T', OPDS, OP) = {T, T'} .
	
	eq buildAuxiliaryOps(TL, T, T', OPDS, OP) = 
		termError('Failed 'to 'add 'auxiliary 'observer 'for '\g OP '\o, 'buildAuxiliaryOps) [owise] .

	***********************************************************************************
	ceq buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) =
		Rl''
	  if {Rls, EST'} := buildSingleRewritingRules(BOPL, EqS, Eq, FM, EST) /\
		Rl := combineRwRules(Rls, EST', OP) /\
		Rl' :=	addConditionPart(Rl, Eq, OPDS, EST', FM, OP) /\
		Rl'' := addAuxiliaryOps(Rl', OPDS, OP) .

	ceq buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) =
		ruleError(QIL eMetaPrettyPrint(FM, (Eq EqS)), 'buildRewritingRulesAux6 QIL') 
	  if {Rls, EST'} := buildSingleRewritingRules(BOPL, EqS, Eq, FM, EST) /\
		Rl := combineRwRules(Rls, EST', OP) /\
		Rl' :=	addConditionPart(Rl, Eq, OPDS, EST', FM, OP) /\
		ruleError(QIL, QIL') := addAuxiliaryOps(Rl', OPDS, OP) .

	
	ceq buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) =
		ruleError(QIL, 'buildRewritingRulesAux6 QIL')
	  if singleRuleError(QIL, QIL') := buildSingleRewritingRules(BOPL, EqS, Eq, FM, EST) .
	  
	ceq buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) =
		ruleError(QIL, 'buildRewritingRulesAux6 QIL')
	  if {Rls, EST'} := buildSingleRewritingRules(BOPL, EqS, Eq, FM, EST) /\
		Rl := combineRwRules(Rls, EST', OP) /\
		ruleError(QIL, QIL') :=	addConditionPart(Rl, Eq, OPDS, EST', FM, OP) .

	eq buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) =
		ruleError('Unknown 'Eorror 'for '\g OP eMetaPrettyPrint(FM, (Eq EqS)), ''buildRewritingRulesAux6) [owise] .


	****************************************************************************************************
	***deal with condition part********
	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, (Eq EqS'), EqS, FM) = 
		 (Rl Rls)
	  if EqS' =/= none /\
	  	 EST := evaluateCondEq(BOPL, Eq) /\
	  	 Rl := buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) /\
	  	 Rls := buildRewritingRulesAux5(BOPL, OPDS, OP, EqS', EqS, FM) .

	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, (Eq EqS'), EqS, FM) = 
		 ruleError(QIL, 'buildRewritingRulesAux5 QIL')
	  if EqS' =/= none /\
	  	 EST := evaluateCondEq(BOPL, Eq) /\
	  	 Rl := buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) /\
	  	 ruleError(QIL, QIL') := buildRewritingRulesAux5(BOPL, OPDS, OP, EqS', EqS, FM) .

  	 
	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, (Eq EqS'), EqS, FM) = 
		 ruleError(QIL, 'buildRewritingRulesAux5 QIL') 
	  if EqS' =/= none /\
	  	 substitutionError(QIL, QIL') := evaluateCondEq(BOPL, Eq) .
			
	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, (Eq EqS'), EqS, FM) = 
		 ruleError(QIL, 'buildRewritingRulesAux5 QIL')
	  if EqS' =/= none /\
	  	 EST := evaluateCondEq(BOPL, Eq) /\
	  	 ruleError(QIL, QIL') := buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST) .

	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, Eq, EqS, FM) = 
		 buildRewritingRulesAux6(BOPL, OPDS, OP, Eq, EqS, FM, EST)
	  if EST := evaluateCondEq(BOPL, Eq) .
	  	 
	ceq buildRewritingRulesAux5(BOPL, OPDS, OP, Eq, EqS, FM) = 
		 ruleError(QIL, 'buildRewritingRulesAux5 QIL') 
	  if substitutionError(QIL, QIL') := evaluateCondEq(BOPL, Eq) .

	eq buildRewritingRulesAux5(BOPL, OPDS, OP, none, EqS, FM) = 
		ruleError('cannot 'find 'related 'equation 'as 'condition 'for '\g OP, 'buildRewritingRulesAux5) .

	
	
	eq buildRewritingRulesAux4(BOPL, OPDS, OP, EqS, FM) =
	    ruleError('no 'effective 'condition, 'buildRewritingRulesAux4) [owise] .
	
	ceq buildRewritingRulesAux4(BOPL, OPDS, OP, EqS, FM) = 
		Rl'
	  if {Rls, EST} := buildSingleRewritingRules(BOPL, EqS, FM, none) /\
							 Rl := combineRwRules(Rls, EST, OP) /\
							Rl' := addAuxiliaryOps(Rl, OPDS, OP) .

	ceq buildRewritingRulesAux4(BOPL, OPDS, OP, EqS, FM) = 
		ruleError(QIL eMetaPrettyPrint(FM, EqS), 'buildRewritingRulesAux4 QIL') 
	  if {Rls, EST} := buildSingleRewritingRules(BOPL, EqS, FM, none) /\
	Rl := combineRwRules(Rls, EST, OP) /\
	ruleError(QIL, QIL') := addAuxiliaryOps(Rl, OPDS, OP) .

	ceq buildRewritingRulesAux4(BOPL, OPDS, OP, EqS, FM) = 
		ruleError(QIL, 'buildRewritingRulesAux4 QIL')
	  if singleRuleError(QIL, QIL') := buildSingleRewritingRules(BOPL, EqS, FM, none) .

	eq getEffectiveCondEq(OP, ((eq OP[TL] = T [Ats] .) EqS)) = (eq OP[TL] = T [Ats] .) .
	eq getEffectiveCondEq(OP, EqS) = none [owise] . 
	eq getRelatedEqsWRTObs(OP, ((ceq OP'[OP[TL], TL'] = T if EqC [Ats] .) EqS)) = 
		  ((ceq OP'[OP[TL], TL'] = T if EqC [Ats] .) getRelatedEqsWRTObs(OP, EqS)) .
	eq getRelatedEqsWRTObs(OP, ((eq OP'[OP[TL], TL'] = T [Ats] .) EqS)) = 
		  ((eq OP'[OP[TL], TL'] = T [Ats] .) getRelatedEqsWRTObs(OP, EqS)) .
	eq getRelatedEqsWRTObs(OP, EqS) = none [owise] .
	
	
	*************************************************************************conditions
	ceq buildRewritingRulesAux3(BOPL, OPDS, OP, Eq, EqS, FM) = 
		buildRewritingRulesAux5(BOPL, OPDS, OP, EqS', EqS, FM) 
	if EqS' := splitConditionEq(Eq) .

	************************************************************************************
	ceq buildRewritingRulesAux2(BOPL, OPDS, OP, FM, FM') = 
	  if EqS =/= none then
		if EQ =/= none then
			buildRewritingRulesAux3(BOPL, OPDS, OP, EQ, EqS, FM') 
		  else 
			buildRewritingRulesAux4(BOPL, OPDS, OP,  EqS, FM')
		  fi		
		else
		  ruleError('no 'related 'equation 'defined 'for '\g OP '\o '!, 'buildRewritingRulesAux2)		
		fi
	  if EqS' := getEqs(FM) /\
		EQ := getEffectiveCondEq(qid("c-" + string(OP)), EqS') /\
		EqS := getRelatedEqsWRTObs(OP, EqS') .
	
	eq buildRewritingRulesAux2(BOPL, OPDS, OP, FM, FM') = 
		ruleError('unkown 'error 'when 'processing 'transition '\g OP '\o, 'buildRewritingRulesAux2) [owise] .
		
	***********************************************************************************
	ceq buildRewritingRulesAux1(BOPL, OPDS, ((bop OP : TyL -> Ty ) OTSDS), FM, FM') = 
		(Rls Rls') 
	  if Rls := buildRewritingRulesAux2(BOPL, OPDS, OP, FM, FM') /\
	     Rls' := buildRewritingRulesAux1(BOPL, OPDS, OTSDS, FM, FM') .

	ceq buildRewritingRulesAux1(BOPL, OPDS, ((bop OP : TyL -> Ty ) OTSDS), FM, FM') = 
		ruleError(QIL, 'buildRewritingRulesAux1 QIL')
	  if Rls := buildRewritingRulesAux2(BOPL, OPDS, OP, FM, FM') /\
	     ruleError(QIL, QIL') := buildRewritingRulesAux1(BOPL, OPDS, OTSDS, FM, FM') .

	ceq buildRewritingRulesAux1(BOPL, OPDS, ((bop OP : TyL -> Ty ) OTSDS), FM, FM') = 
		ruleError(QIL, 'buildRewritingRulesAux1 QIL')
	  if ruleError(QIL, QIL') := buildRewritingRulesAux2(BOPL, OPDS, OP, FM, FM') .

	eq buildRewritingRulesAux1(BOPL, OPDS, none, FM, FM') = none .
	
	****************************************************************
	ceq buildRewritingRules(BOPL, OPDS, OTSDS, FM, FM') = 
		Rls
	  if FM'' := rmEffectiveConds(OTSDS, FM') /\
	  	  Rls := buildRewritingRulesAux1(BOPL, OPDS, OTSDS, FM, FM'') .
	
	ceq buildRewritingRules(BOPL, OPDS, OTSDS, FM, FM') = 
		ruleError(QIL, 'buildRewritingRules QIL')
	  if FM'' := rmEffectiveConds(OTSDS, FM') /\
	  	  ruleError(QIL, QIL') := buildRewritingRulesAux1(BOPL, OPDS, OTSDS, FM, FM'') .  	
	
	eq buildRewritingRules(BOPL, OPDS, none, FM, FM') = none .
	eq buildRewritingRules(BOPL, OPDS, OTSDS, FM, FM') = 
		ruleError('Unkown 'error 'when 'generating 'rules!, 'buildRewritingRules) [owise] .
	***************************************************************************************************************
	eq rmEffectiveConds(OTSDS, FM') = setEqs(FM', rmEffectiveCondEqs(OTSDS, getEqs(FM'))) .
	eq rmEffectiveCondEqs(((bop OP : TyL -> Ty ) OTSDS), EqS) = 
		rmEffectiveCondEqsAux(qid("c-" + string(OP)), rmEffectiveCondEqs(OTSDS, EqS)) .
	eq rmEffectiveCondEqs(none, EqS) = EqS .
	
	eq rmEffectiveCondEqsAux(OP, (ceq T = T' if OP[TL] = 'true.Bool [Ats] .) EqS) = 
		  rmEffectiveCondEqsAux(OP, ((eq T = T' [Ats] .) EqS)) .
	eq rmEffectiveCondEqsAux(OP, EqS) = EqS [owise] .

	eq buildRewModAux1(BOPL, OTSM, SM, FM, FM') =
		convError('Cannot 'get 'parameters 'of 'transition 'operators, 'buildRewModAux1) [owise] .


    ceq buildRewMod(BOPL, OTSM, SM, H, DB) = 
		buildRewModAux1(BOPL, OTSM, SM, FM, FM')
		if FM := getInternalModule(getName(OTSM), DB) /\
		   FM' := getFlatModule(H, DB) .


    eq buildRewMod(BOPL, OTSM, SM, H, DB) = convError('Unkown 'error 'occured!, 'buildRewMod) [owise] .

endfm

fmod META-MAST-SIGNATURE is
	including META-LEVEL .
	including META-FULL-MAUDE-SIGN .
	
	op OTS-GRAMMAR : -> FModule .
	*** add meta-signature of your customized input languages here
	*** Module OTS-META-SIGN includes syntax definition of both
	*** behavioral specification and customized commands
	eq OTS-GRAMMAR = addImports((including 'OTS-META-SIGN .), GRAMMAR ) .

endfm


fmod MAST-BANNER is
	protecting STRING .
	
	op mast-banner : -> String .
	eq mast-banner = "OTS/CafeOBJ2MAUDE, An extension of MAST:  Jun. 2009!" .
endfm

mod MAST-PARSING-STRATEGIES is
	protecting OTS-PARSER .
endm

fmod MAST-TRANSLATION-STRATEGIES is
	 protecting OMG-RWMODULE-STRATEGY .
endfm

mod MAST-DATABASE-HANDLING is
     protecting MAST-TRANSLATION-STRATEGIES .
     protecting MAST-PARSING-STRATEGIES .
     
     sort OTSDatabaseClass .
     subsort OTSDatabaseClass < DatabaseClass .

     op otsDatabase : -> OTSDatabaseClass [ctor] .
     op otsModule :_    : OTSModule -> Attribute [ctor] .
     


     var N 				: Nat .
     var X@Database 		        : DatabaseClass .
     var OTSDB                          : OTSDatabaseClass .
     var OTSM                           : OTSModule .
     var O 				: Oid .
     var QI 				: Qid .
     vars QIL QIL' QIL''	        : QidList .
     vars T T' T''		        : Term .
     vars H H'			        : Header .
     var Q 				: Qid .
     vars DB DB' DB''           	: Database .
     var F					: Qid .
     vars MD SM	SM'	SM''		: SModule .
     var Atts 			        : AttributeSet .
     vars RP RP'			: ResultPair? .
     vars ME ME' ME''	                : ModuleExpression . 
     vars BOPL                          : Bop2opList .

     ***if the input is a ots module, then switch the database to ots database
     ***in case of the first time

     crl [databaseSwitch] : 
         < O         : X@Database | 
           input     : (F[T, T']), Atts > => 
         < O         : otsDatabase | 
           input     : (F[T, T']),
           otsModule : emptyOTSModule, 
           Atts  >
         if (F == 'mod*_`{_`} or F == 'mod!_`{_`}) 
            and not (X@Database :: OTSDatabaseClass) .
             

     *** Do not need to process the built-in dabatase.
     crl [load-OTS-LOOSE] :
                    < O 			: OTSDB |
		     input			: (F['otsToken[T], T']),
                     db                         : DB,
		     output			: nil, 
                     otsModule                  : OTSM, 
                     default                    : ME,
		     Atts > =>
	           < O 				: OTSDB |
		     input			: nilTermList,
                     db                         : procOTSModule(F['otsToken[T], T'], DB),
		     output			: ('\n 'Introduced 'Loose 'OTS 'Module: '\g header2Qid(parseHeader('token[T])) '\o),
                     otsModule                  : parseOTS(F['otsToken[T], T']),
                     default                    : parseHeader('token[T]),
	             Atts   >
	           if F == 'mod*_`{_`} .

     crl [load-OTS-TIGHT] :
                    < O 	: OTSDB      |
		     		input	: (F['otsToken[T], T']),
                     db     : DB,
		     output			: nil, 
                     default                    : ME,
		     Atts > =>
	           < O 				: OTSDB      |
		     input			: nilTermList,
                     db                         : procOTSModule(F['otsToken[T], T'], DB),
		     output			: ('\n 'Introduced 'Tight 'OTS 'Module: '\g header2Qid(parseHeader('token[T])) '\o),
                     default                    : parseHeader('token[T]),
	             Atts   >
	           if F == 'mod!_`{_`} .	
	 
     crl [show-OTS-Module] : < O 				: X@Database |
		    	       db				: DB,
		     	       input			        : ('show`OTS`Module_.[T]),
		     	       default		                : ME,
		     	       output			        : nil,   Atts > =>
			     < O 				: X@Database |
			       db		                : DB',
			       input			        : nilTermList,
			       default	                        : ME,
			       output			        : eMetaPrettyPrint(getFlatModule(ME', DB'), getTopModule(ME', DB')),
							 Atts   > 
	       if < DB' ; ME' > := evalModExp(parseModExp(T), DB) .
	       
   crl [new-strategy] : 
		< O         : OTSDB | 
		  db        : DB,
          input     : ('conv2maude`..@Command@),
          otsModule  : OTSM,
          output    : nil,
          default   : H,
          Atts > => 
       < O          : OTSDB |
         db         : DB',
         input      : nilTermList,
         otsModule  : OTSM, 
         default    : H, 
         output     : ('\n 'Rewrite 'module '\g getName(SM') '\o 'is 'generated 'successfully),
         Atts >
       if < BOPL ; SM > := convert2sysm(OTSM) /\
                   SM'  := buildRewMod(BOPL, OTSM, SM, H, DB) /\
                   DB'  := insTermModule(getName(SM'), SM', DB) .

  crl [new-strategy-error] : 
		< O         : OTSDB | 
		  db        : DB,
          input     : ('conv2maude`..@Command@),
          otsModule  : OTSM,
          output    : nil,
          default   : H,
          Atts > => 
       < O          : OTSDB |
         db         : DB,
         input      : nilTermList,
         otsModule  : OTSM, 
         default    : H, 
         output     : ('\r 'ERROR: QIL '\n 'Execution 'sequence: QIL'),
         Atts >
       if < BOPL ; SM > := convert2sysm(OTSM) /\
                   convError(QIL, QIL')  := buildRewMod(BOPL, OTSM, SM, H, DB) .


endm



mod MAST-INTERFACE is
	extending LOOP-MODE .
	protecting META-MAST-SIGNATURE .
	protecting MAST-BANNER .
    protecting MAST-DATABASE-HANDLING .
	
	subsort Object < State .
	op o : -> Oid .
	
	var H 				: Header .
	var O 				: Oid .
	var X@Database 		        : DatabaseClass .
	var QI 				: Qid .
	vars QIL QIL' QIL''             : QidList .
	var TL 				: TermList .
	var DB 				: Database .
	var Atts 			: AttributeSet .

	op init 			: -> System .
	
	
	
	rl [init] : init => [nil,
						 < o		: Database | 
						   db		: initialDatabase, 
						   input 	: nilTermList , 
                                                   default      : 'CONVERSION ,
						   output 	: nil >,
						 ('\s '\s '\s '\s '\s '\g string2qidList(mast-banner) '\o)] .
	
	rl [input] : 	[QI QIL, 
					< O 			: X@Database | 
					  input 		: nilTermList, 
					  output 		: nil, Atts >,  
				 	  QIL' ] => 
			  		if metaParse(OTS-GRAMMAR, QI QIL, '@Input@) :: ResultPair
				  	then
				  	  [nil, 
				  	  < O 			: X@Database | 
				  	    input 		: getTerm(metaParse(OTS-GRAMMAR, QI QIL, '@Input@)), 
				  	    output 		: nil, Atts >, 
				  	  QIL']
				  	else 
					  [nil, 
					  < O 			: X@Database | 
					    input 		: nilTermList, 
					    output 		: ('\r 'WARNING: '\o printSyntaxError(metaParse(OTS-GRAMMAR, QI QIL, '@Input@), QI QIL) '\n 
					   'ERROR: 'No 'parse 'for 'input.), Atts >, 
					  QIL' ]
				  	fi .
				  	
	rl 	[output] : 	[QIL, < O 		: X@Database | 
							output 	: (QI QIL'), Atts >,
						   QIL''] =>
	  				[QIL, < O 		: X@Database | 
	  						output 	: nil, Atts >, (QI QIL' QIL'')] .
endm

set show loop stats off .
set show loop timing off .

loop init .

trace exclude OTS-INTERFACE .
set show loop stats on .
set show loop timing on .
set show advisories on .