spot 2.12.2
|
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, bool want_strategy=false) |
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... | |
game_relabeling_map | spot::partitioned_game_relabel_here (twa_graph_ptr &arena, bool relabel_env, bool relabel_play, bool split_env=false, bool split_play=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u) |
Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions. More... | |
void | spot::relabel_game_here (twa_graph_ptr &arena, game_relabeling_map &rel_maps) |
Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions. 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, const realizability_simplifier *rs=nullptr) |
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, const realizability_simplifier *rs=nullptr) |
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 mealy machines 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 mealy machines 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, const realizability_simplifier *rs=nullptr) |
Convert multiple mealy machines 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, const realizability_simplifier *rs=nullptr) |
Convert multiple mealy machines 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_mealy (twa_graph_ptr arena, synthesis_info &gi) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
twa_graph_ptr | spot::solved_game_to_mealy (twa_graph_ptr arena) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
twa_graph_ptr | spot::solved_game_to_separated_mealy (twa_graph_ptr arena, synthesis_info &gi) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
twa_graph_ptr | spot::solved_game_to_separated_mealy (twa_graph_ptr arena) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
twa_graph_ptr | spot::solved_game_to_split_mealy (twa_graph_ptr arena, synthesis_info &gi) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
twa_graph_ptr | spot::solved_game_to_split_mealy (twa_graph_ptr arena) |
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More... | |
std::pair< std::vector< formula >, std::vector< std::set< formula > > > | spot::split_independent_formulas (formula f, const std::vector< std::string > &outs) |
Seeks to decompose a formula into independently synthetizable 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_independent_formulas (const std::string &f, const std::vector< std::string > &outs) |
Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More... | |
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.
f | The specification given as an LTL/PSL formula, or as a string. |
all_outs | The names of all output propositions |
gi | synthesis_info structure |
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.
f | The specification given as an LTL/PSL formula, or as a string. |
all_outs | The names of all output propositions |
gi | synthesis_info structure |
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.
f | The specification given as an LTL/PSL formula, or as a string. |
all_outs | The names of all output propositions |
gi | synthesis_info structure |
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.
f | The specification given as an LTL/PSL formula, or as a string. |
all_outs | The names of all output propositions |
gi | synthesis_info structure |
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.
mode | This 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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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.
mode | This 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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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, | ||
const realizability_simplifier * | rs = nullptr |
||
) |
#include <spot/twaalgos/aiger.hh>
Convert a mealy (like) machine into an aig relying on the transformation described by mode.
mode | This 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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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, | ||
const realizability_simplifier * | rs = nullptr |
||
) |
#include <spot/twaalgos/aiger.hh>
Convert a mealy (like) machine into an aig relying on the transformation described by mode.
mode | This 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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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 mealy machines into an aig relying on the transformation described by mode.
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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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, | ||
const realizability_simplifier * | rs = nullptr |
||
) |
#include <spot/twaalgos/aiger.hh>
Convert multiple mealy machines into an aig relying on the transformation described by mode.
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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
aig_ptr spot::mealy_machines_to_aig | ( | const std::vector< mealy_like > & | m_vec, |
const char * | mode | ||
) |
#include <spot/twaalgos/aiger.hh>
Convert multiple mealy machines into an aig relying on the transformation described by mode.
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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
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, | ||
const realizability_simplifier * | rs = nullptr |
||
) |
#include <spot/twaalgos/aiger.hh>
Convert multiple mealy machines into an aig relying on the transformation described by mode.
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.
If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.
std::ostream & spot::operator<< | ( | std::ostream & | os, |
const synthesis_info & | gi | ||
) |
#include <spot/twaalgos/synthesis.hh>
Stream benchmarks and options.
std::ostream & spot::operator<< | ( | std::ostream & | os, |
synthesis_info::algo | s | ||
) |
#include <spot/twaalgos/synthesis.hh>
Stream algo.
game_relabeling_map spot::partitioned_game_relabel_here | ( | twa_graph_ptr & | arena, |
bool | relabel_env, | ||
bool | relabel_play, | ||
bool | split_env = false , |
||
bool | split_play = false , |
||
unsigned | max_letter = -1u , |
||
unsigned | max_letter_mult = -1u |
||
) |
#include <spot/twaalgos/synthesis.hh>
Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions.
void spot::relabel_game_here | ( | twa_graph_ptr & | arena, |
game_relabeling_map & | rel_maps | ||
) |
#include <spot/twaalgos/synthesis.hh>
Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions.
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.
twa_graph_ptr spot::solved_game_to_mealy | ( | twa_graph_ptr | arena | ) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
twa_graph_ptr spot::solved_game_to_mealy | ( | twa_graph_ptr | arena, |
synthesis_info & | gi | ||
) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
twa_graph_ptr spot::solved_game_to_separated_mealy | ( | twa_graph_ptr | arena | ) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
twa_graph_ptr spot::solved_game_to_separated_mealy | ( | twa_graph_ptr | arena, |
synthesis_info & | gi | ||
) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
twa_graph_ptr spot::solved_game_to_split_mealy | ( | twa_graph_ptr | arena | ) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
twa_graph_ptr spot::solved_game_to_split_mealy | ( | twa_graph_ptr | arena, |
synthesis_info & | gi | ||
) |
#include <spot/twaalgos/synthesis.hh>
creates a mealy machine from a solved game arena 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_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations
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'.
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 ∪ 2^2^I and where o = (cond & a) ∪ 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.
aut | automaton to be transformed |
output_bdd | conjunction of all output AP, all APs not present are treated as inputs |
complete_env | Whether the automaton should be complete for the environment, i.e. the player of inputs |
std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independent_formulas | ( | const std::string & | f, |
const std::vector< std::string > & | outs | ||
) |
#include <spot/twaalgos/synthesis.hh>
Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification.
The algorithm is based on work by Finkbeiner et al. [23], [24].
f | the formula to split |
outs | vector with the names of all output propositions |
std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independent_formulas | ( | formula | f, |
const std::vector< std::string > & | outs | ||
) |
#include <spot/twaalgos/synthesis.hh>
Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification.
The algorithm is based on work by Finkbeiner et al. [23], [24].
f | the formula to split |
outs | vector with the names of all output propositions |
mealy_like spot::try_create_direct_strategy | ( | formula | f, |
const std::vector< std::string > & | output_aps, | ||
synthesis_info & | gi, | ||
bool | want_strategy = false |
||
) |
#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.
f | The formula to synthesize a strategy for |
output_aps | A vector with the name of all output properties. All APs not named in this vector are treated as inputs |
want_strategy | Set to false if we don't want to construct the strategy but only test realizability. |
twa_graph_ptr spot::unsplit_2step | ( | const const_twa_graph_ptr & | aut | ) |
#include <spot/twaalgos/synthesis.hh>
the inverse of split_2step