Liana Grammar

Timed Automata and Arenas

The following is the grammar for the Liana DSL used to create Timed Automata and Timed Arenas. Whether the actions are input (?) or output (!) actions must be specified only in the transitions. T and F are syntactic sugar for true and false. Since clock guards cannot directly express disjunctions, OR conditions must be modeled by defining one transition per disjunct. Timed Automata marked as symmetric must be structurally identical (the integer indicates the symmetry group to which they are assigned). In Timed Arenas, each location is assigned to a player: controller (c) or environment (e).

⟨automaton⟩ ――> 'create' 'automaton' ⟨literal⟩ (ε | ⟨symm_rule⟩)
                '{'
                'clocks'        '{' (ε | ⟨literal⟩ (',' ⟨literal⟩)* ';') '}'
                'actions'       '{' ⟨literal⟩ (',' ⟨literal⟩)* ';' '}'
                (ε | 'integers' '{' ⟨literal⟩ (',' ⟨literal⟩)* ';' '}')
                'locations'     '{' ⟨locations_rule⟩ '}'
                'transitions'   '{' ⟨transition_rule⟩ (',' ⟨transition_rule⟩)* ';' '}'
                '}'

⟨arena⟩ ――> 'create' 'arena' ⟨literal⟩ (ε | ⟨symm_rule⟩)
             '{'
             'clocks'        '{' (ε | ⟨literal⟩ (',' ⟨literal⟩)* ';') '}'
             'actions'       '{' ⟨literal⟩ (',' ⟨literal⟩)* ';' '}'
             (ε | 'integers' '{' ⟨literal⟩ (',' ⟨literal⟩)* ';' '}')
             'locations'     '{' ⟨arena_locations_rule⟩ '}'
             'transitions'   '{' ⟨transition_rule⟩ (',' ⟨transition_rule⟩)* ';' '}'
             '}'

⟨symm_rule⟩ ――> '::' 'symm' '<' ⟨int⟩ '>'

⟨locations_rule⟩ ――> ⟨loc_rule⟩ (',' ⟨loc_rule⟩)* ';'

⟨loc_rule⟩ ――> ⟨literal⟩ ⟨loc_content_rule⟩

⟨arena_locations_rule⟩ ――> ⟨arena_loc_rule⟩ (',' ⟨arena_loc_rule⟩)* ';'

⟨arena_loc_rule⟩ ――> ⟨literal⟩ ⟨arena_loc_content_rule⟩

⟨arena_loc_content_rule⟩ ――> '<' 'player' ':' ⟨player⟩ ',' ⟨loc_content_rule⟩ '>'

⟨player⟩ ――> 'c' | 'e'

⟨loc_content_rule⟩ ――> '<'
                       (ε | 
                        ⟨ini⟩ | ⟨urg⟩ | ⟨inv⟩ |
                        ⟨ini⟩ ',' ⟨urg⟩ | ⟨ini⟩ ',' ⟨inv⟩ | ⟨urg⟩ ',' ⟨inv⟩ |
                        ⟨ini⟩ ',' ⟨urg⟩ ',' ⟨inv⟩)
                       '>'

⟨ini⟩ ――> 'ini' ':' ⟨bool⟩

⟨urg⟩ ――> 'urg' ':' ⟨bool⟩

⟨inv⟩ ――> 'inv' ':' ⟨guard_rule⟩

⟨bool⟩ ――> 'T' | 'F' | 'true' | 'false'

⟨transition_rule⟩ ――> '('
                      ⟨literal⟩ ','
                      ⟨actions_rule⟩ ','
                      ⟨guard_rule⟩ ','
                      (ε | ⟨boolean_expr⟩ ',')
                      '[' (ε | ⟨literal⟩ (',' ⟨literal⟩)*) ']' ','
                      (ε | '[' ⟨assignment_expr⟩ (',' ⟨assignment_expr⟩)* ']' ',')
                      ⟨literal⟩
                      ')'

⟨guard_rule⟩ ――> '[' (ε | ⟨clock_constraint_rule⟩ (',' ⟨clock_constraint_rule⟩)*) ']'

