spot
2.8.1

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...  
typedef std::set<formula> spot::atomic_prop_set 
#include <spot/tl/apcollect.hh>
Set of atomic propositions.
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.
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. 
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.
f  the formula to inspect 
a  that automaton that should register the BDD variables used. 
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. nary operators count for n1; 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.