An acceptance condition. More...

#include <spot/twa/acc.hh>

Collaboration diagram for spot::acc_cond:

Classes
struct	mark_t
	An acceptance mark. More...
union	acc_word
	A "node" in an acceptance formulas. More...
struct	acc_code
	An acceptance formula. 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.
	acc_cond (const acc_code &code)
	Build an acceptance condition.
	acc_cond (const acc_cond &o)
	Copy an acceptance condition.
acc_cond &	operator= (const acc_cond &o)
	Copy an acceptance condition.
void	set_acceptance (const acc_code &code)
	Change the acceptance formula.
const acc_code &	get_acceptance () const
	Retrieve the acceptance formula.
acc_code &	get_acceptance ()
	Retrieve the acceptance formula.
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.
bool	is_t () const
	Whether the acceptance formula is "t" (true).
bool	is_all () const
	Whether the acceptance condition is "all".
bool	is_f () const
	Whether the acceptance formula is "f" (false).
bool	is_none () const
	Whether the acceptance condition is "none".
bool	is_buchi () const
	Whether the acceptance condition is "Büchi".
bool	is_co_buchi () const
	Whether the acceptance condition is "co-Büchi".
void	set_generalized_buchi ()
	Change the acceptance condition to generalized-Büchi, over all declared sets.
void	set_generalized_co_buchi ()
	Change the acceptance condition to generalized-co-Büchi, over all declared sets.
bool	is_generalized_buchi () const
	Whether the acceptance condition is "generalized-Büchi".
bool	is_generalized_co_buchi () const
	Whether the acceptance condition is "generalized-co-Büchi".
int	is_rabin () const
	Check if the acceptance condition matches the Rabin acceptance of the HOA format.
int	is_streett () const
	Check if the acceptance condition matches the Streett acceptance of the HOA format.
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>.
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>.
bool	is_generalized_rabin (std::vector< unsigned > &pairs) const
	Is the acceptance condition generalized-Rabin?
bool	is_generalized_streett (std::vector< unsigned > &pairs) const
	Is the acceptance condition generalized-Streett?
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.
bool	is_parity () const
	check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format.
acc_cond	unit_propagation ()
	Remove superfluous Fin and Inf by unit propagation.
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.
unsigned	add_set ()
	Add a single set to the acceptance condition.
mark_t	mark (unsigned u) const
	Build a mark_t with a single set.
mark_t	comp (const mark_t &l) const
	Complement a mark_t.
mark_t	all_sets () const
	Construct a mark_t with all declared sets.
bool	accepting (mark_t inf) const
	Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
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?
acc_cond	keep_one_inf_per_branch () const
	Rewrite an acceptance condition by keeping at most one Inf(x) on each disjunctive branch.
trival	maybe_accepting (mark_t infinitely_often, mark_t always_present) const
	Check potential acceptance of an SCC.
mark_t	accepting_sets (mark_t inf) const
	Return an accepting subset of inf.
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.
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.
acc_cond	remove (mark_t rem, bool missing) const
	Remove all the acceptance sets in rem.
acc_cond	strip (mark_t rem, bool missing) const
	Remove acceptance sets, and shift set numbers.
acc_cond	force_inf (mark_t m) const
	For all x in m, replaces Fin(x) by false.
acc_cond	restrict_to (mark_t rem) const
	Restrict an acceptance condition to a subset of set numbers that are occurring at some point.
std::string	name (const char *fmt="alo") const
	Return the name of this acceptance condition, in the specified format.
mark_t	mafins () const
	Find a Fin(i) that is a unit clause.
mark_t	inf_unit () const
	Find a Inf(i) that is a unit clause.
int	fin_one () const
	Return one acceptance set i that appear as Fin(i) in the condition.
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.
std::vector< acc_cond >	top_disjuncts () const
	Return the top-level disjuncts.
std::vector< acc_cond >	top_conjuncts () const
	Return the top-level conjuncts.

std::tuple< int, acc_cond, acc_cond >	fin_unit_one_split () const
	Split an acceptance condition, trying to select one unit-Fin.
std::tuple< int, acc_cond, acc_cond >	fin_unit_one_split_improved () const
	Split an acceptance condition, trying to select one unit-Fin.

Static Public Member Functions

