|
| | | NBAC format |
The input format of the automaton is a simple low-level format to specify dataflows equations on Booleans and numerics (integers, reals or clocks, which are reals subject to continuous evolution). An optional continuous behaviour may be specified.
| <file> | ::= | <declarations> |
| <definitions> <transitions> [<continuous>] | ||
| <assertion and property formulas> | ||
| [<control_structure>] | ||
| [<control directive>] |
| <type_definitions> | ::= | typedef <type_definition>+ |
| <type_definition> | ::= | <ident> = enum { (<ident> (,<ident>)+ } ; |
| <type> | ::= | bool | int | real | clock |
| | | <ident> | |
| | | sint[<integer>] | uint[<integer>] |
Enumerated types can be defined. Labels should be different among different types, and different from variable names.
The available types for variables and expressions are resp. Booleans, integers, reals, clocks, enumerated types (referenced by their name) and bounded integers, which may be signed (sint) or unsigned (uint). The positive integer between bracket indicates the number of bits used for the encoding. Arithmetic on values of these two types follows the rule of microprocessor's arithmetic.
Clocks are special real variables which may be subject to a continuous evolution. A standard real variable does not evolve during a continuous evolution: its derivative is always equal to 0.
| <declarations> | ::= | [<type_definitions>] |
| <state_declarations> [<input_declarations>] | ||
| [<local_declarations>] | ||
| <state_declarations> | ::= | state <vars_type>+ |
| <input_declarations> | ::= | input <vars_type>+ |
| <local_declarations> | ::= | local <vars_type>+ |
| <vars_type> | ::= | (<ident> (,<ident>)+ : <type> ; |
Possible enumerated types definitions are first declared. Then variables are declared. We distinguish state variables and input variables: at each execution step, state variables take new values computed from their current values and the values of input variables. Local variables can be considered as macros or alias.
| <definitions> | ::= | definition <definition>+ |
| <transitions> | ::= | transition <transition>+ |
| <definition> | ::= | <ident> = <expression> ; |
| <transition> | ::= | <ident>' = <expression> ; |
The definitions define the values of local variables with expressions (of suitable type) depending on state, input an other local variables. Dependencies between local variables should be acyclic ! (this is checked). The transitions define the values of state variables at the next execution step in function of the current values of state, input and local variables.
In case of an hybrid automaton, the continuous behaviour is specified as follows:
| <continuous> | ::= | continuous <dexpr_list> ; |
| <dexpr_list> | ::= | <dexpr> , <dexpr_list> | <dexpr> |
The list of derivative expression should be understood as a conjunction.
| <assertion and property formulas> | ::= | (<property directive>)* |
| <property directive> | ::= | <assertion> | <initial> | <final> |
| <assertion> | ::= | assertion <expression> ; |
| <initial> | ::= | initial <expression> ; |
| <final> | ::= | (invariant | final) <expression> ; |
The assertion allows to constrain the values of input variables depending on the current state. It is defined by a Boolean expression on all variables, which give for each state the possible values for input variables. The initial condition defines the set of initial states by a Boolean expression on state variables, the final condition the set of invariant or final states by a Boolean expression on state variables. Invariant is the same as the negation of final.
If the assertion directive is omitted, the assertion is true.
If the initial or final directives are omitted, they are set to false.
| <control_structure> | ::= | automaton <location>+ <edge>+ |
| <location> | ::= | location <ident> : <expression> ; |
| <edge> | ::= | edge ( <ident> , <ident> ) : <expression> ; |
| | | edge ( <ident> , <ident> ) : <expression> , <expression> ; |
A explicit control structure, defined on the previously defined dataflow system, is specified by a set of locations and edges. A location is defined by a state condition, which give the set of states represented by the location. To edges are associated a Boolean expression on state and input variables that indicate a necessary condition under which the edge can be taken by a discrete transition (first form). If a second expression is given, it indicates a necessary condition for a continuous evolution to jump from the origin location to the destination location.
The union of all state conditions of the locations indicates the considered state-space. The union of all discrete edge conditions allows to enforce the global assertion of the system.
| <control directive> | ::= | control <expression> (, <expression>)* ; |
The expressions involved in the list are supposed to be atomic conditions, that is, Boolean variables, enumerated variables, or linear inequalities. This optional directive specifies that the control structure should first be refined according to these conditions, so that in every location these variables or conditions have definite values, before resorting to refinement heuristics. These behaviour takes place after the optional initial control structure specification has been taken into account.
| <constant> | ::= | true | false |
| | | <num> | |
| | | <sint>[<integer>](<integer>) | <uint>[<integer>](<integer>) | |
| <num> | ::= | <integer> | <integer>/<integer> |
| <expression> | ::= | <constant> |
| | | <ident> | <num><ident> | |
| | | ( <expression> ) | |
| | | not <expression> | |
| | | <expression> <binop> <expression> | |
| | | #( <expression_list> ) | |
| | | <expression> in { <expression_list> } | |
| | | if <expression> then <expression> else <expression> |
| <binop> | ::= | or | and | xor | eq | xor | => |
| | | = | < | <= | >= | > | |
| | | + | - | * | / |
Expressions are Boolean, finite type (enumerated or bounded integer), or guarded linear affine expression. Constants are either Boolean constants, integers or rational constants, or bounded integer constants, for which the type indicates how to interpret the second integer. For instance, sint[3](2) denotes the integer 2 encoded as a 3 bits signed integers.
The operators have the usual meaning. Arithmetic on bounded integers follows the rules of microprocessor's arithmetic. # is the exclusive operator coming from LUSTRE: it returns true if and only if at most one of its operands is true. in is mainly useful for enumerated and bounded integer types. e in {e1,e2,e3} is a shortcut for e=e1 or e=e2 or e=e3.
The priorities are: { *,/ } > { +,- } > { <, <=, =, >=,> } > { not,# } > { =, <>, xor, in } > { and } > { or } > { => } > { if then else }
| <dexpr> | ::= | blocked | anything | <linexpr> |
| | | ( <dexpr> ) | |
| | | <dexpr> and <dexpr> | |
| | | if <expression> then <dexpr> else <dexpr> |
|
| | | NBAC format |