Production rules to build LTL parser.
|
|
__init__(self,
ast=None,
lexer=None)
x.__init__(...) initializes x; see help(type(x)) for signature |
|
|
|
|
build(self,
tabmodule=None,
outputdir='',
write_tables=False,
debug=False,
debuglog=None)
Build parser using `ply.yacc`. |
|
|
|
|
parse(self,
formula,
debuglog=None)
Parse formula string and create abstract syntax tree (AST). |
|
|
|
|
p_nullary_connective(self,
p)
expr : TRUE | FALSE |
|
|
|
|
p_unary_connective(self,
p)
expr : NOT expr | ALWAYS expr | EVENTUALLY expr | NEXT expr |
|
|
|
|
p_postfix_next(self,
p)
expr : expr PRIME |
|
|
|
|
p_binary_connective(self,
p)
expr : expr AND expr | expr OR expr | expr XOR expr | expr IMP expr |
expr BIMP expr | expr UNTIL expr | expr WEAK_UNTIL expr | expr
RELEASE expr |
|
|
|
|
p_ternary_conditional(self,
p)
expr : LPAREN ITE expr COMMA expr COMMA expr RPAREN |
|
|
|
|
p_binary_predicate(self,
p)
expr : expr EQUALS expr | expr NEQUALS expr | expr LT expr | expr LE
expr | expr GT expr | expr GE expr |
|
|
|
|
p_truncator(self,
p)
expr : expr TRUNCATE number |
|
|
|
|
p_binary_function(self,
p)
expr : expr TIMES expr | expr DIV expr | expr PLUS expr | expr MINUS
expr |
|
|
|
|
p_paren(self,
p)
expr : LPAREN expr RPAREN |
|
|
|
|
p_var(self,
p)
expr : NAME |
|
|
|
|
p_number_expr(self,
p)
expr : number |
|
|
|
|
p_number(self,
p)
number : NUMBER |
|
|
|
|
p_negative_number(self,
p)
expr : MINUS NUMBER %prec UMINUS |
|
|
|
|
p_string(self,
p)
expr : DQUOTES NAME DQUOTES |
|
|
|
|
|
|
Inherited from object:
__delattr__,
__format__,
__getattribute__,
__hash__,
__new__,
__reduce__,
__reduce_ex__,
__repr__,
__setattr__,
__sizeof__,
__str__,
__subclasshook__
|