Rewriting Algorithms for Formulas

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::to_delta2 (formula f, tl_simplifier *tls=nullptr)
	Convert an LTL formula to Δ₂ More...
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::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...
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::relabel_overlapping_bse (formula f, relabeling_style style, relabeling_map *m)
	Relabel Boolean subexpressions in a formula using atomic propositions. More...

Detailed Description

Function Documentation

from_ltlf()

formula spot::from_ltlf	(	formula	f,
		const char *	alive = "alive"
	)

#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. [29]

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.

mark_concat_ops()

formula spot::mark_tools::mark_concat_ops

(

formula

f

)

#include <spot/tl/mark.hh>

Mark operators NegClosure and EConcat.

Parameters

f	The formula to rewrite.

negative_normal_form()

formula spot::negative_normal_form	(	formula	f,
		bool	negated = false
	)

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

Parameters

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

relabel()

formula spot::relabel	(	formula	f,
		relabeling_style	style,
		relabeling_map *	m = nullptr
	)

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

See also

relabel_bse

relabel_overlapping_bse

relabel_apply()

formula spot::relabel_apply	(	formula	f,
		relabeling_map *	m
	)

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

relabel_bse()

formula spot::relabel_bse	(	formula	f,
		relabeling_style	style,
		relabeling_map *	m = nullptr
	)

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

The relabel_overlapping_bse() will introduce a new atomic proposition for each maximal Boolean subexpression encountered, even if they overlap (i.e., share common atomic propositions). For instance (a & b & c) U (c & d & e) will be simply be relabeled as p0 U p1. This kind of renaming does not preserve the satisfiability of the input formula.

The relabel_bse() version will make sure that the replaced subexpressions do not share atomic propositions. For instance (a & b & c) U (!c & d & e) will be simply be relabeled as (p0 & p1) U (!p1 & p2), were p1 replaces c and the rest is obvious.

relabel_overlapping_bse()

formula spot::relabel_overlapping_bse	(	formula	f,
		relabeling_style	style,
		relabeling_map *	m
	)

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

The relabel_overlapping_bse() will introduce a new atomic proposition for each maximal Boolean subexpression encountered, even if they overlap (i.e., share common atomic propositions). For instance (a & b & c) U (c & d & e) will be simply be relabeled as p0 U p1. This kind of renaming does not preserve the satisfiability of the input formula.

The relabel_bse() version will make sure that the replaced subexpressions do not share atomic propositions. For instance (a & b & c) U (!c & d & e) will be simply be relabeled as (p0 & p1) U (!p1 & p2), were p1 replaces c and the rest is obvious.

remove_x()

formula spot::remove_x

(

formula

f

)

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

See also

[23]

star_normal_form()

formula spot::star_normal_form	(	formula	sere,
		snf_cache *	cache = nullptr
	)

#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]

Parameters

sere	the SERE to rewrite
cache	an optional cache

star_normal_form_bounded()

formula spot::star_normal_form_bounded	(	formula	sere,
		snf_cache *	cache = nullptr
	)

#include <spot/tl/snf.hh>

A variant of star_normal_form() for r[*0..j] where j < ω.

suffix_operator_normal_form()

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.

Parameters

f	the PSL formula to rewrite
prefix	the prefix to use to name newly introduced aps

Returns

a pair with the rewritten formula, and a vector containing the names of newly introduced aps

to_delta2()

formula spot::to_delta2	(	formula	f,
		tl_simplifier *	tls = nullptr
	)

#include <spot/tl/delta2.hh>

Convert an LTL formula to Δ₂

This implement LTL rewriting rules as given by [21]

Only LTL operators are supported, PSL operators will be left untouched.

If tls is given, it will be used to simplify formulas and puts formulas in negative normal form. If tls is not given, a temporary simplifier will be created.

No transformation is attempted if the input is already Δ₂.

unabbreviate()

formula spot::unabbreviate	(	formula	in,
		const char *	opt = default_unabbrev_string
	)

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