Skip to content

TChecker file format

Jump to bottom
Frédéric Herbreteau edited this page Jul 16, 2023 · 31 revisions

Foreword: this document describes the TChecker file format for TChecker v0.3 and above which extends the file format used in previous versions of TChecker. In case you want to use previous versions of TChecker, please refer to the file format documentation up to v0.2.

The TChecker file format is used to describe timed automata. A file consists in a sequence of declarations of processes, clocks, locations, edges, etc, as described below. Declarations can appear in any order, as soon as these two rules are respected:

  • the system declaration must be the first declaration in the file

  • every item (process, location, edge, event, variable, ...) must be declared before it is used.

All declarations appear in the same global scope. Hence, all declared variables (bounded integers, clocks, etc) are global. Local variables can be simulated by adding a prefix to the name of the variable, e.g. P1_x may represent a clock x in process P1, and P2_x an other clock x in process P2.

A comment starts with symbol # and runs till the end of the line.

Symbols :, @ and # have a special meaning in TChecker files, and are thus reserved. Keywords: clock, edge, event, int, location, process, sync and system are reserved. Every word starting with tck (any letter case) is also reserved.

Identifiers are any string containing letters, numbers, underscore (_) and dot (.) and starting with either a letter or underscore (_). From v0.7, identifiers starting with $ are allowed by the parser. However, all such identifiers are reserved.

The system declaration

system:id{attributes}

declares a system with identifier id and given attributes. There shall be only one system declaration in a TChecker file. And it shall appear as the first declaration in the file.

The {attributes} part of the declaration can be ommitted if no attribute is associated to the system (or it can be left empty: {}). See section Attributes for details.

The process declaration

process:id{attributes}

declares a process with identifier id and given attributes. No other process shall have the same identifier.

A process declaration declares a process name. It does not declare a new scope. Hence all declarations following the process declaration are in the global scope.

There is no way to declare a type of process, and instantiate it in TChecker. In order to specify several instances of the same process type, the process declaration and all the related declarations (locations, edges, etc) shall be duplicated. This can be solved by writing a script that generates the TChecker model and that handles process instantiation smoothly.

The {attributes} part of the declaration can be ommitted if no attribute is associated to the process (or it can be left empty: {}). See section Attributes for details.

The event declaration

event:id{attributes}

declares an event with identifier id and given attributes. No other event shall have the same identifier.

The {attributes} part of the declaration can be ommitted if no attribute is associated to the event (or it can be left empty: {}). See section Attributes for details.

The clock declaration

clock:size:id{attributes}

declares an array of size clocks with identifier id and given attributes. No other clock shall have the same identifier.

For instance:

clock:1:x

declares a single clock x. And:

clock:10:y

declares an array y of 10 clocks. Then, y[0] is the first clock, and y[9] is the last one.

Out-of-bounds access like y[10] are detected and raise a fatal error when the model is analysed.

Clocks have an implicit domain of values ranging from 0 to infinity, and implicit initial value 0. Clocks only admit a restricted set of operations (see Expressions and Statements for details). Some errors can be detected at compilation time, but some others can only be detected when the model is analysed. In particular, assigning a value to clock out of its domain raise a fatal error when the model is analysed.

NB: while arrays of clocks may be convenient for modeling purposes, they make some analysis harder. In particular, the clock bounds that are used for zone abstractions are harder to compute (and often much less precise) when using clock arrays. This may result in exponentially bigger zone graphs. We thus recommend to avoid using clock arrays when possible.

The {attributes} part of the declaration can be ommitted if no attribute is associated to the clock (or it can be left empty: {}). See section Attributes for details.

The int declaration

int:size:min:max:init:id{attributes}

declares the array of size bounded integer variables with identifier id and given attributes. Each variable in the array takes values between min and max (both included) and initial value init. No other integer variable shall have the same identifier.

For instance:

int:1:0:127:0:i

declares a single integer variable i with values between 0 and 127, and initial value 0.

And:

int:5:-128:127:-1:j

declares an array j of 5 integer variables with values between -128 and 127, and initial value -1. The first variable of the array is j[0] and the last one is j[4].

Out-of-bounds access like j[10] are detected and raise a fatal error when the model is analysed.

NB: the semantics of bounded integers in TChecker does not allow to assign an out-of-bound value to a variable. Consider variable i as declared above. Assigning -1 to i is illegal. Similarly, if i has value 127, then adding 1 to i is illegal. Illegal statements are simply deemed invalid and not executable (see section Semantics for details).

The {attributes} part of the declaration can be ommitted if no attribute is associated to the integer variable (or it can be left empty: {}). See section Attributes for details.

The location declaration

location:p:id{attributes}

declares location with identifier id in process with identifier p, and given attributes. The process identifier p shall have been declared previously. No other location within process p shall have the same identifier id. It is perfectly valid that two locations in different processes have the same identifier.

