|
spot 2.13
|
An acceptance formula. More...
#include <spot/twa/acc.hh>
Public Member Functions | |
| acc_code | unit_propagation () |
| 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... | |
| bdd | to_bdd (const bdd *map) const |
| Convert the acceptance formula into a BDD. More... | |
| std::vector< acc_code > | top_disjuncts () const |
| Return the top-level disjuncts. More... | |
| std::vector< acc_code > | top_conjuncts () const |
| Return the top-level conjuncts. 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... | |
| mark_t | mafins () const |
Find a Fin(i) that is mandatory. 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 appears as Fin(i) in the condition. More... | |
| std::pair< int, acc_code > | fin_one_extract () const |
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it with Fin(i) changed to true and Inf(i) to false. 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_code | keep_one_inf_per_branch () const |
| Rewrite an acceptance condition by keeping at most one Inf(x) on each dijunctive branch. More... | |
| acc_cond::mark_t | used_sets () const |
| Return the set of sets appearing in the condition. More... | |
| std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > | useless_colors_patterns () const |
| Find patterns of useless colors. More... | |
| mark_t | used_once_sets () const |
| Return the sets that appears only once in the acceptance. 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... | |
| std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > | fin_unit_one_split () const |
| Split an acceptance condition, trying to select one unit-Fin. More... | |
| std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > | fin_unit_one_split_improved () const |
| Split an acceptance condition, trying to select one unit-Fin. 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 | 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... | |
| static acc_code | parity (bool is_max, bool is_odd, unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_max (bool is_odd, unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_max_odd (unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_max_even (unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_min (bool is_odd, unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_min_odd (unsigned sets) |
| Build a parity acceptance condition. More... | |
| static acc_code | parity_min_even (unsigned sets) |
| Build a parity acceptance condition. 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 specified 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).
Referenced by spot::twa::set_buchi().
|
inlinestatic |
Build a co-Büchi acceptance condition.
This builds the formula Fin(0).
Referenced by spot::twa::set_co_buchi().
| 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 appears as Fin(i) in the condition.
Return -1 if no such set exist.
| std::pair< int, acc_code > spot::acc_cond::acc_code::fin_one_extract | ( | ) | const |
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it with Fin(i) changed to true and Inf(i) to false.
If the condition is a disjunction and one of the disjunct has the shape ...&Fin(i)&..., then i will be preferred over any arbitrary Fin.
The second element of the pair, is the same acceptance condition in which all top-level 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, we would select Fin(1) over Fin(7) because it appears at the top-level. Then we would collect the disjuncts containing Fin(1), that is, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7))). Finally we would replace Fin(1) by true and Inf(1) by false. The return value would then be (1, Inf(2)|Inf(5)).
| 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}.
| std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > spot::acc_cond::acc_code::fin_unit_one_split | ( | ) | const |
Split an acceptance condition, trying to select one unit-Fin.
If the condition is a disjunction and one of the disjunct has the shape ...&Fin(i)&..., then this will return (i, left, right), where left is all disjunct of this form (with Fin(i) replaced by true), and right are all the others.
If the input formula has the shape ...&Fin(i)&... then left is set to the entire formula (with Fin(i) replaced by true), and right is empty.
If no disjunct has the right shape, then a random Fin(i) is searched in the formula, and the output (i, left, right). is such that left contains all disjuncts containing Fin(i) (at any depth), and right contains the original formula where Fin(i) has been replaced by false.
| std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > spot::acc_cond::acc_code::fin_unit_one_split_improved | ( | ) | const |
Split an acceptance condition, trying to select one unit-Fin.
If the condition is a disjunction and one of the disjunct has the shape ...&Fin(i)&..., then this will return (i, left, right), where left is all disjunct of this form (with Fin(i) replaced by true), and right are all the others.
If the input formula has the shape ...&Fin(i)&... then left is set to the entire formula (with Fin(i) replaced by true), and right is empty.
If no disjunct has the right shape, then a random Fin(i) is searched in the formula, and the output (i, left, right). is such that left contains all disjuncts containing Fin(i) (at any depth), and right contains the original formula where Fin(i) has been replaced by false.
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.
Referenced by spot::twa::set_generalized_buchi().
|
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.
Referenced by spot::twa::set_generalized_co_buchi().
|
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.
| mark_t spot::acc_cond::acc_code::inf_unit | ( | ) | const |
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 unit-Inf appear as unit-clauses, the set of those will be returned. For instance applied to Inf(0)&Inf(1)&(Inf(2)|Fin(3)), this will return {0,1}.
| 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|=().
| acc_code spot::acc_cond::acc_code::keep_one_inf_per_branch | ( | ) | const |
Rewrite an acceptance condition by keeping at most one Inf(x) on each dijunctive branch.
For instance (Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5) will become (Fin(0)&Inf(1) | Inf(4)
| mark_t spot::acc_cond::acc_code::mafins | ( | ) | const |
Find a Fin(i) that is mandatory.
This return a mark_t {i} such that Fin(i) appears in all branches of the AST of the acceptance conditions. This is therefore a bit stronger than fin_unit(). For instance on Inf(1)&Fin(2) | Fin(2)&Fin(3) this will return {2}.
If multiple mandatory Fins exist, the set of those will be returned.
| 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 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::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 run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions will build a formula for that, as specified in the HOA format.
|
inlinestatic |
Build a parity acceptance condition.
In parity acceptance a run is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). These functions 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.
| bdd spot::acc_cond::acc_code::to_bdd | ( | const bdd * | map | ) | const |
Convert the acceptance formula into a BDD.
map should be a vector indexed by colors, that maps each color to the desired BDD representation.
| 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::vector< acc_code > spot::acc_cond::acc_code::top_conjuncts | ( | ) | const |
Return the top-level conjuncts.
For instance, if the formula is Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns [Fin(0), Fin(1), 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_code > spot::acc_cond::acc_code::top_disjuncts | ( | ) | const |
Return the top-level disjuncts.
For instance, if the formula is Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns [Fin(0), Fin(1), Fin(2)&(Inf(3)|Fin(4))].
If the formula is not a disjunction, this returns a vector with the formula as only element.
| 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.
| mark_t spot::acc_cond::acc_code::used_once_sets | ( | ) | const |
Return the sets that appears only once in the acceptance.
For instance if the condition is Fin(0)&(Inf(1)|(Fin(1)&Inf(2))), this returns {0,2}, because set 1 is used more than once.
| acc_cond::mark_t spot::acc_cond::acc_code::used_sets | ( | ) | const |
Return the set of sets appearing in the condition.
| std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > spot::acc_cond::acc_code::useless_colors_patterns | ( | ) | const |
Find patterns of useless colors.
If any subformula of the acceptance condition looks like (Inf(y₁)&Inf(y₂)&...&Inf(yₙ)) | f(x₁,...,xₙ) or (Fin(y₁)|Fin(y₂)|...|Fin(yₙ)) & f(x₁,...,xₙ) then for each transition with all colors {y₁,y₂,...,yₙ} we can add or remove all the xᵢ that are used only once in the formula.
This method returns a vector of pairs: [({y₁,y₂,...,yₙ},{x₁,x₂,...,xₙ}),...]
1.9.4