(fmod ACTION is
  including QID .
  sort Action .

  op act : Qid -> Action .
endfm)

(view Action from TRIV to ACTION is
  sort Elt to Action .
endv)

(view List`[Action`] from TRIV to LIST[Action] is
  sort Elt to List[Action] .
endv)


(fmod PROCESS is
  protecting SET[Action] .
  protecting LIST[Action] .
  protecting MULTISET[Action] .
  protecting LIST[List`[Action`]] .

  sort Process .
  subsort Action < Process .

  *** Process constructors
  op nil : -> Process .
  op deadlock : -> Process .
  op _;;_ : Process Process -> Process [ctor assoc prec 30] .
  op _++_ : Process Process -> Process [ctor assoc comm prec 35] .
  op _||_ : Process Process -> Process [ctor assoc comm prec 25] .
  op _** : Process -> Process [ctor prec 20] .

  *** Process normalisation
  op nf : Process -> Process .

  vars A A' : Action .
  vars P P1 P2 : Process .

  eq nf(A) = A .
  eq nf(nil) = nil .
  eq nf(deadlock) = deadlock .
  eq nf(nil ;; P) = nf(P) .
  eq nf(deadlock ;; P) = deadlock .
  eq nf(deadlock ++ P) = nf(P) .
  eq nf(P ++ P) = nf(P) .
  eq nf(nil || P) = nf(P) .
  eq nf(deadlock || P) = deadlock .
  ceq nf(P1 ;; P2) = (if (nf(P1) == P1) and (nf(P2) == P2)
                      then P1 ;; P2
                      else nf(nf(P1) ;; nf(P2)) fi)
    if (P1 =/= nil) and (P2 =/= nil) and (P1 =/= deadlock) .
  ceq nf(P1 ++ P2) = (if (nf(P1) == P1) and (nf(P2) == P2)
                      then P1 ++ P2
                      else nf(nf(P1) ++ nf(P2)) fi)
    if (P1 =/= deadlock) and (P2 =/= deadlock) .
  ceq nf(P1 || P2) = (if (nf(P1) == P1) and (nf(P2) == P2)
                      then P1 || P2
                      else nf(nf(P1) || nf(P2)) fi)
    if (P1 =/= nil) and (P2 =/= nil) and
       (P1 =/= deadlock) and (P2 =/= deadlock) .
  eq nf(P **) = (nf(P)) ** .

  *** Process termination
  op terminates : Process -> Bool .

  eq terminates(nil) = true .
  eq terminates(A) = false .
  eq terminates(P1 ;; P2) = terminates(P1) and terminates(P2) .
  eq terminates(P1 ++ P2) = terminates(P1) or terminates(P2) .
  eq terminates(P1 || P2) = terminates(P1) and terminates(P2) .
  eq terminates(P **) = true .

  *** Process destructors
  op hd : Process -> Set[Action] .
  ops tl tl' : Action Process -> Process .

  eq hd(nil) = (empty).Set`[Action`] .
  eq hd(deadlock) = (empty).Set`[Action`] .
  eq hd(A) = singletonSet(A) .
  eq hd(P1 ;; P2) = if terminates(P1)
                    then union(hd(P1), hd(P2))
                    else hd(P1) fi .
  eq hd(P1 ++ P2) = union(hd(P1), hd(P2)) .
  eq hd(P1 || P2) = union(hd(P1), hd(P2)) .
  eq hd(P **) = hd(P) .

  eq tl(A, P) = nf(tl'(A, P)) .

  eq tl'(A, nil) = deadlock .
  eq tl'(A, deadlock) = deadlock .
  eq tl'(A, A') = if (A == A')
                  then nil
                  else deadlock
                  fi .
  eq tl'(A, (P1 ;; P2)) = if in(A, hd(P1))
                          then tl'(A, P1) ;; P2
                          else if terminates(P1)
                               then tl'(A, P2)
                               else deadlock fi fi .
  eq tl'(A, (P1 ++ P2)) = if (in(A, hd(P1)) and in(A, hd(P2)))
                          then tl'(A, P1) ++ tl'(A, P2)
                          else if in(A, hd(P1))
                               then tl'(A, P1)
                               else tl'(A, P2) fi fi .
  eq tl'(A, (P1 || P2)) = (tl'(A, P1) || P2) ++ (P1 || tl'(A, P2)) .
  eq tl'(A, (P **)) = tl'(A, ((P ;; (P **)) ++ nil)) .

  *** Does a process accept a list of actions?
  op accept : List[Action] Process -> Process .

  var AL : List[Action] .

  eq accept(nil, P) = P .
  ceq accept(AL, P) = (if in(hd(AL), hd(P))
                       then accept(tl(AL), tl(hd(AL), P))
                       else deadlock fi)
        if (length(AL) >= 1) .

  op acceptMultiSet : MultiSet[Action] Process -> Process .

  var AM : MultiSet[Action] .
  eq acceptMultiSet(AM, P) = acceptPerm(makeList(AM), P) .

  *** Does a process accept any permutation of a list of actions?
  op acceptPerm : List[Action] Process -> Process .
  op acceptPerm : List[List`[Action`]] Process -> Process .

  eq acceptPerm(AL, P) = if (AL == nil)
                         then nf(P)
                         else nf(acceptPerm(permutations(AL), P)) fi .
  eq acceptPerm((nil).List`[List`[Action`]`], P) = deadlock .
  ceq acceptPerm(ALL, P) = accept(hd(ALL), P) ++ acceptPerm(tl(ALL), P)
        if (ALL =/= nil) .

  *** Auxiliary functions: permutations of a list
  op permutations : List[Action] -> List[List`[Action`]] .
  op permutations : MachineInt List[Action] -> List[List`[Action`]] .
  op consall : Action List[List`[Action`]] -> List[List`[Action`]] .

  var ALL : List[List`[Action`]] .

  eq permutations(nil) = nil .
  ceq permutations(AL) = cons(cons(hd(AL), nil), nil)
        if length(AL) == 1 .
  ceq permutations(AL) = permutations(length(AL) - 1, AL)
        if length(AL) > 1 .
  ceq permutations(N, AL) =
        (if (N == 0)
         then consall(nth(N, AL), permutations(removenth(N, AL)))
         else append(consall(nth(N, AL), permutations(removenth(N, AL))),
                     permutations(N - 1, AL)) fi)
       if N >= 0 .

  var N : MachineInt .

  eq consall(A, nil) = nil .
  ceq consall(A, ALL) = cons(cons(A, hd(ALL)), consall(A, tl(ALL)))
        if ALL =/= nil .
