diff --git a/doc/spot.bib b/doc/spot.bib index a706056db..ae5e120b0 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -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, diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 846bc6fdb..06bc77b48 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -43,6 +43,7 @@ namespace spot typedef std::shared_ptr aig_ptr; typedef std::shared_ptr 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& ins, + const std::vector& 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& 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& ins, - const std::vector& 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& strat_vec, const char* mode, const std::vector& ins, const std::vector>& outs); - - /// \brief Like above, but works on strategy_like elements SPOT_API aig_ptr strategies_to_aig(const std::vector& strat_vec, const char* mode, const std::vector& ins, const std::vector>& 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); diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index 558349534..9f3530f12 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -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 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 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); diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index b641fc851..a540cfc11 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -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& 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& 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& 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& 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>> split_independant_formulas(formula f, const std::vector& outs); - /// \brief Like split_independant_formulas but the formula given as string SPOT_API std::pair, std::vector>> split_independant_formulas(const std::string& f, const std::vector& 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& output_aps, game_info& gi); -} \ No newline at end of file +}