spot 2.13.1.dev
Loading...
Searching...
No Matches
ltlf2dfa.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3//
4// This file is part of Spot, a model checking library.
5//
6// Spot is free software; you can redistribute it and/or modify it
7// under the terms of the GNU General Public License as published by
8// the Free Software Foundation; either version 3 of the License, or
9// (at your option) any later version.
10//
11// Spot is distributed in the hope that it will be useful, but WITHOUT
12// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14// License for more details.
15//
16// You should have received a copy of the GNU General Public License
17// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19#pragma once
20
21#include <spot/twa/twagraph.hh>
22#include <spot/misc/bddlt.hh>
23#include <spot/twaalgos/backprop.hh>
24
25namespace spot
26{
38
43 struct SPOT_API mtdfa_stats
44 {
49 unsigned states;
50
56 unsigned aps;
57
61 unsigned nodes;
62
68 unsigned terminals;
69
77
82 unsigned long long paths;
83
87 unsigned long long edges;
88 };
89
105 struct SPOT_API mtdfa: public std::enable_shared_from_this<mtdfa>
106
107 {
108 public:
113 mtdfa(const bdd_dict_ptr& dict) noexcept
114 : dict_(dict)
115 {
116 }
117
118 ~mtdfa()
119 {
120 dict_->unregister_all_my_variables(this);
121 }
122
123 std::vector<bdd> states;
124 std::vector<formula> names;
134 std::vector<formula> aps;
135
140 unsigned num_roots() const
141 {
142 return states.size();
143 }
144
150 unsigned num_states() const
151 {
152 return states.size() + bdd_has_true(states);
153 }
154
155 // This assumes that all states are reachable, so we just have to
156 // check if one terminal is accepting.
157 bool is_empty() const;
158
167 std::ostream& print_dot(std::ostream& os,
168 int index = -1,
169 bool labels = true) const;
170
188 twa_graph_ptr as_twa(bool state_based = false, bool labels = true) const;
189
203 mtdfa_stats get_stats(bool nodes, bool paths) const;
204
206 bdd_dict_ptr get_dict() const
207 {
208 return dict_;
209 }
210
223 void set_controllable_variables(const std::vector<std::string>& vars,
224 bool ignore_non_registered_ap = false);
227
230 {
231 return controllable_variables_;
232 }
233
234 private:
235 bdd_dict_ptr dict_;
236 bdd controllable_variables_ = bddtrue;
237 };
238
239 typedef std::shared_ptr<mtdfa> mtdfa_ptr;
240 typedef std::shared_ptr<const mtdfa> const_mtdfa_ptr;
241
266 SPOT_API mtdfa_ptr
267 ltlf_to_mtdfa(formula f, const bdd_dict_ptr& dict,
268 bool fuse_same_bdds = true,
269 bool simplify_terms = true,
270 bool detect_empty_univ = true);
271
272
273 enum ltlf_synthesis_backprop {
274 state_refine, // no backpropagation, just local refinement
275 bfs_node_backprop, // on-the-fly
276 dfs_node_backprop, // on-the-fly
277 };
278
311 SPOT_API mtdfa_ptr
312 ltlf_to_mtdfa_for_synthesis(formula f, const bdd_dict_ptr& dict,
313 const std::vector<std::string>& outvars,
314 ltlf_synthesis_backprop backprop
315 = dfs_node_backprop,
316 bool one_step_preprocess = false,
317 bool realizability = false,
318 bool fuse_same_bdds = true,
319 bool simplify_terms = true,
320 bool detect_empty_univ = true);
321
353 SPOT_API mtdfa_ptr
354 ltlf_to_mtdfa_compose(formula f, const bdd_dict_ptr& dict,
355 bool minimize = true, bool order_for_aps = true,
356 bool want_names = true,
357 bool fuse_same_bdds = true,
358 bool simplify_terms = true);
359
380 SPOT_API mtdfa_ptr minimize_mtdfa(const mtdfa_ptr& dfa);
381
384 SPOT_API mtdfa_ptr product(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
385
388 SPOT_API mtdfa_ptr product_or(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
389
395 SPOT_API mtdfa_ptr product_xor(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
396
403 SPOT_API mtdfa_ptr product_xnor(const mtdfa_ptr& dfa1, const mtdfa_ptr& dfa2);
404
410 SPOT_API mtdfa_ptr product_implies(const mtdfa_ptr& dfa1,
411 const mtdfa_ptr& dfa2);
412
415 SPOT_API mtdfa_ptr complement(const mtdfa_ptr& dfa);
416
419 SPOT_API mtdfa_ptr twadfa_to_mtdfa(const twa_graph_ptr& twa);
420
421
428 class SPOT_API ltlf_translator
429 {
430 public:
431 ltlf_translator(const bdd_dict_ptr& dict,
432 bool simplify_terms = true);
433
434 mtdfa_ptr ltlf_to_mtdfa(formula f, bool fuse_same_bdds,
435 bool detect_empty_univ = true,
436 const std::vector<std::string>* outvars = nullptr,
437 bool do_backprop = false,
438 bool realizability = false,
439 bool one_step_preprocess = false);
440
441 mtdfa_ptr ltlf_synthesis_with_dfs(formula f,
442 const std::vector<std::string>*
443 outvars = nullptr,
444 bool realizability = false,
445 bool ont_step_preprocess = false);
446
447 bdd ltlf_to_mtbdd(formula f);
448 std::pair<formula, bool> leaf_to_formula(int b, int term) const;
449
450 formula terminal_to_formula(int t) const;
451 int formula_to_int(formula f);
452 int formula_to_terminal(formula f, bool may_stop = false);
453 bdd formula_to_terminal_bdd(formula f, bool may_stop = false);
454 int formula_to_terminal_bdd_as_int(formula f, bool may_stop = false);
455
456 bdd combine_and(bdd left, bdd right);
457 bdd combine_or(bdd left, bdd right);
458 bdd combine_implies(bdd left, bdd right);
459 bdd combine_equiv(bdd left, bdd right);
460 bdd combine_xor(bdd left, bdd right);
461 bdd combine_not(bdd b);
462
463 formula propeq_representative(formula f);
464
465 bddExtCache* get_cache()
466 {
467 return &cache_;
468 }
469
471 private:
472 std::unordered_map<formula, int> formula_to_var_;
473 std::unordered_map<bdd, formula, bdd_hash> propositional_equiv_;
474
475 std::unordered_map<formula, bdd> formula_to_bdd_;
476 std::unordered_map<formula, int> formula_to_int_;
477 std::vector<formula> int_to_formula_;
478 bdd_dict_ptr dict_;
479 bddExtCache cache_;
480 bool simplify_terms_;
481 };
482
496 SPOT_API std::vector<bool>
497 mtdfa_winning_region(mtdfa_ptr dfa);
498
505 SPOT_API std::vector<bool>
507
508 #include <spot/graph/adjlist.hh>
509
510
519 SPOT_API mtdfa_ptr mtdfa_restrict_as_game(mtdfa_ptr dfa);
520 SPOT_API mtdfa_ptr
522 const std::vector<bool>& winning_states);
524
525
540 SPOT_API backprop_graph
541 mtdfa_to_backprop(mtdfa_ptr dfa, bool early_stop = true,
542 bool preserve_names = false);
543
559 SPOT_API mtdfa_ptr
560 mtdfa_winning_strategy(mtdfa_ptr dfa, bool backprop_nodes);
561
569 SPOT_API twa_graph_ptr
570 mtdfa_strategy_to_mealy(mtdfa_ptr strategy, bool labels = true);
571}
Definition backprop.hh:31
Main class for temporal logic formula.
Definition formula.hh:786
"Semi-internal" class used to implement spot::ltlf_to_mtdfa()
Definition ltlf2dfa.hh:429
A Transition-based ω-Automaton.
Definition twa.hh:619
mtdfa_ptr product_or(const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
Combine two MTDFAs to sum their languages.
mtdfa_ptr twadfa_to_mtdfa(const twa_graph_ptr &twa)
Convert a TWA (representing a DFA) into an MTDFA.
mtdfa_ptr product_xor(const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
Combine two MTDFAs to build the exclusive sum of their languages.
twa_graph_ptr mtdfa_strategy_to_mealy(mtdfa_ptr strategy, bool labels=true)
Convert an MTDFA representing a strategy to a TwA with the "synthesis-output" property.
mtdfa_ptr product_xnor(const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
Combine two MTDFAs to keep words that are handled similarly in both operands.
mtdfa_ptr ltlf_to_mtdfa_compose(formula f, const bdd_dict_ptr &dict, bool minimize=true, bool order_for_aps=true, bool want_names=true, bool fuse_same_bdds=true, bool simplify_terms=true)
Convert an LTLf formula into a MTDFA, with a compositional approach.
mtdfa_ptr ltlf_to_mtdfa(formula f, const bdd_dict_ptr &dict, bool fuse_same_bdds=true, bool simplify_terms=true, bool detect_empty_univ=true)
Convert an LTLf formula into a MTDFA.
std::vector< bool > mtdfa_winning_region(mtdfa_ptr dfa)
Compute the winning region of the MTDFA interpreted as a game.
mtdfa_ptr minimize_mtdfa(const mtdfa_ptr &dfa)
Minimize a MTDFA.
mtdfa_ptr ltlf_to_mtdfa_for_synthesis(formula f, const bdd_dict_ptr &dict, const std::vector< std::string > &outvars, ltlf_synthesis_backprop backprop=dfs_node_backprop, bool one_step_preprocess=false, bool realizability=false, bool fuse_same_bdds=true, bool simplify_terms=true, bool detect_empty_univ=true)
Solve (or start solving) LTLf synthesis.
mtdfa_ptr mtdfa_winning_strategy(mtdfa_ptr dfa, bool backprop_nodes)
Compute a strategy for an MTDFA interpreted as a game.
mtdfa_ptr mtdfa_restrict_as_game(mtdfa_ptr dfa)
Build a generalized strategy from a set of winning states.
backprop_graph mtdfa_to_backprop(mtdfa_ptr dfa, bool early_stop=true, bool preserve_names=false)
Build a backprop_graph from dfa.
mtdfa_ptr product_implies(const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
Combine two MTDFAs to build an implication.
Definition automata.hh:26
std::vector< bool > mtdfa_winning_region_lazy(mtdfa_ptr dfa)
Compute the winning region of the MTDFA interpreted as a game. Lazy version.
twa_graph_ptr complement(const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr)
Complement a TωA.
statistics about an mtdfa instance
Definition ltlf2dfa.hh:44
unsigned nodes
Number of internal nodes (or decision nodes)
Definition ltlf2dfa.hh:61
unsigned long long paths
Number of paths between a root and a leaf (terminal or constant)
Definition ltlf2dfa.hh:82
unsigned terminals
Number of terminal nodes.
Definition ltlf2dfa.hh:68
unsigned aps
number of atomic propositions
Definition ltlf2dfa.hh:56
bool has_false
Whether the true and false constants are used.
Definition ltlf2dfa.hh:75
bool has_true
Whether the true and false constants are used.
Definition ltlf2dfa.hh:74
unsigned states
number of roots
Definition ltlf2dfa.hh:49
unsigned long long edges
Number of pairs (root, leaf) for which a path exists.
Definition ltlf2dfa.hh:87
a DFA represented using shared multi-terminal BDDs
Definition ltlf2dfa.hh:107
unsigned num_states() const
The number of states in the automaton.
Definition ltlf2dfa.hh:150
twa_graph_ptr as_twa(bool state_based=false, bool labels=true) const
Convert this automaton to a spot::twa_graph.
void set_controllable_variables(const std::vector< std::string > &vars, bool ignore_non_registered_ap=false)
declare a list of controllable variables
bdd_dict_ptr get_dict() const
get the bdd_dict associated to this automaton
Definition ltlf2dfa.hh:206
std::vector< formula > aps
The list of atomic propositions possibly used by the automaton.
Definition ltlf2dfa.hh:134
void set_controllable_variables(bdd vars)
declare a list of controllable variables
mtdfa_stats get_stats(bool nodes, bool paths) const
compute some statistics about the automaton
bdd get_controllable_variables() const
Returns the conjunction of controllable variables.
Definition ltlf2dfa.hh:229
unsigned num_roots() const
the number of MTBDDs roots
Definition ltlf2dfa.hh:140
std::ostream & print_dot(std::ostream &os, int index=-1, bool labels=true) const
Print the states array of MTBDD in graphviz format.
mtdfa(const bdd_dict_ptr &dict) noexcept
create an empty mtdfa
Definition ltlf2dfa.hh:113

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