spot
2.11.6
|
Generate random PSL formulae. More...
#include <spot/tl/randomltl.hh>
Public Member Functions | |
random_psl (const atomic_prop_set *ap) | |
const atomic_prop_set * | ap () const |
Return the set of atomic proposition used to build formulae. More... | |
formula | generate (int n) const |
Generate a formula of size n. More... | |
std::ostream & | dump_priorities (std::ostream &os) const |
Print the priorities of each operator, constants, and atomic propositions. More... | |
const char * | parse_options (char *options) |
Update the priorities used to generate the formulae. More... | |
Public Attributes | |
random_sere | rs |
The SERE generator used to generate SERE subformulae. More... | |
Protected Member Functions | |
void | setup_proba_ () |
void | update_sums () |
Protected Attributes | |
unsigned | proba_size_ |
op_proba * | proba_ |
double | total_1_ |
op_proba * | proba_2_ |
double | total_2_ |
op_proba * | proba_2_or_more_ |
double | total_2_and_more_ |
const atomic_prop_set * | ap_ |
Generate random PSL formulae.
This class recursively constructs PSL formulae of a given size. The formulae will use the use atomic propositions from the set of propositions passed to the constructor, in addition to the constant and all PSL operators supported by Spot.
spot::random_psl::random_psl | ( | const atomic_prop_set * | ap | ) |
Create a random PSL generator using atomic propositions from ap.
PSL formulae are built by combining LTL operators, plus three operators (EConcat, UConcat, Closure) taking a SERE as parameter.
The default priorities are defined as follows:
ap n false 1 true 1 not 1 F 1 G 1 X 1 Closure 1 equiv 1 implies 1 xor 1 R 1 U 1 W 1 M 1 and 1 or 1 EConcat 1 UConcat 1
Where n
is the number of atomic propositions in the set passed to the constructor.
This means that each operator has equal chance to be selected. Also, each atomic proposition has as much chance as each constant (i.e., true and false) to be picked.
These priorities can be changed use the parse_options method.
In addition, you can set the properties of the SERE generator used to build SERE subformulae using the parse_options method of the rs
attribute.
|
inlineinherited |
Return the set of atomic proposition used to build formulae.
|
inherited |
Print the priorities of each operator, constants, and atomic propositions.
|
inherited |
Generate a formula of size n.
It is possible to obtain formulae that are smaller than n, because some simple simplifications are performed by the AST. (For instance the formula a | a
is automatically reduced to a
by spot::multop.)
|
inherited |
Update the priorities used to generate the formulae.
options should be comma-separated list of KEY=VALUE assignments, using keys from the above list. For instance "xor=0, F=3"
will prevent xor
from being used, and will raise the relative probability of occurrences of the F
operator.
random_sere spot::random_psl::rs |
The SERE generator used to generate SERE subformulae.