spot
2.7.4
|
An acceptance formula. 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 co-Büchi acceptance condition. More... | |
static acc_code | generalized_buchi (unsigned n) |
Build a generalized-Büchi acceptance condition with n sets. More... | |
static acc_code | generalized_co_buchi (unsigned n) |
Build a generalized-co-Bü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 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 m) |
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... | |
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 formula.
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 stack-based interpreter; however it turned out that such a stack-based interpretation would prevent us from doing short-circuit 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", "generalized-Rabin 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 co-Bü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 non-deterministic 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 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}).
|
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}).
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.
|
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.
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 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}`.
For all x
in m, replaces Fin(x)
by false
.
|
inlinestatic |
Build a generalized-Büchi acceptance condition with n sets.
This builds the formula Inf(0)&Inf(1)&...&Inf(n-1)
.
When n is zero, the acceptance condition reduces to true.
|
inlinestatic |
Build a generalized-co-Büchi acceptance condition with n sets.
This builds the formula Fin(0)|Fin(1)|...|Fin(n-1)
.
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 -x-1 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(2n-2)&Inf(2n-1))
|
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(2n-2)|Inf(2n-1))
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 sum-of-products. 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