alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

games, synthetis: improve Doxygen

Browse source 
* spot/twaalgos/game.hh, spot/twaalgos/synthesis.hh,
spot/twaalgos/aiger.hh: Declare new Doxygen groups for games and
synthesis.
* doc/spot.bib: Cleanup.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-03 19:13:15 +02:00
parent 188fee4756
commit 405f76f0a0
4 changed files with 129 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

22
doc/spot.bib
View file

@ -361,11 +361,23 @@
doi = {10.1016/S0020-0190(00)00113-7}
}
@article{finkbeiner2021specification,
title={Specification Decomposition for Reactive Synthesis (Full Version)},
author={Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi},
journal={arXiv preprint arXiv:2103.08459},
year={2021}
@TechReport{ finkbeiner.21.arxiv,
title = {Specification Decomposition for Reactive Synthesis (Full
Version)},
author = {Bernd Finkbeiner and Gideon Geier and Noemi Passing},
year = 2021,
url = {https://arxiv.org/abs/2103.08459/}
}
@InProceedings{ finkbeiner.21.nfm,
title = {Specification Decomposition for Reactive Synthesis},
author = {Bernd Finkbeiner and Gideon Geier and Noemi Passing},
booktitle = {Procedings of NASA Formal Methods (NFM'21)},
volume = {12673},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
doi = {10.1007/978-3-030-76384-8_8},
year = {2021}
}
@InProceedings{ gastin.01.cav,

71
spot/twaalgos/aiger.hh
View file

@ -43,6 +43,7 @@ namespace spot
typedef std::shared_ptr<aig> aig_ptr;
typedef std::shared_ptr<const aig> const_aig_ptr;
/// \ingroup synthesis
/// \brief A class representing AIG circuits
///
/// AIG circuits consist of (named) inputs, (named) outputs, latches which
@ -413,6 +414,7 @@ namespace spot
};
/// \ingroup synthesis
/// \brief Convert a strategy into an aig relying on the transformation
/// described by \a mode.
/// \param mode This param has to be of the form
@ -429,48 +431,50 @@ namespace spot
/// blocks with `sub0` being no separation, `sub1` separation into
/// input/latches/gates (`isop` only) and `sub2` tries to seek
/// common subformulas.
///
/// If \a ins and \a outs are specified, the named-property
/// synthesis-output is ignored and all properties in \a ins and \a
/// outs are guaranteed to appear in the aiger circuit.
///@{
SPOT_API aig_ptr
strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode);
SPOT_API aig_ptr
strategy_to_aig(const twa_graph_ptr& aut, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs);
///@}
/// \ingroup synthesis
/// \brief 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.
/// \note Attention: 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 create_game
/// are absent.
///
/// Unless \a ins and \a 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 create_game are absent.
/// If \a ins and \a outs are used, all properties they list are
/// guaranteed to appear in the aiger circuit.
/// @{
SPOT_API aig_ptr
strategies_to_aig(const std::vector<const_twa_graph_ptr>& strat_vec,
const char* mode);
/// \brief Like above, but explicitly handing over which propositions
/// are inputs and outputs and does therefore not rely on the
/// named property "synthesis-outputs"
/// \note All properties in ins and out are guaranteed to appear in the
/// aiger circuit.
SPOT_API aig_ptr
strategy_to_aig(const twa_graph_ptr& aut, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs);
/// \brief Like above, but explicitly handing over the propositions
/// \note All properties in ins and out are guaranteed to appear in the
/// aiger circuit.
SPOT_API aig_ptr
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);
/// \brief Like above, but works on strategy_like elements
SPOT_API aig_ptr
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);
/// @}
/// \ingroup twa_io
/// \brief Print the aig to stream in AIGER format
SPOT_API std::ostream&
print_aiger(std::ostream& os, const_aig_ptr circuit);
@ -494,23 +498,22 @@ namespace spot
/// does not need to be a minterm.
/// Correct graphs are generated by spot::unsplit_2step
///
///
/// \param os The output stream to print on.
/// \param aut The automaton to output.
/// \param mode This param has to be of the form
/// ite|isop|both [+dc][+dual][+so0|+so1|+so2|+so3]
/// Where ite means encoded via if-then-else normalform
/// isop means encoded via irreducible sum of products
/// both means trying both encodings and keep the smaller circuit.
/// +dc is optional and tries to take advantage of "do not care"
/// outputs to minimize the circuit.
/// +dual is optional and indicates that the algorithm
/// should also try to encode the negation to generate smaller
/// circuits.
/// +sox indicates that the conditions can be seperated into
/// blocks with so0 being no separation, so1 separation into
/// input/latches/gates (isop only) and so2 tries to
/// seek common subformulas.
/// `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.
SPOT_API std::ostream&
print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
const char* mode);

