spot  2.11.6
Classes | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
spot::random_formula Class Reference

Base class for random formula generators. More...

#include <spot/tl/randomltl.hh>

Inheritance diagram for spot::random_formula:
Collaboration diagram for spot::random_formula:

Classes

struct  op_proba
 

Public Member Functions

 random_formula (unsigned proba_size, const atomic_prop_set *ap)
 
const atomic_prop_setap () 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...
 

Protected Member Functions

void update_sums ()
 

Protected Attributes

unsigned proba_size_
 
op_probaproba_
 
double total_1_
 
op_probaproba_2_
 
double total_2_
 
op_probaproba_2_or_more_
 
double total_2_and_more_
 
const atomic_prop_setap_
 

Detailed Description

Base class for random formula generators.

Member Function Documentation

◆ ap()

const atomic_prop_set* spot::random_formula::ap ( ) const
inline

Return the set of atomic proposition used to build formulae.

◆ dump_priorities()

std::ostream& spot::random_formula::dump_priorities ( std::ostream &  os) const

Print the priorities of each operator, constants, and atomic propositions.

◆ generate()

formula spot::random_formula::generate ( int  n) const

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.)

◆ parse_options()

const char* spot::random_formula::parse_options ( char *  options)

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.


The documentation for this class was generated from the following file:

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.1