On-the-fly LTL→TGBA explorer. More...

#include <spot/twaalgos/ltl2tgba_fm.hh>

Collaboration diagram for spot::ltl_to_tgba_fm_otf:

Classes
struct	options
	Bundle the boolean options for translation. More...

Public Member Functions
	ltl_to_tgba_fm_otf (formula f, twa_graph_ptr aut, options opts=options(), tl_simplifier simplifier=nullptr, const atomic_prop_set unobs=nullptr)
	Constructor.

	ltl_to_tgba_fm_otf (const ltl_to_tgba_fm_otf &)=delete

ltl_to_tgba_fm_otf &	operator= (const ltl_to_tgba_fm_otf &)=delete

formula	init_state () const
	The initial formula-state (canonicalized if symb_merge is on).

formula	orig_formula () const

bdd	succ_as_bdd (formula s)

std::vector< fm_edge >	succ_as_edges (formula s)

std::vector< fm_simple_edge >	succ_as_acc_and_dest (formula s)
	Decompose the successors of s into edges without conditions.

const bdd &	var_set () const
	Variable set: atomic propositions.

const bdd &	next_set () const
	Variable set: Next variables (destination encoding).

const bdd &	a_set () const
	Variable set: acceptance promises.

formula	conj_bdd_to_formula (bdd cube) const
	Convert a cube over next_set() into a formula.

acc_cond::mark_t	bdd_to_mark (bdd a) const
	Convert a cube over a_set() into acceptance marks.

int	register_next_variable (formula f)

const bdd_dict_ptr &	get_dict () const
	The BDD dictionary.

Detailed Description

On-the-fly LTL→TGBA explorer.

Encapsulates the data structures from ltl_to_tgba_fm() so that successors of a formula-state can be computed without building the full automaton. Two views are provided:

succ_as_bdd(): a symbolic BDD view (cached, no exprop)
succ_as_edges(): an explicit edge list (exprop, simplification, canonicalization, and branching postponement applied here)

The class also exposes accessors so that a client can decompose the BDD returned by succ_as_bdd() on its own if needed.

Acceptance condition semantics

This class does not own a twa_graph; it receives one from the caller (aut) and uses it only to call register_ap() as new atomic propositions are discovered, and to update its acceptance condition as new colors are allocated. The acceptance condition of aut is therefore mutated during the lifetime of the explorer.

The Couvreur translation internally encodes promises P(…) using negated Inf sets: the acceptance condition of aut effectively represents Inf(!0)&Inf(!1)&…&Inf(!(N-1)), a form Spot does not directly support. The acceptance marks returned in fm_edge::acc therefore correspond to this negated semantics.

Because the number of acceptance sets N grows during exploration (each new promise allocates a fresh color), the marks cannot be complemented on-the-fly; complementation must wait until exploration is complete and the final N is known. At that point, build a proper TGBA by complementing each edge's mark with respect to N and setting the acceptance condition to generalized-Büchi:

auto& acc = aut->acc();
for (auto& e: aut->edges())
  e.acc = acc.comp(e.acc);
acc.set_generalized_buchi();

This is exactly what ltl_to_tgba_fm() does before returning the completed automaton.

Constructor & Destructor Documentation

◆ ltl_to_tgba_fm_otf()

spot::ltl_to_tgba_fm_otf::ltl_to_tgba_fm_otf	(	formula	f,
		twa_graph_ptr	aut,
		options	opts = `options()`,
		tl_simplifier *	simplifier = `nullptr`,
		const atomic_prop_set *	unobs = `nullptr`
	)

Constructor.

Normalizes the formula, initializes the BDD variable mappings, and prepares all internal data structures.

Parameters

f	the LTL/PSL formula
aut	the automaton being built, used only to call register_ap(); the explorer never adds states or edges itself
opts	translation options
simplifier	optional LTL simplifier (owned by caller)
unobs	optional set of unobservable events

Member Function Documentation

◆ a_set()

const bdd & spot::ltl_to_tgba_fm_otf::a_set ( ) const

Variable set: acceptance promises.

◆ bdd_to_mark()

acc_cond::mark_t spot::ltl_to_tgba_fm_otf::bdd_to_mark ( bdd a ) const

Convert a cube over a_set() into acceptance marks.

◆ conj_bdd_to_formula()

formula spot::ltl_to_tgba_fm_otf::conj_bdd_to_formula ( bdd cube ) const

Convert a cube over next_set() into a formula.

◆ get_dict()

const bdd_dict_ptr & spot::ltl_to_tgba_fm_otf::get_dict ( ) const

The BDD dictionary.

◆ init_state()

formula spot::ltl_to_tgba_fm_otf::init_state ( ) const

The initial formula-state (canonicalized if symb_merge is on).

◆ next_set()

const bdd & spot::ltl_to_tgba_fm_otf::next_set ( ) const

Variable set: Next variables (destination encoding).

◆ orig_formula()

formula spot::ltl_to_tgba_fm_otf::orig_formula ( ) const

The original formula after normalization and quantifier extraction, but before canonicalization. Useful for property checks on the resulting automaton.

◆ register_next_variable()

int spot::ltl_to_tgba_fm_otf::register_next_variable ( formula f )

Register a new Next variable for f and return its BDD variable index.

◆ succ_as_acc_and_dest()

std::vector< fm_simple_edge > spot::ltl_to_tgba_fm_otf::succ_as_acc_and_dest ( formula s )

Decompose the successors of s into edges without conditions.

This is a lighter variant of succ_as_edges() that omits the BDD condition on atomic propositions. It is useful for on-the-fly emptiness checks where the condition is known to be bddtrue (e.g., after realizability simplification has removed all atomic propositions). Skipping the condition computation avoids unnecessary BDD work.

Internally calls succ_as_bdd(), existentially quantifies all atomic propositions away (so the BDD only contains Next and acceptance variables), then extracts (acc, dst) pairs via minato_isop. Applies simplification and canonicalization (symb_merge), but skips branching postponement and all condition-related post-processing. The exprop option is ignored: since no conditions are extracted, there is no need to iterate over all combinations of atomic propositions.

Results are NOT cached.

◆ succ_as_bdd()

bdd spot::ltl_to_tgba_fm_otf::succ_as_bdd ( formula s )

Translate s into a single BDD representing all its successors.

This calls the internal formula_canonicalizer and caches the result. The returned BDD uses three variable families:

var_set(): atomic propositions (edge conditions)
next_set(): destination encoding (one variable per formula)
a_set(): acceptance promises (one variable per promise)

Note: exprop and branching_postponement are NOT applied here; they only affect succ_as_edges().

◆ succ_as_edges()

std::vector< fm_edge > spot::ltl_to_tgba_fm_otf::succ_as_edges ( formula s )

Decompose the successors of s into individual edges.

Internally calls succ_as_bdd(), then extracts edges via minato_isop (with minterm iteration when exprop is enabled). Applies simplification, canonicalization (symb_merge), and branching postponement. Promises are converted to mark_t.

The acceptance marks returned in fm_edge::acc use negated Inf semantics; see the class-level documentation for how to convert them to proper generalized-Büchi marks.