Linear temporal logic to Büchi automaton: Difference between revisions

Revision as of 23:02, 16 March 2017

Revision as of 08:49, 26 May 2017

Line 160:

For a node q, ''Now''(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at node(state) q.

''Next''(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at the next node(state) after q.

{{pre|1=

'''typedefs'''

'''LTL''': LTL formulas

Line 176:

'''return''' (''Nodes'', ''Now'', ''Incoming'')

}

}}

'''function''' expand('''LTLSet''' curr, '''LTLSet''' old, '''LTLSet''' next, '''NodeSet''' incoming){

1: '''if''' curr = ∅ '''then'''