Times Documentation

This chapter contains BNF grammars of languages used in the Times tool. Note that words made of capital letters represent non-terminals.

Modeling Language

Declarations
Processes and Templates
Locations
Transitions
Tasks
Reserved Words

Query Language

Modeling Language

The input language of the Times tool is a network of timed automata extended with real-time tasks. Each timed automata is represented as a process instantiated from a template with the set of arguments. In addition there is a task table describing various task parameters.

Declarations
Declarations can be either local or global. Local declarations relate to the different templates while global ones belong to the whole system. Every declaration must have an identifier, type and optionally an initial value. An identifier must satisfy the following regular expression:
```
                 ID:   [a-zA-Z]([a-zA-Z0-9_])*
```
In this document non-terminals CLOCK, INTEGER, CHANNEL, URGENT_CHANNEL, EXTERNAL_CHANNEL and CONSTANT denote identifiers of the respective declaration types. The valid declaration types are:
```
   DECLARATION_TYPE:   clock
                     | int
                     | int[CONST_EXPR,CONST_EXPR]
                     | chan
                     | urgent chan
                     | extern chan
                     | const
```
where int[...,...] is a bounded integer with lower and upper bounds defined as constant expressions. Constant expressions have the following syntax:
```
         CONST_EXPR:   CONST_TERM{+|-}CONST_TERM
         CONST_TERM:   CONST_UNAR{*|/}CONST_UNAR
         CONST_UNAR:   CONST_ELEM
                     | -CONST_ELEM
         CONST_ELEM:   NATURAL
                     | CONSTANT
                     | (CONSTANT_EXPR)
            NATURAL:   ([0-9])+
```
Declaration identifiers of types clock, int and int[,] defined:
```
        CLOCK_ARRAY:   ID[CONST_EXPR]
      INTEGER_ARRAY:   ID[CONST_EXPR]
```
represent arrays of clocks and integers respectively. The size of array is set equal to the value of the constant expression given in square brackets. Declaration initial value is specified as a constant expression. In case of arrays the same value is assigned to all the elements in the array.

Processes and Templates
Processes are templates instantiated with the set of arguments. Process has the following attributes:
```
       PROCESS_NAME:   ID_WITH_SPACES
   PROCESS_TEMPLATE:   ID
  PROCESS_ARGUMENTS:   [ID(,ID)*]
```
where ID_WITH_SPACES is an identifier with spaces allowed:
```
     ID_WITH_SPACES:   [a-zA-Z]([a-zA-Z0-9_ ])*
```
Note that during process instantiation spaces in the process name are replaced with underscores. Be sure that you use underscores instead of spaces specifying properties in verifier.
Attributes of a template include the template name and the list of formal parameters, defined as following:
```
      TEMPLATE_NAME:   ID
TEMPLATE_PARAMETERS:   [TEMPLATE_PARAMETER(;TEMPLATE_PARAMETER)*]
 TEMPLATE_PARAMETER:   DECLARATION_TYPE ID
```

Locations

The location attributes are:

      LOCATION_NAME:   [ID_WITH_SPACES]
      LOCATION_TASK:   [TASK_NAME]
 LOCATION_INVARIANT:   INVARIANT_LIST

where:

     INVARIANT_LIST:   [INVARIANT(,INVARIANT)*]
          INVARIANT:   CLOCK{<|<=}INTEGER_EXPR

and the syntax of the integer expression is:

       INTEGER_EXPR:   INTEGER_TERM{+|-}INTEGER_TERM
       INTEGER_TERM:   INTEGER_UNAR{*|/}INTEGER_UNAR
       INTEGER_UNAR:   INTEGER_ELEM
                     | -INTEGER_ELEM
       INTEGER_ELEM:   INTEGER
                     | CONSTANT
                     | (INTEGER_EXPR)
                     | (INTEGER_GUARD?INTEGER_EXPR:INTEGER_EXPR)
      INTEGER_GUARD:   INTEGER_EXPR RELATION INTEGER_EXPR
           RELATION:   !=
                     | <
                     | <=
                     | ==
                     | >=
                     | >

The name of the location is an optional attribute; if not given, assigned automatically in the form Sx, where 'x' is a zero-based index. The name of the task associated with the location is also optional; if not specified, no task is released for execution when the automaton reaches given location.

Transitions

The transition attributes are:

    TRANSITION_NAME:   [ID_WITH_SPACES]
   TRANSITION_GUARD:   GUARD_LIST 
    TRANSITION_SYNC:   {CHANNEL|URGENT_CHANNEL|EXTERNAL_CHANNEL}{?|!}
  TRANSITION_ASSIGN:   ASSIGNMENT_LIST

where the syntax of the guard is:

         GUARD_LIST:   [GUARD(,GUARD)*]
              GUARD:   INTEGER_GUARD
                     | CLOCK_GUARD
        CLOCK_GUARD:   CLOCK RELATION CLOCK_EXPR_WITH_INT
CLOCK_EXPR_WITH_INT:   CLOCK ({+|-} CONST_TERM)*
                     | INTEGER_EXPR

and the syntax of the assignment is:

    ASSIGNMENT_LIST:   [ASSIGNMENT(,ASSIGNMENT)*]
         ASSIGNMENT:   INTEGER := INTEGER_EXPR
                     | CLOCK := CLOCK_EXPR
                     | (INTEGER_GUARD?CLOCK_RESET)
         CLOCK_EXPR:   CLOCK ({+|-} CONST_TERM)*
                     | CONST_EXPR (should be equal to zero)
        CLOCK_RESET:   CLOCK := CONST_TERM (should be equal to zero)

Tasks
Tasks and their parameters are defined in the task table. The name of the task should satisfy the identifier's regular expression and should be different from the channel names declared in the system.

Reserved Words

The following words are reserved and cannot be used as identifiers, names of locations, transitions or tasks:

assign, commit, externalDecl, globalDecl, graphinfo, guard, hide, imports
init, invariant, localDecl, location, locationName, paramList, procAssign,
process, rate, state, sync, system, systemDef, templateName, trans, int, 
clock, chan, urgent, extern, const

Query Language

The syntax of the query string is as follows:

     QUERY:   A[] PROP_EXPR
            | A<> PROP_EXPR
            | E[] PROP_EXPR
            | E<> PROP_EXPR
            | PROP_EXPR -> PROP_EXPR
 PROP_EXPR:   PROPERTY
            | not PROP_EXPR
            | (PROPERTY)
            | PROP_EXPR or PROP_EXPR
            | PROP_EXPR and PROP_EXPR
            | PROP_EXPR imply PROP_EXPR
  PROPERTY:   ID.ID
            | CLOCK RELATION CLOCK_EXPR
            | INTEGER_GUARD
            | deadlock