in ../../../../maude/bin/full-maude.maude
in basic.maude
in process.maude
in engine.maude


(fmod EURO is
  protecting MACHINE-INT .

  sort Euro .

  op _E : MachineInt -> Euro .
  op _+_ : Euro Euro -> Euro [assoc comm] .

  vars X Y : MachineInt .

  eq (X E) + (Y E) = (X + Y) E .
endfm)

(fmod METER is
  protecting MACHINE-INT .

  sort Meter .

  op _MM : MachineInt -> Meter .
endfm)

(fmod CITEM is
  sort CItem .

  op bottle : -> CItem .
endfm)

(view CItem from TRIV to CITEM is
  sort Elt to CItem .
endv)

(fmod DEPOSITITEM is
  protecting QID .
  protecting CITEM .
  protecting METER .
  protecting EURO .

  sort DepositItem .
  sort Bottle .
  subsort Bottle < DepositItem .

  op name : DepositItem -> Qid .
  op price : DepositItem -> Euro .
  op height : Bottle -> Meter .
  op width : Bottle -> Meter .
  op desc : CItem -> DepositItem .

  eq name(desc(bottle)) = 'Bottle .
  eq price(desc(bottle)) = 10 E .
  eq height(desc(bottle)) = 290 MM .
  eq width(desc(bottle)) = 85 MM .
endfm)

(view DepositItem from TRIV to DEPOSITITEM is
  sort Elt to DepositItem .
endv)

(fmod DEPOSITITEMS is
  protecting LIST[DepositItem] .

  op amount : List[DepositItem] -> Euro .

  var I : DepositItem .
  var Ib : List[DepositItem] .

  eq amount(Ib) = if Ib == (nil).List`[DepositItem`]
                  then 0 E
                  else price(hd(Ib)) + amount(tl(Ib)) fi .
endfm)


(omod ARM is
  protecting LIST[DepositItem] .

  class CustomerPanel | rc : Oid .
  class Receiver | cp : Oid, cur : Oid, dt : Oid .
  class Current | list : List[DepositItem], amount : Euro, rc : Oid, cp : Oid .
  class DayTotal | list : List[DepositItem] .

  msg return : CItem Oid -> Msg .
  msg new : Oid DepositItem Oid -> Msg .
  msg add : Oid DepositItem Oid -> Msg .
  msg conc : Oid DepositItem Oid -> Msg .
  msg ack : -> Msg .
  msg receipt : Oid -> Msg .
  msg printreceipt : Oid Oid -> Msg .
  msg get : Oid Oid -> Msg .
  msg to : Oid List[DepositItem] Euro Oid -> Msg .
  msg send : Oid List[DepositItem] Euro Oid -> Msg .
  msg print : Oid List[DepositItem] Euro -> Msg .

  vars Cp Rc Cur Dt : Oid .
  var Ci : CItem .
  var I : DepositItem .
  var L : List[DepositItem] .
  var S : Euro .

  rl [return] :
    return(Ci, Cp)
    < Cp : CustomerPanel | rc : Rc > =>
      < Cp : CustomerPanel | rc : Rc >
      new(Cp, desc(Ci), Rc) .
  rl [new] :
    new(Cp, I, Rc)
    < Rc : Receiver | cur : Cur, dt : Dt > =>
      < Rc : Receiver | cur : Cur, dt : Dt >
      conc(Rc, I, Cur)
      add(Rc, I, Dt)
      ack .
  rl [conc] :
    conc(Rc, I, Cur)
    < Cur : Current | list : L, amount : S > =>
      < Cur : Current | list : cons(I, L), amount : price(I) + S > .
  rl [add] :
    add(Rc, I, Dt)
    < Dt : DayTotal | list : L > =>
      < Dt : DayTotal | list : cons(I, L) > .
  rl [receipt] :
    receipt(Cp)
    < Cp : CustomerPanel | rc : Rc > =>
      < Cp : CustomerPanel | rc : Rc >
      printreceipt(Cp, Rc) .
  rl [printreceipt] :
    printreceipt(Cp, Rc)
    < Rc : Receiver | cur : Cur > =>
      < Rc : Receiver | cur : Cur >
      get(Rc, Cur) .
  rl [get] :
    get(Rc, Cur)
    < Cur : Current | list : L, amount : S, rc : Rc > =>
      < Cur : Current | list : nil, amount : 0 E, rc : Rc >
      to(Cur, L, S, Rc) .
  rl [to] :
    to(Cur, L, S, Rc)
    < Rc : Receiver | cp : Cp > =>
      < Rc : Receiver | cp : Cp >
      send(Rc, L, S, Cp) .
  rl [send] :
    send(Rc, L, S, Cp)
    < Cp : CustomerPanel | > =>
      < Cp : CustomerPanel | >
      print(Cp, L, S) .
endom)

