spot
2.5.1
|
Classes | |
struct | acc_code |
union | acc_word |
struct | mark_t |
struct | rs_pair |
Rabin/streett pairs used by is_rabin_like and is_streett_like. More... | |
Public Types | |
enum | acc_op : unsigned short { Inf, Fin, InfNeg, FinNeg, And, Or } |
Public Member Functions | |
acc_cond (unsigned n_sets=0, const acc_code &code={}) | |
acc_cond (const acc_code &code) | |
acc_cond (const acc_cond &o) | |
acc_cond & | operator= (const acc_cond &o) |
void | set_acceptance (const acc_code &code) |
const acc_code & | get_acceptance () const |
acc_code & | get_acceptance () |
bool | operator== (const acc_cond &other) const |
bool | operator!= (const acc_cond &other) const |
bool | uses_fin_acceptance () const |
bool | is_t () const |
bool | is_all () const |
bool | is_f () const |
bool | is_none () const |
bool | is_buchi () const |
bool | is_co_buchi () const |
void | set_generalized_buchi () |
void | set_generalized_co_buchi () |
bool | is_generalized_buchi () const |
bool | is_generalized_co_buchi () const |
int | is_rabin () const |
int | is_streett () const |
bool | is_streett_like (std::vector< rs_pair > &pairs) const |
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<rs_pair>. More... | |
bool | is_rabin_like (std::vector< rs_pair > &pairs) const |
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_pair>. More... | |
bool | is_generalized_rabin (std::vector< unsigned > &pairs) const |
bool | is_generalized_streett (std::vector< unsigned > &pairs) const |
bool | is_parity (bool &max, bool &odd, bool equiv=false) const |
bool | is_parity () const |
std::pair< bool, acc_cond::mark_t > | unsat_mark () const |
unsigned | add_sets (unsigned num) |
unsigned | add_set () |
mark_t | mark (unsigned u) const |
mark_t | comp (mark_t l) const |
mark_t | all_sets () const |
bool | accepting (mark_t inf) const |
bool | inf_satisfiable (mark_t inf) const |
trival | maybe_accepting (mark_t infinitely_often, mark_t always_present) const |
mark_t | accepting_sets (mark_t inf) const |
std::ostream & | format (std::ostream &os, mark_t m) const |
std::string | format (mark_t m) const |
unsigned | num_sets () const |
template<class iterator > | |
mark_t | useless (iterator begin, iterator end) const |
acc_cond | remove (mark_t rem, bool missing) const |
acc_cond | strip (mark_t rem, bool missing) const |
acc_cond | restrict_to (mark_t rem) const |
std::string | name (const char *fmt="alo") const |
Return the name of this acceptance condition, in the specified format. More... | |
Static Public Member Functions | |
static acc_code | inf (mark_t mark) |
static acc_code | inf (std::initializer_list< unsigned > vals) |
static acc_code | inf_neg (mark_t mark) |
static acc_code | inf_neg (std::initializer_list< unsigned > vals) |
static acc_code | fin (mark_t mark) |
static acc_code | fin (std::initializer_list< unsigned > vals) |
static acc_code | fin_neg (mark_t mark) |
static acc_code | fin_neg (std::initializer_list< unsigned > vals) |
Protected Member Functions | |
bool | check_fin_acceptance () const |
mark_t::value_t | all_sets_ () const |
Protected Attributes | |
unsigned | num_ |
mark_t::value_t | all_ |
acc_code | code_ |
bool | uses_fin_acceptance_ = false |
bool spot::acc_cond::is_rabin_like | ( | std::vector< rs_pair > & | pairs | ) | const |
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_pair>.
An acceptance condition is Rabin-like if it can be transformed into a Rabin acceptance with little modification to its automaton. A Rabin-like acceptance condition follows one of those rules: -It is a disjunction of conjunctive clauses containing at most one Inf and at most one Fin. -It is true (1 pair [0U, 0U]) -It is false (0 pairs)
bool spot::acc_cond::is_streett_like | ( | std::vector< rs_pair > & | pairs | ) | const |
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<rs_pair>.
An acceptance condition is Streett-like if it can be transformed into a Streett acceptance with little modification to its automaton. A Streett-like acceptance condition follows one of those rules: -It is a conjunction of disjunctive clauses containing at most one Inf and at most one Fin. -It is true (with 0 pair) -It is false (1 pair [0U, 0U])
std::string spot::acc_cond::name | ( | const char * | fmt = "alo" | ) | const |
Return the name of this acceptance condition, in the specified format.
The empty string is returned if no name is known.
fmt should be a combination of the following letters. (0) no parameters, (a) accentuated, (b) abbreviated, (d) style used in dot output, (g) no generalized parameter, (l) recognize Street-like and Rabin-like, (m) no main parameter, (p) no parity parameter, (o) name unknown acceptance as 'other', (s) shorthand for 'lo0'.