static acc_code	inf (mark_t mark)
	Construct a generalized Büchi acceptance.
static acc_code	inf (std::initializer_list< unsigned > vals)
	Construct a generalized Büchi acceptance.

static acc_code	inf_neg (mark_t mark)
	Construct a generalized Büchi acceptance for complemented sets.
static acc_code	inf_neg (std::initializer_list< unsigned > vals)
	Construct a generalized Büchi acceptance for complemented sets.

static acc_code	fin (mark_t mark)
	Construct a generalized co-Büchi acceptance.
static acc_code	fin (std::initializer_list< unsigned > vals)
	Construct a generalized co-Büchi acceptance.

static acc_code	fin_neg (mark_t mark)
	Construct a generalized co-Büchi acceptance for complemented sets.
static acc_code	fin_neg (std::initializer_list< unsigned > vals)
	Construct a generalized co-Büchi acceptance for complemented sets.

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

Detailed Description

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

Member Enumeration Documentation

◆ acc_op

enum class spot::acc_cond::acc_op : unsigned short

strong

Operators for acceptance formulas.

Constructor & Destructor Documentation

◆ acc_cond() [1/3]

spot::acc_cond::acc_cond	(	unsigned	n_sets = 0,
		const acc_code &	code = {} )

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.

Referenced by acc_cond(), force_inf(), keep_one_inf_per_branch(), operator=(), remove(), restrict_to(), strip(), and unit_propagation().

◆ acc_cond() [2/3]

spot::acc_cond::acc_cond ( const acc_code & code )

inline

Build an acceptance condition.

In this version, the number of sets is set to the smallest number necessary for code.

References spot::U.

◆ acc_cond() [3/3]

spot::acc_cond::acc_cond ( const acc_cond & o )

inline

Copy an acceptance condition.

References acc_cond().

Member Function Documentation

◆ accepting()

bool spot::acc_cond::accepting ( mark_t inf ) const

inline

Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.

References inf().

◆ accepting_sets()

mark_t spot::acc_cond::accepting_sets ( mark_t inf ) const

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.

References inf().

◆ add_set()

unsigned spot::acc_cond::add_set ( )

inline

Add a single set to the acceptance condition.

This simply augment the number of sets, without changing the acceptance formula.

References add_sets().

◆ add_sets()

unsigned spot::acc_cond::add_sets ( unsigned num )

inline

Add more sets to the acceptance condition.

This simply augment the number of sets, without changing the acceptance formula.

References spot::acc_cond::mark_t::max_accsets().

Referenced by add_set().

◆ all_sets()

mark_t spot::acc_cond::all_sets ( ) const

inline

Construct a mark_t with all declared sets.

Referenced by is_buchi(), is_generalized_buchi(), is_generalized_co_buchi(), restrict_to(), set_generalized_buchi(), set_generalized_co_buchi(), and strip().

◆ comp()

mark_t spot::acc_cond::comp ( const mark_t & l ) const

inline

Complement a mark_t.

Complementation is done with respect to the number of sets declared.

Referenced by useless().

◆ fin() [1/2]

acc_code spot::acc_cond::fin ( mark_t mark )

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

References spot::acc_cond::acc_code::fin(), and mark().

Referenced by fin(), and set_generalized_co_buchi().

◆ fin() [2/2]

acc_code spot::acc_cond::fin ( std::initializer_list< unsigned > vals )

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

References fin().

◆ fin_neg() [1/2]

acc_code spot::acc_cond::fin_neg ( mark_t mark )

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.

References spot::acc_cond::acc_code::fin_neg(), and mark().

Referenced by fin_neg().

◆ fin_neg() [2/2]

acc_code spot::acc_cond::fin_neg ( std::initializer_list< unsigned > vals )

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.

References fin_neg().

◆ fin_one()

int spot::acc_cond::fin_one ( ) const

inline

Return one acceptance set i that appear as Fin(i) in the condition.

Return -1 if no such set exist.

◆ fin_one_extract()

std::pair< int, acc_cond > spot::acc_cond::fin_one_extract ( ) const

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

References num_sets().

◆ fin_unit_one_split()

std::tuple< int, acc_cond, acc_cond > spot::acc_cond::fin_unit_one_split ( ) const

inline

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.

References num_sets().

◆ fin_unit_one_split_improved()

