|
spot 2.15
|
"Semi-internal" for translating LTL using MTBDDs More...
#include <spot/twaalgos/mtdswa.hh>
Public Member Functions | |
| simple_ltl_translator (const bdd_dict_ptr &dict, bool simplify_terms=true) | |
| mtdswa_ptr | ltl_to_mtdswa (formula f, bool fuse_same_bdds) |
| mtdswa_ptr | ltl_to_mtdswa_synthesis (formula f, const std::vector< std::string > &outvars, bool realizability, int debug=-1) |
| bdd | ltl_to_mtbdd (formula f) |
| formula | leaf_to_formula (int b, int term) const |
| formula | terminal_to_formula (int t) const |
| int | formula_to_int (formula f) |
| int | formula_propeq_to_int (formula f) |
| int | formula_to_terminal (formula f) |
| bdd | formula_to_terminal_bdd (formula f) |
| int | formula_to_terminal_bdd_as_int (formula f) |
| int | formula_propeq_to_terminal_bdd_as_int (formula f) |
| 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) |
| bdd | propeq_encode (formula f, int level=0) |
| formula | propeq_representative (formula f, bool isacc) |
| bddExtCache * | get_cache () |
"Semi-internal" for translating LTL using MTBDDs
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.8