spot 2.12.2
|
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 | |
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 "co-Büchi". More... | |
void | set_generalized_buchi () |
Change the acceptance condition to generalized-Büchi, over all declared sets. More... | |
void | set_generalized_co_buchi () |
Change the acceptance condition to generalized-co-Büchi, over all declared sets. More... | |
bool | is_generalized_buchi () const |
Whether the acceptance condition is "generalized-Büchi". More... | |
bool | is_generalized_co_buchi () const |
Whether the acceptance condition is "generalized-co-Büchi". More... | |
int | is_rabin () const |
Check if the acceptance condition matches the Rabin acceptance of the HOA format. More... | |
int | is_streett () const |
Check if the acceptance condition matches the Streett acceptance of the HOA format. More... | |
bool | is_streett_like (std::vector< rs_pair > &pairs) const |
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<rs_pair>. More... | |
bool | is_rabin_like (std::vector< rs_pair > &pairs) const |
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_pair>. More... | |
bool | is_generalized_rabin (std::vector< unsigned > &pairs) const |
Is the acceptance condition generalized-Rabin? More... | |
bool | is_generalized_streett (std::vector< unsigned > &pairs) const |
Is the acceptance condition generalized-Streett? More... | |
bool | is_parity (bool &max, bool &odd, bool equiv=false) const |
check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format. More... | |
bool | is_parity () const |
check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format. More... | |
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... | |
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 | 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 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 with Fin(i) changed to true and Inf(i) to false. More... | |
std::vector< acc_cond > | top_disjuncts () const |
Return the top-level disjuncts. More... | |
std::vector< acc_cond > | top_conjuncts () const |
Return the top-level conjuncts. More... | |
std::tuple< int, acc_cond, acc_cond > | fin_unit_one_split () const |
Split an acceptance condition, trying to select one unit-Fin. More... | |
std::tuple< int, acc_cond, acc_cond > | fin_unit_one_split_improved () const |
Split an acceptance condition, trying to select one unit-Fin. More... | |
Static Public Member Functions | |
static acc_code | inf (mark_t mark) |
Construct a generalized Büchi acceptance. More... | |
static acc_code | inf (std::initializer_list< unsigned > vals) |
Construct a generalized Büchi acceptance. More... | |
static acc_code | inf_neg (mark_t mark) |
Construct a generalized Büchi acceptance for complemented sets. More... | |
static acc_code | inf_neg (std::initializer_list< unsigned > vals) |
Construct a generalized Büchi acceptance for complemented sets. More... | |
static acc_code | fin (mark_t mark) |
Construct a generalized co-Büchi acceptance. More... | |
static acc_code | fin (std::initializer_list< unsigned > vals) |
Construct a generalized co-Büchi acceptance. More... | |
static acc_code | fin_neg (mark_t mark) |
Construct a generalized co-Büchi acceptance for complemented sets. More... | |
static acc_code | fin_neg (std::initializer_list< unsigned > vals) |
Construct a generalized co-Büchi acceptance for complemented sets. More... | |
Protected Member Functions | |
bool | check_fin_acceptance () const |
std::pair< bool, acc_cond::mark_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 Fin-less acceptance, and returns a subset of inf that is enough to satisfy the acceptance condition. This is typically used when an accepting SCC that visits all sets in inf has been found, and we want to find an accepting cycle: maybe it is not necessary for the accepting cycle to intersect all sets in inf.
This returns mark_t({})
if inf does not satisfies the acceptance condition, or if the acceptance condition is t
. So usually you should only use this method in cases you know that the condition is satisfied.
|
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 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.
|
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 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))
.
|
inline |
Find a Fin(i)
that is a unit clause.
This return a mark_t {i}
such that Fin(i)
appears as a unit clause in the acceptance condition. I.e., either the condition is exactly Fin(i)
, or the condition has the form ...&Fin(i)&...
. If there is no such Fin(i)
, an empty mark_t is returned.
If multiple unit-Fin appear as unit-clauses, the set of those will be returned. For instance applied to Fin(0)&Fin(1)&(Inf(2)|Fin(3))
, this will return
{0,1}`.
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.
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.
|
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 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}
.
|
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 "co-Büchi".
The acceptance condition is co-Bü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 "generalized-Büchi".
The acceptance condition with n sets is generalized-Büchi if its formula is Inf(0)&Inf(1)&...&Inf(n-1).
|
inline |
Whether the acceptance condition is "generalized-co-Büchi".
The acceptance condition with n sets is generalized-co-Büchi if its formula is Fin(0)|Fin(1)|...|Fin(n-1).
bool spot::acc_cond::is_generalized_rabin | ( | std::vector< unsigned > & | pairs | ) | const |
Is the acceptance condition generalized-Rabin?
Check if the condition follows the generalized-Rabin definition of the HOA format. So one Fin should be in front of each generalized pair, and set numbers should all be used once.
When true is returned, the pairs vector contains the number of Inf
term in each pair. Otherwise, pairs is emptied.
bool spot::acc_cond::is_generalized_streett | ( | std::vector< unsigned > & | pairs | ) | const |
Is the acceptance condition generalized-Streett?
There is no definition of generalized Streett in HOA v1, so this uses the definition from the development version of the HOA format, that should eventually become HOA v1.1 or HOA v2.
One Inf should be in front of each generalized pair, and set numbers should all be used once.
When true is returned, the pairs vector contains the number of Fin
term in each pair. Otherwise, pairs is emptied.
|
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(2n-2)&Inf(2n-1))
; i.e., a disjunction of n pairs of the form Fin(2i)&Inf(2i+1)
.
f
is a special kind of Rabin acceptance with 0 pairs.
This function returns a number of pairs (>=0) or -1 if the acceptance condition is not Rabin.
bool spot::acc_cond::is_rabin_like | ( | std::vector< rs_pair > & | pairs | ) | const |
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_pair>.
An acceptance condition is Rabin-like if it can be transformed into a Rabin acceptance with little modification to its automaton. A Rabin-like acceptance condition follows one of those rules: -It is a disjunction of conjunctive clauses containing at most one Inf and at most one Fin. -It is true (1 pair [0U, 0U]) -It is false (0 pairs)
int spot::acc_cond::is_streett | ( | ) | const |
Check if the acceptance condition matches the Streett acceptance of the HOA format.
Streett acceptance over 2n sets look like (Fin(0)|Inf(1))&...&(Fin(2n-2)|Inf(2n-1))
; i.e., a conjunction of n pairs of the form Fin(2i)|Inf(2i+1)
.
t
is a special kind of Streett acceptance with 0 pairs.
This function returns a number of pairs (>=0) or -1 if the acceptance condition is not Streett.
bool spot::acc_cond::is_streett_like | ( | std::vector< rs_pair > & | pairs | ) | const |
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<rs_pair>.
An acceptance condition is Streett-like if it can be transformed into a Streett acceptance with little modification to its automaton. A Streett-like acceptance condition follows one of those rules: -It is a conjunction of disjunctive clauses containing at most one Inf and at most one Fin. -It is true (with 0 pair) -It is false (1 pair [0U, 0U])
|
inline |
Whether the acceptance formula is "t" (true)
|
inline |
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.
|
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 Street-like and Rabin-like, (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 generalized-Büchi, over all declared sets.
|
inline |
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
std::vector< acc_cond > spot::acc_cond::top_conjuncts | ( | ) | const |
Return the top-level 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 top-level 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.