spot
2.11.6
|
Classes | |
class | spot::tl_simplifier |
Rewrite or simplify f in various ways. More... | |
class | spot::unabbreviator |
Clone and rewrite a formula to remove specified operators logical operators. More... | |
Functions | |
formula | spot::from_ltlf (formula f, const char *alive="alive") |
Convert an LTLf into an LTL formula. More... | |
formula | spot::mark_tools::mark_concat_ops (formula f) |
Mark operators NegClosure and EConcat. More... | |
formula | spot::negative_normal_form (formula f, bool negated=false) |
Build the negative normal form of f. More... | |
formula | spot::relabel (formula f, relabeling_style style, relabeling_map *m=nullptr) |
Relabel the atomic propositions in a formula. More... | |
formula | spot::relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr) |
Relabel Boolean subexpressions in a formula using atomic propositions. More... | |
formula | spot::relabel_apply (formula f, relabeling_map *m) |
Replace atomic propositions of f by subformulas specified in m. More... | |
formula | spot::remove_x (formula f) |
Rewrite a stutter-insensitive formula f without using the X operator. More... | |
formula | spot::star_normal_form (formula sere, snf_cache *cache=nullptr) |
Helper to rewrite a sere in Star Normal Form. More... | |
formula | spot::star_normal_form_bounded (formula sere, snf_cache *cache=nullptr) |
A variant of star_normal_form() for r[*0..j] where j < ω . More... | |
std::pair< formula, std::vector< std::string > > | spot::suffix_operator_normal_form (formula f, const std::string prefix) |
Helper to rewrite a PSL formula in Suffix Operator Normal Form. More... | |
formula | spot::unabbreviate (formula in, const char *opt=default_unabbrev_string) |
Clone and rewrite a formula to remove specified operators logical operators. More... | |
#include <spot/tl/ltlf.hh>
Convert an LTLf into an LTL formula.
This is based on De Giacomo & Vardi (IJCAI'13) reduction from LTLf (finite-LTL) to LTL. [26]
In this reduction, finite words are extended into infinite words in which a new atomic proposition alive
marks the prefix of the infinite word that corresponds to the original finite word. The formula is rewritten to ensure that the eventualities occur during the "alive" portion. For instance a U b
becomes alive&(a U (b & alive))&(alive U G!alive)
.
The alive argument can be used to change the name of the atomic property used to introduce. Additionally if alive is a string starting with and exclamation mark, e.g., !dead
then the atomic property will be built from the rest of the string, and its negation will be used in the transformation. Using !dead
rather than alive
makes more sense if the state-space introduces a dead
property on states representing the end of finite computations.
#include <spot/tl/mark.hh>
Mark operators NegClosure and EConcat.
f | The formula to rewrite. |
#include <spot/tl/nenoform.hh>
Build the negative normal form of f.
All negations of the formula are pushed in front of the atomic propositions.
f | The formula to normalize. |
negated | If true , return the negative normal form of !f |
Note that this will not remove abbreviated operators. If you want to remove abbreviations, call spot::unabbreviate first. (Calling this function after spot::negative_normal_form would likely produce a formula which is not in negative normal form.)
#include <spot/tl/relabel.hh>
Relabel the atomic propositions in a formula.
If m is non-null, it is filled with correspondence between the new names (keys) and the old names (values).
#include <spot/tl/relabel.hh>
Replace atomic propositions of f by subformulas specified in m.
Atomic proposition that do not appear in m are not replaced.
#include <spot/tl/relabel.hh>
Relabel Boolean subexpressions in a formula using atomic propositions.
If m is non-null, it is filled with correspondence between the new names (keys) and the old names (values).
#include <spot/tl/remove_x.hh>
Rewrite a stutter-insensitive formula f without using the X operator.
This function may also be applied to stutter-sensitive formulas, but in that case the resulting formula is not equivalent.
#include <spot/tl/snf.hh>
Helper to rewrite a sere in Star Normal Form.
This should only be called on children of a Star operator. It corresponds to the E° operation defined by Brüggemann-Klein. [6]
sere | the SERE to rewrite |
cache | an optional cache |
#include <spot/tl/snf.hh>
A variant of star_normal_form() for r[*0..j]
where j < ω
.
std::pair<formula, std::vector<std::string> > spot::suffix_operator_normal_form | ( | formula | f, |
const std::string | prefix | ||
) |
#include <spot/tl/sonf.hh>
Helper to rewrite a PSL formula in Suffix Operator Normal Form.
SONF is described in section 4 of [11]
The formula output by this function is guaranteed to be in Negative Normal Form.
f | the PSL formula to rewrite |
prefix | the prefix to use to name newly introduced aps |
#include <spot/tl/unabbrev.hh>
Clone and rewrite a formula to remove specified operators logical operators.
The set of operators to remove should be passed as a string which in which each letter denote an operator (using LBT's convention).