spot
2.4.4
|
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::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.
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>
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/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).