spot 2.11.6.dev
Loading...
Searching...
No Matches
randomltl.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2010-2016, 2018 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
33namespace spot
34{
37 class SPOT_API random_formula
38 {
39 public:
40 random_formula(unsigned proba_size,
41 const atomic_prop_set* ap):
42 proba_size_(proba_size), proba_(new op_proba[proba_size_]), ap_(ap)
43 {
44 }
45
46 virtual ~random_formula()
47 {
48 delete[] proba_;
49 }
50
52 const atomic_prop_set*
53 ap() const
54 {
55 return ap_;
56 }
57
64 formula generate(int n) const;
65
68 std::ostream& dump_priorities(std::ostream& os) const;
69
77 const char* parse_options(char* options);
78
79 protected:
80 void update_sums();
81
82 struct op_proba
83 {
84 const char* name;
85 int min_n;
86 double proba;
87 typedef formula (*builder)(const random_formula* rl, int n);
88 builder build;
89 void setup(const char* name, int min_n, builder build);
90 };
91 unsigned proba_size_;
92 op_proba* proba_;
93 double total_1_;
94 op_proba* proba_2_;
95 double total_2_;
96 op_proba* proba_2_or_more_;
97 double total_2_and_more_;
98 const atomic_prop_set* ap_;
99 };
100
101
114 class SPOT_API random_ltl: public random_formula
115 {
116 public:
121
149
150 protected:
151 void setup_proba_();
152 random_ltl(int size, const atomic_prop_set* ap);
153 };
154
164 class SPOT_API random_boolean final: public random_formula
165 {
166 public:
172
193 };
194
204 class SPOT_API random_sere final: public random_formula
205 {
206 public:
211
234
236 };
237
245 class SPOT_API random_psl: public random_ltl
246 {
247 public:
256
291
294 };
295
296 class SPOT_API randltlgenerator
297 {
298 typedef std::unordered_set<formula> fset_t;
299
300
301 public:
302 enum output_type { Bool, LTL, SERE, PSL };
303 static constexpr unsigned MAX_TRIALS = 100000U;
304
305 randltlgenerator(int aprops_n, const option_map& opts,
306 char* opt_pL = nullptr,
307 char* opt_pS = nullptr,
308 char* opt_pB = nullptr);
309
310 randltlgenerator(atomic_prop_set aprops, const option_map& opts,
311 char* opt_pL = nullptr,
312 char* opt_pS = nullptr,
313 char* opt_pB = nullptr);
314
316
317 formula next();
318
319 void dump_ltl_priorities(std::ostream& os);
320 void dump_bool_priorities(std::ostream& os);
321 void dump_psl_priorities(std::ostream& os);
322 void dump_sere_priorities(std::ostream& os);
323 void dump_sere_bool_priorities(std::ostream& os);
324 void remove_some_props(atomic_prop_set& s);
325
326 formula GF_n();
327
328 private:
329 fset_t unique_set_;
330 atomic_prop_set aprops_;
331
332 int opt_seed_;
333 int opt_tree_size_min_;
334 int opt_tree_size_max_;
335 bool opt_unique_;
336 bool opt_wf_;
337 int opt_simpl_level_;
338 tl_simplifier simpl_;
339
340 int output_;
341
342 random_formula* rf_ = nullptr;
343 random_psl* rp_ = nullptr;
344 random_sere* rs_ = nullptr;
345 };
346}
Main class for temporal logic formula.
Definition formula.hh:728
Manage a map of options.
Definition optionmap.hh:38
Definition randomltl.hh:297
Generate random Boolean formulae.
Definition randomltl.hh:165
random_boolean(const atomic_prop_set *ap)
Base class for random formula generators.
Definition randomltl.hh:38
std::ostream & dump_priorities(std::ostream &os) const
Print the priorities of each operator, constants, and atomic propositions.
const char * parse_options(char *options)
Update the priorities used to generate the formulae.
formula generate(int n) const
Generate a formula of size n.
const atomic_prop_set * ap() const
Return the set of atomic proposition used to build formulae.
Definition randomltl.hh:53
Generate random LTL formulae.
Definition randomltl.hh:115
random_ltl(const atomic_prop_set *ap)
Generate random PSL formulae.
Definition randomltl.hh:246
random_sere rs
The SERE generator used to generate SERE subformulae.
Definition randomltl.hh:293
random_psl(const atomic_prop_set *ap)
Generate random SERE.
Definition randomltl.hh:205
random_sere(const atomic_prop_set *ap)
Rewrite or simplify f in various ways.
Definition simplify.hh:110
@ ap
Atomic proposition.
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition apcollect.hh:36
Definition automata.hh:27
Definition randomltl.hh:83

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