*** First attempt; Luxembourg meeting

--- No hierarchical models
--- No physical time, like LF-verif paper
--- 

--- in rtm-prelude
in rtm-tctl.maude

(tomod LF-REPR is  
   protecting NAT-TIME-DOMAIN-WITH-INF .

 sorts PortId IPortId BPortId VarId IVarId BVarId ReactorId TimerId
        ActionId IActionId BActionId ReactionId ReactorState
	ActionTrigger IntExpr BoolExpr Expr ReactionIdSet OidSet
	ReactionList Reaction NatValue TimeValue BoolValue Value Connection ActionPolicy .

  subsort TimeValue BoolValue < Value .
  subsort NatValue < IntExpr .
  subsort BoolValue < BoolExpr .
  
 
  subsorts  ReactorId ReactionId < Oid .
  subsorts IPortId BPortId < PortId .
  subsorts IVarId BVarId < VarId .
  subsorts IActionId BActionId < ActionId .

  subsorts TimerId PortId ActionId < ActionTrigger < Oid .

---- Here we don't know what we are doing ...
  subsort IntExpr BoolExpr < Expr .

 
  subsorts TimerId PortId ActionId < ActionTrigger < Oid .

  subsorts ReactionId < ReactionIdSet < OidSet .
  op none : -> ReactionIdSet [ctor] .
  op _;_ : ReactionIdSet ReactionIdSet -> ReactionIdSet
                                          [ctor assoc comm id: none] .

  subsort Oid < OidSet .
    
  op none : -> OidSet [ctor] .
  op _;_ : OidSet OidSet -> OidSet [ctor assoc comm id: none] .

  op _in_ : Oid OidSet -> Bool .
  var O : Oid .   var OS : OidSet .
  eq O in O ; OS = true .
  eq O in OS = false [owise] .


  subsort Reaction < ReactionList .
 
  subsort NatValue < TimeValue .

  
 
  class Port | value : Value .

  class Reactor | inports : Configuration,
                  outports : Configuration,
		        state : ReactorState,
                  reactions : ReactionList,
		        timers : Configuration,
		        actions : Configuration .

  class Action | minDelay : Time, minSpacing : Time, policy : ActionPolicy,
                 payload : Value .

   class PhysicalAction .
   class LogicalAction .


   subclasses PhysicalAction LogicalAction < Action .
  --- unclear whether payload needed for all.  Subclass instead?

  ops defer drop replace : -> ActionPolicy [ctor] .

  subsort Connection < Configuration .

  op _:_-->_:_ : ReactorId PortId ReactorId PortId -> Connection [ctor] .
  op _:_--_-->_:_ : ReactorId PortId Time ReactorId PortId -> Connection [ctor] .



  op `[_`] : Nat -> NatValue [ctor] .
  op `[_`] : Time -> TimeValue [ctor] .
  op `[_`] : Bool -> BoolValue [ctor] .



  subsort TimeValue BoolValue < Value .
  subsort NatValue < IntExpr .
  subsort BoolValue < BoolExpr .
  
  op empty : -> ReactorState [ctor] .
  op _|->_ : VarId Value -> ReactorState [ctor] .
  op _;_ : ReactorState ReactorState -> ReactorState [ctor assoc comm id: empty] .

--- All kinds of Oids:




  op _._ : ReactorId ActionTrigger -> ReactionId [ctor] .
  *** Important: under the current assumption that each
  ***   reaction is triggered by exactly ONE trigger, we can
  ***   identify a reaction by its reactor and its trigger.
  ---  Of course, in a future more general setting, we can use
  ---    reactor.n   as the reaction id.

  ***  NOW in complex version we try the following ReactionId instead:
  op _._ : ReactorId Nat -> ReactionId [ctor] .




 class Timer | offset : Time, period : TimeInf .



***(
  op [_] : PortId -> Expr [ctor] .   --- only input ports can be called for value
  op [_] : IPortId -> IntExpr [ctor] .
  op [_] : BPortId -> BoolExpr [ctor] .

  op [_] : ActionId -> Expr [ctor] .
  op [_] : IActionId -> IntExpr [ctor] .
  op [_] : BActionId -> BoolExpr [ctor] .
)***


  subsorts IPortId IVarId IActionId < IntExpr .
  subsorts BPortId BVarId BActionId < BoolExpr .
  op _+_ : IntExpr IntExpr -> IntExpr .
  op _-_ : IntExpr IntExpr -> IntExpr .
  op _*_ : IntExpr IntExpr -> IntExpr .

  
  sort ReactionBody .

  ops _<_ _>_ _<=_ _>=_ : IntExpr IntExpr ->   BoolExpr [ctor] .
  op _===_ : Expr Expr -> BoolExpr [ctor] .

  op skip : -> ReactionBody [ctor] .
  op _;_ : ReactionBody ReactionBody -> ReactionBody [ctor assoc id: skip] .
  op _:=_ : VarId Expr -> ReactionBody [ctor] .
  op if_then_fi : BoolExpr ReactionBody -> ReactionBody [ctor] .
  op if_then_else_fi : BoolExpr ReactionBody ReactionBody -> ReactionBody [ctor] .
  op while_do_done : BoolExpr ReactionBody -> ReactionBody [ctor] .
  op _<-_ : PortId Expr ->  ReactionBody [ctor] .   
  op schedule : ActionId IntExpr Expr -> ReactionBody [ctor] .  --- ???????
  --- schedule(action, extra time, value)




  *** NEW IN TBILISI:
  op isPresent : ActionTrigger -> BoolExpr [ctor] .  
  op _==/=_ : Expr Expr -> BoolExpr [ctor] .
  op !_ : BoolExpr -> BoolExpr [ctor] .
  ops _&&_ _||_ : BoolExpr BoolExpr -> BoolExpr [ctor assoc comm] .


    subsort Reaction < ReactionList .
  
  op nil : -> ReactionList . 
  op __ : ReactionList ReactionList -> ReactionList [ctor assoc id: nil] .
  
 
  op reaction`when_-->_do`{_`} : OidSet OidSet ReactionBody -> Reaction [ctor] .
  op reaction`when_do`{_`} : OidSet ReactionBody -> Reaction .
  eq reaction when OS do { RB } = reaction when OS --> none do { RB } .





  var RB : ReactionBody .
  var RL : ReactionList .
  var N : Nat .
  var REST : Configuration .
  var OS2 : OidSet .
  var REACTORID : ReactorId .
  



  --- for more complex, journal paper, setting:
  op reaction_when_-->_do`{_`} : Nat OidSet OidSet ReactionBody -> Reaction [ctor] .

  op addIndices : ReactionList Nat -> ReactionList .
  eq addIndices(nil, N) = nil .
  eq addIndices((reaction when OS --> OS2 do {RB}) RL, N)
   = (reaction N when OS --> OS2 do {RB}) addIndices(RL, s N) .

  op addReactionIndices : Configuration -> Configuration .
  eq addReactionIndices(< REACTORID : Reactor | reactions : RL > REST)
   = < REACTORID : Reactor | reactions : addIndices(RL, 1) > addReactionIndices(REST) . 
  eq addReactionIndices(REST) = REST [owise] .

  *** Remember to add indices to reactions ASAP in the more complex setting!

endtom)


  
  
  
  
