Fine-tuning options for LTLf synthesis. More...

#include <spot/twaalgos/ltlf2dfa.hh>

Collaboration diagram for spot::ltlf_synthesis_options:

Public Attributes
bool	one_step_preprocess = true
	Perform one-step preprocessing.

bool	terminating_semantics = true
	Use terminating semantics when building a controller.

bool	fuse_same_bdds = true
	Merge states with identical MTBDD representation.

bool	simplify_terms = true
	Simplify formulas generated for states using cheap rewritings.

bool	detect_empty_univ = true
	Detect empty or universal languages after construction.

Detailed Description

Fine-tuning options for LTLf synthesis.

These options can be passed to ltlf_to_mtdfa_for_synthesis() to control the optimizations performed during the construction.

Member Data Documentation

◆ detect_empty_univ

bool spot::ltlf_synthesis_options::detect_empty_univ = true

Detect empty or universal languages after construction.

If, after construction of the whole automaton, it was found that all states were rejecting, or all states were accepting, the automaton is reduced to a rejecting or accepting sink state.

◆ fuse_same_bdds

bool spot::ltlf_synthesis_options::fuse_same_bdds = true

Merge states with identical MTBDD representation.

◆ one_step_preprocess

bool spot::ltlf_synthesis_options::one_step_preprocess = true

Perform one-step preprocessing.

When enabled, the formula for each step is first simplified in an attempt to prove realizability or unrealizability in one step.

◆ simplify_terms

bool spot::ltlf_synthesis_options::simplify_terms = true

Simplify formulas generated for states using cheap rewritings.

◆ terminating_semantics

bool spot::ltlf_synthesis_options::terminating_semantics = true

Use terminating semantics when building a controller.

Build a controller that knows when to stop. This disables some minor optimizations of the game.

This option is ignored when checking for realizability.

The documentation for this struct was generated from the following file:

spot/twaalgos/ltlf2dfa.hh