The {attributes} part of the declaration can be ommitted if no attribute is associated to the location (or it can be left empty: {}). See section Attributes for details.

The edge declaration

edge:p:source:target:e{attributes}

declares an edge in process p from location source to location target and labelled with event e. The process p shall have been declared previously. The two locations source and target shall have been declared as well, and they shall both belong to process p. The event e shall have been declared before the edge is declared.

The {attributes} part of the declaration can be omitted if no attribute is associated to the edge (or it can be left empty: {}). See section Attributes for details.

The sync declaration

sync:sync_constraints{attributes}

declares a synchronisation constraint with given attributes. sync_constraints is a colon-separated list of synchronisation constraints of the form p@e or p@e? where p is a process name, e is an event name, and the option question mark ? denotes a weak synchronisation. Process p and event e shall have been declared before the synchronisation is declared.

A sync declaration must contain at least 2 synchronisation constraints, and at most one synchronisation constraint for each process in the model. A (strong) synchronization constraint p@e means that process p shall synchronise one of its e labeled edge. A weak synchronisation constraint p@e? means that process p may synchronize one of its e labeled edge. Process p shall synchronize if it has an enabled e labelled edge. It does not prevent synchronization of the other processes otherwise.

If an event e appears in a sync declaration along with process p (i.e. in a constraint p@e or p@e?), then e labeled edges of process p shall only be taken synchronously (according to sync declarations). An event e that does not appear in any synchronisation constraint with process p is asynchronous in process p.

For instance, the following declarations (assuming processes and events have been declared):

sync:P1@a:P2@a
sync:P1@a:P2@b:P3@c?:P4@d?

entails that event a is synchronous in processes P1 and P2, event b is synchronous in process P2, event c is synchronous in process P3, and event d is synchronous in process P4. All other events are asynchronous.

Thus assuming the following set of edges (and that locations and events have been declared):

edge:P1:l0:l1:a
edge:P1:l0:l2:a

edge:P2:l0:l1:b

edge:P3:l0:l1:a

edge:P4:l0:l1:d

the set of global edges from the tuple of locations <l0,l0,l0,l0> (i.e. all the processes are in location l0) is:

<l0,l0,l0,l0> - <P1@a,P2@b,P4@d> -> <l1,l1,l0,l1>  // 2nd `sync` declaration
<l0,l0,l0,l0> - <P1@a,P2@b,P4@d> -> <l2,l1,l0,l1>  // 2nd `sync` declaration
<l0,l0,l0,l0> - <P3@a>           -> <l0,l0,l1,l0>  // asynchronous

Observe that the first sync declaration cannot be instantiated as process P2 has no a labelled edge from l0.

The second sync declaration can be instantiated as the two strong constraints P1@a and P2@b have corresponding edges. The weak synchronisation constraint P4@d? has a corresponding edge in P4 from l0, so P4 is involved in the global edge. P3 however has no c labelled edge from l0. Thus, the weak constraint P3@c? cannot be instantiated, and P3 does not participate to the global edge. However this does not prevent synchronisation of the other three processes. The second sync declaration is instantiated twice since process P1 has two a labelled edges from location l0.

Event a is asynchronous in process P3 as it does not appear in any sync declaration along with process P3. Hence there is a global asynchronous edge involving only process P3 with event a.

A sync declaration consisting only of weak synchronisation constraints like:

sync:P1@e?:P2@f?

is instantiated as soon as at least one of the constraint can be instantiated. Hence there is no global edge when P1 has no e labelled edge, and P2 has no f edge.

The {attributes} part of the declaration can be omitted if no attribute is associated to the synchronisation (or it can be left empty: {}). See section Attributes for details.

Attributes

Attributes allow to define properties of declarations. A list of attributes {attributes} is a colon-separated list of pairs key:value. Keys are identifier and values are any string not containing reserved symbols :, @ and spaces. The value may be empty.

There is no fixed list of allowed attributes. New attributes can be introduced at will as a way to provide information to algorithms. Current algorithms may emit a warning when an unknown attribute is encountered. But this shall not prevent the algorithm to analyse the model (without taking the unknown attribute into account).

Current models support the attributes described below.

Supported location attributes

  • initial: (no value) declares an initial location. Each process shall have at least one initial location, and it can have several of them

  • labels: list_of_labels declares the labels of a location (later used for reachability checking for instance). The list of labels is a comma-separated list of strings (not containing any reserved characters or spaces).

  • invariant: expression declares the invariant of the the location. See section Expressions for details on expressions

  • committed: (no value) declares the location committed (see Semantics for details).

  • urgent: (no value) declares the location urgent (see Semantics for details).

Supported edge attributes

  • provided: expression declares the guard of the edge. See section Expressions for details on expressions.

  • do: statement declares the statement of the edge. See section Statements for details on statements.

Expressions

Expressions are conjunctions of atomic expression or negation of atomic expressions. An atomic expression is either a term or a binary predicate applied to two terms. Terms consists in integer constants, variables and arithmetic operators applied to terms. Expressions are defined by the following grammar:

