spot  2.7
Modules | Functions
Conversion between acceptance conditions

Modules

 Algorithms for parity acceptance
 

Functions

twa_graph_ptr spot::cleanup_acceptance_here (twa_graph_ptr aut, bool strip=true)
 Remove useless acceptance sets. More...
 
twa_graph_ptr spot::cleanup_acceptance (const_twa_graph_ptr aut)
 Remove useless acceptance sets. More...
 
twa_graph_ptr spot::degeneralize (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true)
 Degeneralize a spot::tgba into an equivalent sba with only one acceptance condition. More...
 
twa_graph_ptr spot::iar (const const_twa_graph_ptr &aut)
 Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) More...
 
twa_graph_ptr spot::iar_maybe (const const_twa_graph_ptr &aut)
 Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) More...
 
bool spot::rabin_is_buchi_realizable (const const_twa_graph_ptr &aut)
 Check if is Büchi-realizable. This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built. More...
 
twa_graph_ptr spot::rabin_to_buchi_maybe (const const_twa_graph_ptr &aut)
 Convert a Rabin automaton to Büchi automaton, preserving determinism when possible. More...
 
twa_graph_ptr spot::remove_fin (const const_twa_graph_ptr &aut)
 Rewrite an automaton without Fin or f acceptance. More...
 
bool spot::has_separate_sets (const const_twa_graph_ptr &aut)
 Whether the Inf and Fin numbers are disjoints. More...
 
twa_graph_ptr spot::separate_sets_here (const twa_graph_ptr &aut)
 Separate the Fin and Inf sets used by an automaton. More...
 
twa_graph_ptr spot::to_parity (const const_twa_graph_ptr &aut, bool pretty_print=false)
 Take an automaton with any acceptance condition and return an equivalent parity automaton. More...
 
twa_graph_ptr spot::to_generalized_buchi (const const_twa_graph_ptr &aut)
 Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton. More...
 
twa_graph_ptr spot::streett_to_generalized_buchi (const const_twa_graph_ptr &in)
 Convert Streett acceptance into generalized Büchi acceptance. More...
 
twa_graph_ptr spot::streett_to_generalized_buchi_maybe (const const_twa_graph_ptr &in)
 Convert Streett acceptance into generalized Büchi. More...
 
twa_graph_ptr spot::to_generalized_rabin (const const_twa_graph_ptr &aut, bool share_inf=false)
 Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton. More...
 
twa_graph_ptr spot::to_generalized_streett (const const_twa_graph_ptr &aut, bool share_fin=false)
 Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton. More...
 
twa_graph_ptr spot::dnf_to_streett (const const_twa_graph_ptr &aut, bool original_states=false)
 Converts any DNF acceptance condition into Streett-like. More...
 
twa_graph_ptr spot::simplify_acceptance_here (twa_graph_ptr aut)
 Simplify an acceptance condition. More...
 
twa_graph_ptr spot::simplify_acceptance (const_twa_graph_ptr aut)
 Simplify an acceptance condition. More...
 

Detailed Description

Function Documentation

◆ cleanup_acceptance()

twa_graph_ptr spot::cleanup_acceptance ( const_twa_graph_ptr  aut)

#include <spot/twaalgos/cleanacc.hh>

Remove useless acceptance sets.

This removes from the automaton the acceptance marks that are not used in the acceptance condition. This also removes from the acceptance conditions the terms that corresponds to empty or full sets.

◆ cleanup_acceptance_here()

twa_graph_ptr spot::cleanup_acceptance_here ( twa_graph_ptr  aut,
bool  strip = true 
)

#include <spot/twaalgos/cleanacc.hh>

Remove useless acceptance sets.

This removes from the automaton the acceptance marks that are not used in the acceptance condition. This also removes from the acceptance conditions the terms that corresponds to empty or full sets.

If strip is true (the default), the remaining acceptance set numbers will be shifted down to reduce maximal number of acceptance sets used.

◆ degeneralize()

twa_graph_ptr spot::degeneralize ( const const_twa_graph_ptr &  a,
bool  use_z_lvl = true,
bool  use_cust_acc_orders = false,
int  use_lvl_cache = 1,
bool  skip_levels = true,
bool  ignaccsl = false,
bool  remove_extra_scc = true 
)

#include <spot/twaalgos/degen.hh>

Degeneralize a spot::tgba into an equivalent sba with only one acceptance condition.