35
spot/twaalgos/game.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -33,7 +33,10 @@
namespace spot
{
/// \addtogroup games Functions related to game solving
/// \ingroup twa_algorithms
/// \ingroup games
/// \brief Transform an automaton into a parity game by propagating
/// players
///
@ -55,6 +58,7 @@ namespace spot
typedef std::vector<unsigned> strategy_t;
/// \ingroup games
/// \brief solve a parity-game
///
/// The arena is a deterministic max odd parity automaton with a
@ -74,6 +78,7 @@ namespace spot
SPOT_API
bool solve_parity_game(const twa_graph_ptr& arena);
/// \ingroup games
/// \brief Solve a safety game.
///
/// The arena should be represented by an automaton with true
@ -90,6 +95,7 @@ namespace spot
SPOT_API
bool solve_safety_game(twa_graph_ptr game);
/// \ingroup games
/// \brief Benchmarking and options structure for games and synthesis
///
/// \note This structure is designed to interface with the algorithms
@ -142,14 +148,17 @@ namespace spot
bdd_dict_ptr dict;
};
/// \ingroup games
/// \brief Stream solvers
SPOT_API std::ostream&
operator<<(std::ostream& os, game_info::solver s);
/// \ingroup games
/// \brief Stream benchmarks and options
SPOT_API std::ostream &
operator<<(std::ostream &os, const game_info &gi);
/// \ingroup games
/// \brief Generic interface for game solving
///
/// Calls the most suitable solver, depending on the type of game/
@ -163,6 +172,7 @@ namespace spot
SPOT_API bool
solve_game(twa_graph_ptr arena, game_info& gi);
/// \ingroup games
/// \brief Generic interface for game solving
///
/// See solve_game(arena, gi)
@ -170,11 +180,13 @@ namespace spot
solve_game(twa_graph_ptr arena);
/// \ingroup games
/// \brief Print a max odd parity game using PG-solver syntax
SPOT_API
void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
/// \ingroup games
/// \brief Highlight the edges of a strategy on an automaton.
///
/// Pass a negative color to not display the corresponding strategy.
@ -183,34 +195,48 @@ namespace spot
int player0_color = 5,
int player1_color = 4);
/// \ingroup games
/// \brief Set the owner for all the states.
/// @{
SPOT_API
void set_state_players(twa_graph_ptr arena, const region_t& owners);
SPOT_API
void set_state_players(twa_graph_ptr arena, region_t&& owners);
/// @}
/// \ingroup games
/// \brief Set the owner of a state.
SPOT_API
void set_state_player(twa_graph_ptr arena, unsigned state, bool owner);
/// \ingroup games
/// \brief Get the owner of a state.
SPOT_API
bool get_state_player(const_twa_graph_ptr arena, unsigned state);
/// \ingroup games
/// \brief Get the owner of all states
SPOT_API
const region_t& get_state_players(const_twa_graph_ptr arena);
/// \ingroup games
/// \brief Get or set the strategy
/// @{
SPOT_API
const strategy_t& get_strategy(const_twa_graph_ptr arena);
SPOT_API
void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
SPOT_API
void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
/// @}
/// \ingroup games
/// \brief Set all synthesis outputs as a conjunction
SPOT_API
void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
/// \ingroup games
/// \brief Get all synthesis outputs as a conjunction
SPOT_API
bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
@ -219,19 +245,26 @@ namespace spot
std::vector<std::string>
get_synthesis_output_aps(const const_twa_graph_ptr& arena);
/// \ingroup games
/// \brief Set the winner for all the states.
/// @{
SPOT_API
void set_state_winners(twa_graph_ptr arena, const region_t& winners);
SPOT_API
void set_state_winners(twa_graph_ptr arena, region_t&& winners);
/// @}
/// \ingroup games
/// \brief Set the winner of a state.
SPOT_API
void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
/// \ingroup games
/// \brief Get the winner of a state.
SPOT_API
bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
/// \ingroup games
/// \brief Get the winner of all states
SPOT_API
const region_t& get_state_winners(const_twa_graph_ptr arena);

60
spot/twaalgos/synthesis.hh
View file

