Grammar for the low-level input

S ::= Vars

      integer

      Rules

      set_of_rules

      Initial state

      init_states

      Target state

      target_states

      Invariant

      invariant_set

set_of_rules ::= guard -> effectset

guard ::= guard_atom , guard

        | guard_atom

guard_atom ::= variable relop integer

             | variable in [integer, integer]

relop ::= =

        | >=

effectset ::= effect effectset

            | effect

effect ::= variable = assignment_var assignment_cst

assignment_var ::= variable + assignment_var

                 | variable

assignment_cst ::= + integer

                 | - integer

                 | epsilon

init_states ::= guard init_states

              | guard

target_states ::= guard target_states

                | guard

% The format of invariants has not been fixet yet!!!

invariant_set ::= invariant invariant_set

                | epsilon

invariant ::= # variable = integer , invariant

            | # variable = integer

Some Remarks

• The trivial effects like Xi = Xi are not expressed.
• For the invariants: #Xi=c expresses the weight in front of variable Xi.