std::tuple< int, acc_cond, acc_cond > spot::acc_cond::fin_unit_one_split_improved ( ) const

inline

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.

References num_sets().

◆ force_inf()

acc_cond spot::acc_cond::force_inf ( mark_t m ) const

inline

For all x in m, replaces Fin(x) by false.

References acc_cond(), and num_sets().

◆ get_acceptance() [1/2]

acc_code & spot::acc_cond::get_acceptance ( )

inline

Retrieve the acceptance formula.

◆ get_acceptance() [2/2]

const acc_code & spot::acc_cond::get_acceptance ( ) const

inline

Retrieve the acceptance formula.

◆ inf() [1/2]

acc_code spot::acc_cond::inf ( mark_t mark )

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

References spot::acc_cond::acc_code::inf(), and mark().

Referenced by accepting(), accepting_sets(), inf(), inf_satisfiable(), and set_generalized_buchi().

◆ inf() [2/2]

acc_code spot::acc_cond::inf ( std::initializer_list< unsigned > vals )

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

References inf().

◆ inf_neg() [1/2]

acc_code spot::acc_cond::inf_neg ( mark_t mark )

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.

References spot::acc_cond::acc_code::inf_neg(), and mark().

Referenced by inf_neg().

◆ inf_neg() [2/2]

acc_code spot::acc_cond::inf_neg ( std::initializer_list< unsigned > vals )

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.

References inf_neg().

◆ inf_satisfiable()

bool spot::acc_cond::inf_satisfiable ( mark_t inf ) const

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.

References inf().

◆ inf_unit()

mark_t spot::acc_cond::inf_unit ( ) const

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

◆ is_all()

bool spot::acc_cond::is_all ( ) const

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.

References is_t().

◆ is_buchi()

bool spot::acc_cond::is_buchi ( ) const

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.

References all_sets().

◆ is_co_buchi()

bool spot::acc_cond::is_co_buchi ( ) const

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.

References is_generalized_co_buchi().

◆ is_f()

bool spot::acc_cond::is_f ( ) const

inline

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

Referenced by is_none().

◆ is_generalized_buchi()

bool spot::acc_cond::is_generalized_buchi ( ) const

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

References all_sets().

◆ is_generalized_co_buchi()

bool spot::acc_cond::is_generalized_co_buchi ( ) const

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

References all_sets().

Referenced by is_co_buchi().

◆ is_generalized_rabin()

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.

◆ is_generalized_streett()

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.

◆ is_none()

bool spot::acc_cond::is_none ( ) const

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.

References is_f().

◆ is_parity() [1/2]

bool spot::acc_cond::is_parity ( ) const

inline

check is the acceptance condition matches one of the four type of parity acceptance defined in the HOA format.

References is_parity().

◆ is_parity() [2/2]

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.

Referenced by is_parity().

◆ is_rabin()

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.

◆ is_rabin_like()

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)

◆ is_streett()

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.

◆ is_streett_like()

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])

◆ is_t()

bool spot::acc_cond::is_t ( ) const

inline

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

Referenced by is_all().

◆ keep_one_inf_per_branch()

acc_cond spot::acc_cond::keep_one_inf_per_branch ( ) const

inline

Rewrite an acceptance condition by keeping at most one Inf(x) on each disjunctive branch.

