spot
2.7

An acceptance formulas. More...
#include <spot/twa/acc.hh>
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 
Is this the "true" acceptance condition? More...  
bool  is_f () const 
Is this the "false" acceptance condition? More...  
acc_code &  operator &= (const acc_code &r) 
Conjunct the current condition in place with r. More...  
acc_code  operator & (const acc_code &r) const 
Conjunct the current condition with r. More...  
acc_code  operator & (acc_code &&r) const 
Conjunct the current condition with r. More...  
acc_code &  operator= (const acc_code &r) 
Disjunct the current condition in place with r. More...  
acc_code  operator (acc_code &&r) const 
Disjunct the current condition with r. More...  
acc_code  operator (const acc_code &r) const 
Disjunct the current condition with r. More...  
acc_code &  operator<<= (unsigned sets) 
Apply a left shift to all mark_t that appear in the condition. More...  
acc_code  operator<< (unsigned sets) const 
Apply a left shift to all mark_t that appear in the condition. More...  
bool  is_dnf () const 
Whether the acceptance formula is in disjunctive normal form. More...  
bool  is_cnf () const 
Whether the acceptance formula is in conjunctive normal form. More...  
acc_code  to_dnf () const 
Convert the acceptance formula into disjunctive normal form. More...  
acc_code  to_cnf () const 
Convert the acceptance formula into disjunctive normal form. More...  
acc_code  complement () const 
Complement an acceptance formula. 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...  
std::vector< std::vector< int > >  missing (mark_t inf, bool accepting) const 
Help closing accepting or rejecting cycle. 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...  
std::vector< unsigned >  symmetries () const 
compute the symmetry class of the acceptance sets. More...  
acc_code  remove (acc_cond::mark_t rem, bool missing) const 
Remove all the acceptance sets in rem. More...  
acc_code  strip (acc_cond::mark_t rem, bool missing) const 
Remove acceptance sets, and shift set numbers. More...  
acc_code  force_inf (mark_t m) const 
For all x in m, replaces Fin(x) by false . More...  
acc_cond::mark_t  used_sets () const 
Return the set of sets appearing in the condition. More...  
std::pair< acc_cond::mark_t, acc_cond::mark_t >  used_inf_fin_sets () const 
Return the sets used as Inf or Fin in the acceptance condition. More...  
std::ostream &  to_html (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const 
Print the acceptance formula as HTML. More...  
std::ostream &  to_text (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const 
Print the acceptance formula as text. More...  
std::ostream &  to_latex (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const 
Print the acceptance formula as LaTeX. More...  
acc_code (const char *input)  
Construct an acc_code from a string. More...  
acc_code ()  
Build an empty acceptance formula. More...  
acc_code (const acc_word *other)  
Copy a part of another acceptance formula. More...  
Static Public Member Functions  
static acc_code  f () 
Construct the "false" acceptance condition. More...  
static acc_code  t () 
Construct the "true" acceptance condition. More...  
static acc_code  buchi () 
Build a Büchi acceptance condition. More...  
static acc_code  cobuchi () 
Build a coBüchi acceptance condition. More...  
static acc_code  generalized_buchi (unsigned n) 
Build a generalizedBüchi acceptance condition with n sets. More...  
static acc_code  generalized_co_buchi (unsigned n) 
Build a generalizedcoBüchi acceptance condition with n sets. More...  
static acc_code  rabin (unsigned n) 
Build a Rabin condition with n pairs. More...  
static acc_code  streett (unsigned n) 
Build a Streett condition with n pairs. More...  
template<class Iterator >  
static acc_code  generalized_rabin (Iterator begin, Iterator end) 
Build a generalized Rabin condition. More...  
static acc_code  parity (bool max, bool odd, unsigned sets) 
Build a parity acceptance condition. More...  
static acc_code  random (unsigned n, double reuse=0.0) 
Build a random acceptance condition. More...  
static acc_code  fin (mark_t m) 
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 m) 
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...  
static acc_code  inf (mark_t m) 
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 m) 
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...  
Friends  
std::ostream &  operator<< (std::ostream &os, const acc_code &code) 
prints the acceptance formula as text More...  
An acceptance formulas.
Acceptance formulas are stored as a vector of acc_word in a kind of reverse polish notation. The motivation for this design was that we could evaluate the acceptance condition using a very simple stackbased interpreter; however it turned out that such a stackbased interpretation would prevent us from doing shortcircuit evaluation, so we are not evaluating acceptance conditions this way, and maybe the implementation of acc_code could change in the future. It's best not to rely on the fact that formulas are stored as vectors. Use the provided methods instead.
spot::acc_cond::acc_code::acc_code  (  const char *  input  ) 
Construct an acc_code from a string.
The string should either 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 could be the name of an acceptance condition, as speficied in the HOA format. (E.g. "Rabin 2", "parity max odd 3", "generalizedRabin 4 2 1", etc.).
A spot::parse_error is thrown on syntax error.

inline 
Build an empty acceptance formula.
This is the same as t().

inline 
Copy a part of another acceptance formula.
bool spot::acc_cond::acc_code::accepting  (  mark_t  inf  )  const 
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.

inlinestatic 
Build a Büchi acceptance condition.
This builds the formula Inf(0)
.

inlinestatic 
Build a coBüchi acceptance condition.
This builds the formula Fin(0)
.
acc_code spot::acc_cond::acc_code::complement  (  )  const 
Complement an acceptance formula.
Also known as "dualizing the acceptance condition" since this replaces Fin
↔ Inf
, and &
↔ 
.
Not that dualizing the acceptance condition on a deterministic automaton is enough to complement that automaton. On a nondeterministic automaton, you should also replace existential choices by universal choices, as done by the dualize() function.

inlinestatic 
Construct the "false" acceptance condition.
This corresponds to "f" in the HOA format. Under this acceptance condition, no runs is accepting. Obviously, this has very few practical application, except as neutral element in some construction.
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.
int spot::acc_cond::acc_code::fin_one  (  )  const 
Return one acceptance set i that appear as Fin(i)
in the condition.
Return 1 if no such set exist.
mark_t spot::acc_cond::acc_code::fin_unit  (  )  const 
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}`.
For all x
in m, replaces Fin(x)
by false
.

inlinestatic 
Build a generalizedBüchi acceptance condition with n sets.
This builds the formula Inf(0)&Inf(1)&...&Inf(n1)
.
When n is zero, the acceptance condition reduces to true.

inlinestatic 
Build a generalizedcoBüchi acceptance condition with n sets.
This builds the formula Fin(0)Fin(1)...Fin(n1)
.
When n is zero, the acceptance condition reduces to false.

inlinestatic 
Build a generalized Rabin condition.
The two iterators should point to a range of integers, each integer being the number of Inf term in a generalized Rabin pair.
For instance if the input is [2,3,0]
, the output will have three clauses (=generalized pairs), with 2 Inf terms in the first clause, 3 in the second, and 0 in the last: (Fin(0)&Inf(1)&Inf(2))Fin(3)&Inf(4)&Inf(5)&Inf(6)Fin(7)
.
Since set numbers are not reused, the number of sets used is the sum of all input integers plus their count.
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.
bool spot::acc_cond::acc_code::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?
This return false only when it is sure that visiting more set will never make the condition satisfiable.
bool spot::acc_cond::acc_code::is_cnf  (  )  const 
Whether the acceptance formula is in conjunctive normal form.
The formula is in DNF if it is either:
t
, f
, Fin(i)
, Inf(i)
bool spot::acc_cond::acc_code::is_dnf  (  )  const 
Whether the acceptance formula is in disjunctive normal form.
The formula is in DNF if it is either:
t
, f
, Fin(i)
, Inf(i)

inline 
Is this the "false" acceptance condition?
This corresponds to "f" in the HOA format. Under this acceptance condition, no runs is accepting. Obviously, this has very few practical application, except as neutral element in some construction.
Referenced by operator &=(), and operator=().

inline 
Is this the "true" acceptance condition?
This corresponds to "t" in the HOA format. Under this acceptance condition, all runs are accepting.
Referenced by operator &=(), and operator=().
trival spot::acc_cond::acc_code::maybe_accepting  (  mark_t  infinitely_often, 
mark_t  always_present  
)  const 
Check potential acceptance of an SCC.
Assuming that an SCC intersects all sets in infinitely_often (i.e., for each set in infinetely_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::vector<std::vector<int> > spot::acc_cond::acc_code::missing  (  mark_t  inf, 
bool  accepting  
)  const 
Help closing accepting or rejecting cycle.
Assuming you have a partial cycle visiting all acceptance sets in inf, this returns the combination of set you should see or avoid when closing the cycle to make it accepting or rejecting (as specified with accepting).
The result is a vector of vectors of integers. A positive integer x denote a set that should be seen, a negative value x means the set x1 must be absent. The different inter vectors correspond to different solutions satisfying the accepting criterion.
Conjunct the current condition with r.
Conjunct the current condition with r.

inline 
Apply a left shift to all mark_t that appear in the condition.
Shifting Fin(0)&Inf(3)
by 2 will give Fin(2)&Inf(5)
.

inline 
Apply a left shift to all mark_t that appear in the condition.
Shifting Fin(0)&Inf(3)
by 2 will give Fin(2)&Inf(5)
.
The result is modified in place.
Disjunct the current condition with r.
Disjunct the current condition with r.

static 
Build a parity acceptance condition.
In parity acceptance a word is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). This function will build a formula for that, as specified in the HOA format.

inlinestatic 
Build a Rabin condition with n pairs.
This builds the formula (Fin(0)&Inf(1))(Fin(2)&Inf(3))...(Fin(2n2)&Inf(2n1))

static 
Build a random acceptance condition.
If n is 0, this will always generate the true acceptance, because working with false acceptance is somehow pointless.
For n>0, we randomly create a term Fin(i) or Inf(i) for each set 0≤i<n. If reuse>0.0, it gives the probability that a set i can generate more than one Fin(i)/Inf(i) term. Set i will be reused as long as our [0,1) random number generator gives a value ≤reuse. (Do not set reuse≥1.0 as that will give an infinite loop.)
All these Fin/Inf terms are the leaves of the tree we are building. That tree is then build by picking two random subtrees, and joining them with & and  randomly, until we are left with a single tree.
acc_code spot::acc_cond::acc_code::remove  (  acc_cond::mark_t  rem, 
bool  missing  
)  const 
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)
.

inlinestatic 
Build a Streett condition with n pairs.
This builds the formula (Fin(0)Inf(1))&(Fin(2)Inf(3))&...&(Fin(2n2)Inf(2n1))
acc_code spot::acc_cond::acc_code::strip  (  acc_cond::mark_t  rem, 
bool  missing  
)  const 
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.
std::vector<unsigned> spot::acc_cond::acc_code::symmetries  (  )  const 
compute the symmetry class of the acceptance sets.
Two sets x and y are symmetric if swapping them in the acceptance condition produces an equivalent formula. For instance 0 and 2 are symmetric in Inf(0)&Fin(1)&Inf(2).
The returned vector is indexed by set numbers, and each entry points to the "root" (or representative element) of its symmetry class. In the above example the result would be [0,1,0], showing that 0 and 2 are in the same class.

inlinestatic 
Construct the "true" acceptance condition.
This corresponds to "t" in the HOA format. Under this acceptance condition, all runs are accepting.
acc_code spot::acc_cond::acc_code::to_cnf  (  )  const 
Convert the acceptance formula into disjunctive normal form.
This works by distributing 
over &
, resulting in a formula that can be exponentially larger than the input.
This implementation is the dual of to_dnf()
.
acc_code spot::acc_cond::acc_code::to_dnf  (  )  const 
Convert the acceptance formula into disjunctive normal form.
This works by distributing &
over 
, resulting in a formula that can be exponentially larger than the input.
The implementation works by converting the formula into a BDD where Inf(i)
is encoded by vᵢ and Fin(i)
is encoded by !vᵢ, and then finding prime implicants to build an irredundant sumofproducts. In practice, the results are usually better than what we would expect by hand.
std::ostream& spot::acc_cond::acc_code::to_html  (  std::ostream &  os, 
std::function< void(std::ostream &, int)>  set_printer = nullptr 

)  const 
Print the acceptance formula as HTML.
The set_printer function can be used to customize the output of set numbers.
std::ostream& spot::acc_cond::acc_code::to_latex  (  std::ostream &  os, 
std::function< void(std::ostream &, int)>  set_printer = nullptr 

)  const 
Print the acceptance formula as LaTeX.
The set_printer function can be used to customize the output of set numbers.
std::ostream& spot::acc_cond::acc_code::to_text  (  std::ostream &  os, 
std::function< void(std::ostream &, int)>  set_printer = nullptr 

)  const 
Print the acceptance formula as text.
The set_printer function can be used to customize the output of set numbers.
std::pair<acc_cond::mark_t, acc_cond::mark_t> spot::acc_cond::acc_code::used_inf_fin_sets  (  )  const 
Return the sets used as Inf or Fin in the acceptance condition.
acc_cond::mark_t spot::acc_cond::acc_code::used_sets  (  )  const 
Return the set of sets appearing in the condition.

friend 
prints the acceptance formula as text