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 CITEM is
  sort CItem .

  op bottle : -> CItem .
endfm)

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

(fmod ITEM is
  protecting CITEM .
  protecting EURO .

  sort Item .

  op price : Item -> Euro .
  op desc : CItem -> Item .

  eq price(desc(bottle)) = 10 E .
endfm)

(view Item from TRIV to ITEM is
  sort Elt to Item .
endv)

(fmod ITEMS is
  protecting MULTISET[CItem] .
  protecting MULTISET[Item] .

  op description : MultiSet[CItem] -> MultiSet[Item] .
  op description : CItem MultiSet[CItem] -> MultiSet[Item] .
  op amount : MultiSet[Item] -> Euro .
  op amount : Item MultiSet[Item] -> Euro .

  var C : CItem .
  var I : Item .
  var Cb : MultiSet[CItem] .
  var Ib : MultiSet[Item] .

  eq description(Cb) = if Cb == (empty).MultiSet`[CItem`]
                       then (empty).MultiSet`[Item`]
                       else description(choose(Cb), Cb) fi .
  eq description(C, Cb) = union(singletonMultiSet(desc(C)), description(diff(Cb, singletonMultiSet(C)))) .
  eq amount(Ib) = if Ib == (empty).MultiSet`[Item`]
                  then 0 E
                  else amount(choose(Ib), Ib) fi .
  eq amount(I, Ib) = price(I) + amount(diff(Ib, singletonMultiSet(I))) .
endfm)

(omod RM is
  protecting ITEMS .

  class User | rm : Oid, state : MachineInt .
  class RM | total : MultiSet[Item], current : MultiSet[Item] .

  msg return : MultiSet[CItem] Oid -> Msg .
  msg print : MultiSet[Item] Euro -> Msg .

  var U : Oid .
  var Rm : Oid .
  var Cb : MultiSet[CItem] .
  vars Ib Ib' : MultiSet[Item] .
  var X : Object .

  rl [r] :
    < U : User | rm : Rm, state : 0 > X =>
      < U : User | rm : Rm, state : 1 > X
      return(multiset(bottle, multiset(bottle, multiset(bottle, empty))), Rm) .
  rl [return] :
    return(Cb, Rm)
    < Rm : RM | total : Ib, current : Ib' > =>
      < Rm : RM | total : union(description(Cb), Ib),
                  current : union(description(Cb), Ib') >
      print(description(Cb), amount(description(Cb))) .
endom)

(omod RM-CONTROL is
  protecting RM .
  protecting PROCESS .

  op u : -> Oid .
  op rm : -> Oid .
  op initial : -> Configuration .
  eq initial =
    < u : User | rm : rm, state : 0 >
    < rm : RM | total : empty, current : empty > .

  op control : -> Process .
  eq control =
        act('!return)
     || act('?return) ;; act('!print) .
endom)

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

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

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

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

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

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

quit