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

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

atomic_prop_set	spot::collect_literals (formula f)
	Collect the literals occurring in f. More...

std::map< formula, unsigned char >	spot::collect_aps_with_polarities (formula f)
	Collect the APs occurring in f, along with their polarities. More...

std::vector< std::vector< spot::formula > >	spot::collect_equivalent_literals (formula f)
	Collect equivalent APs. 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...

bool	spot::ltl_satisfiable (formula f)
	Decide if an LTL formula is satisfiable. More...

std::vector< unsigned char >	spot::collect_apids_with_polarities (formula f)
	Collect the APs occurring in f, along with their polarities. More...

void	spot::collect_apids_with_polarities (formula f, std::vector< unsigned char > &v)
	Collect the APs occurring in f, along with their polarities. More...

std::vector< unsigned char >	spot::collect_quantified_apids (formula f)
	Collect quantified APs occurring in f. More...

void	spot::collect_quantified_apids (formula f, std::vector< unsigned char > &v)
	Collect quantified APs occurring in f. 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

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	the automaton that should register the BDD variables used.

Returns: A conjunction of the atomic propositions.

◆ collect_apids_with_polarities() [1/2]

std::vector<unsigned char> spot::collect_apids_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), and we assume that atomic propositions a, b, and c, use APID 0, 1, and 2, respectively then this will output the vector [0b01, 0b11, 0b10] where 0b01 means negative polarity, 0b10 is positive polarity, and 0b11 is both.

This function is expected to be faster than collect_aps_with_polarities(), with the only drawback that the returned vector is as large as the number of declared atomic propositions, independently of the propositions actually used by the formula.

If the formula is quantified, this ignores quantifiers.

◆ collect_apids_with_polarities() [2/2]

void spot::collect_apids_with_polarities	(	formula	f,
		std::vector< unsigned char > &	v
	)

#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), and we assume that atomic propositions a, b, and c, use APID 0, 1, and 2, respectively then this will output the vector [0b01, 0b11, 0b10] where 0b01 means negative polarity, 0b10 is positive polarity, and 0b11 is both.

This function is expected to be faster than collect_aps_with_polarities(), with the only drawback that the returned vector is as large as the number of declared atomic propositions, independently of the propositions actually used by the formula.

If the formula is quantified, this ignores quantifiers.

◆ 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 0b01 means negative polarity, 0b10 is positive polarity, and 0b11 is both.

If the formula is quantified, this ignores quantifiers.

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

If the formula is quantified, this ignores quantifiers.

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

◆ collect_quantified_apids() [1/2]

std::vector<unsigned char> spot::collect_quantified_apids ( formula f )

#include <spot/tl/apcollect.hh>

Collect quantified APs occurring in f.

This returns or updates a vector indexed by APIDs. An APID that is not quantified in f will have value 0. If it is existentially quantified it will have value 1. If it is universally quantified it will have value 2. (If it is both existentially and universally quantified, it will have value 3. In this case, consider using normalize_quantifiers() to remove the superfluous quantification.)

◆ collect_quantified_apids() [2/2]

void spot::collect_quantified_apids	(	formula	f,
		std::vector< unsigned char > &	v
	)

#include <spot/tl/apcollect.hh>

Collect quantified APs occurring in f.

This returns or updates a vector indexed by APIDs. An APID that is not quantified in f will have value 0. If it is existentially quantified it will have value 1. If it is universally quantified it will have value 2. (If it is both existentially and universally quantified, it will have value 3. In this case, consider using normalize_quantifiers() to remove the superfluous quantification.)

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

◆ ltl_satisfiable()

bool spot::ltl_satisfiable ( formula f )

#include <spot/tl/sat.hh>

Decide if an LTL formula is satisfiable.

This is not a very smart implementation currently: the formula is first simplified by removing atomic propositions that always have the same polarity, then the result is translated into a TGBA that is checked for emptiness. Note that building an entire automaton is overkill when the formula is satisfiable, so eventually this could be done on-the-fly or using other techniques.

Classes

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ atomic_prop_set

Function Documentation

◆ atomic_prop_collect()

◆ atomic_prop_collect_as_bdd()

◆ collect_apids_with_polarities() [1/2]

◆ collect_apids_with_polarities() [2/2]

◆ collect_aps_with_polarities()

◆ collect_equivalent_literals()

◆ collect_literals()

◆ collect_quantified_apids() [1/2]

◆ collect_quantified_apids() [2/2]

◆ create_atomic_prop_set()

◆ length()

◆ length_boolone()

◆ ltl_satisfiable()