This algorithms will build a new explicit automaton that has at most (N+1) times the number of states of the original automaton.

When use_z_lvl is set, the level of the degeneralized automaton is reset everytime an SCC is exited. If use_cust_acc_orders is set, the degeneralization will compute a custom acceptance order for each SCC (this option is disabled by default because our benchmarks show that it usually does more harm than good). If use_lvl_cache is set, everytime an SCC is entered on a state that as already been associated to some level elsewhere, reuse that level (set it to 2 to keep the smallest number, 3 to keep the largest level, and 1 to keep the first level found). If ignaccsl is set, we do not directly jump to the accepting level if the entering state has an accepting self-loop. If remove_extra_scc is set (the default) we ensure that the output automaton has as many SCCs as the input by removing superfluous SCCs.

Any of these three options will cause the SCCs of the automaton a to be computed prior to its actual degeneralization.

The degeneralize_tba() variant produce a degeneralized automaton with transition-based acceptance.

The mapping between each state of the resulting automaton and the original state of the input automaton is stored in the "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it. Note that these functions may return the original automaton as-is if it is already degeneralized; in this case the "original-states" property is not defined. Similarly, the property "degen-levels" keeps track of the degeneralization levels. To retrieve it, call aut->get_named_prop<std::vector<unsigned>>("degen-levels"). @{

◆ dnf_to_streett()

twa_graph_ptr spot::dnf_to_streett ( const const_twa_graph_ptr &  aut,
bool  original_states = false 
)

#include <spot/twaalgos/totgba.hh>

Converts any DNF acceptance condition into Streett-like.

This function is an optimized version of the construction described by Lemma 4 and 5 of the paper below.

@Article{boker.2011.fossacs,
  author    = {Udi Boker and Orna Kupferman},
  title     = {Co-Büching Them All},
  booktitle = {Foundations of Software Science and Computational
               Structures - 14th International Conference, FOSSACS 2011}
  year      = {2011},
  pages     = {184--198},
  url       = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}

In the described construction, as many copies as there are minterms in the acceptance condition are made and the union of all those copies is returned. Instead of cloning the automaton for each minterm and end up with many rejecting and useless SCC, we construct the automaton SCC by SCC. Each SCC is copied at most as many times as there are minterms for which it is not rejecting and at least one time if it is always rejecting (to be consistent with the recognized language).

aut The automaton to convert. original_states Enable mapping between each state of the resulting automaton and the original state of the input automaton. This is stored in the "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it. Additionally, the correspondence between each created state and the associated DNF clause is recorded in the "original-clauses" property (also a vector of unsigned).

◆ has_separate_sets()

bool spot::has_separate_sets ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/sepsets.hh>

Whether the Inf and Fin numbers are disjoints.

◆ iar()

twa_graph_ptr spot::iar ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/rabin2parity.hh>

Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR)

If the input automaton has n states and k pairs, the output automaton has at most k!*n states and 2k+1 colors. If the input automaton is deterministic, the output automaton is deterministic as well, which is the intended use case for this function. If the input automaton is non-deterministic, the result is still correct, but way larger than an equivalent Büchi automaton. If the input automaton is Rabin-like (resp. Streett-like), the output automaton has max odd (resp. min even) acceptance condition. Details on the algorithm can be found in: https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)

Throws an std::runtime_error if the input is neither Rabin-like nor Street-like.

◆ iar_maybe()

twa_graph_ptr spot::iar_maybe ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/rabin2parity.hh>

Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR)

Returns nullptr if the input automaton is neither Rabin-like nor Streett-like, and calls spot::iar() otherwise.

◆ rabin_is_buchi_realizable()

bool spot::rabin_is_buchi_realizable ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/remfin.hh>

Check if is Büchi-realizable. This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built.

◆ rabin_to_buchi_maybe()

twa_graph_ptr spot::rabin_to_buchi_maybe ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/remfin.hh>

Convert a Rabin automaton to Büchi automaton, preserving determinism when possible.

Return nullptr if the input is not a Rabin (or Rabin-like) automaton.

This essentially applies the algorithm from "Deterministic ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94), but SCC-wise.

Unless you know what you are doing, you are probably better off calling remove_fin() instead, as this will call more specialized algorithms (e.g., for weak automata) when appropriate.

◆ remove_fin()

twa_graph_ptr spot::remove_fin ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/remfin.hh>

Rewrite an automaton without Fin or f acceptance.

