spot  2.7.2
Classes | Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members

An acceptance condition. More...

#include <spot/twa/acc.hh>

Collaboration diagram for spot::acc_cond:

Classes

struct  acc_code
 An acceptance formula. More...
 
union  acc_word
 A "node" in an acceptance formulas. More...
 
struct  mark_t
 An acceptance mark. More...
 
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
}
 Operators for acceptance formulas. More...
 

Public Member Functions

 acc_cond (unsigned n_sets=0, const acc_code &code={})
 Build an acceptance condition. More...
 
 acc_cond (const acc_code &code)
 Build an acceptance condition. More...
 
 acc_cond (const acc_cond &o)
 Copy an acceptance condition. More...
 
acc_condoperator= (const acc_cond &o)
 Copy an acceptance condition. More...
 
void set_acceptance (const acc_code &code)
 Change the acceptance formula. More...
 
const acc_codeget_acceptance () const
 Retrieve the acceptance formula. More...
 
acc_codeget_acceptance ()
 Retrieve the acceptance formula. More...
 
bool operator== (const acc_cond &other) const
 
bool operator!= (const acc_cond &other) const
 
bool uses_fin_acceptance () const
 Whether the acceptance condition uses Fin terms. More...
 
bool is_t () const
 Whether the acceptance formula is "t" (true) More...
 
bool is_all () const
 Whether the acceptance condition is "all". More...
 
bool is_f () const
 Whether the acceptance formula is "f" (false) More...
 
bool is_none () const
 Whether the acceptance condition is "none". More...
 
bool is_buchi () const
 Whether the acceptance condition is "Büchi". More...
 
bool is_co_buchi () const
 Whether the acceptance condition is "co-Büchi". More...
 
void set_generalized_buchi ()
 Change the acceptance condition to generalized-Büchi, over all declared sets. More...
 
void set_generalized_co_buchi ()
 Change the acceptance condition to generalized-co-Büchi, over all declared sets. More...
 
bool is_generalized_buchi () const
 Whether the acceptance condition is "generalized-Büchi". More...
 
bool is_generalized_co_buchi () const
 Whether the acceptance condition is "generalized-co-Büchi". More...
 
int is_rabin () const
 Check if the acceptance condition matches the Rabin acceptance of the HOA format. More...
 
int is_streett () const
 Check if the acceptance condition matches the Streett acceptance of the HOA format. More...
 
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
 Is the acceptance condition generalized-Rabin? More...
 
bool is_generalized_streett (std::vector< unsigned > &pairs) const
 Is the acceptance condition generalized-Streett? More...
 
bool is_parity (bool &max, bool &odd, bool equiv=false) const
 check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format. More...
 
bool is_parity () const
 check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format. More...
 
std::pair< bool, acc_cond::mark_tunsat_mark () const
 
std::pair< bool, acc_cond::mark_tsat_mark () const
 
unsigned add_sets (unsigned num)
 Add more sets to the acceptance condition. More...
 
unsigned add_set ()
 Add a single set to the acceptance condition. More...
 
mark_t mark (unsigned u) const
 Build a mark_t with a single set. More...
 
mark_t comp (const mark_t &l) const
 Complement a mark_t. More...
 
mark_t all_sets () const
 Construct a mark_t with all declared sets. More...
 
bool accepting (mark_t inf) const
 Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition. More...
 
bool inf_satisfiable (mark_t inf) const
 Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the condition? More...
 
trival maybe_accepting (mark_t infinitely_often, mark_t always_present) const
 Check potential acceptance of an SCC. More...
 
mark_t accepting_sets (mark_t inf) const
 Return an accepting subset of inf. More...
 
std::ostream & format (std::ostream &os, mark_t m) const
 
std::string format (mark_t m) const
 
unsigned num_sets () const
 The number of sets used in the acceptance condition. More...
 
template<class iterator >
mark_t useless (iterator begin, iterator end) const
 Compute useless acceptance sets given a list of mark_t that occur in an SCC. More...
 
acc_cond remove (mark_t rem, bool missing) const
 Remove all the acceptance sets in rem. More...
 
acc_cond strip (mark_t rem, bool missing) const
 Remove acceptance sets, and shift set numbers. More...
 
acc_cond force_inf (mark_t m) const
 For all x in m, replaces Fin(x) by false. More...
 
