Class Parser

Production rules to build parser for ltl2ba output.

Instance Methods

__init__(self)
Build lexer and parser.

parse(self, ltl2ba_output)
Return a Buchi automaton from parsing ltl2ba_output.

p_claim(self, p)
claim : NEVER LBRACE COMMENT clauses RBRACE

p_clauses(self, p)
clauses : clauses clause

p_clauses_end(self, p)
clauses : clause

p_clause(self, p)
clause : if_clause

p_clause_labeled(self, p)
clause : state COLON if_clause

p_if_clause(self, p)
if_clause : IF cases FI SEMI

p_cases(self, p)
cases : cases case

p_cases_end(self, p)
cases : case

p_case(self, p)
case : COLON2 expr IMP goto

p_expr_paren(self, p)
expr : LPAREN expr RPAREN

p_and(self, p)
expr : expr AND expr

p_or(self, p)
expr : expr OR expr

p_not(self, p)
expr : NOT expr

p_number(self, p)
expr : NUMBER

p_expr_name(self, p)
expr : NAME

p_goto(self, p)
goto : GOTO state

p_state(self, p)
state : NAME

p_empty(self, p)
empty :

p_error(self, p)

Inherited from object: __delattr__, __format__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __repr__, __setattr__, __sizeof__, __str__, __subclasshook__

Class Variables
	precedence = `(('right', 'BIMP'), ('right', 'IMP'), ('left', 'X...`

Properties
Inherited from `object`: `__class__`

Method Details

init(self)
(Constructor)

Build lexer and parser.

Overrides: object.__init__

parse(self, ltl2ba_output)

Return a Buchi automaton from parsing ltl2ba_output.

Returns:

Buchi automaton as a 3-`tuple` containing:

`dict` mapping symbols to types (all `"boolean"`)
`networkx.MultiDiGraph`, each edge labeled with a `"guard"` that is a Boolean formula as `str`
`set` of initial nodes
`set` of accepting nodes

Class Variable Details

precedence

Value:

(('right', 'BIMP'),
 ('right', 'IMP'),
 ('left', 'XOR'),
 ('left', 'OR'),
 ('left', 'AND'),
 ('right', 'NOT'),
 ('nonassoc', 'EQUALS', 'NEQUALS', 'LT', 'LE', 'GT', 'GE'),
 ('nonassoc', 'TIMES', 'DIV'),
...

Class Parser

__init__(self) (Constructor)

parse(self, ltl2ba_output)

precedence

init(self)
(Constructor)