spot  2.4.4
Classes | Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
spot::acc_cond Class Reference
Collaboration diagram for spot::acc_cond:
Collaboration graph

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_condoperator= (const acc_cond &o)
 
void set_acceptance (const acc_code &code)
 
const acc_codeget_acceptance () const
 
acc_codeget_acceptance ()
 
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 ()
 
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_parity (bool &max, bool &odd, bool equiv=false) const
 
bool is_parity () const
 
std::pair< bool, acc_cond::mark_tunsat_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
 

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
 

Member Function Documentation

◆ is_rabin_like()

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)

◆ is_streett_like()

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])


The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Dec 25 2017 14:51:15 for spot by doxygen 1.8.13