acc_cond restrict_to (mark_t rem) const
 Restrict an acceptance condition to a subset of set numbers that are occurring at some point. More...
 
std::string name (const char *fmt="alo") const
 Return the name of this acceptance condition, in the specified format. More...
 
mark_t fin_unit () const
 Find a Fin(i) that is a unit clause. More...
 
int fin_one () const
 Return one acceptance set i that appear as Fin(i) in the condition. More...
 

Static Public Member Functions

static acc_code inf (mark_t mark)
 Construct a generalized Büchi acceptance. More...
 
static acc_code inf (std::initializer_list< unsigned > vals)
 Construct a generalized Büchi acceptance. More...
 
static acc_code inf_neg (mark_t mark)
 Construct a generalized Büchi acceptance for complemented sets. More...
 
static acc_code inf_neg (std::initializer_list< unsigned > vals)
 Construct a generalized Büchi acceptance for complemented sets. More...
 
static acc_code fin (mark_t mark)
 Construct a generalized co-Büchi acceptance. More...
 
static acc_code fin (std::initializer_list< unsigned > vals)
 Construct a generalized co-Büchi acceptance. More...
 
static acc_code fin_neg (mark_t mark)
 Construct a generalized co-Büchi acceptance for complemented sets. More...
 
static acc_code fin_neg (std::initializer_list< unsigned > vals)
 Construct a generalized co-Büchi acceptance for complemented sets. More...
 

Protected Member Functions

bool check_fin_acceptance () const
 
std::pair< bool, acc_cond::mark_tsat_unsat_mark (bool) const
 
mark_t all_sets_ () const
 

Protected Attributes

unsigned num_
 
mark_t all_
 
acc_code code_
 
bool uses_fin_acceptance_ = false
 

Detailed Description

An acceptance condition.

This represent an acceptance condition in the HOA sense, that is, an acceptance formula plus a number of acceptance sets. The acceptance formula is expected to use a subset of the acceptance sets. (It usually uses all sets, otherwise that means that some of the sets have no influence on the automaton language and could be removed.)

Member Enumeration Documentation

◆ acc_op

enum spot::acc_cond::acc_op : unsigned short
strong

Operators for acceptance formulas.

Constructor & Destructor Documentation

◆ acc_cond() [1/3]

spot::acc_cond::acc_cond ( unsigned  n_sets = 0,
const acc_code code = {} 
)
inline

Build an acceptance condition.

This takes a number of sets n_sets, and an acceptance formula (code) over those sets.

The number of sets should be at least cover all the sets used in code.

References spot::U.

◆ acc_cond() [2/3]

spot::acc_cond::acc_cond ( const acc_code code)
inline

Build an acceptance condition.

In this version, the number of sets is set the the smallest number necessary for code.

◆ acc_cond() [3/3]

spot::acc_cond::acc_cond ( const acc_cond o)
inline

Copy an acceptance condition.

Member Function Documentation

◆ accepting()

bool spot::acc_cond::accepting ( mark_t  inf) const
inline

Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.

◆ accepting_sets()

mark_t spot::acc_cond::accepting_sets ( mark_t  inf) const

Return an accepting subset of inf.

This function works only on Fin-less acceptance, and returns a subset of inf that is enough to satisfy the acceptance condition. This is typically used when an accepting SCC that visits all sets in inf has been found, and we want to find an accepting cycle: maybe it is not necessary for the accepting cycle to intersect all sets in inf.

This returns mark_t({}) if inf does not satisfies the acceptance condition, or if the acceptance condition is t. So usually you should only use this method in cases you know that the condition is satisfied.

◆ add_set()

unsigned spot::acc_cond::add_set ( )
inline

Add a single set to the acceptance condition.

This simply augment the number of sets, without changing the acceptance formula.

◆ add_sets()

unsigned spot::acc_cond::add_sets ( unsigned  num)
inline

Add more sets to the acceptance condition.

This simply augment the number of sets, without changing the acceptance formula.

References spot::U.

Referenced by spot::twa::acc().

◆ all_sets()

mark_t spot::acc_cond::all_sets ( ) const
inline

Construct a mark_t with all declared sets.

◆ comp()

mark_t spot::acc_cond::comp ( const mark_t l) const
inline

Complement a mark_t.

Complementation is done with respect to the number of sets declared.

◆ fin() [1/2]

static acc_code spot::acc_cond::fin ( mark_t  mark)
inlinestatic