For instance (Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5) will become (Fin(0)&Inf(1) | Inf(4)

References acc_cond(), and num_sets().

◆ mafins()

mark_t spot::acc_cond::mafins ( ) const

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

See also: acc_cond::mafins */ mark_t fin_unit() const { return code_.fin_unit(); }

/** 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.

See also: acc_cond::fin_unit

◆ mark()

mark_t spot::acc_cond::mark ( unsigned u ) const

inline

Build a mark_t with a single set.

References num_sets().

Referenced by fin(), fin_neg(), inf(), inf_neg(), spot::acc_cond::acc_code::operator&=(), and spot::acc_cond::acc_code::operator|=().

◆ maybe_accepting()

trival spot::acc_cond::maybe_accepting	(	mark_t	infinitely_often,
		mark_t	always_present ) const

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:

trival::yes() the SCC is necessarily accepting,
trival::no() the SCC is necessarily rejecting,
trival::maybe() the SCC could contain an accepting cycle.

◆ name()

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'.

◆ num_sets()

unsigned spot::acc_cond::num_sets ( ) const

inline

The number of sets used in the acceptance condition.

References num_sets().

Referenced by fin_one_extract(), fin_unit_one_split(), fin_unit_one_split_improved(), force_inf(), keep_one_inf_per_branch(), mark(), num_sets(), remove(), restrict_to(), and strip().

◆ operator=()

acc_cond & spot::acc_cond::operator= ( const acc_cond & o )

inline

Copy an acceptance condition.

References acc_cond().

◆ remove()

acc_cond spot::acc_cond::remove	(	mark_t	rem,
		bool	missing ) const

inline

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 acc_cond(), and num_sets().

◆ restrict_to()

acc_cond spot::acc_cond::restrict_to ( mark_t rem ) const

inline

Restrict an acceptance condition to a subset of set numbers that are occurring at some point.

References acc_cond(), all_sets(), and num_sets().

◆ set_acceptance()

void spot::acc_cond::set_acceptance ( const acc_code & code )

inline

Change the acceptance formula.

Beware, this does not change the number of declared sets.

Referenced by set_generalized_buchi(), and set_generalized_co_buchi().

◆ set_generalized_buchi()

void spot::acc_cond::set_generalized_buchi ( )

inline

Change the acceptance condition to generalized-Büchi, over all declared sets.

References all_sets(), inf(), and set_acceptance().

◆ set_generalized_co_buchi()

void spot::acc_cond::set_generalized_co_buchi ( )

inline

Change the acceptance condition to generalized-co-Büchi, over all declared sets.

References all_sets(), fin(), and set_acceptance().

◆ strip()

acc_cond spot::acc_cond::strip	(	mark_t	rem,
		bool	missing ) const

inline

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.

References acc_cond(), all_sets(), and num_sets().

◆ top_conjuncts()

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.

References spot::acc_cond::mark_t::all().

◆ top_disjuncts()

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.

◆ unit_propagation()

acc_cond spot::acc_cond::unit_propagation ( )

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.

References acc_cond().

◆ useless()

template<class iterator>

mark_t spot::acc_cond::useless	(	iterator	begin,
		iterator	end ) const

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.

References comp().

◆ uses_fin_acceptance()

bool spot::acc_cond::uses_fin_acceptance ( ) const

inline

Whether the acceptance condition uses Fin terms.

The documentation for this class was generated from the following file:

spot/twa/acc.hh

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ acc_op

Constructor & Destructor Documentation

◆ acc_cond() [1/3]

◆ acc_cond() [2/3]

◆ acc_cond() [3/3]

Member Function Documentation

◆ accepting()

◆ accepting_sets()

◆ add_set()

◆ add_sets()

◆ all_sets()

◆ comp()

◆ fin() [1/2]

◆ fin() [2/2]

◆ fin_neg() [1/2]

◆ fin_neg() [2/2]

◆ fin_one()

◆ fin_one_extract()

◆ fin_unit_one_split()

◆ fin_unit_one_split_improved()

◆ force_inf()

◆ get_acceptance() [1/2]

◆ get_acceptance() [2/2]

◆ inf() [1/2]

◆ inf() [2/2]

◆ inf_neg() [1/2]

◆ inf_neg() [2/2]

◆ inf_satisfiable()

◆ inf_unit()

◆ is_all()

◆ is_buchi()

◆ is_co_buchi()

◆ is_f()

◆ is_generalized_buchi()

◆ is_generalized_co_buchi()

◆ is_generalized_rabin()

◆ is_generalized_streett()

◆ is_none()

◆ is_parity() [1/2]

◆ is_parity() [2/2]

◆ is_rabin()

◆ is_rabin_like()

◆ is_streett()

◆ is_streett_like()

◆ is_t()

◆ keep_one_inf_per_branch()

◆ mafins()

◆ mark()

◆ maybe_accepting()

◆ name()

◆ num_sets()

◆ operator=()

◆ remove()

◆ restrict_to()

◆ set_acceptance()

◆ set_generalized_buchi()

◆ set_generalized_co_buchi()

◆ strip()

◆ top_conjuncts()

◆ top_disjuncts()

◆ unit_propagation()

◆ useless()

◆ uses_fin_acceptance()