spot
2.8.5

Functions  
twa_graph_ptr  spot::tgba_determinize (const const_twa_graph_ptr &aut, bool pretty_print=false, bool use_scc=true, bool use_simulation=true, bool use_stutter=true, const output_aborter *aborter=nullptr) 
Determinize a TGBA. More...  
twa_graph_ptr  spot::product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, const output_aborter *aborter=nullptr) 
Intersect two automata using a synchronous product. More...  
twa_graph_ptr  spot::product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state, const output_aborter *aborter=nullptr) 
Intersect two automata using a synchronous product. More...  
twa_graph_ptr  spot::product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right) 
Sum two automata using a synchronous product. More...  
twa_graph_ptr  spot::product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state) 
Sum two automata using a synchronous product. More...  
twa_graph_ptr  spot::product_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp) 
Build the product of an automaton with a suspendable automaton. More...  
twa_graph_ptr  spot::product_or_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp) 
Build the "or" product of an automaton with a suspendable automaton. More...  
twa_graph_ptr  spot::sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right) 
Sum two twa into a new twa, performing the union of the two input automata. More...  
twa_graph_ptr  spot::sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state) 
Sum two twa into a new twa, performing the union of the two input automata. More...  
twa_graph_ptr  spot::sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right) 
Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...  
twa_graph_ptr  spot::sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state) 
Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...  
twa_graph_ptr spot::product  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right,  
const output_aborter *  aborter = nullptr 

) 
#include <spot/twaalgos/product.hh>
Intersect two automata using a synchronous product.
The resulting automaton will accept the intersection of both languages and have an acceptance condition that is the conjunction of the acceptance conditions of the two input automata. In case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets.
The algorithm also defines a named property called "productstates" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.
If an aborter is given, the function will return nullptr whenever the resulting product would be too large.
twa_graph_ptr spot::product  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right,  
unsigned  left_state,  
unsigned  right_state,  
const output_aborter *  aborter = nullptr 

) 
#include <spot/twaalgos/product.hh>
Intersect two automata using a synchronous product.
This variant allows changing the initial state of both automata in case you want to start the product at a different place.
The resulting automaton will accept the intersection of the languages recognized by each input automaton (with its initial state changed) and have an acceptance condition that is the conjunction of the acceptance conditions of the two input automata. In case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets.
The algorithm also defines a named property called "productstates" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.
If an aborter is given, the function will return nullptr whenever the resulting product would be too large.
twa_graph_ptr spot::product_or  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right  
) 
#include <spot/twaalgos/product.hh>
Sum two automata using a synchronous product.
The resulting automaton will accept the union of both languages and have an acceptance condition that is the disjunction of the acceptance conditions of the two input automata. In case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets.
The algorithm also defines a named property called "productstates" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.
twa_graph_ptr spot::product_or  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right,  
unsigned  left_state,  
unsigned  right_state  
) 
#include <spot/twaalgos/product.hh>
Sum two automata using a synchronous product.
This variant allows changing the initial state of both automata in case you want to start the product at a different place.
The resulting automaton will accept the sum of the languages recognized by each input automaton (with its initial state changed) and have an acceptance condition that is the disjunction of the acceptance conditions of the two input automata. In case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets.
The algorithm also defines a named property called "productstates" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.
twa_graph_ptr spot::product_or_susp  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right_susp  
) 
#include <spot/twaalgos/product.hh>
Build the "or" product of an automaton with a suspendable automaton.
The language of this product is the union of the languages of both input automata.
This function assumes that right_susp is a suspendable automaton, i.e., it its language L satisfies L = Σ*.L. Therefore, after left has been completed (this will be done by product_or_susp) the product between the two automata need only be done with the SCCs of left that contains some rejecting cycles.
The current implementation is currently suboptimal as instead of looking for SCC with rejecting cycles, it simply loop for nontrivial SCC, (or in the case of weak automata, with nontrivial and rejecting SCCs).
twa_graph_ptr spot::product_susp  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right_susp  
) 
#include <spot/twaalgos/product.hh>
Build the product of an automaton with a suspendable automaton.
The language of this product is the intersection of the languages of both input automata.
This function assumes that right_susp is a suspendable automaton, i.e., it its language L satisfies L = Σ*.L. Therefore the product between the two automata need only be done with the accepting SCCs of left.
If left is a weak automaton, the acceptance condition of the output will be that of right_susp. Otherwise the acceptance condition is the conjunction of both acceptances.
twa_graph_ptr spot::sum  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right  
) 
#include <spot/twaalgos/sum.hh>
Sum two twa into a new twa, performing the union of the two input automata.
left  Left term of the sum. 
right  Right term of the sum. 
twa_graph_ptr spot::sum  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right,  
unsigned  left_state,  
unsigned  right_state  
) 
#include <spot/twaalgos/sum.hh>
Sum two twa into a new twa, performing the union of the two input automata.
left  Left term of the sum. 
right  Right term of the sum. 
left_state  Initial state of the left term of the sum. 
right_state  Initial state of the right term of the sum. 
twa_graph_ptr spot::sum_and  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right  
) 
#include <spot/twaalgos/sum.hh>
Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata.
left  Left term of the sum. 
right  Right term of the sum. 
twa_graph_ptr spot::sum_and  (  const const_twa_graph_ptr &  left, 
const const_twa_graph_ptr &  right,  
unsigned  left_state,  
unsigned  right_state  
) 
#include <spot/twaalgos/sum.hh>
Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata.
left  Left term of the sum. 
right  Right term of the sum. 
left_state  Initial state of the left term of the sum. 
right_state  Initial state of the right term of the sum. 
twa_graph_ptr spot::tgba_determinize  (  const const_twa_graph_ptr &  aut, 
bool  pretty_print = false , 

bool  use_scc = true , 

bool  use_simulation = true , 

bool  use_stutter = true , 

const output_aborter *  aborter = nullptr 

) 
#include <spot/twaalgos/determinize.hh>
Determinize a TGBA.
The main algorithm works only with automata using Büchi acceptance (preferably transitionbased). If generalized Büchi is input, it will be automatically degeneralized first.
The output will be a deterministic automaton using parity acceptance.
This procedure is based on an algorithm by Roman Redziejowski (Fundamenta Informaticae 119, 34 (2012)). Redziejowski's algorithm is similar to Piterman's improvement of Safra's algorithm, except it is presented on transitionbased acceptance and use simpler notations. We implement three additional optimizations (they can be individually disabled) based on
The last optimization is an idea described by Joachim Klein & Christel Baier (CIAA'07) and implemented in ltl2dstar. In fact, ltl2dstar even has a finer version (letterbased stuttering) that is not implemented here.
aut  the automaton to determinize 
pretty_print  whether to decorate states with names showing the paths they track (this only makes sense if the input has Büchi acceptance already, otherwise the input automaton will be degeneralized and the names will refer to the states in the degeneralized automaton). 
use_scc  whether to simplify the construction based on the SCCs in the input automaton. 
use_simulation  whether to simplify the construction based on simulation relations between states in the original automaton. 
use_stutter  whether to simplify the construction when the input automaton is known to be stutterinvariant. (The stutterinvariant flag of the input automaton is used, so it might be worth to call spot::check_stutter_invariance() first if possible.) 
aborter  abort the construction if the constructed automaton would be too large. Return nullptr in this case. 