Construct a generalized co-Büchi acceptance.

For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9).

Internally, such a formula is stored using a single word Fin({1,8,9}).

◆ fin() [2/2]

static acc_code spot::acc_cond::fin ( std::initializer_list< unsigned >  vals)
inlinestatic

Construct a generalized co-Büchi acceptance.

For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9).

Internally, such a formula is stored using a single word Fin({1,8,9}).

◆ fin_neg() [1/2]

static acc_code spot::acc_cond::fin_neg ( mark_t  mark)
inlinestatic

Construct a generalized co-Büchi acceptance for complemented sets.

For the input m={1,8,9}, this constructs Fin(!1)|Fin(!8)|Fin(!9).

Internally, such a formula is stored using a single word FinNeg({1,8,9}).

Note that FinNeg formulas are not supported by most methods of this class, and not supported by algorithms in Spot. This is mostly used in the parser for HOA files: if the input file uses Fin(!0) as acceptance condition, the condition will eventually be rewritten as Fin(0) by toggling the membership to set 0 of each transition.

◆ fin_neg() [2/2]

static acc_code spot::acc_cond::fin_neg ( std::initializer_list< unsigned >  vals)
inlinestatic

Construct a generalized co-Büchi acceptance for complemented sets.

For the input m={1,8,9}, this constructs Fin(!1)|Fin(!8)|Fin(!9).

Internally, such a formula is stored using a single word FinNeg({1,8,9}).

Note that FinNeg formulas are not supported by most methods of this class, and not supported by algorithms in Spot. This is mostly used in the parser for HOA files: if the input file uses Fin(!0) as acceptance condition, the condition will eventually be rewritten as Fin(0) by toggling the membership to set 0 of each transition.

◆ fin_one()

int spot::acc_cond::fin_one ( ) const
inline

Return one acceptance set i that appear as Fin(i) in the condition.

Return -1 if no such set exist.

References spot::acc_cond::mark_t::max_accsets().

◆ fin_unit()

mark_t spot::acc_cond::fin_unit ( ) const
inline

Find a Fin(i) that is a unit clause.

This return a mark_t {i} such that Fin(i) appears as a unit clause in the acceptance condition. I.e., either the condition is exactly Fin(i), or the condition has the form ...&Fin(i)&.... If there is no such Fin(i), an empty mark_t is returned.

