|
spot 2.13
|
separate edges so that their labels are disjoint More...
#include <spot/twaalgos/split.hh>
Public Member Functions | |
| twa_graph_ptr | separate_implying (const const_twa_graph_ptr &aut) |
| Separate an automaton. More... | |
| twa_graph_ptr | separate_compat (const const_twa_graph_ptr &aut) |
| Separate an automaton. More... | |
| edge_separator_filter< true > | separate_implying (bdd label) |
| Separate a label. More... | |
| edge_separator_filter< false > | separate_compat (bdd label) |
| Separate a label. More... | |
| unsigned | basis_size () const |
| const std::vector< bdd > & | basis () const |
| void | add_to_basis (bdd label) |
| add label(s) to a basis More... | |
| void | add_to_basis (const const_twa_graph_ptr &aut) |
| add label(s) to a basis More... | |
| bool | add_to_basis (const const_twa_graph_ptr &aut, unsigned long max_label) |
| add label(s) to a basis More... | |
separate edges so that their labels are disjoint
To use this class, first call add_to_basis() for each label that you want to separate. Then call separate() to get a new automaton.
Note that all labels seen by separate() should have been previously declared using add_to_basis(), but more can be declared.
For instance an automaton has labels in {a,b,!a&!b&c} and those are used as basis, the separated automaton should have its labels among {a&!b,a&b,!a&b,!a&!b&c}.
| void spot::edge_separator::add_to_basis | ( | bdd | label | ) |
add label(s) to a basis
Add a single label, or all the labels of an automaton.
The version that takes an automaton will also record the atomic propositions used by the automaton. Those atomic propositions will be registered by separate_implying() or separate_compat(). If you call the BDD version of add_to_basis() and add a new atomic proposition, you should remember to register it in the result of separate_implying() or separate_compat() yourself.
If max_label is given, at most max_label unique labels are added to the basis. False is returned iff the automaton used more labels.
| void spot::edge_separator::add_to_basis | ( | const const_twa_graph_ptr & | aut | ) |
add label(s) to a basis
Add a single label, or all the labels of an automaton.
The version that takes an automaton will also record the atomic propositions used by the automaton. Those atomic propositions will be registered by separate_implying() or separate_compat(). If you call the BDD version of add_to_basis() and add a new atomic proposition, you should remember to register it in the result of separate_implying() or separate_compat() yourself.
If max_label is given, at most max_label unique labels are added to the basis. False is returned iff the automaton used more labels.
| bool spot::edge_separator::add_to_basis | ( | const const_twa_graph_ptr & | aut, |
| unsigned long | max_label | ||
| ) |
add label(s) to a basis
Add a single label, or all the labels of an automaton.
The version that takes an automaton will also record the atomic propositions used by the automaton. Those atomic propositions will be registered by separate_implying() or separate_compat(). If you call the BDD version of add_to_basis() and add a new atomic proposition, you should remember to register it in the result of separate_implying() or separate_compat() yourself.
If max_label is given, at most max_label unique labels are added to the basis. False is returned iff the automaton used more labels.
|
inline |
Separate a label.
This returns a pseudo-container that can be used to iterate over the elements of the basis compatible with the current label.
For instance if the basis was created from {a,b} (i.e., the basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is {c&a}, the result will be {a&!b&c,a&b&c}.
| twa_graph_ptr spot::edge_separator::separate_compat | ( | const const_twa_graph_ptr & | aut | ) |
Separate an automaton.
This variant replaces each edge labeled by L by an edge for each label of the basis that compatible implies L. This faster than separate_compat when all edges of aut have been declared in the basis.
|
inline |
Separate a label.
This returns a pseudo-container that can be used to iterate over the elements of the basis that imply the current label.
For instance if the basis was created from {a,b} (i.e., the basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is {a}, the result will be {a&!b,a&b}.
| twa_graph_ptr spot::edge_separator::separate_implying | ( | const const_twa_graph_ptr & | aut | ) |
Separate an automaton.
This variant replaces each edge labeled by L by an edge for each label of the basis that is implies L. This faster than separate_compat when all edges of aut have been declared in the basis.
1.9.4