spot  2.2.2
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Typedefs | Functions
Miscellaneous Algorithms for Formulas

Typedefs

typedef std::set< formula > spot::atomic_prop_set
 Set of atomic propositions. More...
 

Functions

atomic_prop_set spot::create_atomic_prop_set (unsigned n)
 construct an atomic_prop_set with n propositions More...
 
atomic_prop_set * spot::atomic_prop_collect (formula f, atomic_prop_set *s=nullptr)
 Return the set of atomic propositions occurring in a formula. More...
 
bdd spot::atomic_prop_collect_as_bdd (formula f, const twa_ptr &a)
 Return the set of atomic propositions occurring in a formula, as a BDD. More...
 
int spot::length (formula f)
 Compute the length of a formula. More...
 
int spot::length_boolone (formula f)
 Compute the length of a formula, squashing Boolean formulae. More...
 

Detailed Description

Typedef Documentation

typedef std::set<formula> spot::atomic_prop_set

#include <spot/tl/apcollect.hh>

Set of atomic propositions.

Function Documentation

atomic_prop_set* spot::atomic_prop_collect ( formula  f,
atomic_prop_set *  s = nullptr 
)

#include <spot/tl/apcollect.hh>

Return the set of atomic propositions occurring in a formula.

Parameters
fthe formula to inspect
san existing set to fill with atomic_propositions discovered, or 0 if the set should be allocated by the function.
Returns
A pointer to the supplied set, s, augmented with atomic propositions occurring in f; or a newly allocated set containing all these atomic propositions if s is 0.
bdd spot::atomic_prop_collect_as_bdd ( formula  f,
const twa_ptr &  a 
)

#include <spot/tl/apcollect.hh>

Return the set of atomic propositions occurring in a formula, as a BDD.

Parameters
fthe formula to inspect
athat automaton that should register the BDD variables used.
Returns
A conjunction the atomic propositions.
atomic_prop_set spot::create_atomic_prop_set ( unsigned  n)

#include <spot/tl/apcollect.hh>

construct an atomic_prop_set with n propositions

int spot::length ( formula  f)

#include <spot/tl/length.hh>

Compute the length of a formula.

The length of a formula is the number of atomic propositions, constants, and operators (logical and temporal) occurring in the formula. n-ary operators count for n-1; for instance a | b | c has length 5, even if there is only as single | node internally.

int spot::length_boolone ( formula  f)

#include <spot/tl/length.hh>

Compute the length of a formula, squashing Boolean formulae.

This is similar to spot::length(), except all Boolean formulae are assumed to have length one.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Dec 16 2016 06:04:08 for spot by doxygen 1.8.8