fmod COMMAND-LIST is 
  inc COMMAND .
  sort CommandList .  
  subsort Command < CommandList .

  op nil : -> CommandList .
  op _;_ : CommandList CommandList -> CommandList [ctor assoc id: nil] .
  op first : CommandList -> Command .
  op rest : CommandList -> CommandList .

  var cmdl : CommandList .
  var cmd : Command .

  eq first(nil) = noCmd .
  eq first(cmd ; cmdl) = cmd .
  eq rest(nil) = noCmd .
  eq rest(cmd ; cmdl) = cmdl .
endfm

*****************************************************************************
***                    Controller                                         ***
***  knows its StateVariable, Actuator                                    ***
***  saves current constraint and the requester of that constraint        ***
***  also keeps lates value of state variable                             ***
*****************************************************************************

mod CONTROLLER is 
  inc ATTRIBUTES . 
  inc STATE-VARIABLE-CONTROLLER-INTERFACE .
  inc CONTROLLER-ACTUATOR-INTERFACE .
  inc COMMAND-LIST .

  sort CtrlCid .
  subsort CtrlCid < Cid .


  *** Attributes
  op  currentCstr : Constraint -> Attribute . 
                    *** constraint that is currently handled
  op  currentCstrReq : Oid -> Attribute . 
                    *** requester who started current constraint
  op  currentSVVal : StateValue -> Attribute . 
                    *** last requested state value of state variable
  op cmds : CommandList -> Attribute .

  *** Internal computations
  op satisfy : StateValue Constraint -> Bool .
               *** tests whether current state satisfies constraint
  op coa : StateValue Constraint -> CommandList .
	       *** determines course of action, 
               *** given current value and constraint

  *** Reason for failure: 
  *** course of action has been executed, constraint still not satisfied
  op COANoSuccess : -> Reason .


  vars c a sv o o' : Oid . 
  var msg : Msg .
  vars cstr cstr' : Constraint . 
  var v v' v'' : StateValue .
  var b : Bool .
  var r : Reason .
  var ccid  : CtrlCid .
  var cl : CommandList .



  rl[readyForNewConstraint]:
  < c : ccid | mysv(sv), 
               waitAfter(msg),
               ctrlatts:AttributeSet >
  msg(c,sv,readyReq)
  =>
  if (msg == noMsg)
  then < c : ccid | mysv(sv), 
                    waitAfter(msg(c,sv,readyReq)),
                    ctrlatts:AttributeSet >
       msg(sv,c,readyRep(true))
  else < c : ccid | mysv(sv), 
                    waitAfter(msg),
                    ctrlatts:AttributeSet >
       msg(sv,c,readyRep(false)) 
  fi .
  

  rl[getCstrCompareGoalIssueCommand]:
  < c : ccid | mysv(sv), 
               myactuator(a), 
               currentCstr(cstr'), 
               currentCstrReq(o'), 
               currentSVVal(v'), 
               cmds(cl), 
               waitAfter(msg(c,sv,readyReq)),
               ctrlatts:AttributeSet >
  msg(c,sv,startCstr(cstr,o,v))
  =>
  if satisfy(v,cstr)
  then < c : ccid | mysv(sv), 
                    myactuator(a), 
                    currentCstr(cstr), 
                    currentCstrReq(o), 
                    currentSVVal(v), 
                    cmds(cl), 
                    waitAfter(noMsg),
                    ctrlatts:AttributeSet >
       msg(sv,c,endCstr(cstr,o,noReason))
  else < c : ccid | mysv(sv), 
                    myactuator(a), 
                    currentCstr(cstr), 
                    currentCstrReq(o), 
                    currentSVVal(v),  
                    cmds(rest(coa(v,cstr))), 
                    waitAfter(msg(c,sv,startCstr(cstr,o,v))),
                    ctrlatts:AttributeSet >
       msg(a,c,issueCmd(first(coa(v,cstr))))
  fi .


  rl[getNewValueCompareGoal]:
  < c : ccid | mysv(sv), 
               myactuator(a), 
               currentCstr(cstr), 
               currentCstrReq(o), 
               currentSVVal(v), 
               cmds(cl),  
               waitAfter(msg(c,sv,startCstr(cstr,o,v''))),
               ctrlatts:AttributeSet >
  msg(c,sv,newVal(v'))
  => 
  if satisfy(v',cstr)
  then < c : ccid | mysv(sv),
                    myactuator(a),
                    currentCstr(cstr), 
                    currentCstrReq(o), 
                    currentSVVal(v'), 
                    cmds(cl), 
                    waitAfter(noMsg),
                    ctrlatts:AttributeSet >
       msg(sv,c,endCstr(cstr,o,noReason))
  else (if cl == nil
        then < c : ccid | mysv(sv), 
                          myactuator(a),
                          currentCstr(cstr), 
                          currentCstrReq(o), 
                          currentSVVal(v'), 
                          cmds(cl), 
                          waitAfter(noMsg),
                          ctrlatts:AttributeSet >
             msg(sv,c,endCstr(cstr,o,COANoSuccess))
        else < c : ccid | mysv(sv), 
                          myactuator(a),
                          currentCstr(cstr), 
                          currentCstrReq(o), 
                          currentSVVal(v'), 
                          cmds(rest(cl)), 
                          waitAfter(msg(c,sv,startCstr(cstr,o,v))),
                          ctrlatts:AttributeSet >
             msg(a,c,issueCmd(first(cl)))
        fi)
  fi .



endm

mod CONTROLLER-TEST is
  inc CONTROLLER .

  op Ctrl : -> CtrlCid .

  op mycontroller : -> Object .
  eq mycontroller = 
     < o("MyController") : Ctrl | mysv(o("MyStateVar")),
                                  myactuator(o("MyActuator")),
                                  waitAfter(noMsg) > .
 
endm