⟨actions_rule⟩ ――> ⟨literal⟩ (ε | ⟨input_output_action⟩)

⟨input_output_action⟩ ――> '!' | '?'

⟨clock_constraint_rule⟩ ――> '(' ⟨literal⟩ ',' ⟨comparison_operator⟩ ',' ⟨int⟩ ')'

⟨comparison_operator⟩ ――> '<' | '<=' | '==' | '>=' | '>'

⟨int⟩ ――> '1..9' ('0..9')*

⟨literal⟩ ――> ('a..z' | 'A..Z' | '0..9' | '_')+

---

Arithmetic Expressions

The following is the grammar for the Liana DSL used to declare arithmetic expressions. Integer variables in Timed Automata are automatically initialized to zero. To overcome this, a transition can be added to initialize them in the Timed Automaton itself.

⟨assignment_expr⟩ ――> ⟨variable⟩ '=' ⟨arithmetic_expr⟩

⟨arithmetic_expr⟩ ――> ⟨additive_expr⟩

⟨additive_expr⟩ ――> ⟨multiplicative_expr⟩ (⟨add_op⟩ ⟨multiplicative_expr⟩)*

⟨multiplicative_expr⟩ ――> ⟨primary_expr⟩ (⟨mult_op⟩ ⟨primary_expr⟩)*

⟨primary_expr⟩ ――> ⟨int⟩ | ⟨variable⟩ | '(' ⟨additive_expr⟩ ')'

⟨variable⟩ ――> ⟨literal⟩

⟨add_op⟩ ――> '+' | '-'

⟨mult_op⟩ ――> '*' | '/'

⟨boolean_expr⟩ ――> ⟨boolean_or_expr⟩

⟨boolean_or_expr⟩ ――> ⟨boolean_and_expr⟩ (⟨or_op⟩ ⟨boolean_and_expr⟩)*

⟨boolean_and_expr⟩ ――> ⟨boolean_term⟩ (⟨and_op⟩ ⟨boolean_term⟩)*

⟨boolean_term⟩ ――> '(' ⟨boolean_or_expr⟩ ')' | ⟨comparison_expr⟩ | ⟨bool⟩

⟨comparison_expr⟩ ――> ⟨arithmetic_expr⟩ ⟨comparison_operator⟩ ⟨arithmetic_expr⟩

⟨or_op⟩ ――> '||'

⟨and_op⟩ ――> '&&'

---

CLTLoc Formulae

The following is the grammar for CLTLoc (Constraint Linear Temporal Logic over clocks) formulae.

⟨general_cltloc_formula⟩ ――> '(' (⟨unary_cltloc_formula⟩ | ⟨binary_cltloc_formula⟩ | ⟨pure_cltloc_formula⟩) ')'

⟨unary_cltloc_formula⟩ ――> ⟨unary_cltloc_op⟩ (ε | '^' ⟨int⟩) ⟨general_cltloc_formula⟩

⟨binary_cltloc_formula⟩ ――> ⟨general_cltloc_formula⟩ ⟨binary_cltloc_op⟩ ⟨general_cltloc_formula⟩

⟨pure_cltloc_formula⟩ ――> ⟨pure_disjunct⟩ ('||' ⟨pure_disjunct⟩)*

⟨pure_disjunct⟩ ――> '[' (ε | ⟨literal⟩ (',' ⟨literal⟩)*) ']' ','
                    '[' (ε | ⟨clock_constraint_rule⟩ (',' ⟨clock_constraint_rule⟩)*) ']'

⟨unary_cltloc_op⟩ ――> 'BOX' | 'DIAMOND'

⟨binary_cltloc_op⟩ ――> 'UNTIL'

⟨conjunction_of_formulae⟩ ――> ⟨conjunction_type⟩ ⟨general_cltloc_formula⟩ (⟨and_op⟩ ⟨general_cltloc_formula⟩)*

⟨conjunction_type⟩ ――> 'AND_GENERAL' | 'AND_NEXT'

← Back to Main Page