spot  2.9.8.dev
Classes | Functions

Classes

class  spot::aig
 A class representing AIG circuits. More...
 
struct  spot::synthesis_info
 Benchmarking data and options for synthesis. More...
 
struct  spot::strategy_like_t
 A struct that represents different types of strategy like objects. More...
 

Functions

twa_graph_ptr spot::split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env)
 make each transition a 2-step transition, transforming the graph into an alternating arena More...
 
twa_graph_ptr spot::unsplit_2step (const const_twa_graph_ptr &aut)
 the reverse of split_2step More...
 
std::ostream & spot::operator<< (std::ostream &os, synthesis_info::algo s)
 Stream algo. More...
 
std::ostream & spot::operator<< (std::ostream &os, const synthesis_info &gi)
 Stream benchmarks and options. More...
 
spot::twa_graph_ptr spot::apply_strategy (const spot::twa_graph_ptr &arena, bool unsplit, bool keep_acc)
 Takes a solved game and restricts the automaton to the winning strategy of the player. More...
 
strategy_like_t spot::try_create_direct_strategy (formula f, const std::vector< std::string > &output_aps, synthesis_info &gi)
 Creates a strategy for the formula given by calling all intermediate steps. More...
 
bool spot::solve_game (twa_graph_ptr arena, synthesis_info &gi)
 Solve a game, and update synthesis_info. More...
 
aig_ptr spot::strategy_to_aig (const const_twa_graph_ptr &aut, const char *mode)
 Convert a strategy into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::strategy_to_aig (const twa_graph_ptr &aut, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs)
 Convert a strategy into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::strategies_to_aig (const std::vector< const_twa_graph_ptr > &strat_vec, const char *mode)
 Convert multiple strategies into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::strategies_to_aig (const std::vector< twa_graph_ptr > &strat_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs)
 Convert multiple strategies into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::strategies_to_aig (const std::vector< strategy_like_t > &strat_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs)
 Convert multiple strategies into an aig relying on the transformation described by mode. More...
 
void spot::split_2step_fast_here (const twa_graph_ptr &aut, const bdd &output_bdd)
 make each transition a 2-step transition. More...
 
twa_graph_ptr spot::split_2step_fast (const const_twa_graph_ptr &aut, const bdd &output_bdd)
 make each transition a 2-step transition. More...
 
twa_graph_ptr spot::ltl_to_game (const formula &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr spot::ltl_to_game (const formula &f, const std::vector< std::string > &all_outs)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr spot::ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr spot::ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs)
 Creates a game from a specification and a set of output propositions. More...
 
void spot::minimize_strategy_here (twa_graph_ptr &strat, int min_lvl)
 Minimizes a strategy. Strategies are infact Mealy machines. So we can use techniques designed for them. More...
 
twa_graph_ptr spot::minimize_strategy (const_twa_graph_ptr &strat, int min_lvl)
 Minimizes a strategy. Strategies are infact Mealy machines. So we can use techniques designed for them. More...
 
twa_graph_ptr spot::create_strategy (twa_graph_ptr arena, synthesis_info &gi)
 creates a strategy from a solved game taking into account the options given in gi More...
 
twa_graph_ptr spot::create_strategy (twa_graph_ptr arena)
 creates a strategy from a solved game taking into account the options given in gi More...
 
std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independant_formulas (formula f, const std::vector< std::string > &outs)
 Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
 
std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independant_formulas (const std::string &f, const std::vector< std::string > &outs)
 Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
 

Detailed Description

Function Documentation

◆ apply_strategy()

spot::twa_graph_ptr spot::apply_strategy ( const spot::twa_graph_ptr &  arena,
bool  unsplit,
bool  keep_acc 
)

#include <spot/twaalgos/synthesis.hh>

Takes a solved game and restricts the automaton to the winning strategy of the player.

Parameters
arenatwa_graph with named properties "state-player", "strategy" and "state-winner"
unsplitWhether or not to unsplit the automaton
keep_accWhether or not keep the acceptance condition
Returns
the resulting twa_graph

◆ create_strategy() [1/2]

twa_graph_ptr spot::create_strategy ( twa_graph_ptr  arena)

#include <spot/twaalgos/synthesis.hh>

creates a strategy from a solved game taking into account the options given in gi

◆ create_strategy() [2/2]

