Classes
struct	spot::mtdfa_stats
	statistics about an mtdfa instance More...

struct	spot::mtdfa
	a DFA represented using shared multi-terminal BDDs More...

class	spot::ltlf_translator
	"Semi-internal" class used to implement spot::ltlf_to_mtdfa() More...

Functions
mtdfa_ptr	spot::ltlf_to_mtdfa (formula f, const bdd_dict_ptr &dict, bool fuse_same_bdds=true, bool simplify_terms=true, bool detect_empty_univ=true)
	Convert an LTLf formula into an MTDFA. More...

mtdfa_ptr	spot::ltlf_to_mtdfa_for_synthesis (formula f, const bdd_dict_ptr &dict, const std::vector< std::string > &outvars, ltlf_synthesis_backprop backprop=dfs_node_backprop, bool one_step_preprocess=false, bool realizability=false, bool fuse_same_bdds=true, bool simplify_terms=true, bool detect_empty_univ=true)
	Solve (or start solving) LTLf synthesis. More...

mtdfa_ptr	spot::ltlf_to_mtdfa_compose (formula f, const bdd_dict_ptr &dict, bool minimize=true, bool order_for_aps=true, bool want_names=true, bool fuse_same_bdds=true, bool simplify_terms=true)
	Convert an LTLf formula into a MTDFA, with a compositional approach. More...

mtdfa_ptr	spot::minimize_mtdfa (const mtdfa_ptr &dfa)
	Minimize a MTDFA. More...

