spot  2.2.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
translate.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2013, 2014, 2015, 2016 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/twaalgos/postproc.hh>
23 #include <spot/tl/simplify.hh>
24 
25 namespace spot
26 {
47  class SPOT_API translator: protected postprocessor
48  {
49  public:
50  translator(tl_simplifier* simpl, const option_map* opt = nullptr)
51  : postprocessor(opt), simpl_(simpl), simpl_owned_(nullptr)
52  {
53  SPOT_ASSERT(simpl);
54  setup_opt(opt);
55  }
56 
57  translator(const bdd_dict_ptr& dict, const option_map* opt = nullptr)
58  : postprocessor(opt)
59  {
60  build_simplifier(dict);
61  setup_opt(opt);
62  }
63 
64  translator(const option_map* opt = nullptr)
65  : postprocessor(opt)
66  {
67  build_simplifier(make_bdd_dict());
68  setup_opt(opt);
69  }
70 
71  ~translator()
72  {
73  // simpl_owned_ is 0 if simpl_ was supplied to the constructor.
74  delete simpl_owned_;
75  }
76 
77  using postprocessor::output_type;
78 
79  void
80  set_type(output_type type)
81  {
82  this->postprocessor::set_type(type);
83  }
84 
85  using postprocessor::output_pref;
86 
87  void
88  set_pref(output_pref pref)
89  {
90  this->postprocessor::set_pref(pref);
91  }
92 
93  using postprocessor::optimization_level;
94 
95  void
96  set_level(optimization_level level)
97  {
98  level_ = level;
99  if (simpl_owned_)
100  {
101  auto d = simpl_owned_->get_dict();
102  delete simpl_owned_;
103  build_simplifier(d);
104  }
105  }
106 
110  twa_graph_ptr run(formula f);
111 
116  twa_graph_ptr run(formula* f);
117 
118  protected:
119  void setup_opt(const option_map* opt);
120  void build_simplifier(const bdd_dict_ptr& dict);
121 
122  private:
123  tl_simplifier* simpl_;
124  tl_simplifier* simpl_owned_;
125  int comp_susp_;
126  int early_susp_;
127  int skel_wdba_;
128  int skel_simul_;
129  };
131 }
Definition: graph.hh:32
Manage a map of options.
Definition: optionmap.hh:37
Main class for temporal logic formula.
Definition: formula.hh:669
void set_type(output_type type)
Select the desired output type.
Definition: postproc.hh:90
Translate an LTL formula into an optimized spot::tgba.
Definition: translate.hh:47
Rewrite or simplify f in various ways.
Definition: simplify.hh:97
void set_pref(output_pref pref)
Select the desired characteristics of the output automaton.
Definition: postproc.hh:136
Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface.
Definition: postproc.hh:63

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Nov 21 2016 08:26:36 for spot by doxygen 1.8.8