Miscellaneous Algorithms for Formulas

Classes
class	spot::realizability_simplifier_base
	Simplify a reactive specification, preserving realizability. More...
class	spot::realizability_simplifier
	Simplify a reactive specification, preserving realizability. More...

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

Functions
atomic_prop_set	spot::create_atomic_prop_set (unsigned n, const char *prefix="p")
	construct an atomic_prop_set with n propositions starting with prefix
atomic_prop_set *	spot::atomic_prop_collect (formula f, atomic_prop_set *s=nullptr)
	Return the set of atomic propositions occurring in a formula.
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.
atomic_prop_set	spot::collect_literals (formula f)
	Collect the literals occurring in f.
std::map< formula, unsigned char >	spot::collect_aps_with_polarities (formula f)
	Collect the APs occurring in f, along with their polarities.
std::vector< std::vector< spot::formula > >	spot::collect_equivalent_literals (formula f)
	Collect equivalent APs.
int	spot::length (formula f)
	Compute the length of a formula.
int	spot::length_boolone (formula f)
	Compute the length of a formula, squashing Boolean formulae.

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

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.

collect_aps_with_polarities()

std::map< formula, unsigned char > spot::collect_aps_with_polarities

(

formula

f

)

#include <spot/tl/apcollect.hh>

Collect the APs occurring in f, along with their polarities.

This function records each atomic proposition occurring in f along with the polarity of its occurrence. For instance if the formula is G(a -> b) & X(!b & c), then this will output the map {a: 0b01, b: 0b11, c: 0b10} where 0x01 means negative polarity, 0x10 is positive polarity, and 0x11 is both.

collect_equivalent_literals()

std::vector< std::vector< spot::formula > > spot::collect_equivalent_literals

(

formula

f

)

#include <spot/tl/apcollect.hh>

Collect equivalent APs.

Looks for patterns like ...&G(...&(x->y)&...)&... or other forms of constant implications, then build a graph of implications to compute equivalence classes of literals.

collect_literals()

atomic_prop_set spot::collect_literals

(

formula

f

)

#include <spot/tl/apcollect.hh>

Collect the literals occurring in f.

This function records each atomic proposition occurring in f along with the polarity of its occurrence. For instance if the formula is G(a -> b) & X(!b & c), then this will output {!a, b, !b, c}.

create_atomic_prop_set()

atomic_prop_set spot::create_atomic_prop_set	(	unsigned	n,
		const char *	prefix = "p"
	)

#include <spot/tl/apcollect.hh>

construct an atomic_prop_set with n propositions starting with prefix

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.