|
spot 2.15.1
|
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. | |
| bool | spot::ltl_satisfiable (formula f) |
| Decide if an LTL formula is satisfiable. | |
| std::vector< unsigned char > | spot::collect_apids_with_polarities (formula f) |
| Collect the APs occurring in f, along with their polarities. | |
| void | spot::collect_apids_with_polarities (formula f, std::vector< unsigned char > &v) |
| Collect the APs occurring in f, along with their polarities. | |
| std::vector< unsigned char > | spot::collect_quantified_apids (formula f) |
| Collect quantified APs occurring in f. | |
| void | spot::collect_quantified_apids (formula f, std::vector< unsigned char > &v) |
| Collect quantified APs occurring in f. | |
| 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 | the automaton that should register the BDD variables used. |
| 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.
| 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.
#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.
| 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.
| 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}.
| 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.)
| 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.)
| 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
| 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.
| 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.
| 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.
1.9.8