This module features a parser for CTL* formula. Function build parses the formula (see concrete syntax below) and expands sub-formulas; then it returns an abstract syntax tree (see abstract syntax) below.

>>> from snakes.utils.ctlstar.build import *
>>> spec = '''
... atom even (x : int) :
...     return x % 2 == 0
... atom odd (x : int) :
...     return x % 2 == 1
... prop evenplace (p : place) :
...     exists tok in p (even(x=tok))
... prop oddplace (p : place) :
...     exists tok in p (odd(x=tok))
... A (G (evenplace(p=@'some_place') => F oddplace(p=@'another_place')))
... '''
>>> tree = build(spec)
>>> print ast.dump(tree)
CtlUnary(op=All(), child=CtlUnary(op=Globally(), child=CtlBinary(op=Imply(), ...

In the example above, atom allows to define parameterised atomic propositions and prop allows to define sub-formulas. In the returned syntax tree, all these objects are inlined and fully instantiated.

Concrete syntax

file_input: (NEWLINE | ctl_atomdef | ctl_propdef)* [ ctl_formula ] NEWLINE* ENDMARKER

ctl_atomdef: 'atom' NAME '(' [ctl_parameters] ')' ':' suite
ctl_propdef: 'prop' NAME '(' [ctl_parameters] ')' ':' ctl_suite
ctl_suite: ( ctl_formula NEWLINE
        | NEWLINE INDENT ctl_formula NEWLINE+ DEDENT )
ctl_parameters: (ctl_param ',')* ctl_param
ctl_param: NAME ( '=' '@' STRING+ | ':' NAME )

ctl_formula: ctl_or_formula [ ctl_connector ctl_or_formula ]
ctl_connector: ( '=' '>' | '<=' '>' )
ctl_or_formula: ctl_and_formula ('or' ctl_and_formula)*
ctl_and_formula: ctl_not_formula ('and' ctl_not_formula)*
ctl_not_formula: ('not' ctl_not_formula | ctl_binary_formula)
ctl_binary_formula: ctl_unary_formula [ ctl_binary_op ctl_unary_formula ]
ctl_unary_formula: [ ctl_unary_op ] (ctl_atom_formula | '(' ctl_formula ')')
ctl_unary_op: ('A' | 'G' | 'F' | 'E' | 'X')
ctl_binary_op: ('R' | 'U' | 'W')
ctl_atom_formula: ( 'empty' '(' ctl_place ')'
                   | 'marked' '(' ctl_place ')'
           | 'has' ['not'] '(' ctl_place ',' test (',' test)* ')'
           | 'deadlock' | 'True' | 'False'
           | NAME '(' ctl_arguments ')'
           | 'forall' [ 'distinct' ] NAME (',' NAME)*
                     'in' ctl_place '(' ctl_atom_formula ')'
           | 'exists' [ 'distinct' ] NAME (',' NAME)*
                     'in' ctl_place '(' ctl_atom_formula ')' )
ctl_arguments: (NAME '=' ctl_place_or_test ',')* NAME '=' ctl_place_or_test
ctl_place: '@' STRING+ | NAME
ctl_place_or_test: test | '@' STRING+

Abstract syntax

    ctlstar = Spec(ctldecl* atoms,
                   ctldecl* properties,
                   form? main)
            attributes (int lineno, int col_offset)

    ctldecl = Atom(identifier name,
                   ctlarg* args,
                   ctlparams* params,
                   stmt* body)
            | Property(identifier name,
                       ctlargs* args,
                       ctlparams* params,
                       form body)
            attributes (int lineno, int col_offset)

    ctlarg = Place(identifier name,
                   string place)
            | Token(identifier name,
                    string place)
            | Argument(identifier name,
                       expr value,
                       identifier type)
            attributes (int lineno, int col_offset)

    ctlparam = Parameter(identifier name,
                         identifier type)
             attributes (int lineno, int col_offset)

    form = atom
          | CtlUnary(ctlunary op,
                     form child)
          | CtlBinary(ctlbinary op,
                      form left,
                      form right)
          attributes (int lineno, int col_offset)

    ctlunary = notop | All | Exists | Next
             | Future | Globally

    notop = Not

    ctlbinary = boolop | Imply | Iff
              | Until | WeakUntil | Release

    atom = InPlace(expr* data, ctlarg place)
          | NotInPlace(expr* data, ctlarg place)
          | EmptyPlace(ctlarg place)
          | MarkedPlace(ctlarg place)
          | Deadlock
          | Boolean(bool val)
          | Instance(identifier name, arg* args)
          | Quantifier(ctlunary op,
                       identifier* vars,
                       ctlarg place,
                       form child,
                       bool distinct)
          attributes (int lineno, int col_offset)