spot
2.10.6

An acceptance condition. More...
#include <spot/twa/acc.hh>
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 class  acc_op : unsigned short { Inf , Fin , InfNeg , FinNeg , And , Or } 
Operators for acceptance formulas. More...  
Public Member Functions  
bool  has_parity_prefix (acc_cond &new_acc, std::vector< unsigned > &colors) const 
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_cond &  operator= (const acc_cond &o) 
Copy an acceptance condition. More...  
void  set_acceptance (const acc_code &code) 
Change the acceptance formula. More...  
const acc_code &  get_acceptance () const 
Retrieve the acceptance formula. More...  
acc_code &  get_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 "coBüchi". More...  
void  set_generalized_buchi () 
Change the acceptance condition to generalizedBüchi, over all declared sets. More...  
void  set_generalized_co_buchi () 
Change the acceptance condition to generalizedcoBüchi, over all declared sets. More...  
bool  is_generalized_buchi () const 
Whether the acceptance condition is "generalizedBüchi". More...  
bool  is_generalized_co_buchi () const 
Whether the acceptance condition is "generalizedcoBü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 Streettlike 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 Rabinlike 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 generalizedRabin? More...  
bool  is_generalized_streett (std::vector< unsigned > &pairs) const 
Is the acceptance condition generalizedStreett? 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_max_equiv (std::vector< int > &permut, bool even) const 
bool  is_parity () const 
check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format. More...  
acc_cond  unit_propagation () 
Remove superfluous Fin and Inf by unit propagation. More...  
std::pair< bool, acc_cond::mark_t >  unsat_mark () const 
std::pair< bool, acc_cond::mark_t >  sat_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...  
acc_cond  apply_permutation (std::vector< unsigned >permut) 
acc_code  apply_permutation_aux (std::vector< unsigned >permut) 
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...  
mark_t  inf_unit () const 
Find a Inf(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...  
std::pair< int, acc_cond >  fin_one_extract () const 
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it. More...  
std::vector< acc_cond >  top_disjuncts () const 
Return the toplevel disjuncts. More...  
std::vector< acc_cond >  top_conjuncts () const 
Return the toplevel conjuncts. 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 coBüchi acceptance. More...  
static acc_code  fin (std::initializer_list< unsigned > vals) 
Construct a generalized coBüchi acceptance. More...  
static acc_code  fin_neg (mark_t mark) 
Construct a generalized coBüchi acceptance for complemented sets. More...  
static acc_code  fin_neg (std::initializer_list< unsigned > vals) 
Construct a generalized coBüchi acceptance for complemented sets. More...  
Protected Member Functions  
bool  check_fin_acceptance () const 
std::pair< bool, acc_cond::mark_t >  sat_unsat_mark (bool) const 
mark_t  all_sets_ () const 
Protected Attributes  
unsigned  num_ 
mark_t  all_ 
acc_code  code_ 
bool  uses_fin_acceptance_ = false 
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.)

strong 
Operators for acceptance formulas.

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.

inline 
Build an acceptance condition.
In this version, the number of sets is set the the smallest number necessary for code.
References spot::U.

inline 
Copy an acceptance condition.

inline 
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Return an accepting subset of inf.
This function works only on Finless 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.

inline 
Add a single set to the acceptance condition.
This simply augment the number of sets, without changing the acceptance formula.

inline 
Add more sets to the acceptance condition.
This simply augment the number of sets, without changing the acceptance formula.
Complement a mark_t.
Complementation is done with respect to the number of sets declared.
Construct a generalized coBü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}).

inlinestatic 
Construct a generalized coBü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}).
Construct a generalized coBü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.

inlinestatic 
Construct a generalized coBü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.

inline 
Return one acceptance set i that appear as Fin(i)
in the condition.
Return 1 if no such set exist.