If multiple unit-Fin appear as unit-clauses, the set of those will be returned. For instance applied to Fin(0)&Fin(1)&(Inf(2)|Fin(3)), this will return{0,1}`.

◆ force_inf()

acc_cond spot::acc_cond::force_inf ( mark_t  m) const
inline

For all x in m, replaces Fin(x) by false.

References force_inf().

Referenced by force_inf().

◆ get_acceptance() [1/2]

const acc_code& spot::acc_cond::get_acceptance ( ) const
inline

Retrieve the acceptance formula.

Referenced by spot::twa::get_acceptance(), and get_acceptance().

◆ get_acceptance() [2/2]

acc_code& spot::acc_cond::get_acceptance ( )
inline

Retrieve the acceptance formula.

References get_acceptance(), and num_sets().

◆ inf() [1/2]

static acc_code spot::acc_cond::inf ( mark_t  mark)
inlinestatic

Construct a generalized Büchi acceptance.

For the input m={1,8,9}, this constructs Inf(1)&Inf(8)&Inf(9).

Internally, such a formula is stored using a single word Inf({1,8,9}).

◆ inf() [2/2]

static acc_code spot::acc_cond::inf ( std::initializer_list< unsigned >  vals)
inlinestatic

Construct a generalized Büchi acceptance.

For the input m={1,8,9}, this constructs Inf(1)&Inf(8)&Inf(9).

Internally, such a formula is stored using a single word Inf({1,8,9}).

◆ inf_neg() [1/2]

static acc_code spot::acc_cond::inf_neg ( mark_t  mark)
inlinestatic

Construct a generalized Büchi acceptance for complemented sets.

For the input m={1,8,9}, this constructs Inf(!1)&Inf(!8)&Inf(!9).

Internally, such a formula is stored using a single word InfNeg({1,8,9}).

Note that InfNeg formulas are not supported by most methods of this class, and not supported by algorithms in Spot. This is mostly used in the parser for HOA files: if the input file uses Inf(!0) as acceptance condition, the condition will eventually be rewritten as Inf(0) by toggling the membership to set 0 of each transition.

◆ inf_neg() [2/2]

static acc_code spot::acc_cond::inf_neg ( std::initializer_list< unsigned >  vals)
inlinestatic

Construct a generalized Büchi acceptance for complemented sets.

For the input m={1,8,9}, this constructs Inf(!1)&Inf(!8)&Inf(!9).

Internally, such a formula is stored using a single word InfNeg({1,8,9}).

Note that InfNeg formulas are not supported by most methods of this class, and not supported by algorithms in Spot. This is mostly used in the parser for HOA files: if the input file uses Inf(!0) as acceptance condition, the condition will eventually be rewritten as Inf(0) by toggling the membership to set 0 of each transition.

◆ inf_satisfiable()

bool spot::acc_cond::inf_satisfiable ( mark_t  inf) const
inline

Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the condition?

This return false only when it is sure that visiting more set will never make the condition satisfiable.

◆ is_all()

bool spot::acc_cond::is_all ( ) const
inline

Whether the acceptance condition is "all".

In the HOA format, the acceptance condition "all" correspond to the formula "t" with 0 declared acceptance sets.

◆ is_buchi()

bool spot::acc_cond::is_buchi ( ) const
inline

Whether the acceptance condition is "Büchi".

The acceptance condition is Büchi if its formula is Inf(0) and only 1 set is used.

◆ is_co_buchi()

bool spot::acc_cond::is_co_buchi ( ) const
inline

Whether the acceptance condition is "co-Büchi".

The acceptance condition is co-Büchi if its formula is Fin(0) and only 1 set is used.

◆ is_f()

bool spot::acc_cond::is_f ( ) const
inline

Whether the acceptance formula is "f" (false)

◆ is_generalized_buchi()

bool spot::acc_cond::is_generalized_buchi ( ) const
inline

Whether the acceptance condition is "generalized-Büchi".

The acceptance condition with n sets is generalized-Büchi if its formula is Inf(0)&Inf(1)&...&Inf(n-1).

◆ is_generalized_co_buchi()

bool spot::acc_cond::is_generalized_co_buchi ( ) const
inline

Whether the acceptance condition is "generalized-co-Büchi".

The acceptance condition with n sets is generalized-co-Büchi if its formula is Fin(0)|Fin(1)|...|Fin(n-1).

◆ is_generalized_rabin()

bool spot::acc_cond::is_generalized_rabin ( std::vector< unsigned > &  pairs) const

Is the acceptance condition generalized-Rabin?

Check if the condition follows the generalized-Rabin definition of the HOA format. So one Fin should be in front of each generalized pair, and set numbers should all be used once.

When true is returned, the pairs vector contains the number of Inf term in each pair. Otherwise, pairs is emptied.

◆ is_generalized_streett()

bool spot::acc_cond::is_generalized_streett ( std::vector< unsigned > &  pairs) const

Is the acceptance condition generalized-Streett?

There is no definition of generalized Streett in HOA v1, so this uses the definition from the development version of the HOA format, that should eventually become HOA v1.1 or HOA v2.

One Inf should be in front of each generalized pair, and set numbers should all be used once.

When true is returned, the pairs vector contains the number of Fin term in each pair. Otherwise, pairs is emptied.

◆ is_none()

bool spot::acc_cond::is_none ( ) const
inline

Whether the acceptance condition is "none".

In the HOA format, the acceptance condition "all" correspond to the formula "f" with 0 declared acceptance sets.

◆ is_parity() [1/2]

bool spot::acc_cond::is_parity ( bool &  max,
bool &  odd,
bool  equiv = false 
) const

check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format.

On success, this return true and sets max, and odd to the type of parity acceptance detected. By default equiv = false, and the parity acceptance should match exactly the order of operators given in the HOA format. If equiv is set, any formula that this logically equivalent to one of the HOA format will be accepted.

◆ is_parity() [2/2]

bool spot::acc_cond::is_parity ( ) const
inline

check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format.

◆ is_rabin()

int spot::acc_cond::is_rabin ( ) const

Check if the acceptance condition matches the Rabin acceptance of the HOA format.

Rabin acceptance over 2n sets look like (Fin(0)&Inf(1))|...|(Fin(2n-2)&Inf(2n-1)); i.e., a disjunction of n pairs of the form Fin(2i)&Inf(2i+1).

f is a special kind of Rabin acceptance with 0 pairs.

This function returns a number of pairs (>=0) or -1 if the acceptance condition is not Rabin.

◆ 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()

int spot::acc_cond::is_streett ( ) const

Check if the acceptance condition matches the Streett acceptance of the HOA format.

Streett acceptance over 2n sets look like (Fin(0)|Inf(1))&...&(Fin(2n-2)|Inf(2n-1)); i.e., a conjunction of n pairs of the form Fin(2i)|Inf(2i+1).

t is a special kind of Streett acceptance with 0 pairs.

This function returns a number of pairs (>=0) or -1 if the acceptance condition is not Streett.

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

◆ is_t()

bool spot::acc_cond::is_t ( ) const
inline

Whether the acceptance formula is "t" (true)

◆ mark()

mark_t spot::acc_cond::mark ( unsigned  u) const
inline

Build a mark_t with a single set.

Referenced by spot::twa::set_buchi(), and spot::twa::set_co_buchi().

◆ maybe_accepting()

trival spot::acc_cond::maybe_accepting ( mark_t  infinitely_often,
mark_t  always_present 
) const
inline

Check potential acceptance of an SCC.

Assuming that an SCC intersects all sets in infinitely_often (i.e., for each set in infinitely_often, there exist one marked transition in the SCC), and is included in all sets in always_present (i.e., all transitions are marked with always_present), this returns one tree possible results:

  • trival::yes() the SCC is necessarily accepting,
  • trival::no() the SCC is necessarily rejecting,
  • trival::maybe() the SCC could contain an accepting cycle.

◆ name()

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'.

◆ num_sets()

unsigned spot::acc_cond::num_sets ( ) const
inline

The number of sets used in the acceptance condition.

Referenced by spot::twa::acc(), get_acceptance(), and spot::twa::num_sets().

◆ operator=()

acc_cond& spot::acc_cond::operator= ( const acc_cond o)
inline

Copy an acceptance condition.

◆ remove()

acc_cond spot::acc_cond::remove ( mark_t  rem,
bool  missing 
) const
inline

Remove all the acceptance sets in rem.

If missing is set, the acceptance sets are assumed to be missing from the automaton, and the acceptance is updated to reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will become Fin(3) if we remove 2 because it is missing from this automaton. Indeed there is no way to fulfill Inf(1)&Inf(2) in this case. So essentially missing=true causes Inf(rem) to become f, and Fin(rem) to become t.

If missing is unset, Inf(rem) become t while Fin(rem) become f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give Inf(1)|Fin(3).

References remove().

Referenced by remove(), and restrict_to().

◆ restrict_to()

acc_cond spot::acc_cond::restrict_to ( mark_t  rem) const
inline

Restrict an acceptance condition to a subset of set numbers that are occurring at some point.

References remove().

◆ set_acceptance()

void spot::acc_cond::set_acceptance ( const acc_code code)
inline

Change the acceptance formula.

Beware, this does not change the number of declared sets.

Referenced by spot::twa::set_acceptance().

◆ set_generalized_buchi()

void spot::acc_cond::set_generalized_buchi ( )
inline

Change the acceptance condition to generalized-Büchi, over all declared sets.

Referenced by spot::twa::set_generalized_buchi().

◆ set_generalized_co_buchi()

void spot::acc_cond::set_generalized_co_buchi ( )
inline

Change the acceptance condition to generalized-co-Büchi, over all declared sets.

Referenced by spot::twa::set_generalized_co_buchi().

◆ strip()

acc_cond spot::acc_cond::strip ( mark_t  rem,
bool  missing 
) const
inline

Remove acceptance sets, and shift set numbers.

Same as remove, but also shift set numbers in the result so that all used set numbers are continuous.

References strip().

Referenced by strip().

◆ useless()

template<class iterator >
mark_t spot::acc_cond::useless ( iterator  begin,
iterator  end 
) const
inline

Compute useless acceptance sets given a list of mark_t that occur in an SCC.

Assuming that the condition is generalized Büchi using all declared sets, this scans all the mark_t between begin and end, and return the set of acceptance sets that are useless because they are always implied by other sets.

◆ uses_fin_acceptance()

bool spot::acc_cond::uses_fin_acceptance ( ) const
inline

Whether the acceptance condition uses Fin terms.


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 Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13