23#include <unordered_map>
24#include <spot/misc/common.hh>
25#include <spot/twacube/cube.hh>
26#include <spot/twacube/twacube.hh>
27#include <spot/twa/twagraph.hh>
35 std::unordered_map<int, int>& binder);
40 std::unordered_map<int, int>& reverse_binder);
44 SPOT_API std::vector<std::string>*
46 std::unordered_map<int, int>& ap_binder);
55 SPOT_API spot::twa_graph_ptr
57 spot::bdd_dict_ptr d =
nullptr);
61 const spot::const_twa_graph_ptr
twa);
A Transition-based ω-Automaton.
Definition: twa.hh:619
Class for representing a thread-safe twa.
Definition: twacube.hh:122
bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right)
Test if the language of left is equivalent to that of right.
Definition: automata.hh:26
bdd cube_to_bdd(spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes.
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:65
spot::cube satone_to_cube(bdd one, cubeset &cubeset, std::unordered_map< int, int > &binder)
Transform one truth assignment represented as a BDD into a cube cube passed in parameter....
twacube_ptr twa_to_twacube(spot::const_twa_graph_ptr aut)
Convert a twa into a twacube.
spot::twa_graph_ptr twacube_to_twa(spot::twacube_ptr twacube, spot::bdd_dict_ptr d=nullptr)
Convert a twacube into a twa. When d is specified, the BDD_dict in parameter is used rather than crea...
std::vector< std::string > * extract_aps(spot::const_twa_graph_ptr aut, std::unordered_map< int, int > &ap_binder)
Extract the atomic propositions from the automaton. This method also fill the binder,...