Rewriting Algorithms for Formulas

Classes
class	spot::mark_tools
	Utilities for marking NegClosure and EConcat operators in temporal formulas. More...
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...

Enumerations
enum	spot::mut_opts {   spot::Mut_Ap2Const = 1U << 0 , spot::Mut_Simplify_Bounds = 1U << 1 , spot::Mut_Remove_Multop_Operands = 1U << 2 , spot::Mut_Remove_Ops = 1U << 3 ,   spot::Mut_Split_Ops = 1U << 4 , spot::Mut_Rewrite_Ops = 1U << 5 , spot::Mut_Remove_One_Ap = 1U << 6 , spot::Mut_All = -1U }
	Types of mutations supported by mutate(). More...

Functions
formula	spot::to_delta2 (formula f, tl_simplifier *tls=nullptr)
	Convert an LTL formula to Δ₂
formula	spot::distribute_next (formula f)
	Distribute X at the top-level of a formula.
std::vector< formula >	spot::mutate (formula f, unsigned opts=Mut_All, unsigned max_output=-1U, unsigned mutation_count=1, bool sort=true)
	Generate mutations of a formula.
formula	spot::negative_normal_form (formula f, bool negated=false)
	Build the negative normal form of f.
formula	spot::relabel (formula f, relabeling_style style, relabeling_map *m=nullptr)
	Relabel the atomic propositions in a formula.
formula	spot::remove_x (formula f)
	Rewrite a stutter-insensitive formula f without using the X operator.
formula	spot::star_normal_form (formula sere, snf_cache *cache=nullptr)
	Helper to rewrite a sere in Star Normal Form.
formula	spot::star_normal_form_bounded (formula sere, snf_cache *cache=nullptr)
	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)
	Helper to rewrite a PSL formula in Suffix Operator Normal Form.
formula	spot::unabbreviate (formula in, const char *opt=default_unabbrev_string)
	Clone and rewrite a formula to remove specified operators logical operators.
formula	spot::unit_propagate (formula f)
	Simplify a formula via one-pass unit propagation.
formula	spot::relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr)
	Relabel Boolean subexpressions in a formula using atomic propositions.
formula	spot::relabel_apply (formula f, relabeling_map *m)
	Replace atomic propositions of f by subformulas specified in m.
formula	spot::relabel_overlapping_bse (formula f, relabeling_style style, relabeling_map *m)
	Relabel Boolean subexpressions in a formula using atomic propositions.
formula	spot::relabel_apply (formula f, const std::vector< formula > &m)
	Relabel Boolean subexpressions in a formula using atomic propositions.

Detailed Description

Enumeration Type Documentation

mut_opts

enum spot::mut_opts

#include <spot/tl/mutation.hh>

Types of mutations supported by mutate().

Enumerator
Mut_Ap2Const	Convert atomic propositions to constants.
Mut_Simplify_Bounds	Simplify bounds of bounded operators. If a bound is not formula::unbounded(), it can be reduced by one, or set to formula::unbounded().
Mut_Remove_Multop_Operands	Remove operands from n-ary operators.
Mut_Remove_Ops	Remove operators. Unary operators can be replaced by their operand. Binary operators can be replaced by one of their operands.
Mut_Split_Ops	Split syntactic sugar into simpler forms. For instance a<->b could be rewritten as a->b or b->a.
Mut_Rewrite_Ops	Rewrite some operators. Currently U can be changed to W. M can be changed to R or U. R can be changed to W.
Mut_Remove_One_Ap	Replace one atomic proposition by another one.
Mut_All	Attempt every mutation possible.

Function Documentation

distribute_next()

formula spot::distribute_next

(

formula

f

)

#include <spot/tl/distribute.hh>

Distribute X at the top-level of a formula.

Convert a formula like X(a | X(b | X(c & Xd))) into X(a) | XX(b) | (XXX(c) & XXXXd)

If some of the X operators in the chain are X[!] (strong next), the corresponding operators in the output will be X[!] as well, making this transformation suitable for both LTL (infinite semantics) and LTLf (finite semantics).

mutate()

std::vector< formula > spot::mutate	(	formula	f,
		unsigned	opts = Mut_All,
		unsigned	max_output = -1U,
		unsigned	mutation_count = 1,
		bool	sort = true
	)

#include <spot/tl/mutation.hh>

Generate mutations of a formula.

Returns up to max_output mutated formulas derived from f by applying mutation_count simultaneous mutations selected by opts (a bitmask of mut_opts values). If sort is true, the results are sorted.

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() [1/2]

formula spot::relabel_apply	(	formula	f,
		const std::vector< formula > &	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), where p1 replaces c and the rest is obvious.

relabel_apply() [2/2]

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.

The std::vector<formula> variant will be indexed by APIDs.

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), where 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), where 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

[etessami.00.ipl]

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. [bruggeman.96.tcs]

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 [cimatti.06.fmcad]

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 implements LTL rewriting rules as given by [esparza.24.acm]

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 in which each letter denotes an operator (using LBT's convention).

unit_propagate()

formula spot::unit_propagate

(

formula

f

)

#include <spot/tl/unitprop.hh>

Simplify a formula via one-pass unit propagation.

This function traverses the formula tree top-down, collecting facts (subformulas known to be true or false in context) and using them to simplify sibling subformulas. Facts are gathered without constructing new formulas: only existing subformulas can become facts.

Examples:

• G(a) & (a | b) → G(a) & b
• !a & (a | b) → !a & b
• (a | b) -> b → a -> b
• G(a & b & F(c)) propagates a, b, F(c) globally