(omod ARM-CONTROL is
  including ARM .
  protecting LIST[CItem] .
  protecting PROCESS .

  class User | items : List[CItem], receipt : Bool, cp : Oid .

  vars U Cp : Oid .
  var Cl : List[CItem] .
  var X : Object .

  crl [returning] :
    < U : User | items : Cl, cp : Cp > X =>
      < U : User | items : tl(Cl), cp : Cp > X
      return(hd(Cl), Cp)
    if (Cl =/= nil) .
  rl [ack] :
    ack
    < U : User | > =>
      < U : User | > .
  rl [request] :
    < U : User | items : nil, receipt : false, cp : Cp > X =>
      < U : User | items : nil, receipt : true, cp : Cp > X
      receipt(Cp) .

  op u : -> Oid .
  op cp : -> Oid .
  op rc : -> Oid .
  op cur : -> Oid .
  op dt : -> Oid .
  op initial : -> Configuration .
  eq initial =
    < u : User | items : cons(bottle, cons(bottle, cons(bottle, nil))),
                 receipt : false, cp : cp >
    < cp : CustomerPanel | rc : rc >
    < rc : Receiver | cp : cp, cur : cur, dt : dt >
    < cur : Current | list : nil, amount : 0 E, rc : rc, cp : cp >
    < dt : DayTotal | list : nil > .

  op control : -> Process .
  eq control =
    	((act('!return) ;; act('?ack)) ** ;; act('!receipt))
     || ((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)) .
endom)

(mod META-ARM-CONTROL is
  including META-LEVEL .
  protecting ARM-CONTROL .

  op mod : -> Module .
  eq mod = up(ARM-CONTROL) .

  op term : -> Term .
  eq term = up(ARM-CONTROL, initial) .
endm)

(view ARM-CONTROL from MOD-CONTROL to META-ARM-CONTROL is
  (op mod to mod .)
  (op term to term .)
  (op control to control .)
endv)

(mod ARM-CONTROL-ENGINE is
  protecting ENGINE[ARM-CONTROL] .
endm)

*** set trace on .
*** set trace select on .
*** trace select accepting .

(red-in ENGINE[ARM-CONTROL] :
  accepting .)

quit

(red-in ENGINE[ARM-CONTROL] :
  allRewrites(meta-reduce(mod, term), control) .)

(red-in ENGINE[ARM-CONTROL] :
   acceptMultiSet(
     inoutMsg(
       meta-reduce(mod, term),
       fst(meta-apply(mod, meta-reduce(mod, term), 'return, none, 0))),
     control) .)


(omod TEST is
  protecting MACHINE-INT .

  class Test | A : MachineInt, B : MachineInt .
  msg test : MachineInt MachineInt -> Msg .

  var O : Oid .
  vars X, X', Y, Y' : MachineInt .

  rl [ test ] :
    test(X, Y)
    < O : Test | A : X', B : Y' > =>
      < O : Test | A : X, B : Y > .

  op conf : -> Configuration .
  op o : -> Oid .

  eq conf = (< o : Test | A : 0, B : 0 > test(1, 2)) .

  mb o : Oid .
endom)

*** (red meta-reduce(up(TEST), { 'conf } 'Configuration) .)
*** (red getMsg(meta-rewrite(up(TEST), meta-reduce(up(TEST), up(TEST, conf)), 1)) .)
*** (red-in ENGINE[RM] : getMsg(meta-rewrite(mod, meta-reduce(mod, up(RM, initial)), 1)) .)
*** (red-in ENGINE[RM] : getMsg(meta-rewrite(mod, meta-reduce(mod, up(RM, initial)), 2)) .)
*** (red meta-reduce(up(TEST), ('test [ { '1 } 'NzMachineInt , { '2 } 'NzMachineInt ] : 'Msg)) .)
*** (red leastSort(up(TEST), 'test [ { '1 } 'NzMachineInt , { '2 } 'NzMachineInt ]) .)
*** (red leastSort(up(TEST), { '1 } 'MachineInt) .)