spot 2.12.0.dev
Loading...
Searching...
No Matches
randomltl.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/tl/apcollect.hh>
22#include <iosfwd>
23
24#include <unordered_set>
25#include <spot/misc/optionmap.hh>
26#include <spot/misc/hash.hh>
27#include <spot/tl/simplify.hh>
28
29namespace spot
30{
33 class SPOT_API random_formula
34 {
35 public:
36 random_formula(unsigned proba_size,
37 const atomic_prop_set* ap):
38 proba_size_(proba_size), proba_(new op_proba[proba_size_]), ap_(ap)
39 {
40 }
41
42 virtual ~random_formula()
43 {
44 delete[] proba_;
45 }
46
48 const atomic_prop_set* ap() const
49 {
50 return ap_;
51 }
52
55 {
56 return patterns_;
57 }
58
60 bool draw_literals() const
61 {
62 return draw_literals_;
63 }
64
66 void draw_literals(bool lit)
67 {
68 draw_literals_ = lit;
69 }
70
77 formula generate(int n) const;
78
81 std::ostream& dump_priorities(std::ostream& os) const;
82
90 const char* parse_options(char* options);
91
93 bool has_unary_ops() const
94 {
95 return total_2_ > 0.0;
96 }
97
98 protected:
99 void update_sums();
100
101 struct op_proba
102 {
103 const char* name;
104 int min_n;
105 double proba;
106 typedef formula (*builder)(const random_formula* rl, int n);
107 builder build;
108 void setup(const char* name, int min_n, builder build);
109 };
110 unsigned proba_size_;
111 op_proba* proba_;
112 double total_1_;
113 op_proba* proba_2_;
114 double total_2_;
115 op_proba* proba_2_or_more_;
116 double total_2_and_more_;
117 const atomic_prop_set* ap_;
118 const atomic_prop_set* patterns_ = nullptr;
119 bool draw_literals_;
120 };
121
122
135 class SPOT_API random_ltl: public random_formula
136 {
137 public:
143
177 const atomic_prop_set* subformulas = nullptr);
178
179 protected:
180 void setup_proba_(const atomic_prop_set* patterns);
181 random_ltl(int size, const atomic_prop_set* ap);
182 };
183
193 class SPOT_API random_boolean final: public random_formula
194 {
195 public:
202
228 const atomic_prop_set* subformulas = nullptr);
229 };
230
240 class SPOT_API random_sere final: public random_formula
241 {
242 public:
247
270
272 };
273
281 class SPOT_API random_psl: public random_ltl
282 {
283 public:
292
327
330 };
331
332 class SPOT_API randltlgenerator
333 {
334 typedef std::unordered_set<formula> fset_t;
335
336
337 public:
338 enum output_type { Bool, LTL, SERE, PSL };
339 static constexpr unsigned MAX_TRIALS = 100000U;
340
341 randltlgenerator(int aprops_n, const option_map& opts,
342 char* opt_pL = nullptr,
343 char* opt_pS = nullptr,
344 char* opt_pB = nullptr,
345 const atomic_prop_set* subformulas = nullptr);
346
347 randltlgenerator(atomic_prop_set aprops, const option_map& opts,
348 char* opt_pL = nullptr,
349 char* opt_pS = nullptr,
350 char* opt_pB = nullptr,
351 const atomic_prop_set* subformulas = nullptr);
352
354
355 formula next();
356
357 void dump_ltl_priorities(std::ostream& os);
358 void dump_bool_priorities(std::ostream& os);
359 void dump_psl_priorities(std::ostream& os);
360 void dump_sere_priorities(std::ostream& os);
361 void dump_sere_bool_priorities(std::ostream& os);
362 void remove_some_props(atomic_prop_set& s);
363
364 formula GF_n();
365
366 private:
367 fset_t unique_set_;
368 atomic_prop_set aprops_;
369
370 int opt_seed_;
371 int opt_tree_size_min_;
372 int opt_tree_size_max_;
373 bool opt_unique_;
374 bool opt_wf_;
375 int opt_simpl_level_;
376 tl_simplifier simpl_;
377
378 int output_;
379
380 random_formula* rf_ = nullptr;
381 random_psl* rp_ = nullptr;
382 random_sere* rs_ = nullptr;
383 };
384
385
386}
Main class for temporal logic formula.
Definition formula.hh:760
Manage a map of options.
Definition optionmap.hh:34
Definition randomltl.hh:333
Generate random Boolean formulas.
Definition randomltl.hh:194
random_boolean(const atomic_prop_set *ap, const atomic_prop_set *subformulas=nullptr)
Base class for random formula generators.
Definition randomltl.hh:34
std::ostream & dump_priorities(std::ostream &os) const
Print the priorities of each operator, constants, and atomic propositions.
bool draw_literals() const
Check whether relabeling APs should use literals.
Definition randomltl.hh:60
void draw_literals(bool lit)
Set whether relabeling APs should use literals.
Definition randomltl.hh:66
bool has_unary_ops() const
whether we can use unary operators
Definition randomltl.hh:93
const char * parse_options(char *options)
Update the priorities used to generate the formulas.
const atomic_prop_set * patterns() const
Return the set of patterns (sub-formulas) used to build formulas.
Definition randomltl.hh:54
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 formulas.
Definition randomltl.hh:48
Generate random LTL formulas.
Definition randomltl.hh:136
random_ltl(const atomic_prop_set *ap, const atomic_prop_set *subformulas=nullptr)
Generate random PSL formulas.
Definition randomltl.hh:282
random_sere rs
The SERE generator used to generate SERE subformulas.
Definition randomltl.hh:329
random_psl(const atomic_prop_set *ap)
Generate random SERE.
Definition randomltl.hh:241
random_sere(const atomic_prop_set *ap)
Rewrite or simplify f in various ways.
Definition simplify.hh:109
@ ap
Atomic proposition.
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition apcollect.hh:33
Definition automata.hh:26
Definition randomltl.hh:102

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