@ -25,6 +25,10 @@
namespace spot
{
/// \addtogroup synthesis Reactive Synthesis
/// \ingroup twa_algorithms
/// \ingroup synthesis
/// \brief make each transition a 2-step transition, transforming
/// the graph into an alternating arena
///
@ -40,42 +44,49 @@ namespace spot
/// (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.
///
/// \param aut automaton to be transformed
/// \param output_bdd conjunction of all output AP, all APs not present
/// are treated as inputs
/// \param complete_env Whether the automaton should be complete for the
/// environment, i.e. the player of I
/// \note: This function also computes the state players
/// \note: If the automaton is to be completed for both env and player
/// then egdes between the sinks will be added
/// \note This function also computes the state players
/// \note 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
SPOT_API twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut,
const bdd& output_bdd, bool complete_env);
/// \ingroup synthesis
/// \brief 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
///
/// 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
///
/// \param aut automaton to be transformed
/// \param output_bdd conjunction of all output AP, all APs not present
/// are treated as inputs
/// @{
SPOT_API void
split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd);
SPOT_API twa_graph_ptr
split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd);
/// @}
/// \ingroup synthesis
/// \brief the reverse of split_2step
///
/// \note: This function relies on the named property "state-player"
/// \note This function relies on the named property "state-player"
SPOT_API twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut);
/// \ingroup synthesis
/// \brief Creates a game from a specification and a set of
/// output propositions
///
@ -89,22 +100,26 @@ namespace spot
const std::vector<std::string>& all_outs,
game_info& gi);
/// \ingroup synthesis
/// \brief create_game called with default options
SPOT_API twa_graph_ptr
create_game(const formula& f,
const std::vector<std::string>& all_outs);
/// \ingroup synthesis
/// \brief Like create_game but formula given as string
SPOT_API twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs,
game_info& gi);
/// \ingroup synthesis
/// \brief create_game called with default options
SPOT_API twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs);
/// \ingroup synthesis
/// \brief Takes a solved game and restricts the automaton to the
/// winning strategy of the player
///
@ -117,6 +132,7 @@ namespace spot
apply_strategy(const spot::twa_graph_ptr& arena,
bool unsplit, bool keep_acc);
/// \ingroup synthesis
/// \brief Minimizes a strategy. Strategies are infact
/// Mealy machines. So we can use techniques designed for them
///
@ -130,24 +146,25 @@ namespace spot
/// 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
/// @{
SPOT_API void
minimize_strategy_here(twa_graph_ptr& strat, int min_lvl);
///\brief Like minimize_strategy_here
SPOT_API twa_graph_ptr
minimize_strategy(const_twa_graph_ptr& strat, int min_lvl);
/// @}
/// \ingroup synthesis
/// \brief creates a strategy from a solved game taking into account the
/// options given in gi
/// options given in \a gi
/// @{
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena, game_info& gi);
/// \brief Like create_strategy but with default options
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena);
/// @}
/// \ingroup synthesis
/// \brief A struct that represents different types of strategy like
/// objects
struct SPOT_API
@ -162,24 +179,28 @@ namespace spot
bdd glob_cond;
};
/// \ingroup synthesis
/// \brief Seeks to decompose a formula into independently synthesizable
/// sub-parts. The conjunction of all sub-parts then
/// satisfies the specification
///
/// The algorithm is largely based on \cite{finkbeiner2021specification}.
/// The algorithm is based on work by Finkbeiner et al.
/// \cite finkbeiner.21.nfm, \cite finkbeiner.21.arxiv.
///
/// \param f the formula to split
/// \param outs vector with the names of all output propositions
/// \return A vector of pairs holding a subformula and the used output
/// propositions each.
/// @{
SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
split_independant_formulas(formula f, const std::vector<std::string>& outs);
/// \brief Like split_independant_formulas but the formula given as string
SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
split_independant_formulas(const std::string& f,
const std::vector<std::string>& outs);
/// @}
/// \ingroup synthesis
/// \brief Creates a strategy for the formula given by calling all
/// intermediate steps
///
@ -187,6 +208,7 @@ namespace spot
/// 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.
///
/// \param f The formula to synthesize a strategy for
/// \param output_aps A vector with the name of all output properties.
/// All APs not named in this vector are treated as inputs
@ -195,4 +217,4 @@ namespace spot
const std::vector<std::string>& output_aps,
game_info& gi);
}
}