spot
2.3.2
|
Public Member Functions | |
bool | operator== (const acc_code &other) const |
bool | operator< (const acc_code &other) const |
bool | operator> (const acc_code &other) const |
bool | operator<= (const acc_code &other) const |
bool | operator>= (const acc_code &other) const |
bool | operator!= (const acc_code &other) const |
bool | is_t () const |
bool | is_f () const |
acc_code & | operator&= (acc_code &&r) |
acc_code & | operator&= (const acc_code &r) |
acc_code | operator& (acc_code &&r) |
acc_code | operator& (const acc_code &r) |
acc_code & | operator|= (acc_code &&r) |
acc_code & | operator|= (const acc_code &r) |
acc_code | operator| (acc_code &&r) |
acc_code | operator| (const acc_code &r) |
acc_code & | operator<<= (unsigned sets) |
acc_code | operator<< (unsigned sets) const |
bool | is_dnf () const |
bool | is_cnf () const |
acc_code | to_dnf () const |
acc_code | to_cnf () const |
acc_code | complement () const |
std::vector< std::vector< int > > | missing (mark_t inf, bool accepting) const |
bool | accepting (mark_t inf) const |
bool | inf_satisfiable (mark_t inf) const |
acc_code | strip (acc_cond::mark_t rem, bool missing) const |
acc_cond::mark_t | used_sets () const |
std::pair< acc_cond::mark_t, acc_cond::mark_t > | used_inf_fin_sets () const |
std::ostream & | to_html (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const |
std::ostream & | to_text (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const |
acc_code (const char *input) | |
Construct an acc_code from a string. More... | |
acc_code () | |
Build an empty acceptance condition. More... | |
Static Public Member Functions | |
static acc_code | f () |
static acc_code | t () |
static acc_code | fin (mark_t m) |
static acc_code | fin (std::initializer_list< unsigned > vals) |
static acc_code | fin_neg (mark_t m) |
static acc_code | fin_neg (std::initializer_list< unsigned > vals) |
static acc_code | inf (mark_t m) |
static acc_code | inf (std::initializer_list< unsigned > vals) |
static acc_code | inf_neg (mark_t m) |
static acc_code | inf_neg (std::initializer_list< unsigned > vals) |
static acc_code | buchi () |
static acc_code | cobuchi () |
static acc_code | generalized_buchi (unsigned n) |
static acc_code | generalized_co_buchi (unsigned n) |
static acc_code | rabin (unsigned n) |
static acc_code | streett (unsigned n) |
template<class Iterator > | |
static acc_code | generalized_rabin (Iterator begin, Iterator end) |
static acc_code | parity (bool max, bool odd, unsigned sets) |
static acc_code | random (unsigned n, double reuse=0.0) |
Friends | |
std::ostream & | operator<< (std::ostream &os, const acc_code &code) |
spot::acc_cond::acc_code::acc_code | ( | const char * | input | ) |
Construct an acc_code from a string.
The string can follow the following grammar:
acc ::= "t" | "f" | "Inf" "(" num ")" | "Fin" "(" num ")" | "(" acc ")" | acc "&" acc | acc "|" acc
Where num is an integer and "&" has priority over "|". Note that "Fin(!x)" and "Inf(!x)" are not supported by this parser.
Or the string can be the name of an acceptance condition, as speficied in the HOA format. (E.g. "Rabin 2", "parity max odd 3", "generalized-Rabin 4 2 1", etc.).
A spot::parse_error is thrown on syntax error.
|
inline |
Build an empty acceptance condition.
This is the same as t().