*** Written by : Nirman Kumar (nkumar5@cs.uiuc.edu) - 05/30/03


*** This file shows (outlines) how actors with message delays, computational delays 
*** and message drops
*** whose random behavior is known beforehand can be modeled as a probabilistic 
*** rewrite theory.




*** Discrete probabilistic time in Maude
*** Time progresses in unit steps
*** All intervals are units of the basic time step
*** That interval can be the least count of a clock in the system

*** It is also possible to simulate real (continuos) time
*** This can be achieved by letting the time and delay fields in Objects and
*** Messages be specified as real numbers
*** and the tick rule (see below) incrementing the msg, objs time (and decrementing nonzero delays)
*** by the LEAST nonzero delay in the system conditional on the fact that there is some
*** nonzero delay in the system
*** Of course such a theory is NOT EXECUTABLE because real numbers are not representable 
*** computationally BUT at the theoretical level they define a semantics which models 
*** real time in actor systems.

pmod ACTOR-TIME is

  pr NAT .

  *** Configuration of Objects
  sort ObConfiguration .
  subsort Object < ObConfiguration .
  subsort ObConfiguration < Configuration .
  op __ : ObConfiguration ObConfiguration -> Obconfiguration [ctor assoc comm id : none ] .

  *** Configuration of Messages
  sort MsgConfiguration .
  subsort Msg < MsgConfiguration .
  subsort MsgConfiguration < Configuration .
  op __ : MsgConfiguration MsgConfiguration -> MsgConfiguration [ctor assoc comm id : none] . 

  *** sort representing an actor state
  sort State .
  class Actor | S : State , time : Nat , delay : Nat , queue : MsgConfiguration .

  *** Declarations of actors 
  subclass A < Actor .

  *** sort of Communicable values
  sort CV .
  
  *** third argument is the delay assigned to the message
  op _<-`(_,_`) : Oid CV Nat -> Msg .

  *** this sort is used to define automatons
  *** which cause the emission of messages
  sort AutomatonState .
  *** define constructors here for AutomatonState
  *** the constructors allow for infinite values for AutomatonState
 
  op setOfMessages : AutomatonState -> MsgConfiguration .
  op as : State Oid CV -> AutomatonState .
  *** define "as" by the use of equations
 
  
  var a : Oid .
  vars t d : Nat .
  vars Oc Oc' : ObConfiguration .
  op tick : ObConfiguration -> ObConfiguration .
  tick (none) = none .
  tick ( < a : Actor | time : t , delay : d , queue : Mc > ) = 
						  if (d > 0) 
						   then < a : Actor | time : t+1 , delay : d-1 , queue : tickMessages(Mc) > 
						   else < a : Actor | time : t+1 , delay : d   , queue : tickMessages(Mc) > 
						  fi .
  
  tick ( Oc Oc' ) = tick (Oc) tick(Oc') .

  op tickMessages : MsgConfiguration -> MsgConfiguration .
  eq tickMessages(none) = none .
  eq tickMessages ( X <- (Cv,d) ) = if (d > 0) then (X <- (Cv,d-1)) else (X <- (Cv,d)) fi .
  eq tickMessages( Mc Mc') = tickMessages(Mc) tickMessages(Mc') .

  *** tick is essentially non probabilistic
  prl [tick] Oc => tick(Oc) .

  
  var s : State .
  var M : Msg .
  vars Mc Mc' : MsgConfiguration .
  var v : CV .
  var X : Oid .

  *** Rewrite rule of an actor 
  *** probability function pi_compute defines d
  *** messages are considered not delivered unless the delay is 0
  *** actors are not considered free for computation unless the delay is 0
  prl [compute] : < X : Actor | S : s , time : t , delay : 0 , queue : ( X <- (v,0) ) Mc > => 
  		  < X : Actor | s : f(S,X) , time : t , delay : d , queue : Mc > 
				setOfMessagesAndActors(as(s,x,v)) .


  *** setOfMessagesAndActors MUST BE DEFINED BY USE OF REWRITE RULES (and not equations) OF THE FORM
  *** essentially this rule must define by recursion the set of Messages and actors created
  *** var s' : AutomatonState .
  *** op next : AutomatonState -> AutomatonState .
  *** prl [expand-set] : setOfMessagesAndActors(s') => ( Y <- (Z,d) ) 
						 setOfMessagesAndActors(next(s')) if condition(s) .
  *** prl [finish-expansion] setofMessagesAndActors(s') => (Y <- (Z,d) ) < A1 : Actor | .. > if condition'(s) .
 
  *** receive rule of actors
  *** this rule is probabilistic
  *** M can be none (message drop) OR
  *** it can be the same as X <- (Cv,d) as defined by some probability function
  *** Notice here that this function can only depend on X,Cv,d,MC 
  *** however message delays and drop probabilities MAY DEPEND on the entire system of actors
  *** as for example in computer networks
  *** when that happens we must model the entire routing protocol into the system to exactly capture
  *** the semantics. 
  *** When that happens the drop, delay depends ONLY on the receiver (sender) and the
  *** buffer at receiver as also the contents (size etc. may matter) of the message.
  prl < X : Actor | queue : Mc >  X <- (Cv,d) => < X : Actor | queue : Mc M > . 

endpm