spot  2.8.1
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

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_codeoperator &= (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_codeoperator|= (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_codeoperator<<= (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...

std::vector< acc_codetop_disjuncts () const
Return the top-level disjuncts. More...

std::vector< acc_codetop_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...

int fin_one () const
Return one acceptance set i that appear as `Fin(i)` in the condition. More...

std::vector< std::vector< int > > missing (mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle. More...

bool accepting (mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition. More...

bool inf_satisfiable (mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the condition? More...

trival maybe_accepting (mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC. More...

std::vector< unsigned > symmetries () const
compute the symmetry class of the acceptance sets. More...

acc_code remove (acc_cond::mark_t rem, bool missing) const
Remove all the acceptance sets in rem. More...

acc_code strip (acc_cond::mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers. More...

acc_code force_inf (mark_t m) const
For all `x` in m, replaces `Fin(x)` by `false`. More...

acc_cond::mark_t used_sets () const
Return the set of sets appearing in the condition. More...

std::pair< acc_cond::mark_t, acc_cond::mark_tused_inf_fin_sets () const
Return the sets used as Inf or Fin in the acceptance condition. More...

std::ostream & to_html (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as HTML. More...

std::ostream & to_text (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text. More...

std::ostream & to_latex (std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX. More...

acc_code (const char *input)
Construct an acc_code from a string. More...

acc_code ()
Build an empty acceptance formula. More...

acc_code (const acc_word *other)
Copy a part of another acceptance formula. More...

## Static Public Member Functions

static acc_code f ()
Construct the "false" acceptance condition. More...

static acc_code t ()
Construct the "true" acceptance condition. More...

static acc_code buchi ()
Build a Büchi acceptance condition. More...

static acc_code cobuchi ()
Build a co-Büchi acceptance condition. More...

static acc_code generalized_buchi (unsigned n)
Build a generalized-Büchi acceptance condition with n sets. More...

static acc_code generalized_co_buchi (unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets. More...

static acc_code rabin (unsigned n)
Build a Rabin condition with n pairs. More...

static acc_code streett (unsigned n)
Build a Streett condition with n pairs. More...

template<class Iterator >
static acc_code generalized_rabin (Iterator begin, Iterator end)
Build a generalized Rabin condition. More...

static acc_code parity (bool max, bool odd, unsigned sets)
Build a parity acceptance condition. More...

static acc_code random (unsigned n, double reuse=0.0)
Build a random acceptance condition. More...

static acc_code fin (mark_t m)
Construct a generalized co-Büchi acceptance. More...

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

static acc_code fin_neg (mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets. More...

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

static acc_code inf (mark_t m)
Construct a generalized Büchi acceptance. More...

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

static acc_code inf_neg (mark_t m)
Construct a generalized Büchi acceptance for complemented sets. More...

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

## Friends

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

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

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

## ◆ 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)`.

## ◆ cobuchi()

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

Build a co-Büchi acceptance condition.

This builds the formula `Fin(0)`.

## ◆ 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 appear as `Fin(i)` in the condition.

Return -1 if no such set exist.

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

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

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

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

## ◆ 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 > 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& ( const acc_code & r ) const
inline

Conjunct the current condition with r.

## ◆ operator &() [2/2]

 acc_code spot::acc_cond::acc_code::operator& ( 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 spot::And, 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(), is_t(), and spot::Or.

## ◆ parity()

 static acc_code spot::acc_cond::acc_code::parity ( bool max, bool odd, unsigned sets )
static

Build a parity acceptance condition.

In parity acceptance a word is accepting if the maximum (or minimum) set number that is seen infinitely often is odd (or even). This function will build a formula for that, as specified in the HOA format.

## ◆ 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 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_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 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 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 spot::acc_cond::acc_code::used_inf_fin_sets ( ) const

Return the sets used as Inf or Fin in the acceptance condition.

## ◆ used_sets()

 acc_cond::mark_t spot::acc_cond::acc_code::used_sets ( ) const

Return the set of sets appearing in the condition.

## ◆ 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:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by 1.8.13