LTLf Algorithms

Classes
class	spot::ltlf_simplifier
	Cheap simplification rules for LTLf formulas. More...
class	spot::ltlf_one_step_sat_rewrite_with_cache
	Cached version of the one-step satisfiability rewriting for LTLf formulas. More...
class	spot::ltlf_one_step_unsat_rewrite_with_cache
	Cached version of the one-step unsatisfiability rewriting for LTLf formulas. More...

Functions
formula	spot::from_ltlf (formula f, const char *alive, int algo)
	Convert an LTLf into an LTL formula.
formula	spot::from_ltlf (formula f, const char *alive="alive")
	Convert an LTLf into an LTL formula.
formula	spot::ltlf_one_step_sat_rewrite (formula f)
	One-step satisfiability rewriting for LTLf formulas.
formula	spot::ltlf_one_step_unsat_rewrite (formula f, bool negate=false)
	One-step unsatisfiability rewriting for LTLf formulas.

Detailed Description

Function Documentation

from_ltlf() [1/2]

formula spot::from_ltlf	(	formula	f,
		const char *	alive,
		int	algo
	)

#include <spot/tl/ltlf.hh>

Convert an LTLf into an LTL formula.

Parameters

f	an LTLf formula
alive	name of the "alive" proposition (default: "alive"). If the name starts with '!', e.g., !dead, the atomic proposition is built from the rest of the string and its negation is 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.
algo	translation algorithm to use: 1 (default) — translation that guarantees the result is a syntactic-obligation formula; 0 — original De Giacomo & Vardi (IJCAI'13) translation [degiacomo.13.ijcai].

Note that the description of the translation in [degiacomo.13.ijcai] has a typo in the definition of $t(a U b)$. This typo is fixed in [dutta.14.memocode] but that second paper forgets to ensure that $alive$ holds initially.

from_ltlf() [2/2]

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

#include <spot/tl/ltlf.hh>

Convert an LTLf into an LTL formula.

Parameters

f	an LTLf formula
alive	name of the "alive" proposition (default: "alive"). If the name starts with '!', e.g., !dead, the atomic proposition is built from the rest of the string and its negation is 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.

This overload reads the environment variable SPOT_FROM_LTLF (values: 0 = original, 1 = syntactic-obligation) exactly once and caches the result. The default when the variable is unset is 1.

[duret.26.arxiv]

ltlf_one_step_sat_rewrite()

formula spot::ltlf_one_step_sat_rewrite

(

formula

f

)

#include <spot/tl/ltlf.hh>

One-step satisfiability rewriting for LTLf formulas.

ltlf_one_step_unsat_rewrite()

formula spot::ltlf_one_step_unsat_rewrite	(	formula	f,
		bool	negate = false
	)

#include <spot/tl/ltlf.hh>

One-step unsatisfiability rewriting for LTLf formulas.