spot  2.10.1
synthesis.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2020-2021 Laboratoire de Recherche et
3 // Développement de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <spot/twa/twagraph.hh>
23 #include <spot/twaalgos/game.hh>
24 #include <bddx.h>
25 
26 namespace spot
27 {
30 
57  SPOT_API twa_graph_ptr
58  split_2step(const const_twa_graph_ptr& aut,
59  const bdd& output_bdd, bool complete_env);
60 
69  SPOT_API twa_graph_ptr
70  unsplit_2step(const const_twa_graph_ptr& aut);
71 
74  struct SPOT_API synthesis_info
75  {
76  enum class algo
77  {
78  DET_SPLIT=0,
79  SPLIT_DET,
80  DPA_SPLIT,
81  LAR,
82  LAR_OLD,
83  };
84 
85  struct bench_var
86  {
87  double total_time = 0.0;
88  double trans_time = 0.0;
89  double split_time = 0.0;
90  double paritize_time = 0.0;
91  double solve_time = 0.0;
92  double strat2aut_time = 0.0;
93  double aig_time = 0.0;
94  unsigned nb_states_arena = 0;
95  unsigned nb_states_arena_env = 0;
96  unsigned nb_strat_states = 0;
97  unsigned nb_strat_edges = 0;
98  unsigned nb_latches = 0;
99  unsigned nb_gates = 0;
100  bool realizable = false;
101  };
102 
104  : force_sbacc{false},
105  s{algo::LAR},
106  minimize_lvl{2},
107  bv{},
108  verbose_stream{nullptr},
109  dict(make_bdd_dict())
110  {
111  }
112 
113  bool force_sbacc;
114  algo s;
115  int minimize_lvl;
116  std::optional<bench_var> bv;
117  std::ostream* verbose_stream;
118  option_map opt;
119  bdd_dict_ptr dict;
120  };
121 
124  SPOT_API std::ostream&
125  operator<<(std::ostream& os, synthesis_info::algo s);
126 
129  SPOT_API std::ostream &
130  operator<<(std::ostream &os, const synthesis_info &gi);
131 
132 
144  SPOT_API twa_graph_ptr
146  const std::vector<std::string>& all_outs,
147  synthesis_info& gi);
148  SPOT_API twa_graph_ptr
150  const std::vector<std::string>& all_outs);
151  SPOT_API twa_graph_ptr
152  ltl_to_game(const std::string& f,
153  const std::vector<std::string>& all_outs,
154  synthesis_info& gi);
155  SPOT_API twa_graph_ptr
156  ltl_to_game(const std::string& f,
157  const std::vector<std::string>& all_outs);
159 
166  SPOT_API twa_graph_ptr
168  SPOT_API twa_graph_ptr
169  solved_game_to_separated_mealy(twa_graph_ptr arena);
171 
175  struct SPOT_API mealy_like
176  {
177  enum class realizability_code
178  {
179  UNREALIZABLE,
180  UNKNOWN,
181  REALIZABLE_REGULAR,
182  // strat is DTGBA and a glob_cond
183  REALIZABLE_DTGBA
184  };
185 
186  realizability_code success;
187  twa_graph_ptr mealy_like;
188  bdd glob_cond;
189  };
190 
204  SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
205  split_independant_formulas(formula f, const std::vector<std::string>& outs);
206 
207  SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
208  split_independant_formulas(const std::string& f,
209  const std::vector<std::string>& outs);
211 
224  SPOT_API mealy_like
226  const std::vector<std::string>& output_aps,
227  synthesis_info& gi);
228 
234  SPOT_API bool
235  solve_game(twa_graph_ptr arena, synthesis_info& gi);
236 
237 }
Main class for temporal logic formula.
Definition: formula.hh:715
Manage a map of options.
Definition: optionmap.hh:38
bool solve_game(const twa_graph_ptr &arena)
Generic interface for game solving.
twa_graph_ptr 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....
twa_graph_ptr unsplit_2step(const const_twa_graph_ptr &aut)
the inverse of split_2step
twa_graph_ptr 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.
std::pair< std::vector< formula >, std::vector< std::set< formula > > > 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-p...
twa_graph_ptr 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
mealy_like 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.
Definition: automata.hh:27
A struct that represents different types of mealy like objects.
Definition: synthesis.hh:176
Definition: synthesis.hh:86
Benchmarking data and options for synthesis.
Definition: synthesis.hh:75

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