spot::acc_cond::acc_code Struct Reference

An acceptance formula. More...

#include <spot/twa/acc.hh>

Inheritance diagram for spot::acc_cond::acc_code:

Collaboration diagram for spot::acc_cond::acc_code:

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

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

Friends
std::ostream &	operator<< (std::ostream &os, const acc_code &code)
	prints the acceptance formula as text More...

Detailed Description

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.

Constructor & Destructor Documentation

acc_code() [1/3]

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.

acc_code() [2/3]

spot::acc_cond::acc_code::acc_code ( )

inline

Build an empty acceptance formula.

This is the same as t().

acc_code() [3/3]

spot::acc_cond::acc_code::acc_code ( const acc_word *  other )

inline

Copy a part of another acceptance formula.

Member Function Documentation

accepting()

bool spot::acc_cond::acc_code::accepting

(

mark_t

inf

)

const

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

buchi()

static acc_code spot::acc_cond::acc_code::buchi ( )

inlinestatic

Build a Büchi acceptance condition.

This builds the formula Inf(0).

Referenced by spot::twa::set_buchi().

cobuchi()

static acc_code spot::acc_cond::acc_code::cobuchi ( )

inlinestatic

Build a co-Büchi acceptance condition.

This builds the formula Fin(0).

Referenced by spot::twa::set_co_buchi().

complement()

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.

f()

static acc_code spot::acc_cond::acc_code::f ( )

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.

fin() [1/2]

static acc_code spot::acc_cond::acc_code::fin ( mark_t  m )

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

fin() [2/2]

static acc_code spot::acc_cond::acc_code::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}).

fin_neg() [1/2]

static acc_code spot::acc_cond::acc_code::fin_neg ( mark_t  m )

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.

fin_neg() [2/2]

static acc_code spot::acc_cond::acc_code::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.

fin_one()

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.

fin_one_extract()

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

fin_unit()

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

fin_unit_one_split()

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 as has the shape ...&Fin(i)&..., then this will return (i, left, right), where left is all disjunct of this form, and right are all the others.

If the input formula has the shape ...&Fin(i)&... then left is set to the entire formula, 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 formlula where Fin(i) has been replaced by false.

force_inf()

acc_code spot::acc_cond::acc_code::force_inf

(

mark_t

m

)

const

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

generalized_buchi()

static acc_code spot::acc_cond::acc_code::generalized_buchi ( unsigned  n )

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

generalized_co_buchi()

static acc_code spot::acc_cond::acc_code::generalized_co_buchi ( unsigned  n )

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

generalized_rabin()

template<class Iterator >

static acc_code spot::acc_cond::acc_code::generalized_rabin ( Iterator  begin, Iterator  end  )

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.

inf() [1/2]

static acc_code spot::acc_cond::acc_code::inf ( mark_t  m )

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

inf() [2/2]

static acc_code spot::acc_cond::acc_code::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}).

inf_neg() [1/2]

static acc_code spot::acc_cond::acc_code::inf_neg ( mark_t  m )

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.

inf_neg() [2/2]

static acc_code spot::acc_cond::acc_code::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.

inf_satisfiable()

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.

inf_unit()

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

is_cnf()

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:

• one of t, f, Fin(i), Inf(i)
• a disjunction of any of the above
• a conjunction of any of the above (including the disjunctions).

is_dnf()

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:

• one of t, f, Fin(i), Inf(i)
• a conjunction of any of the above
• a disjunction of any of the above (including the conjunctions).

is_f()

bool spot::acc_cond::acc_code::is_f ( ) const

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

is_t()

bool spot::acc_cond::acc_code::is_t ( ) const

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

maybe_accepting()

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:

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

missing()

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.

operator&() [1/2]

acc_code spot::acc_cond::acc_code::operator& ( acc_code &&  r ) const

inline

Conjunct the current condition with r.

operator&() [2/2]

acc_code spot::acc_cond::acc_code::operator& ( const acc_code &  r ) const

inline

Conjunct the current condition with r.

operator&=()

acc_code& spot::acc_cond::acc_code::operator&= ( const acc_code &  r )

inline

Conjunct the current condition in place with r.

References is_f(), and is_t().

operator<<()

acc_code spot::acc_cond::acc_code::operator<< ( unsigned  sets ) const

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

operator<<=()

acc_code& spot::acc_cond::acc_code::operator<<= ( unsigned  sets )

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.

operator|() [1/2]

acc_code spot::acc_cond::acc_code::operator| ( acc_code &&  r ) const

inline

Disjunct the current condition with r.

operator|() [2/2]

acc_code spot::acc_cond::acc_code::operator| ( const acc_code &  r ) const

inline

Disjunct the current condition with r.

operator|=()

acc_code& spot::acc_cond::acc_code::operator|= ( const acc_code &  r )

inline

Disjunct the current condition in place with r.

References is_f(), and is_t().

parity()

static acc_code spot::acc_cond::acc_code::parity ( bool  is_max, bool  is_odd, unsigned  sets  )

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.

parity_max()

static acc_code spot::acc_cond::acc_code::parity_max ( bool  is_odd, unsigned  sets  )

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.

parity_max_even()

static acc_code spot::acc_cond::acc_code::parity_max_even ( unsigned  sets )

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.

parity_max_odd()

static acc_code spot::acc_cond::acc_code::parity_max_odd ( unsigned  sets )

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.

parity_min()

static acc_code spot::acc_cond::acc_code::parity_min ( bool  is_odd, unsigned  sets  )

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.

parity_min_even()

static acc_code spot::acc_cond::acc_code::parity_min_even ( unsigned  sets )

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.

parity_min_odd()

static acc_code spot::acc_cond::acc_code::parity_min_odd ( unsigned  sets )

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.

rabin()

static acc_code spot::acc_cond::acc_code::rabin ( unsigned  n )

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

random()

static acc_code spot::acc_cond::acc_code::random ( unsigned  n, double  reuse = 0.0  )

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.

remove()

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

streett()

static acc_code spot::acc_cond::acc_code::streett ( unsigned  n )

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

strip()

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.

symmetries()

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.

t()

static acc_code spot::acc_cond::acc_code::t ( )

inlinestatic

Construct the "true" acceptance condition.

This corresponds to "t" in the HOA format. Under this acceptance condition, all runs are accepting.

to_bdd()

bdd spot::acc_cond::acc_code::to_bdd

(

const bdd *

map

)

const

Convert the acceptance formula into a BDD.

map should be a vector indiced by colors, that maps each color to the desired BDD representation.

to_cnf()

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

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.

to_html()

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.

to_latex()

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.

to_text()

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.

top_conjuncts()

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.

top_disjuncts()

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.

used_inf_fin_sets()

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.

used_once_sets()

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.

used_sets()

acc_cond::mark_t spot::acc_cond::acc_code::used_sets

(

)

const

Return the set of sets appearing in the condition.

useless_colors_patterns()

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ₙ}),...]

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  os, const acc_code &  code  )

friend

prints the acceptance formula as text

---

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

• spot/twa/acc.hh