spot  2.5.3
Modules | Functions

Modules

 TωA on-the-fly algorithms
 
 Input/Output of TωA
 
 Stutter-invariance checks and related functions
 
 Conversion between acceptance conditions
 
 Translating LTL formulas into TωA
 
 Algorithm patterns
 
 TωA simplifications
 
 Miscellaneous algorithms on TωA
 
 Emptiness-checks
 

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)
 Determinize a TGBA. More...
 
twa_graph_ptr spot::product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 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)
 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::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...
 

Detailed Description

Function Documentation

◆ product() [1/2]

twa_graph_ptr spot::product ( const const_twa_graph_ptr &  left,
const const_twa_graph_ptr &  right 
)

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

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product() [2/2]

twa_graph_ptr spot::product ( const const_twa_graph_ptr &  left,
const const_twa_graph_ptr &  right,
unsigned  left_state,
unsigned  right_state 
)

#include <spot/twaalgos/product.hh>

Intersect two automata using a synchronous product.

These variant allow 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.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product_or() [1/2]

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.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product_or() [2/2]

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.

These variant allow 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.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ sum() [1/2]

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.

Parameters
leftLeft term of the sum.
rightRight term of the sum.
Returns
A spot::twa_graph containing the sum of left and right

◆ sum() [2/2]

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.

Parameters
leftLeft term of the sum.
rightRight term of the sum.
left_stateInitial state of the left term of the sum.
right_stateInitial state of the right term of the sum.
Returns
A spot::twa_graph containing the sum of left and right

◆ sum_and() [1/2]

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.

Parameters
leftLeft term of the sum.
rightRight term of the sum.
Returns
A spot::twa_graph containing the sum of left and right

◆ sum_and() [2/2]

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.

Parameters
leftLeft term of the sum.
rightRight term of the sum.
left_stateInitial state of the left term of the sum.
right_stateInitial state of the right term of the sum.
Returns
A spot::twa_graph containing the sum of left and right

◆ tgba_determinize()

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 
)

#include <spot/twaalgos/determinize.hh>

Determinize a TGBA.

The main algorithm works only with automata using Büchi acceptance (preferably transition-based). 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, 3-4 (2012)). Redziejowski's algorithm is similar to Piterman's improvement of Safra's algorithm, except it is presented on transition-based acceptance and use simpler notations. We implement three additional optimizations (they can be individually disabled) based on

  • knowledge about SCCs of the input automaton
  • knowledge about simulation relations in the input automaton
  • knowledge about stutter-invariance of the input automaton

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 (letter-based stuttering) that is not implemented here.

Parameters
autthe automaton to determinize
pretty_printwhether 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_sccwhether to simplify the construction based on the SCCs in the input automaton.
use_simulationwhether to simplify the construction based on simulation relations between states in the original automaton.
use_stutterwhether to simplify the construction when the input automaton is known to be stutter-invariant. (The stutter-invariant flag of the input automaton is used, so it might be worth to call spot::check_stutter_invariance() first if possible.)

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