mtdfa_ptr	spot::product (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to intersect their languages. More...

mtdfa_ptr	spot::product_or (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to sum their languages. More...

mtdfa_ptr	spot::product_xor (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to build the exclusive sum of their languages. More...

mtdfa_ptr	spot::product_xnor (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to keep words that are handled similarly in both operands. More...

mtdfa_ptr	spot::product_implies (const mtdfa_ptr &dfa1, const mtdfa_ptr &dfa2)
	Combine two MTDFAs to build an implication. More...

mtdfa_ptr	spot::complement (const mtdfa_ptr &dfa)
	Complement an MTDFA. More...

mtdfa_ptr	spot::twadfa_to_mtdfa (const twa_graph_ptr &twa)
	Convert a TWA (representing a DFA) into an MTDFA. More...

std::vector< bool >	spot::mtdfa_winning_region (mtdfa_ptr dfa)
	Compute the winning region of the MTDFA interpreted as a game. More...

backprop_graph	spot::mtdfa_to_backprop (mtdfa_ptr dfa, bool early_stop=true, bool preserve_names=false)
	Build a backprop_graph from dfa. More...

mtdfa_ptr	spot::mtdfa_winning_strategy (mtdfa_ptr dfa, bool backprop_nodes)
	Compute a strategy for an MTDFA interpreted as a game. More...

twa_graph_ptr	spot::mtdfa_strategy_to_mealy (mtdfa_ptr strategy, bool labels=true)
	Convert an MTDFA representing a strategy to a TwA with the "synthesis-output" property. More...

mtdfa_ptr	spot::mtdfa_restrict_as_game (mtdfa_ptr dfa)
	Build a generalized strategy from a set of winning states. More...

mtdfa_ptr	spot::mtdfa_restrict_as_game (mtdfa_ptr dfa, const std::vector< bool > &winning_states)
	Build a generalized strategy from a set of winning states. More...

mtdfa_ptr	spot::mtdfa_restrict_as_game (mtdfa_ptr dfa, const std::vector< trival > &winning_states)
	Build a generalized strategy from a set of winning states. More...

Detailed Description

MTDFAs are a representation of transition-based finite deterministic automata labeled by Boolean formulas. Each state is represented by a BDD encoding the Boolean formulas labeling the successor transition. The leaves of these BDDs are not only the usual bddfalse and bddtrue, but some integer-valued terminal representing the destination state. A terminal with integer label $2d+b$ represents destination state $d$ and uses $b\in\{0,1

Function Documentation

◆ complement()

mtdfa_ptr spot::complement ( const mtdfa_ptr & dfa )

#include <spot/twaalgos/ltlf2dfa.hh>

Complement an MTDFA.

◆ ltlf_to_mtdfa()

mtdfa_ptr spot::ltlf_to_mtdfa	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	fuse_same_bdds = `true`,
		bool	simplify_terms = `true`,
		bool	detect_empty_univ = `true`
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Convert an LTLf formula into an MTDFA.

This converts the LTLf formula f into an MTDFA, one state at a time, using a recursive computation of the successors of an LTLf-labeled state.

By default, the construction includes some very cheap optimizations that can be disabled with the relevant flags to study their effact:

States that have exactly the same MTBDD representation are merged (fuse_same_bdds)
formulas generated for states are simplified using very cheap rewritings (simplify_terms)
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 (detect_empty_univ)

States will be labeled using LTLf formulas, this is required by the construction.

[20]

◆ ltlf_to_mtdfa_compose()

mtdfa_ptr spot::ltlf_to_mtdfa_compose	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	minimize = `true`,
		bool	order_for_aps = `true`,
		bool	want_names = `true`,
		bool	fuse_same_bdds = `true`,
		bool	simplify_terms = `true`
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Convert an LTLf formula into a MTDFA, with a compositional approach.

This splits the LTLf formula on the Boolean operators at the top of the formula. Maximal subformula that have a temporal operator as root are translated using ltlf_to_mtdfa(), and the resulting automata are then minimized and then composed according to the Boolean operators above those subformulas.

This approach makes it possible to minimize the intermediate automata before combining them. (Set minimize to false to disable that.)

When combining multiple automata with AND or OR, there is some flexibility in the order in which this is done. When order_for_aps is false, a heap of automata to combine is used: the two smallest automata are combined and their result it put back in the heap. When order_for_aps is true, the automata are also ordered by size, but the smallest automaton is combined with the next smallest automaton that share an atomic proposition. The idea is to delay the combination of automata with disjoint APs as late as possible: indeed, the combination of those automata do not need to be minimized.

The compositional approach will keep track of LTLf formulas labeling the state by default, but this is not necessary. Set want_names to false to save tiny amount of work.

Options fuse_same_bdds and simplify_terms are passed directly to ltlf_to_mtdfa(), so see this function for details.

◆ ltlf_to_mtdfa_for_synthesis()

mtdfa_ptr spot::ltlf_to_mtdfa_for_synthesis	(	formula	f,
		const bdd_dict_ptr &	dict,
		const std::vector< std::string > &	outvars,
		ltlf_synthesis_backprop	backprop = `dfs_node_backprop`,
		bool	one_step_preprocess = `false`,
		bool	realizability = `false`,
		bool	fuse_same_bdds = `true`,
		bool	simplify_terms = `true`,
		bool	detect_empty_univ = `true`
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Solve (or start solving) LTLf synthesis.

This is similar to ltlf_to_mtdfa, but with the intent of solving LTLf synthesis problems. Typically, all accepting terminals will be replaced by bddtrue, and some nodes will be simplified according to their controllability.

The set of output variables should be specified with outvars.

If backprop is set to bdd_node_backprop, dfs_node_backprop, or dfs_strict_node_backprop, then a backpropagation graph it constructed while the automaton for f is explored. This may help to abort the construction earlier, and it is enough to solve the game and return a strategy. That strategy is returned if realizability is set to false (if a strategy does not exist, a DFA that has a single bddfalse state is reaturned. When realizability is true, then the returned MTDFA will just have a single state that is bddtrue (realizable) or bddfalse (unrealizable).

When backprop is set to state_refine, each state is locally simplified according to the accepting terminals/bddtrue/bddfalse it can reach, but the game still needs to be solved by other means.

If one_step_preprocess is set, the formula for each step is first simplified in attempt to prove realizability or unrealizability in one step. This require translating two different Boolean formulas to BDDs and then quantifying them.

See ltlf_to_mtdfa for the purpose of fuse_same_bdds, simplify_terms, detect_empty_univ.

[20]

◆ minimize_mtdfa()

mtdfa_ptr spot::minimize_mtdfa ( const mtdfa_ptr & dfa )

#include <spot/twaalgos/ltlf2dfa.hh>

Minimize a MTDFA.

Build a minimal DFA equivalent to dfa. This implements Moore's minimization algorithm by partition refinement: the MTDFA data structure make this particularly easy to implement.

Each state is assigned to an equivalence class. Initially, all state are in the same class. At each iteration, the original state array of MTBDD has its terminal relabeled according to the class of their state, preserving only the acceptance bit. After this relabeling, the set of equivalence classes is adjusted to that state are in the same class iff they have the MTBDD encoding.

Each iteration is linear in the number of nodes of the entire MTBDD array, and the number of iteration is at most linear in the number of states.

◆ mtdfa_restrict_as_game() [1/3]

mtdfa_ptr spot::mtdfa_restrict_as_game ( mtdfa_ptr dfa )

#include <spot/twaalgos/ltlf2dfa.hh>

Build a generalized strategy from a set of winning states.

This maps all accepting terminal to true. If a winning_states array is given, this also maps all non-winning terminal to false.

This will renumber all states.

◆ mtdfa_restrict_as_game() [2/3]

mtdfa_ptr spot::mtdfa_restrict_as_game	(	mtdfa_ptr	dfa,
		const std::vector< bool > &	winning_states
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Build a generalized strategy from a set of winning states.

This maps all accepting terminal to true. If a winning_states array is given, this also maps all non-winning terminal to false.

This will renumber all states.

◆ mtdfa_restrict_as_game() [3/3]

mtdfa_ptr spot::mtdfa_restrict_as_game	(	mtdfa_ptr	dfa,
		const std::vector< trival > &	winning_states
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Build a generalized strategy from a set of winning states.

This maps all accepting terminal to true. If a winning_states array is given, this also maps all non-winning terminal to false.

This will renumber all states.

◆ mtdfa_strategy_to_mealy()

twa_graph_ptr spot::mtdfa_strategy_to_mealy	(	mtdfa_ptr	strategy,
		bool	labels = `true`
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Convert an MTDFA representing a strategy to a TwA with the "synthesis-output" property.

By default the created automaton will have its states named using the LTLf formula for the original state if available. Set labels to false if you do not want that.

◆ mtdfa_to_backprop()

backprop_graph spot::mtdfa_to_backprop	(	mtdfa_ptr	dfa,
		bool	early_stop = `true`,
		bool	preserve_names = `false`
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Build a backprop_graph from dfa.

This creates a backprop_graph based in the game interpretation of dfa.

Set early_stop to false if you want to build the entire graph. Otherwise, this will stop as soon as the initial state is determined.

Set preserve_names to true if you want to decorate the backprop_graph with a few annotations indicating which the correspondence between some states of the backprop_graph and the roots of dfa.

[20]

◆ mtdfa_winning_region()

std::vector< bool > spot::mtdfa_winning_region ( mtdfa_ptr dfa )

#include <spot/twaalgos/ltlf2dfa.hh>

Compute the winning region of the MTDFA interpreted as a game.

This assumes that controllable variable have been registered with set_controllable_variables().

The winning region is the set of states from which the controllable variables can force the automaton to reach an accepting state.

Returns: a Boolean vector indicating whether a state is winning (true) or losing (false).

◆ mtdfa_winning_strategy()

mtdfa_ptr spot::mtdfa_winning_strategy	(	mtdfa_ptr	dfa,
		bool	backprop_nodes
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Compute a strategy for an MTDFA interpreted as a game.

Create a strategy, i.e, an MTDFA in which each controllable node has exactly one "bddfalse" child. If the initial state cannot be won by the controller, the strategy returned is bddfalse.

The backprop_node argument controls the algorithm used to solve the game. If is true, a backprop_graph is constructed from the MTDFA, mapping each MTBDD node to a node of the graph. This allows a linear-time resolution. If false, the game is solved by refining the MTDFA in-place; this use some kind of state-based back propagation that does not have linear complexity.

◆ product()

mtdfa_ptr spot::product	(	const mtdfa_ptr &	dfa1,
		const mtdfa_ptr &	dfa2
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Combine two MTDFAs to intersect their languages.

◆ product_implies()

mtdfa_ptr spot::product_implies	(	const mtdfa_ptr &	dfa1,
		const mtdfa_ptr &	dfa2
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Combine two MTDFAs to build an implication.

The results will recognize words that are rejected by dfa1 or accepted by dfa2.

◆ product_or()

mtdfa_ptr spot::product_or	(	const mtdfa_ptr &	dfa1,
		const mtdfa_ptr &	dfa2
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Combine two MTDFAs to sum their languages.

◆ product_xnor()

mtdfa_ptr spot::product_xnor	(	const mtdfa_ptr &	dfa1,
		const mtdfa_ptr &	dfa2
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Combine two MTDFAs to keep words that are handled similarly in both operands.

The results will recognize words that are their recognized by dfa1 and dfa2, or that are rejected by both.

◆ product_xor()

mtdfa_ptr spot::product_xor	(	const mtdfa_ptr &	dfa1,
		const mtdfa_ptr &	dfa2
	)

#include <spot/twaalgos/ltlf2dfa.hh>

Combine two MTDFAs to build the exclusive sum of their languages.

The results will recognize words that are their by only one of dfa1 or dfa2. If the resulting automaton has an empty language, then the two input automata were equivalent.

◆ twadfa_to_mtdfa()

mtdfa_ptr spot::twadfa_to_mtdfa ( const twa_graph_ptr & twa )

#include <spot/twaalgos/ltlf2dfa.hh>

Convert a TWA (representing a DFA) into an MTDFA.

Classes

Functions

Detailed Description

Function Documentation

◆ complement()

◆ ltlf_to_mtdfa()

◆ ltlf_to_mtdfa_compose()

◆ ltlf_to_mtdfa_for_synthesis()

◆ minimize_mtdfa()

◆ mtdfa_restrict_as_game() [1/3]

◆ mtdfa_restrict_as_game() [2/3]

◆ mtdfa_restrict_as_game() [3/3]

◆ mtdfa_strategy_to_mealy()

◆ mtdfa_to_backprop()

◆ mtdfa_winning_region()

◆ mtdfa_winning_strategy()

◆ product()

◆ product_implies()

◆ product_or()

◆ product_xnor()

◆ product_xor()

◆ twadfa_to_mtdfa()