• Ticc
• Guarded Commands

Ticc guarded commands occur in action blocks. They have the following generic format:

  guard ==> command

Syntactically, we need to distinguish between two kinds of guarded commands:

• Guarded commands occurring in local rules, output rules, or in the global portion of an input rule;

• Guarded commands occurring in the local portion of an input rule.

This because, as detailed in the FROCOS 2005 Paper, the local portion of an input rule needs to be deterministic.

Let us examine the structure of these commands.

Guarded Commands for Output and Local Rules, and for the Global Part of Input Rules

For an action a, these have the following formats:

• Output:

  •   output a : { 
        guard_1 ==> command_1;
        guard_2 ==> command_2; 
        ... 
        guard_n ==> command_n } 
    

• Local:

  •   local a : { 
        guard_1 ==> command_1;
        guard_2 ==> command_2; 
        ... 
        guard_n ==> command_n } 
    

• Global portion of input rules (the local portion is described in the next section):

  •   input a : { 
        global: 
        guard_1 ==> command_1;
        guard_2 ==> command_2; 
        ... 
        guard_n ==> command_n
        local: 
        ...
         }
    

We refer to a block of the form

{   guard_1 ==> command_1;
    guard_2 ==> command_2; 
    ... 
    guard_n ==> command_n }

as a block of guarded commands. Each of these blocks indicates a way in which the variables can be updated, according to the following rules:

• Guards and commands are boolean expressions. Please refer to Input Grammar for the syntax of Ticc expressions. A concrete example is the following:

  • s = 1 ==> s' < 3 & t' = t + 1 
    

  Note that, as the example above hints, there is no need for a guarded command to have deterministic effect. In the above example, if the guarded command is executed, the variable s can have value 0, 1, or 2 in the successor state.

• Primed variables (such as t' above) refer to the value after the transition, unprimed variables to the value before. Primed variables cannot appear in guards.

• The local rule is a rule that allows to modify the value of the local variables of a module, leaving the global variables unchanged. The commands of its block of guarded commands cannot thus reference primed global variables.

• Ticc automatically renames local rules to ensure that two modules will not own local rules with the same name.

• The semantics of a guarded command guard ==> command is given by conjoining the expressions of the guard and of the command. This means that if the evaluation of the expression for the command is false, the guarded command will never be executed, even if its guard is true! Indeed, the distinction between what constitutes the guard and the command is purely arbitrary, and ==> could be replaced by conjunction(&). Nevertheless, the ==> serves as a useful (if potentially misleading) mnemonic.

• The semantics of a rule body

  •   {   guard_1 ==> command_1;
          guard_2 ==> command_2; 
          ... 
          guard_n ==> command_n }
    

  is given by taking the disjunction of the expressions for each guarded command. Intuitively, this means that, if more than one guard is true, the guarded command to be executed is chosen nondeterministically.

Local Portion of Input Commands

As explained in the FROCOS 2005 Paper, the local part of input transitions must be deterministic. To ensure this, the guarded commands for the local portion of an input action have the following modified syntax:

  input a : { 
    global: ... ; 
    local: guard_1 ==> var_1_1' := expr_1_1, var_1_2' := expr_1_2, ..., var_1_m' := expr_1_m 
      else guard_2 ==> var_2_1' := expr_2_1, var_2_2' := expr_2_2, ..., var_2_n' := expr_2_n
      else ... 
      else guard_k ==> var_k_1' := expr_k_1, var_k_2' := expr_k_2, ..., var_k_l' := expr_k_l

The else clauses above give a prioritization of the guards, so that guard_i+1 is checked only if the guards guard_0, guard_1, ..., guard_i are all false. Moreover, in a command

   ... ==> var_1_1' := expr_1_1, var_1_2' := expr_1_2, ..., var_1_m' := expr_1_m 

we require that expr_1_j mentions only primed variables in the following sets:

• primed global variables. This allows the local part to sense the update to the global variables, and update accordingly private variables.

• the primed variables var_1_1', ..., var_1_j-1'.

Interaction Between the Local and Global Guarded Commands for an Input Action

An input action has both a local and a global set of guarded commands. If the global portion is false, then the input action cannot be accepted. What if the local portion is false? Also in this case the input action cannot be accepted! Hence, in the following example:

input a : { 
  global: t > 0 ==> t' = t - 1 
  local:  s = 2 ==> s' := 0    }

the action a can be received only when t > 0 and s = 2. If you wish to leave s unchanged when different from 2, you have to write instead:

input a : { 
  global: t > 0 ==> t' = t - 1 

  local:  s = 2 ==> s' := 0 
    else  true  ==>         }

Which Variables Can Change Value?

What happens to the variables that are not mentioned in a guarded command?

• Output, local, and input local rules: The general idea for output and local rules is simple:

  • If a variable is not mentioned primed in a guarded command, then it does not change value if the guarded command is executed.

  This semantics is due to the fact that the guarded commands for output, input local, and local portions of actions represent prescriptions on how to change the value of some variables.

• Global portion of input rules: For the global part of an input rule, the following holds:

  • If a variable is not mentioned primed in a guarded command, then its value can change freely.

  The latter semantics is due to the fact that the global part of an input rule represents a constraint on the way in which global variables can change value. So, if a variable is not mentioned, no constraint is put on its value.

Example

For instance, consider the following guarded command, as part of an output rule:

  busy & size > 4 ==> not busy'

As size' is not mentioned in the command, the value of the variable size does not change as the guarded command is executed. Likewise, if the Ticc program contains a variable x, then the value of x would be equally unaffected.

How to encode full nondeterminism

How can we let a variable x be free to change in a fully nondeterministic fashion, if failure to mention x ensures that x does not change value?

• we can of course write something like  ... ==> x' > 0 & ... : since all variables are non-negative, the condition x' > 0 mentions x' without constraining its value.

• A better (more readable) solution, however, consists in writing  ... ==> nondet x' & ... 

Abbreviations

Commands and whole rule bodies can be left empty to express common conditions.

• A guarded command with an empty command  expr ==>   is equivalent to  expr ==> true 

• A guarded command with an empty guard  ==> expr  is not allowed.

• For output or local rules, an empty rule body  output a { }  is equivalent to  output a {true ==> true} . So, the action is always enabled and all variables keep their value.

• For input rules, if any part (local or global) is empty or missing (not even the local or global delimiter), that part is assumed to be  true ==> true . So, an empty or missing local part states that all (local) variables keep their value. An empty or missing global part states that there are no global constraints on the occurrence of the action in question.