spot  2.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
randomltl.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
3 // Recherche et Développement de l'Epita (LRDE).
4 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
6 // et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // under the terms of the GNU General Public License as published by
12 // the Free Software Foundation; either version 3 of the License, or
13 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // You should have received a copy of the GNU General Public License
21 // along with this program. If not, see <http://www.gnu.org/licenses/>.
22 
23 #pragma once
24 
25 #include <spot/tl/apcollect.hh>
26 #include <iosfwd>
27 
28 #include <unordered_set>
29 #include <spot/misc/optionmap.hh>
30 #include <spot/misc/hash.hh>
31 #include <spot/tl/simplify.hh>
32 
33 #define OUTPUTBOOL 1
34 #define OUTPUTLTL 2
35 #define OUTPUTSERE 3
36 #define OUTPUTPSL 4
37 #define MAX_TRIALS 100000
38 
39 namespace spot
40 {
43  class SPOT_API random_formula
44  {
45  public:
46  random_formula(unsigned proba_size,
47  const atomic_prop_set* ap):
48  proba_size_(proba_size), proba_(new op_proba[proba_size_]), ap_(ap)
49  {
50  }
51 
52  virtual ~random_formula()
53  {
54  delete[] proba_;
55  }
56 
58  const atomic_prop_set*
59  ap() const
60  {
61  return ap_;
62  }
63 
70  formula generate(int n) const;
71 
74  std::ostream& dump_priorities(std::ostream& os) const;
75 
83  const char* parse_options(char* options);
84 
85  protected:
86  void update_sums();
87 
88  struct op_proba
89  {
90  const char* name;
91  int min_n;
92  double proba;
93  typedef formula (*builder)(const random_formula* rl, int n);
94  builder build;
95  void setup(const char* name, int min_n, builder build);
96  };
97  unsigned proba_size_;
98  op_proba* proba_;
99  double total_1_;
100  op_proba* proba_2_;
101  double total_2_;
102  op_proba* proba_2_or_more_;
103  double total_2_and_more_;
104  const atomic_prop_set* ap_;
105  };
106 
107 
120  class SPOT_API random_ltl: public random_formula
121  {
122  public:
127 
145  random_ltl(const atomic_prop_set* ap);
155 
156  protected:
157  void setup_proba_();
158  random_ltl(int size, const atomic_prop_set* ap);
159  };
160 
170  class SPOT_API random_boolean final: public random_formula
171  {
172  public:
178 
199  };
200 
210  class SPOT_API random_sere final: public random_formula
211  {
212  public:
217 
240 
241  random_boolean rb;
242  };
243 
251  class SPOT_API random_psl: public random_ltl
252  {
253  public:
262 
283  random_psl(const atomic_prop_set* ap);
297 
300  };
301 
302  class SPOT_API randltlgenerator
303  {
304  typedef std::unordered_set<formula> fset_t;
305 
306 
307  public:
308  randltlgenerator(int aprops_n, const option_map& opts,
309  char* opt_pL = nullptr,
310  char* opt_pS = nullptr,
311  char* opt_pB = nullptr);
312 
313  randltlgenerator(atomic_prop_set aprops, const option_map& opts,
314  char* opt_pL = nullptr,
315  char* opt_pS = nullptr,
316  char* opt_pB = nullptr);
317 
318  ~randltlgenerator();
319 
320  formula next();
321 
322  void dump_ltl_priorities(std::ostream& os);
323  void dump_bool_priorities(std::ostream& os);
324  void dump_psl_priorities(std::ostream& os);
325  void dump_sere_priorities(std::ostream& os);
326  void dump_sere_bool_priorities(std::ostream& os);
327  void remove_some_props(atomic_prop_set& s);
328 
329  formula GF_n();
330 
331  private:
332  fset_t unique_set_;
333  atomic_prop_set aprops_;
334 
335  int opt_seed_;
336  int opt_tree_size_min_;
337  int opt_tree_size_max_;
338  bool opt_unique_;
339  bool opt_wf_;
340  int opt_simpl_level_;
341  tl_simplifier simpl_;
342 
343  int output_;
344 
345  random_formula* rf_ = nullptr;
346  random_psl* rp_ = nullptr;
347  random_sere* rs_ = nullptr;
348  };
349 }
Definition: graph.hh:33
random_sere rs
The SERE generator used to generate SERE subformulae.
Definition: randomltl.hh:299
Manage a map of options.
Definition: optionmap.hh:37
Definition: randomltl.hh:302
Base class for random formula generators.
Definition: randomltl.hh:43
Main class for temporal logic formula.
Definition: formula.hh:669
Generate random Boolean formulae.
Definition: randomltl.hh:170
const atomic_prop_set * ap() const
Return the set of atomic proposition used to build formulae.
Definition: randomltl.hh:59
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:36
Definition: randomltl.hh:88
Generate random LTL formulae.
Definition: randomltl.hh:120
Generate random SERE.
Definition: randomltl.hh:210
Rewrite or simplify f in various ways.
Definition: simplify.hh:97
Atomic proposition.
Generate random PSL formulae.
Definition: randomltl.hh:251

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jan 19 2017 11:08:40 for spot by doxygen 1.8.8