This algorithm dispatches between many strategies. It has dedicated algorithms for weak automata, automata with Rabin-like acceptance, automata with Streett-like acceptance, and some generic code that will work on any kind of acceptance condition.

In Spot "f" acceptance is not considered Fin-less, because it can be seen as a case of generalized co-Büchi with 0 sets. Just like "t" corresponds generalized Büchi with 0 sets.)

◆ separate_sets_here()

twa_graph_ptr spot::separate_sets_here ( const twa_graph_ptr &  aut)

#include <spot/twaalgos/sepsets.hh>

Separate the Fin and Inf sets used by an automaton.

This makes sure that the numbers used a Fin and Inf are disjoints.

◆ simplify_acceptance()

twa_graph_ptr spot::simplify_acceptance ( const_twa_graph_ptr  aut)

#include <spot/twaalgos/cleanacc.hh>

Simplify an acceptance condition.

Does evereything cleanup_acceptance() does, but additionally: merge identical sets, detect whether to sets i and j are complementary to apply the following reductions:

  • Fin(i) & Inf(j) = Fin(i)
  • Fin(i) & Fin(j) = f
  • Fin(i) & Inf(i) = f
  • Fin(i) | Inf(j) = Inf(j)
  • Inf(i) | Inf(j) = t
  • Fin(i) | Inf(i) = t

◆ simplify_acceptance_here()

twa_graph_ptr spot::simplify_acceptance_here ( twa_graph_ptr  aut)

#include <spot/twaalgos/cleanacc.hh>

Simplify an acceptance condition.

Does evereything cleanup_acceptance() does, but additionally: merge identical sets, detect whether to sets i and j are complementary to apply the following reductions:

  • Fin(i) & Inf(j) = Fin(i)
  • Fin(i) & Fin(j) = f
  • Fin(i) & Inf(i) = f
  • Fin(i) | Inf(j) = Inf(j)
  • Inf(i) | Inf(j) = t
  • Fin(i) | Inf(i) = t

◆ streett_to_generalized_buchi()

twa_graph_ptr spot::streett_to_generalized_buchi ( const const_twa_graph_ptr &  in)

#include <spot/twaalgos/totgba.hh>

Convert Streett acceptance into generalized Büchi acceptance.

◆ streett_to_generalized_buchi_maybe()

twa_graph_ptr spot::streett_to_generalized_buchi_maybe ( const const_twa_graph_ptr &  in)

#include <spot/twaalgos/totgba.hh>

Convert Streett acceptance into generalized Büchi.

This version only works SPOT_STREET_CONF_MIN is set to a number of pairs less than the number of pairs used by in. The default is 3. It returns nullptr of that condition is not met, or if the input automaton does not have Streett-like acceptance.

◆ to_generalized_buchi()

twa_graph_ptr spot::to_generalized_buchi ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/totgba.hh>

Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton.

This dispatch between many algorithms. If the input has Streett (or Streett-like) acceptance, spot::streett_to_generalized_buchi() is called right away and produces a TGBA. Otherwise, it calls spot::remove_in() which returns a TBA.

◆ to_generalized_rabin()

twa_graph_ptr spot::to_generalized_rabin ( const const_twa_graph_ptr &  aut,
bool  share_inf = false 
)

#include <spot/twaalgos/totgba.hh>

Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton.

This works by putting the acceptance condition in disjunctive normal form, and then merging all the Fin(x1)&Fin(x2)&...&Fin(xn) that may occur in clauses into a single Fin(X).

The acceptance-set numbers used by Inf may appear in multiple clauses if share_inf is set.

◆ to_generalized_streett()

twa_graph_ptr spot::to_generalized_streett ( const const_twa_graph_ptr &  aut,
bool  share_fin = false 
)

#include <spot/twaalgos/totgba.hh>

Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton.

This works by putting the acceptance condition in cunjunctive normal form, and then merging all the Inf(x1)|Inf(x2)|...|Inf(xn) that may occur in clauses into a single Inf(X).

The acceptance-set numbers used by Fin may appear in multiple clauses if share_fin is set.

◆ to_parity()

twa_graph_ptr spot::to_parity ( const const_twa_graph_ptr &  aut,
bool  pretty_print = false 
)

#include <spot/twaalgos/toparity.hh>

Take an automaton with any acceptance condition and return an equivalent parity automaton.

The parity condition of the returned automaton is max even.


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 doxygen 1.8.13