*****************************************************************************
***                           Interfaces                                  ***
***                                                                       ***
*****************************************************************************

fmod ATTRIBUTES is
  inc MYCONF .
  
  op myest  : Oid -> Attribute .
  op mysv  : Oid -> Attribute .
  op myctrl  : Oid -> Attribute .
  op mydevice  : Oid -> Attribute .
  op myactuator : Oid -> Attribute .
  op mysensor  : Oid -> Attribute .
     *** for simplicity, we defined the above attributes in one module
     *** that is to be imported in all other module
     *** correct use 
     *** (could have been reflected in more complicated module structure)
     *** sv knows ctrl and estimator (and vice a versa)
     *** ctrl knows actuator (and vice a versa)
     *** estimator knows sensor (and vice a versa)
     *** device knows actuator and sensor (and vice a versa)
     

  op waitAfter : Msg -> Attribute . 
     *** attribute for control-flow within an object
     *** contains the last message received
     *** if there was no last message received, then it contains the current 
     *** message sent
endfm

*****************************************************************************
***               StateVariable-Environment-Interface                     ***
***  messages between controller and statevariable                        ***
***                                                                       ***
*****************************************************************************

fmod CONSTRAINT is
  sort Constraint .   
  op noCstr : -> Constraint .
endfm

fmod REASON is
  sort Reason .  
  op noReason : -> Reason .
endfm

fmod STATE-VARIABLE-ENVIRONMENT-INTERFACE is
  inc MYCONF . 
  inc CONSTRAINT .
  inc REASON .

  op startConstraint : Constraint -> MsgBody .          
  op constraintSuccess : Constraint -> MsgBody . 
  op constraintFailure : Constraint Reason -> MsgBody . 
                         *** Reason - for failure 
endfm

*****************************************************************************
***               StateVariable-Controller-Interface                      ***
***  messages between controller and statevariable                        ***
***                                                                       ***
*****************************************************************************


fmod STATE-VALUE is
  sort StateValue .  

  sort UnknownStateValue .    
  subsort UnknownStateValue < StateValue .    

  op uk : -> UnknownStateValue .
endfm


fmod STATE-VARIABLE-CONTROLLER-INTERFACE is
  inc MYCONF .
  inc CONSTRAINT .
  inc REASON .
  inc STATE-VALUE .
 

  op readyReq : -> MsgBody .
  op readyRep : Bool -> MsgBody .

  op startCstr : Constraint Oid StateValue -> MsgBody .
  op endCstr : Constraint Oid  Reason -> MsgBody .
 
  op newVal : StateValue -> MsgBody .

endfm


*****************************************************************************
***               StateVariable-Estimator-Interface                       ***
***  messages between controller and statevariable                        ***
***                                                                       ***
*****************************************************************************

fmod STATE-VARIABLE-ESTIMATOR-INTERFACE is
  inc MYCONF .
  inc STATE-VALUE .

  op updStateReq : StateValue -> MsgBody .
  op ackUpdStateReq : StateValue -> MsgBody .
endfm


*****************************************************************************
***                 Controller-Actuator-Interface                         ***
***                                                                       ***
*****************************************************************************

fmod COMMAND is
  sort Command .  
  op noCmd : -> Command .
endfm


fmod CONTROLLER-ACTUATOR-INTERFACE is   
  inc MYCONF .
  inc COMMAND .

  op issueCmd : Command -> MsgBody . 
endfm

*****************************************************************************
***                     Device-Actuator-Interface                         ***
***                                                                       ***
*****************************************************************************

fmod DEVICE-ACTUATOR-INTERFACE is   
  inc MYCONF .
  inc COMMAND .
             
  op executeCmd : Command -> MsgBody . 
 
endfm


*****************************************************************************
***                     Device-Sensor-Interface                           ***
***                                                                       ***
*****************************************************************************

fmod SENSOR-VALUE is
  sort SensorValue .  
endfm

fmod DEVICE-SENSOR-INTERFACE is   
  inc MYCONF .
  inc SENSOR-VALUE .
 
  op sensorValues : SensorValue -> MsgBody . 
endfm


*****************************************************************************
***                     Estimator-Sensor-Interface                           ***
***                                                                       ***
*****************************************************************************

fmod MEASUREMENT is
  sort Measurement .
  op  noMeas : -> Measurement .
endfm 

fmod ESTIMATOR-SENSOR-INTERFACE is   
  inc MYCONF .
  inc MEASUREMENT .
 
  op newMeasurement : Measurement -> MsgBody . 
endfm