spot  2.8.3
Miscellaneous Algorithms for Formulas

## Typedefs

typedef std::set< formulaspot::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_setspot::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...

## ◆ atomic_prop_set

 typedef std::set spot::atomic_prop_set

`#include <spot/tl/apcollect.hh>`

Set of atomic propositions.

## ◆ atomic_prop_collect()

 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
 f the formula to inspect s an 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.

## ◆ atomic_prop_collect_as_bdd()

 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
 f the formula to inspect a that automaton that should register the BDD variables used.
Returns
A conjunction the atomic propositions.

## ◆ create_atomic_prop_set()

 atomic_prop_set spot::create_atomic_prop_set ( unsigned n )

`#include <spot/tl/apcollect.hh>`

construct an atomic_prop_set with n propositions

## ◆ length()

 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.

## ◆ length_boolone()

 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 Feb 27 2015 10:00:07 for spot by 1.8.13