endfm)

(view Process from TRIV to PROCESS is
  sort Elt to Process .
endv)

eof

(select PROCESS .)
(red acceptMultiSet(multiset(act('?new),
                    multiset(act('!add),
                    multiset(act('!conc),
                    multiset(act('!ack), empty)))),
     tl(act('!new),
     tl(act('?return),
    	((act('!return) ;; act('?ack)) **)
     || ((act('?return) ;; act('!new) ;; act('?new)) ** ;;
         act('?receipt) ;; act('!printreceipt) ;; act('?send) ;; act('!print))
     || (((act('!add) ;; act('?add)) || (act('!conc) ;; act('?conc)) || (act('!ack))) ** ;;
         act('?printreceipt) ;; act('!get) ;; act('?to) ;; act('!send))
     || (act('?get) ;; act('!to))))) .)

quit

(red tl(act('?receipt),
        ((act('?return) ;; act('!new)) ** ;;
         act('?receipt) ;; act('!printreceipt) ;; act('?send) ;; act('!print))
     || ((act('?new) ;; (act('!add) || act('!conc))) ** ;;
         act('?printreceipt) ;; act('!get) ;;
         act('?to) ;; act('!send))
     || ((act('?conc)) ** ;;
         act('?get) ;; act('!to))
     || ((act('?add) **))) .)

quit

(red acceptMultiSet(multiset(act('?return),
                    multiset(act('!new),
                    multiset(act('?new), empty))),
        ((act('?return) ;; act('!new) ;; act('?new)) ** ;;
         act('?receipt) ;; act('!printreceipt) ;; act('?send) ;; act('!print))
     || ((act('!add) ;; act('?add) || act('!conc) ;; act('?conc)) ** ;;
         act('?printreceipt) ;; act('!get) ;;
         act('?to) ;; act('!send))
     || (act('?get) ;; act('!to))) .)

(red hd(((act('a) **) ++ (act('b) **)) || deadlock) .)
(red nf(((act('a) **) ++ (act('b) **)) || (nil ++ deadlock)) .)
(red tl(act('a), (((act('a) **) ++ (act('b) **)) || (act('a) ++ deadlock))) .)
(red accept(cons(act('a), cons(act('a), nil)), ((act('a) **) ++ (act('b) **))) .)
(red accept(cons(act('a), cons(act('b), cons(act('b), cons(act('a), nil)))), ((act('a) **) || (act('b) **))) .)
(red accept(cons(act('a), cons(act('b), cons(act('b), cons(act('a), nil)))), (((act('a) ;; act('a)) ;; act('b)) ;; act('b))) .)
(red acceptPerm(cons(act('a), cons(act('b), cons(act('a), nil))), ((act('a) **) ;; act('b)) ++ (act('b) ;; act('a) ;; act('a))) .)
(red acceptMultiSet(multiset(act('a), multiset(act('b), multiset(act('a), empty))), ((act('a) **) ;; act('b)) ++ (act('b) ;; act('a) ;; act('a))) .)

(fmod TEST is
  protecting LIST[Action] .
  protecting LIST[List`[Action`]] .
  protecting MULTISET[Action] .
  protecting SET[Action] .
endfm)

(red diff(set('a, set('b, set('b, empty))), set('b, empty)) .)

quit