|
spot 2.14
|
"Semi-internal" class used to implement spot::ltlf_to_mtdfa() More...
#include <spot/twaalgos/ltlf2dfa.hh>
Public Member Functions | |
| ltlf_translator (const bdd_dict_ptr &dict, bool simplify_terms=true) | |
| mtdfa_ptr | ltlf_to_mtdfa (formula f, bool fuse_same_bdds, bool detect_empty_univ=true, const std::vector< std::string > *outvars=nullptr, bool do_backprop=false, bool realizability=false, bool one_step_preprocess=false, bool bfs=true) |
| mtdfa_ptr | ltlf_synthesis_with_dfs (formula f, const std::vector< std::string > *outvars=nullptr, bool realizability=false, bool ont_step_preprocess=false) |
| bdd | ltlf_to_mtbdd (formula f) |
| std::pair< formula, bool > | leaf_to_formula (int b, int term) const |
| formula | terminal_to_formula (int t) const |
| int | formula_to_int (formula f) |
| int | formula_to_terminal (formula f, bool may_stop=false) |
| bdd | formula_to_terminal_bdd (formula f, bool may_stop=false) |
| int | formula_to_terminal_bdd_as_int (formula f, bool may_stop=false) |
| bdd | combine_and (bdd left, bdd right) |
| bdd | combine_or (bdd left, bdd right) |
| bdd | combine_implies (bdd left, bdd right) |
| bdd | combine_equiv (bdd left, bdd right) |
| bdd | combine_xor (bdd left, bdd right) |
| bdd | combine_not (bdd b) |
| formula | propeq_representative (formula f) |
| bddExtCache * | get_cache () |
"Semi-internal" class used to implement spot::ltlf_to_mtdfa()
It is public only to make it possible to demonstrate the inner working of the translation. Do not rely on the interface to be stable.
1.9.4