expr ::= atomic_expr
       | atomic_expr && expr

atomic_expr ::= int_term
              | predicate_expr
	      | ! atomic_expr
	      | clock_expr

predicate_expr ::= ( predicate_expr )
                 | int_term == int_term
		 | int_term != int_term
		 | int_term < int_term
		 | int_term <= int_term
		 | int_term >= int_term
		 | int_term > int_term
                 | int_term {<, <=} int_term {<, <=} int_term

int_term ::= INTEGER
           | lvalue_int
           | - int_term
           | int_term + int_term
           | int_term - int_term
           | int_term * int_term
           | int_term / int_term
           | int_term % int_term

lvalue_int ::= INT_VAR_ID
             | INT_VAR_ID [ term ]

where INT_VAR_ID is a bounded integer variable identifier, and INTEGER is a signed integer constant. Notice that integer terms int_term are atomic expressions with the usual convention that the expression is false iff the term has value 0.

Comined expressions such as 2 < i <= 3*j are supported from release v0.7.

There are restrictions on atomic expressions involving clock variables. We only allow comparisons of clocks or difference of clocks w.r.t. integer terms:

clock_expr ::= clock_term cmp int_term
             | int_term cmp clock_term
       | lvalue_clock cmp lvalue_clock
       | int_term {<, <=} clock_term {<, <=} int_term

clock_term ::= lvalue_clock
             | lvalue_clock - lvalue_clock

lvalue_clock ::= CLOCK_ID
               | CLOCK_ID [ int_term ]

cmp ::= == | < | <= | >= | >

where CLOCK_ID is a clock identifier.

Prior to v0.7, only clock expressions of the first kind were allowed (clock term to the left of the comparator only). From v0.7, clock terms are also allowed to the right of the operator. Combined expressions such as 0 <= x < 5*i have been added. Finally, comparison of two clocks can simply be written as x==y.

Notice that combined clock expressions such as 0 <= x < 5*i have the semantics of the conjunction of the two subformulas: 0 <= x && x < 5*i.

Statements

Statements are sequences of assignements, while loops, if statements or nop:

stmt ::= statement
       | statement ; stmt

statement ::= simple_statement
            | if_statement
            | while_statement

simple_statement ::= int_assigment
                   | clock_assigment
                   | local_statement
                   | nop

if_statement ::= if expr then stmt end
               | if expr then stmt else stmt end

while_statement ::= while expr do stmt end

The expressions expr appearing as conditionals in if and while statements should not contain any clock constraints.

Assignments operate in the standard way: the value of a term is assigned to a left-value expression: a one-dimensional variable, the cell of an array, etc.

int_assignment ::= lvalue_int = int_term

Assignments to clock variables are restricted to assignment of a constant to a clock x = d or "diagonal assignments" of the form x = y or x = d + y where d is any integer term:

clock_assignment ::= lvalue_clock = int_term
		               | lvalue_clock = int_term + lvalue_clock

Local statements allow to declare local variables:

local_statement ::= local id
                  | local id = term
                  | local id[term]

The first statement declares a uninitialised local variable id. The second one declares a local variable id initialised to the value of term. And the last statement declares an array id of local variables of the size given by the value of term.

Local variables can be used to define loop ranges, for instances:

local i = 0;
while (i < 10) do
  ...
  i = i + 1
end

Please, notice that statements are evaluated sequentially (not concurrently). As a result, assuming that i has value 2 and j has value 3, executing i=j; j=i results in i having value 3 and j having value 3 as well.

Semantics

The configurations of the timed automaton consists in a tuple of locations L and a valuation V of the bounded integer variables (as for finite-state machines) and a valuation X of the clocks in the model.

The initial configurations are triples (L,V,X) such that L is a tuple of initial locations, V maps each variable to its initial value, and X maps each clock to 0, and the invariant attribute if each location in L is satisfied by V and X.

There are two kinds of transitions:

There is a discrete transition (L,V,X) -- E -> (L',V',X') if there is a tuple E of edges from L that instantiates a sync declaration, or E consists of a single asynchronous edge, and:

  • the provided attribute of each edge in E is satisfied by V and X,

  • V' and X' is obtained from V and X by applying the do attribute of each edge in E consecutively

  • for each variable i, V'(i) is in the domain of i

  • L' is obtained from L according to the edges in E

  • V' and X' satisfies the invariant of each location in in L'

  • and E involves (at least) one process with a committed location in L if any

There is a timed transition (L,V,X) ---> (L,V,X') if:

  • L has no committed and no urgent location

  • there is a non-negative real number d such that X'(y)=X(y)+d for each clock y

  • and the invariant in L is satisfied by V and X'.

This defines a transition system with configurations, initial configurations and transitions as described above.

NB: due to while statements, the evaluation of a discrete transition may not terminate. This is considered as an error in the model.

Clone this wiki locally