(fmod METAMOD is
  including META-LEVEL .
  protecting SET[Qid] .

  op fst : ResultPair -> Term .

  var T : Term .
  var S : Substitution .

  eq fst({ T, S }) = T .

  op getLabels : Module -> Set[Qid] .
  op getLabels : RuleSet -> Set[Qid] .

  var IL : ImportList .
  var SD : SortDecl .
  var SDS : SubsortDeclSet .
  var ODS : OpDeclSet .
  var VDS : VarDeclSet .
  var MS : MembAxSet .
  var ES : EquationSet .
  var RS : RuleSet .
  var Q : Qid .
  vars T' T'' T''' : Term .

  eq getLabels((mod T is IL SD SDS ODS VDS MS ES RS endm)) = getLabels(RS) .
  eq getLabels(none) = (empty).Set`[Qid`] .
  eq getLabels((rl [ Q ] : T => T' .) RS) = union(singletonSet(Q), getLabels(RS)) .
  eq getLabels((crl [ Q ] : T => T' if T'' = T''' .) RS) = union(singletonSet(Q), getLabels(RS)) .
endfm)


(fth MOD-CONTROL is
  including META-LEVEL .
  protecting PROCESS .

  op mod : -> Module .
  op term : -> Term .
  op control : -> Process .
endfth)

(view Pair`[Term`,Process`] from TRIV to PAIR[Term, Process] is
  sort Elt to Pair[Term, Process] .
endv)

(fmod ENGINE[M :: MOD-CONTROL] is
  protecting METAMOD .
  protecting MULTISET[Term] .
  protecting SET[Pair`[Term`,Process`]] .
  protecting MULTISET[Action] .

  op getMsg : Term -> MultiSet[Term] .

  vars Q Q' : Qid .
  vars T T' T'' : Term .
  var TL : TermList .

  eq getMsg({ Q } Q') = if (meta-reduce(mod, ({ Q } Q') : 'Msg) == { 'true } 'Bool)
                        then singletonMultiSet({ Q } Q')
                        else (empty).MultiSet`[Term`] fi .
  ceq getMsg(Q[TL]) = if (meta-reduce(mod, Q[TL] : 'Msg) == { 'true } 'Bool)
                      then singletonMultiSet(Q[TL])
                      else (empty).MultiSet`[Term`] fi
        if Q =/= '__ .
  eq getMsg('__[T, T']) = union(getMsg(T), getMsg(T')) .
  ceq getMsg('__[T, TL]) = union(getMsg(T), getMsg('__[TL]))
        if not (TL : Term) .

  op inMsg : Term -> Action .
  op inMsg : MultiSet[Term] -> MultiSet[Action] .
  op inMsg : Term MultiSet[Term] -> MultiSet[Action] .

  var TM : MultiSet[Term] .

  eq inMsg(Q[TL]) = act(conc('?, Q)) .
  eq inMsg({ Q } Q') = act(conc('?, Q)) .
  eq inMsg(empty) = empty .
  eq inMsg(TM) = if TM == empty
                 then (empty).MultiSet`[Action`]
                 else inMsg(choose(TM), TM) fi .
  eq inMsg(T, TM) = union(singletonMultiSet(inMsg(T)), inMsg(diff(TM, singletonMultiSet(T)))) .

  op outMsg : Term -> Action .
  op outMsg : MultiSet[Term] -> MultiSet[Action] .
  op outMsg : Term MultiSet[Term] -> MultiSet[Action] .

  eq outMsg(Q[TL]) = act(conc('!, Q)) .
  eq outMsg({ Q } Q') = act(conc('!, Q)) .
  eq outMsg(empty) = empty .
  eq outMsg(TM) = if TM == empty
                  then (empty).MultiSet`[Action`]
                  else outMsg(choose(TM), TM) fi .
  eq outMsg(T, TM) = union(singletonMultiSet(outMsg(T)), outMsg(diff(TM, singletonMultiSet(T)))) .

  op inoutMsg : Term Term -> MultiSet[Action] .

  var TM' : MultiSet[Term] .

  eq inoutMsg(T, T') = union(inMsg(diff(getMsg(T), getMsg(T'))), outMsg(diff(getMsg(T'), getMsg(T)))) .

  op allRewrites : Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .
  op allRewrites : Pair[Term, Process] Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .
  op allRewrites : Term Process -> Set[Pair`[Term`,Process`]] .
  op allRewrites : Set[Qid] Term Process -> Set[Pair`[Term`,Process`]] .
  op allRewrites : Qid Set[Qid] Term Process MachineInt -> Set[Pair`[Term`,Process`]] .

  var P : Process .
  var QS : Set[Qid] .
  var N : MachineInt .
  var TP : Pair[Term, Process] .
  var TPS : Set[Pair`[Term`,Process`]] .

  eq allRewrites(TPS) = if (TPS == empty)
                        then (empty).Set`[Pair`[Term`,Process`]`]
                        else allRewrites(choose(TPS), TPS) fi .
  eq allRewrites(TP, TPS) = union(allRewrites(fst(TP), snd(TP)), allRewrites(diff(TPS, singletonSet(TP)))) .
  eq allRewrites(T, P) = allRewrites(getLabels(mod), T, P) .
  eq allRewrites(QS, T, P) = if (QS == empty)
                             then (empty).Set`[Pair`[Term`,Process`]`]
                             else allRewrites(choose(QS), QS, T, P, 0) fi .
  eq allRewrites(Q, QS, T, P, N) =
       if (fst(meta-apply(mod, T, Q, none, N)) == error*)
       then allRewrites(diff(QS, singletonSet(Q)), T, P)
       else (if (acceptMultiSet(inoutMsg(T, fst(meta-apply(mod, T, Q, none, N))), P) == deadlock)
             then allRewrites(Q, QS, T, P, N + 1)
             else union(singletonSet(pair(fst(meta-apply(mod, T, Q, none, N)), acceptMultiSet(inoutMsg(T, fst(meta-apply(mod, T, Q, none, N))), P))), allRewrites(Q, QS, T, P, N + 1)) fi) fi .

  op accepting : -> Set[Pair`[Term`,Process`]] .
  op accepting : Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .

  eq accepting = accepting(singletonSet(pair(meta-reduce(mod, term), control))) .
  eq accepting(TPS) = if (TPS == empty)
                      then (empty).Set`[Pair`[Term`,Process`]`]
                      else union(final(TPS), accepting(allRewrites(reduce(TPS)))) fi .

  *** Compute final configurations, i.e. no rewrite rule is applicable
  *** Caution: should test whether a rewrite is applicable according
  *** to the process of the configuration
  op final : Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .
  op final : Pair[Term, Process] Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .

  eq final(TPS) = if (TPS == empty)
                  then (empty).Set`[Pair`[Term`,Process`]`]
                  else final(choose(TPS), TPS) fi .
  eq final(TP, TPS) = if (snd(TP) =/= deadlock) and (meta-rewrite(mod, fst(TP), 1) == fst(TP))
                      then union(singletonSet(TP), final(diff(TPS, singletonSet(TP))))
                      else final(diff(TPS, singletonSet(TP))) fi .

  op deadlocked : Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .
  op deadlocked : Pair[Term, Process] Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .

  eq deadlocked(TPS) = if (TPS == empty)
                       then (empty).Set`[Pair`[Term`,Process`]`]
                       else deadlocked(choose(TPS), TPS) fi .
  eq deadlocked(TP, TPS) = if (snd(TP) =/= deadlock)
                           then deadlocked(diff(TPS, singletonSet(TP)))
                           else union(singletonSet(TP), deadlocked(diff(TPS, singletonSet(TP)))) fi .

  op reduce : Set[Pair`[Term`,Process`]] -> Set[Pair`[Term`,Process`]] .

  eq reduce(TPS) = diff(diff(TPS, deadlocked(TPS)), final(TPS)) .
endfm)

eof