inline 
Return one acceptance set i that appears as Fin(i)
in the condition, and all disjuncts containing it.
If the condition is a disjunction and one of the disjunct has the shape ...&Fin(i)&...
, then i
will be prefered over any arbitrary Fin.
The second element of the pair, is the same acceptance condition in which all toplevel disjunct not featuring Fin(i)
have been removed.
For example on Fin(1)&Inf(2)Inf(3)&Inf(4)Inf(5)&(Fin(1)Fin(7))
the output would be the pair (1, Fin(1)&Inf(2)Inf(5)&(Fin(1)Fin(7)))
. On that example Fin(1)
is prefered to Fin(7)
because it appears at the toplevel.

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 unitFin appear as unitclauses, the set of those will be returned. For instance applied to Fin(0)&Fin(1)&(Inf(2)Fin(3))
, this will return
{0,1}`.

inline 
Retrieve the acceptance formula.

inline 
Retrieve the acceptance formula.
Referenced by spot::twa::get_acceptance().
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})
.

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})
.
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.

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.

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.

inline 
Find a Inf(i)
that is a unit clause.
This return a mark_t {i}
such that Inf(i)
appears as a unit clause in the acceptance condition. I.e., either the condition is exactly Inf(i)
, or the condition has the form ...&Inf(i)&...
. If there is no such Inf(i)
, an empty mark_t is returned.
If multiple unitInf appear as unitclauses, the set of those will be returned. For instance applied to Inf(0)&Inf(1)&(Inf(2)Fin(3))
, this will return {0,1}
.

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.

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.

inline 
Whether the acceptance condition is "coBüchi".
The acceptance condition is coBüchi if its formula is Fin(0) and only 1 set is used.

inline 
Whether the acceptance formula is "f" (false)

inline 
Whether the acceptance condition is "generalizedBüchi".
The acceptance condition with n sets is generalizedBüchi if its formula is Inf(0)&Inf(1)&...&Inf(n1).

inline 
Whether the acceptance condition is "generalizedcoBüchi".
The acceptance condition with n sets is generalizedcoBüchi if its formula is Fin(0)Fin(1)...Fin(n1).
bool spot::acc_cond::is_generalized_rabin  (  std::vector< unsigned > &  pairs  )  const 
Is the acceptance condition generalizedRabin?
Check if the condition follows the generalizedRabin 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.
bool spot::acc_cond::is_generalized_streett  (  std::vector< unsigned > &  pairs  )  const 
Is the acceptance condition generalizedStreett?
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.

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.

inline 
check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format.
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.
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(2n2)&Inf(2n1))
; 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.
bool spot::acc_cond::is_rabin_like  (  std::vector< rs_pair > &  pairs  )  const 
Test whether an acceptance condition is Rabinlike and returns each Rabin pair in an std::vector<rs_pair>.
An acceptance condition is Rabinlike if it can be transformed into a Rabin acceptance with little modification to its automaton. A Rabinlike 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)
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(2n2)Inf(2n1))
; 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.
bool spot::acc_cond::is_streett_like  (  std::vector< rs_pair > &  pairs  )  const 
Test whether an acceptance condition is Streettlike and returns each Streett pair in an std::vector<rs_pair>.
An acceptance condition is Streettlike if it can be transformed into a Streett acceptance with little modification to its automaton. A Streettlike 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])

inline 
Whether the acceptance formula is "t" (true)

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:
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 Streetlike and Rabinlike, (m) no main parameter, (p) no parity parameter, (o) name unknown acceptance as 'other', (s) shorthand for 'lo0'.

inline 
The number of sets used in the acceptance condition.
Referenced by spot::twa::num_sets().
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 an acceptance condition to a subset of set numbers that are occurring at some point.
References remove().

inline 
Change the acceptance formula.
Beware, this does not change the number of declared sets.

inline 
Change the acceptance condition to generalizedBüchi, over all declared sets.

inline 
Change the acceptance condition to generalizedcoBüchi, over all declared sets.
std::vector<acc_cond> spot::acc_cond::top_conjuncts  (  )  const 
Return the toplevel conjuncts.
For instance, if the formula is (5, Fin(0)Fin(1)(Fin(2)&(Inf(3)Fin(4)))), this returns [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)Fin(4)))].
If the formula is not a conjunction, this returns a vector with the formula as only element.
std::vector<acc_cond> spot::acc_cond::top_disjuncts  (  )  const 
Return the toplevel disjuncts.
For instance, if the formula is (5, Fin(0)Fin(1)(Fin(2)&(Inf(3)Fin(4)))), this returns [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)Fin(4)))].
If the formula is not a disjunction, this returns a vector with the formula as only element.

inline 
Remove superfluous Fin and Inf by unit propagation.
For example in Fin(0)(Inf(0) & Fin(1))
, Inf(0)
is true iff Fin(0)
is false so we can rewrite it as Fin(0)Fin(1)
.
The number of acceptance sets is not modified even if some do not appear in the acceptance condition anymore.

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.

inline 
Whether the acceptance condition uses Fin terms.