spot  2.10.6
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::mealy_like
 A struct that represents different types of mealy like objects. More...
 

Functions

twa_graph_ptr spot::split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true)
 make each transition a 2-step transition, transforming the graph into an alternating arena More...
 
twa_graph_ptr spot::split_2step (const const_twa_graph_ptr &aut, bool complete_env=true)
 Like split_2step but relying on the named property 'synthesis-outputs'. More...
 
twa_graph_ptr spot::unsplit_2step (const const_twa_graph_ptr &aut)
 the inverse 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...
 
mealy_like 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::mealy_machine_to_aig (const const_twa_graph_ptr &m, const char *mode)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machine_to_aig (const twa_graph_ptr &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machine_to_aig (const mealy_like &m, const char *mode)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machine_to_aig (mealy_like &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode)
 Convert multiple strategies into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode)
 Convert multiple strategies into an aig relying on the transformation described by mode. More...
 
aig_ptr spot::mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_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::mealy_machines_to_aig (const std::vector< mealy_like > &m_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...
 
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...
 
twa_graph_ptr spot::solved_game_to_separated_mealy (twa_graph_ptr arena, synthesis_info &gi)
 creates a separated mealy machine from a solved game taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. More...
 
twa_graph_ptr spot::solved_game_to_separated_mealy (twa_graph_ptr arena)
 creates a separated mealy machine from a solved game taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. 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

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

◆ mealy_machine_to_aig() [1/4]

aig_ptr spot::mealy_machine_to_aig ( const const_twa_graph_ptr &  m,
const char *  mode 
)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine 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.

◆ mealy_machine_to_aig() [2/4]

aig_ptr spot::mealy_machine_to_aig ( const mealy_like m,
const char *  mode 
)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine 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.

◆ mealy_machine_to_aig() [3/4]

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

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine 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.

◆ mealy_machine_to_aig() [4/4]

aig_ptr spot::mealy_machine_to_aig ( mealy_like m,
const char *  mode,
const std::vector< std::string > &  ins,
const std::vector< std::string > &  outs 
)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine 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.

◆ mealy_machines_to_aig() [1/4]

aig_ptr spot::mealy_machines_to_aig ( const std::vector< const_twa_graph_ptr > &  m_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.

◆ mealy_machines_to_aig() [2/4]

aig_ptr spot::mealy_machines_to_aig ( const std::vector< const_twa_graph_ptr > &  m_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.

◆ mealy_machines_to_aig() [3/4]

aig_ptr spot::mealy_machines_to_aig ( const std::vector< mealy_like > &  m_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.

◆ mealy_machines_to_aig() [4/4]

aig_ptr spot::mealy_machines_to_aig ( const std::vector< mealy_like > &  m_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.

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

◆ solved_game_to_separated_mealy() [1/2]

twa_graph_ptr spot::solved_game_to_separated_mealy ( twa_graph_ptr  arena)

#include <spot/twaalgos/synthesis.hh>

creates a separated mealy machine from a solved game taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how.

◆ solved_game_to_separated_mealy() [2/2]

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

#include <spot/twaalgos/synthesis.hh>

creates a separated mealy machine from a solved game taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how.

◆ split_2step() [1/2]

twa_graph_ptr spot::split_2step ( const const_twa_graph_ptr &  aut,
bool  complete_env = true 
)

#include <spot/twaalgos/synthesis.hh>

Like split_2step but relying on the named property 'synthesis-outputs'.

◆ split_2step() [2/2]

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

#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. The player of inputs (aka environment) plays first.

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 inputs
Note
This function also computes the state players
If the automaton is to be completed, sink states will be added for both env and player if necessary

◆ 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. [19], [20].

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. [19], [20].

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.

◆ try_create_direct_strategy()

mealy_like 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 inverse of split_2step

Precondition
aut is an alternating arena
Postcondition
All edge conditions in the returned automaton are of the form ins&outs, with ins/outs being a condition over the input/output propositions
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