Global Structure of Ticc Programs for Ticc >= 0.20

For previous versions of Ticc, click on Get Info.

Structure of a Ticc Program

The general structure of a Ticc program is described in the input grammar. Here, we describe the typical structure of a program. We denote by <...> fields that have to be filled in by the user.

A ticc program begins with the declaration of a set of global variables, possibly empty.
```
  var vg1 : <type1>
  var vg2 : <type2>
  ...
  var vgn : <typen>
```
Currently Ticc variables can be of two types:
- Boolean (declared by "bool")
- Integer range (declared by, for example, "[0..4]")
See information about types.
The declaration of the global variables may be followed by the declaration of sets of states, defined by a boolean expression, for example:
```
  stateset is_free: x = 0 & ~busy
```

The boolean expression can contain only unprimed variables. See ../Expressions for more information on expressions.

Next follows the declaration of at least one module. A module declaration looks like:
```
  module <modulename>:

    <body of the module>

  endmodule
```

The <body of the module> has the following form:

  stateless vg1, vg2
  stateless vg5
 
  var vl1 : bool 
  var vl2, vl3: [0..4]

  initial: <state_formula>
  stateset is_zero: <state_formula>

  <actionblock1>
  <actionblock2>
   ...
  <actionblockl>

The stateless declaration is used to declare teh set of global variables that are considered to be history-free. If a variable is history-free, the environment is free to update the value of the variable at any time, and the module does not need to have an input action corresponding to every output action that modifies these history-free variables. For more on history-free variables, see ../Composition.
Local variables can be declared next.
An initial condition for the module can be defined via the keyword initial. The initial condition is a boolean expression over unprimed variables; see ../Expressions for more information about expressions. If no initial condition is defined, the initial condition is assumed to correspond to the expression true.
It is possible to define statesets (sets of states) associated with the module, via the keyword stateset. The sets of states are defined via expressions over the unprimed local and global variables; see ../Expressions for more information about expressions. Statesets have no predefined meaning in Ticc: one can use them from the Ticc Toplevel.
Each action block begins with the <actiontype> and the name of the action and is followed by a set of <guarded commands> contained in a block.
```
  <actiontype> <actionblockname1> : { <set of guarded commands> }
```
There are three values for <actiontype>:
- output denotes output actions. An output action, when taken, can change the value of both local and global variables.
- input denotes input actions. An input action has a global and a local part:
  - The global part specifies when the module is able to accept the action, and specifies how the global variables can be updated by the module that outputs the action.
  - The local part specifies how the module updates the value of its local variables when receiving the input actions.
- local denotes local actions. A local action can update the values of local variables only. Local actions do not synchronize with other modules. We note that local was not mentioned in FROCOS 2005.
The semantics of each type of action is described by a set of guarded commands.

Comments

Ticc programs can be documented with //.
```
// This is my first Ticc program.
```
Ticc programs are written in separate files that can be parsed by the tool. Several ticc programs can be found in the directory ticc/examples/tutorial (See the README file there for more details).

Examples

We suggest that you read the code of the following examples, as a good starting point:

examples/tutorial/fire-detector.*
examples/tutorial/printer-s-frocos.*
examples/tutorial/buffered-receiver.*

Ticc/Global Structure of Ticc Programs (last edited 2006-09-07 04:23:40 by MarcoFaella)