spot  2.11.6
Typedefs | Functions
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...
 

Detailed Description

Typedef Documentation

◆ atomic_prop_set

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

#include <spot/tl/apcollect.hh>

Set of atomic propositions.

Function Documentation

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

◆ 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
fthe formula to inspect
athat 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 doxygen 1.9.1