twa_graph_ptr spot::create_strategy ( twa_graph_ptr  arena,
synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

creates a strategy from a solved game taking into account the options given in gi

◆ ltl_to_game() [1/4]

twa_graph_ptr spot::ltl_to_game ( const formula f,
const std::vector< std::string > &  all_outs 
)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters
fThe specification given as an LTL/PSL formula, or as a string.
all_outsThe names of all output propositions
gisynthesis_info structure
Note
All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [2/4]

twa_graph_ptr spot::ltl_to_game ( const formula f,
const std::vector< std::string > &  all_outs,
synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters
fThe specification given as an LTL/PSL formula, or as a string.
all_outsThe names of all output propositions
gisynthesis_info structure
Note
All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [3/4]

twa_graph_ptr spot::ltl_to_game ( const std::string &  f,
const std::vector< std::string > &  all_outs 
)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters
fThe specification given as an LTL/PSL formula, or as a string.
all_outsThe names of all output propositions
gisynthesis_info structure
Note
All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [4/4]

twa_graph_ptr spot::ltl_to_game ( const std::string &  f,
const std::vector< std::string > &  all_outs,
synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters
fThe specification given as an LTL/PSL formula, or as a string.
all_outsThe names of all output propositions
gisynthesis_info structure
Note
All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ minimize_strategy()

twa_graph_ptr spot::minimize_strategy ( const_twa_graph_ptr &  strat,
int  min_lvl 
)

#include <spot/twaalgos/synthesis.hh>

Minimizes a strategy. Strategies are infact Mealy machines. So we can use techniques designed for them.

Parameters
stratThe machine to minimize
min_lvlHow to minimize the machine: 0: No minimization, 1: Minimizing it like an DFA, means the language is preserved, 2: Inclusion with output assignement, 3: Exact minimization using SAT solving, 4: SAT solving with DFA minimization as preprocessing, 5: SAT solving using inclusion based minimization with output assignment as preprocessing
Note
min_lvl 1 and 2 work more efficiently on UNSPLIT strategies, whereas min_lvl 3, 4 and 5 mandate a SPLIT strategy

◆ minimize_strategy_here()

void spot::minimize_strategy_here ( twa_graph_ptr &  strat,
int  min_lvl 
)

#include <spot/twaalgos/synthesis.hh>

Minimizes a strategy. Strategies are infact Mealy machines. So we can use techniques designed for them.

Parameters
stratThe machine to minimize
min_lvlHow to minimize the machine: 0: No minimization, 1: Minimizing it like an DFA, means the language is preserved, 2: Inclusion with output assignement, 3: Exact minimization using SAT solving, 4: SAT solving with DFA minimization as preprocessing, 5: SAT solving using inclusion based minimization with output assignment as preprocessing
Note
min_lvl 1 and 2 work more efficiently on UNSPLIT strategies, whereas min_lvl 3, 4 and 5 mandate a SPLIT strategy

◆ operator<<() [1/2]

std::ostream& spot::operator<< ( std::ostream &  os,
const synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

Stream benchmarks and options.

◆ operator<<() [2/2]

std::ostream& spot::operator<< ( std::ostream &  os,
synthesis_info::algo  s 
)

#include <spot/twaalgos/synthesis.hh>

Stream algo.

◆ solve_game()

bool spot::solve_game ( twa_graph_ptr  arena,
synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

Solve a game, and update synthesis_info.

This is just a wrapper around the solve_game() function with a single argument. This one measure the runtime and update gi.

◆ split_2step()

twa_graph_ptr spot::split_2step ( const const_twa_graph_ptr &  aut,
const bdd &  output_bdd,
bool  complete_env 
)

#include <spot/twaalgos/synthesis.hh>

make each transition a 2-step transition, transforming the graph into an alternating arena

Given a set of atomic propositions I, split each transition p – cond --> q cond in 2^2^AP into a set of transitions of the form p – {a} --> (p,a) – o --> q for each a in cond \cap 2^2^I and where o = (cond & a) \cap 2^2^(O)

By definition, the states p are deterministic, only the states of the form (p,a) may be non-deterministic. This function is used to transform an automaton into a turn-based game in the context of LTL reactive synthesis.

Parameters
autautomaton to be transformed
output_bddconjunction of all output AP, all APs not present are treated as inputs
complete_envWhether the automaton should be complete for the environment, i.e. the player of I
Note
This function also computes the state players
If the automaton is to be completed for both env and player then egdes between the sinks will be added (assuming that the environnement/player of I) plays first

◆ split_2step_fast()

twa_graph_ptr spot::split_2step_fast ( const const_twa_graph_ptr &  aut,
const bdd &  output_bdd 
)

#include <spot/twaalgos/synthesis.hh>

make each transition a 2-step transition.

This algorithm is only applicable if all transitions of the graph have the form p – ins & outs --> q. That is they are a conjunction of a condition over the input propositions ins and a condition over the output propositions outs

Parameters
autautomaton to be transformed
output_bddconjunction of all output AP, all APs not present are treated as inputs

◆ split_2step_fast_here()

void spot::split_2step_fast_here ( const twa_graph_ptr &  aut,
const bdd &  output_bdd 
)

#include <spot/twaalgos/synthesis.hh>

make each transition a 2-step transition.

This algorithm is only applicable if all transitions of the graph have the form p – ins & outs --> q. That is they are a conjunction of a condition over the input propositions ins and a condition over the output propositions outs

Parameters
autautomaton to be transformed
output_bddconjunction of all output AP, all APs not present are treated as inputs

◆ split_independant_formulas() [1/2]

std::pair<std::vector<formula>, std::vector<std::set<formula> > > spot::split_independant_formulas ( const std::string &  f,
const std::vector< std::string > &  outs 
)

#include <spot/twaalgos/synthesis.hh>

Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification.

The algorithm is based on work by Finkbeiner et al. [18], [19].

Parameters
fthe formula to split
outsvector with the names of all output propositions
Returns
A vector of pairs holding a subformula and the used output propositions each.

◆ split_independant_formulas() [2/2]

std::pair<std::vector<formula>, std::vector<std::set<formula> > > spot::split_independant_formulas ( formula  f,
const std::vector< std::string > &  outs 
)

#include <spot/twaalgos/synthesis.hh>

Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification.

The algorithm is based on work by Finkbeiner et al. [18], [19].

Parameters
fthe formula to split
outsvector with the names of all output propositions
Returns
A vector of pairs holding a subformula and the used output propositions each.

◆ strategies_to_aig() [1/3]

aig_ptr spot::strategies_to_aig ( const std::vector< const_twa_graph_ptr > &  strat_vec,
const char *  mode 
)

#include <spot/twaalgos/aiger.hh>

Convert multiple strategies into an aig relying on the transformation described by mode.

Note
The states of each strategy are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

◆ strategies_to_aig() [2/3]

aig_ptr spot::strategies_to_aig ( const std::vector< strategy_like_t > &  strat_vec,
const char *  mode,
const std::vector< std::string > &  ins,
const std::vector< std::vector< std::string >> &  outs 
)

#include <spot/twaalgos/aiger.hh>

Convert multiple strategies into an aig relying on the transformation described by mode.

Note
The states of each strategy are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

◆ strategies_to_aig() [3/3]

aig_ptr spot::strategies_to_aig ( const std::vector< twa_graph_ptr > &  strat_vec,
const char *  mode,
const std::vector< std::string > &  ins,
const std::vector< std::vector< std::string >> &  outs 
)

#include <spot/twaalgos/aiger.hh>

Convert multiple strategies into an aig relying on the transformation described by mode.

Note
The states of each strategy are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

◆ strategy_to_aig() [1/2]

aig_ptr spot::strategy_to_aig ( const const_twa_graph_ptr &  aut,
const char *  mode 
)

#include <spot/twaalgos/aiger.hh>

Convert a strategy into an aig relying on the transformation described by mode.

Parameters
modeThis param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

◆ strategy_to_aig() [2/2]

aig_ptr spot::strategy_to_aig ( const twa_graph_ptr &  aut,
const char *  mode,
const std::vector< std::string > &  ins,
const std::vector< std::string > &  outs 
)

#include <spot/twaalgos/aiger.hh>

Convert a strategy into an aig relying on the transformation described by mode.

Parameters
modeThis param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

◆ try_create_direct_strategy()

strategy_like_t spot::try_create_direct_strategy ( formula  f,
const std::vector< std::string > &  output_aps,
synthesis_info gi 
)

#include <spot/twaalgos/synthesis.hh>

Creates a strategy for the formula given by calling all intermediate steps.

For certain formulas, we can ''bypass'' the traditional way and find directly a strategy or some other representation of a winning condition without translating the formula as such. If no such simplifications can be made, it executes the usual way.

Parameters
fThe formula to synthesize a strategy for
output_apsA vector with the name of all output properties. All APs not named in this vector are treated as inputs

◆ unsplit_2step()

twa_graph_ptr spot::unsplit_2step ( const const_twa_graph_ptr &  aut)

#include <spot/twaalgos/synthesis.hh>

the reverse of split_2step

Note
This function relies on the named property "state-player"

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