REJO-Jr semantics

Introduction

The semantics of Junior (and REJO) has the standard format of conditional rewriting rules [11].
One writes:
                   ß
              t,E ---> t',E'

which means that:

• t' is the instruction that remains to be executed after executing t in the environment E. t' is called the residual of t, and one says that t rewrites in t'.
• E' is the new environment after execution of t.
• ß is a termination flag with 3 posible values:
  • TERM means that execution terminates for the current instant and that nothing remains to do for the next instant.
  • STOP means that execution is terminated for the current instant but that something remains to do at next instant.
  • SUSP means that execution is not terminated for the current instant and thus must be resumed during it.

The semantic of ß flag is defined by the Execution Context rewriting rules presented at the end of this document. The meaning of this flag changes according to the Junior implementation, for instance, in Storm implementation thare are more than 3 meanings.

Environments

An environment E is made of the following components:

• A set containing present events.
• A boolean flag eoi(E) which is true if the end of the current instant has been decided, and false otherwise.
• A boolean flag move(E) which is set to true to indicate that some change has appeared in the system; in this case, the end of the current instant must be
  dalayed to let the system possibility to react to this change.
• A table used to store the instructions which are frozen during the instant.
  

The following notations are defined:

• To note that an event S is present in E, one simply writes S €  E.
• E+S is the environment equal to E except that event S is added to it; E-S is equal to E except that S is removed from it. E[move = b]
  is equal to E except that flag move is set to b. E[eoi = b] is equal to E except that flag eoi is set to b.
• E/F[S] is equal to E+S if S € F, and is equal to E-S otherwise; E/F[S] is thus equal to E, except for S which is determined by F
• ¥(ø , ß) equals SUSP if either ø or ß is equal to SUSP; it equals TERM if both ø and ß are equals to TERM; it equals STOP in
  all other cases; actually, it is defined by the array:

	SUSP	STOP	TERM
SUSP	SUSP	SUSP	SUSP
STOP	SUSP	STOP	STOP
TERM	SUSP	STOP	TERM

 

• ¥1(ø , ß) equals SUSP if ø is STOP and ß is STOP or TERM; it equals ø otherwise. ¥2(ø , ß) equals SUSP if ß is STOP and ø is STOP or TERM; it equals ß otherwise.

• E{S := t} associates the frozen instruction t to event S; E{S} is the frozen instruction associated to S.

Nothing instruction

                          TERM
               Nothing,E ------> Nothing,E

Stop instruction

                        STOP
               Stop,E ------> Nothing,E

Atom instruction

                          TERM
               Atom(a),E ------> Nothing,E

with the side-effect of executing atomically action a.

Sequence

            TERM                 ß
       t,E ------> t',E'   u,E' ---> u',E''
     ----------------------------------------
                          ß
              Seq(t,u),E ---> u',E''

