spot 2.11.6.dev
Loading...
Searching...
No Matches
synthesis.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2020-2022 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 <spot/twaalgos/relabel.hh>
25#include <bddx.h>
26
27namespace spot
28{
31
58 SPOT_API twa_graph_ptr
59 split_2step(const const_twa_graph_ptr& aut,
60 const bdd& output_bdd, bool complete_env = true);
61
65 SPOT_API twa_graph_ptr
66 split_2step(const const_twa_graph_ptr& aut, bool complete_env = true);
67
76 SPOT_API twa_graph_ptr
77 unsplit_2step(const const_twa_graph_ptr& aut);
78
81 struct SPOT_API synthesis_info
82 {
83 enum class algo
84 {
85 DET_SPLIT=0,
86 SPLIT_DET,
87 DPA_SPLIT,
88 LAR,
89 LAR_OLD,
90 ACD,
91 };
92
93 struct bench_var
94 {
95 double total_time = 0.0;
96 double trans_time = 0.0;
97 double split_time = 0.0;
98 double paritize_time = 0.0;
99 double solve_time = 0.0;
100 double strat2aut_time = 0.0;
101 double simplify_strat_time = 0.0;
102 double aig_time = 0.0;
103 unsigned nb_states_arena = 0;
104 unsigned nb_states_arena_env = 0;
105 unsigned nb_strat_states = 0;
106 unsigned nb_strat_edges = 0;
107 unsigned nb_simpl_strat_states = 0;
108 unsigned nb_simpl_strat_edges = 0;
109 unsigned nb_latches = 0;
110 unsigned nb_gates = 0;
111 bool realizable = false;
112 };
113
115 : force_sbacc{false},
116 s{algo::LAR},
117 minimize_lvl{2},
118 bv{},
119 verbose_stream{nullptr},
120 dict(make_bdd_dict())
121 {
122 }
123
124 bool force_sbacc;
125 algo s;
126 int minimize_lvl;
127 std::optional<bench_var> bv;
128 std::ostream* verbose_stream;
129 option_map opt;
130 bdd_dict_ptr dict;
131 };
132
135 SPOT_API std::ostream&
136 operator<<(std::ostream& os, synthesis_info::algo s);
137
140 SPOT_API std::ostream &
141 operator<<(std::ostream &os, const synthesis_info &gi);
142
143
155 SPOT_API twa_graph_ptr
157 const std::vector<std::string>& all_outs,
158 synthesis_info& gi);
159 SPOT_API twa_graph_ptr
161 const std::vector<std::string>& all_outs);
162 SPOT_API twa_graph_ptr
163 ltl_to_game(const std::string& f,
164 const std::vector<std::string>& all_outs,
165 synthesis_info& gi);
166 SPOT_API twa_graph_ptr
167 ltl_to_game(const std::string& f,
168 const std::vector<std::string>& all_outs);
170
179 SPOT_API twa_graph_ptr
180 solved_game_to_mealy(twa_graph_ptr arena, synthesis_info& gi);
181 SPOT_API twa_graph_ptr
182 solved_game_to_mealy(twa_graph_ptr arena);
183 SPOT_API twa_graph_ptr
185 SPOT_API twa_graph_ptr
186 solved_game_to_separated_mealy(twa_graph_ptr arena);
187 SPOT_API twa_graph_ptr
189 SPOT_API twa_graph_ptr
190 solved_game_to_split_mealy(twa_graph_ptr arena);
192
196 struct SPOT_API mealy_like
197 {
198 enum class realizability_code
199 {
200 UNREALIZABLE,
201 UNKNOWN,
202 REALIZABLE_REGULAR,
203 // strat is DTGBA and a glob_cond
204 REALIZABLE_DTGBA
205 };
206
207 realizability_code success;
208 twa_graph_ptr mealy_like;
209 bdd glob_cond;
210 };
211
225 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
226 split_independant_formulas(formula f, const std::vector<std::string>& outs);
227
228 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
229 split_independant_formulas(const std::string& f,
230 const std::vector<std::string>& outs);
232
247 SPOT_API mealy_like
249 const std::vector<std::string>& output_aps,
250 synthesis_info& gi, bool want_strategy = false);
251
257 SPOT_API bool
258 solve_game(twa_graph_ptr arena, synthesis_info& gi);
259
260 struct SPOT_API game_relabeling_map
261 {
262 relabeling_map env_map;
263 relabeling_map player_map;
264 };
265
278 SPOT_API game_relabeling_map
279 partitioned_game_relabel_here(twa_graph_ptr& arena,
280 bool relabel_env,
281 bool relabel_play,
282 bool split_env = false,
283 bool split_play = false,
284 unsigned max_letter = -1u,
285 unsigned max_letter_mult = -1u);
286
291 SPOT_API void
292 relabel_game_here(twa_graph_ptr& arena,
293 game_relabeling_map& rel_maps);
294
295}
Main class for temporal logic formula.
Definition formula.hh:733
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_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....
twa_graph_ptr 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
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 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....
twa_graph_ptr unsplit_2step(const const_twa_graph_ptr &aut)
the inverse of split_2step
game_relabeling_map 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 dependi...
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.
mealy_like 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.
twa_graph_ptr 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....
void 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...
Definition automata.hh:27
Definition synthesis.hh:261
A struct that represents different types of mealy like objects.
Definition synthesis.hh:197
Definition synthesis.hh:94
Benchmarking data and options for synthesis.
Definition synthesis.hh:82

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