If the first branch is not terminated, then it remains a sequence executing the residual of the first branch:

                ß
           t,E ---> t',E'   ß != TERM
         --------------------------------
                       ß
           Seq(t,u),E ---> Seq(t',u),E'

Call instruction

There are two REJO sentences to invoke a reactive methode: in-line and call. In-line is not a Junior instruction; it just puts the Junior instructions in the line where the keyword appears. Unlike in-line sentence, call is really a Junior instruction (called Run) that behaves like another instruction, i.e. it executes a program returned by a Wrapper. In other words, one can see the in-line instruction as the static execution of a reactive method and call as the dynamic execution.

The rewrite rule of Run instructions is the following:

                           ß
           wp ---> t  t,E ---> t', E'
         --------------------------------
                       ß
            Run(wp),E ---> t',E'

Par instruction

If both branches of the parallel operator are suspended (which is the initial situation at each instant), then execution can nondeterministically chooses to execute one of them, setting the move flag to indicate that end of instant must be postponed in order to let the other branch a chance to be executed. The two corresponding rules are:

                              ß
                         t,E ---> t',E'
     --------------------------------------------------------
                         SUSP
      Par_SUSP,SUSP(t,u),E ------> Par_ß,SUSP(t',u),E'[move=true]
 

                              ø
                         u,E ---> u',E'
     --------------------------------------------------------
                         SUSP
      Par_SUSP,SUSP(t,u),E ------> Par_SUSP,ø(t,u'),E'[move=true]

If both branches of the parallel operator are suspended, execution can also execute both. The rule which executes the first branch, then the second, is called Merge:

                       ß                 ø
                  t,E ---> t',E'   u,E' ---> u',E''
     -------------------------------------------------------
                         ¥(ß,ø)
      Par_SUSP,SUSP(t,u),E ------> Par_{µ1(ß,ø),µ2(ß,ø)}(t',u'),E''

The second rule which executes the second branch, then the first one, is called InvMerge:

                     ø                 ß
                u,E ---> u',E'   t,E' ---> t',E''
     -------------------------------------------------------
                         ¥(ß,ø)
      Par_SUSP,SUSP(t,u),E ------> Par_{µ1(ß,ø),µ2(ß,ø)}(t',u'),E''

Only one branch is suspended

If only one branch is suspended, then it is simply run (and, in this case, the move flag is left unchanged):

                                 ß
                   ø!=SUSP  t,E ---> t',E'
     --------------------------------------------------
                      ¥(ß,ø)
      Par_SUSP,ø(t,u),E ------> Par_{µ1(ß,ø),µ2(ß,ø)}(t',u),E'
 

                                  ø
                    ß!=SUSP  u,E ---> u',E'
     --------------------------------------------------
                      ¥(ß,ø)
      Par_ß,SUSP(t,u),E ------> Par_{µ1(ß,ø),µ2(ß,ø)}(t,u'),E'

Note that, in all the rules of Par, production of a flag different from SUSP is only possible when both branches have also produced a flag different from SUSP; this reflects the synchronous characteristics of the parallel operator which, at each instant, executes its two branches.

Loop instruction

A Loop executes its body and rewrites in a sequence if it does not terminate immediately:

                    ß
               t,E ---> t',E'  ß!=TERM
         -------------------------------------
                      ß
           Loop(t),E ---> Seq(t',Loop(t)),E'

When the loop body terminates immediately, the Loop is restarted:

            TERM                     ß
       t,E ------> t',E'  Loop(t),E ---> u,E''
     -------------------------------------------
                          ß
               Loop(t),E ---> u,E''

Repeat instruction

Repeat terminates immediately if the counter is less or equal to zero:

                        n <= 0
       -----------------------------------
                        TERM
         Repeat(n,t),E ------> Nothing,E

Otherwise, the semantics is the one of a sequence:

                                      ß
       n > 0  Seq(t,Repeat(n-1,t)),E ---> u,E'
     ----------------------------------------
                           ß
            Repeat(n,t),E ---> u,E'

If instruction

                           ß
           bw = true  t,E ---> t', E'
         --------------------------------
                          ß
            If(bw,t,u),E ---> t',E'

The second branch is chosen if the configuration is not satisfied

                            ß
           bw = false  u,E ---> u', E'
         --------------------------------
                          ß
            If(bw,t,u),E ---> u',E'

Events and Event conditions

This section presents some definitions used in the reactive instructions to test if an event is present or not.

Configurations

A configuration is either:

• A positive configuration, that is an event S.
• A negative configuration, that is the negation not C of a configuration.
• A conjunction C1 and C2 of two configurations.
• A disjunction C1 or C2 of two configurations.

Two functions fixed and eval are defined for configurations. A configuration can be evaluated (function eval) only when it is fixed (function fixed):

Fixed

fixed(C,E) is true when configuration C can be evaluated in the environment E:

• fixed(S,E) = S €  E or eoi(E)
• fixed(not C,E) = fixed(C,E)
• fixed(C1 and C2,E) = fixed(C1,E) and fixed(C2,E)

                                         or fixed(C1,E) and eval(C1,E) = false

                                         or fixed(C2,E) and eval(C2,E) = false

• fixed(C1 or C2,E) = fixed(C1,E) and fixed(C2,E)

                                      or fixed(C1,E) and eval(C1,E)

                                      or fixed(C2,E) and eval(C2,E)

Note that in the basic case of an event S, fixed(S,E) is true if S is present or if the end of instant is set; this last case means that S is absent.

Eval

eval(C,E) returns the value of configuration C in the environment E:

• eval(S,E) = S €  E
• eval(not C,E) = not eval(C,E)
• eval(C1 and C2,E) = eval(C1,E) and eval(C2,E)
• eval(C1 or C2,E) = eval(C1,E) or eval(C2,E)

Auxiliary Functions

Three auxiliary functions are also defined:

• sat(C,E)           = fixed(C,E) and eval(C,E)
• unsat(C,E)       = fixed(C,E) and eval(C,E) = false
• unknown(C,E) = fixed(C,E) = false

  Note that unknown(C,E) is true if and only if sat(C,E) and unsat(C,E) are both false.

Note also that in the basic case of an event S, one has:

• sat(S,E) = true means that S is in E: S is present;
• unsat(S,E) = true means that S is not in E and that eoi(E) is true: S is absent.

Generate instruction

A Generate statement adds the generated event in the environment and immediately terminates:

                    TERM
     Generate(S),E ------> Nothing,(E+S)[move=true]

Wait instruction

The wait REJO instruction is translated in a Await Junior instruction. Await terminates if the configuration is satisfied; termination is immediate if satisfaction occurs before the end of the current instant, and is delayed to the next instant otherwise :

         sat(C,E)   eoi(E)=false
     --------------------------------
                  TERM
      Await(C),E ------> Nothing,E
 

         sat(C,E)   eoi(E)=true
     --------------------------------
                  STOP
      Await(C),E ------> Nothing,E

 

Await stops if the configuration is unsatisfied:

               unsat(C,E)
     --------------------------------
                  STOP
      Await(C),E ------> Await(C),E

 

Await is suspended if the configuration is unknown:

              unknown(C,E)
     --------------------------------
                  SUSP
      Await(C),E ------> Await(C),E

When instruction

                                       ß
        sat(C,E)   eoi(E)=false   t,E ---> t',E'
      --------------------------------------------
                              ß
               When(C,t,u),E ---> t',E'
 
 

               sat(C,E)   eoi(E)=true
            -----------------------------
                             STOP
              When(C,t,u),E ------> t,E

The second branch is chosen if the configuration is not satisfied; execution is immediate if unsatisfaction occurs before the end of the current instant, and is delayed to the next instant otherwise:

                                      ß
       unsat(C,E)  eoi(E)=false  u,E ---> u',E'
     --------------------------------------------
                             ß
              When(C,t,u),E ---> u',E'
 
 

               unsat(C,E)   eoi(E)=true
           -------------------------------
                             STOP
              When(C,t,u),E ------> u,E

Note that the two previous rules returning STOP when eoi(E) is false basically forbid immediate reaction to events absences. The test is suspended if the configuration is unknown:

                     unknown(C,E)
        ---------------------------------------
                         SUSP
          When(C,t,u),E ------> When(C,t,u),E

Until instruction

                   ß
              t,E ---> t',E'   ß!=STOP
       ----------------------------------------
                         ß
         Until(C,t,u),E ---> Until(C,t',u),E'

If the body stops, Until behaves as the auxiliary instruction Until*:

         STOP                            ß
    t,E ------> t',E'  Until*(C,t',u),E ---> v,E''
  --------------------------------------------------
                              ß
              Until(C,t,u),E ---> v,E''

Note that the body t is executed in both rules; preemption of Until is said to be weak, by contrast with the strong preemption used in the synchronous approach, which basically implies instantaneous reaction to absence.

Until*

The rules for Until* are the following: The handler is immediately executed if the configuration is satisfied before the end of instant:

                                      ß
        sat(C,E)   eoi(E)=false  u,E ---> u',E'
      -------------------------------------------
                              ß
             Until*(C,t,u),E ---> u',E'

Until* stops and rewrites in the handler, if the configuration is satisfied while end of instant is true:

              sat(C,E)   eoi(E)=true
           ----------------------------
                              ß
             Until*(C,t,u),E ---> u,E

Until* stops and rewrites in Until, if the configuration is unsatisfied:

               unsat(C,E)   eoi(E)=true
     ------------------------------------------
                        STOP
       Until*(C,t,u),E ------> Until(C,t,u),E

Until* is suspended while the configuration is unknown:

                    unknown(C,E)
     -------------------------------------------
                        SUSP
       Until*(C,t,u),E ------> Until*(C,t,u),E

Control instruction

                                 ß
             sat(S,E)   t,E ---> t',E'
     ------------------------------------------
                          ß
          Control(S,t),E ---> Control(S,t'),E

Control stops if the event is absent:

                      unsat(S,E)
     ------------------------------------------
                        STOP
        Control(S,t),E ------> Control(S,t),E

Control is suspended if the event is unknown:

                     unknown(S,E)
     ------------------------------------------
                        SUSP
        Control(S,t),E ------> Control(S,t),E

Local Instruction

                    SUSP
             t,E-S ------> t',E'  S !€ E'
     ----------------------------------------------
                      SUSP
       Local-(S,t),E ------> Local-(S,t'),E'/E[S]

                    SUSP
             t,E-S ------> t',E'  S € E'
     ----------------------------------------------
                      SUSP
       Local-(S,t),E ------> Local+(S,t'),E'/E[S]

                          SUSP
                   t,E+S ------> t',E'
     ----------------------------------------------
                      SUSP
       Local+(S,t),E ------> Local+(S,t'),E'/E[S]

When the body terminates or stops, then the local event is reset for the next instant:

                ß
         t,E-S ---> t',E'  ß=TERM or ß=STOP
     ----------------------------------------------
                      ß
       Local-(S,t),E ---> Local-(S,t'),E'/E[S]


                 ß
          t,E+S ---> t',E'  ß=TERM or ß=STOP
     --------------------------------------------------
                      beta
       Local+(S,t),E ------> Local-(S,t'),E'/E[S]

Freezable instruction

The semantics of Freezable is close to the one of Until. Freezable behaves as the body if it does not stops:

                         ß
                    t,E ---> t',E'  ß!=STOP
         --------------------------------------------
                             ß
           Freezable(S,t),E ---> Freezable(S,t'),E'

If the body stops, Freezable behaves as the auxiliary instruction Freezable*:

            STOP                              ß
       t,E ------> t',E'  Freezable*(S,t'),E' ---> v,E'
     ----------------------------------------------------
                                   ß
                 Freezable(S,t),E ---> v,E''

Note that the body t is executed in both rules; As Until, Freezable performs weak preemption.

Freezable*

The rules for Freezable* are the following: The instruction immediately terminates if the freezing event is present before the end of instant:

                     S € E     eoi(E)=false
     -----------------------------------------------------
                         TERM
      Freezable*(S,t),E ------> Nothing,E{S:=Par(t,E{S})}

Note that the residual instruction t is put in parallel in the frozen instructions table. The instruction terminates at next instant if the freezing event is present while the end of instant is set:

                     S € E     eoi(E)=true
     -----------------------------------------------------
                         STOP
      Freezable*(S,t),E ------> Nothing,E{S:=Par(t,E{S})}

Freezable* stops and rewrites in Freezable, if the freezing event is absent:

                     S !€ E     eoi(E)=true
         ----------------------------------------------
                              STOP
           Freezable*(S,t),E ------> Freezable(S,t),E

Freezable* is suspended while the freezing event is unknown:

                     S !€ E     eoi(E)=false
         -----------------------------------------------
                              SUSP
           Freezable*(S,t),E ------> Freezable*(S,t),E

Execution Context

Execution context rewritings have the forme e => e' meaning that reaction of the execution context e leads to the new execution context e'; b is a boolean which is true if the execution context e' is completely terminated.

Execution Context

An execution context executes one instant of its program in a new fresh environment.

                              ø
            Instant(t),Fresh ---> Instant(t'),E'
         --------------------------------------------
                             ß
           ExecContext(t),E ===> ExecContext(t'),E'

In this rule:

• Fresh is the environment with an empty event set and such that eoi(Fresh) and move(Fresh) are both false, and with an empty frozen instructions table.
• b is true if ø is TERM, and false otherwise.

Instant

Execution of an instruction during one instant means cyclic execution while it is suspended. Moreover, when execution suspends, end of instant is detected if no new move setting was performed. The instant is terminated when the instruction is stopped or terminated:

                   ß
              t,E ---> t',E'  ß!=SUSP
         ------------------------------------
                         ß
           Instant(t),E ---> Instant(t'),E'

Execution is immediately restarted if SUSP is returned and end of instant is set if no new move setting was performed:

                SUSP                                                                                                                        ß
           t,E ------> t',E'  move(E')=false   Instant(t'),E'[eoi=true] ---> u,E''
         ------------------------------------------------------------------------
                                            ß
                              Instant(t),E ---> u,E''

Execution is immediately restarted if SUSP is returned and move is reset if a move appeared:

                SUSP                                                                                                                          ß
           t,E ------> t',E'  move(E')=true   Instant(t'),E'[move=false] ---> u,E''
         -------------------------------------------------------------------------
                                                                               ß
                               Instant(t),E ---> u,E''