spot::mtdfa Struct Reference

A DFA represented using shared multi-terminal BDDs. More...

#include <spot/twaalgos/ltlf2dfa.hh>

Inheritance diagram for spot::mtdfa:

Collaboration diagram for spot::mtdfa:

Public Member Functions
	mtdfa (const bdd_dict_ptr &dict) noexcept
	Create an empty mtdfa. More...
unsigned	num_roots () const
	The number of MTBDDs roots. More...
unsigned	num_states () const
	The number of states in the automaton. More...
bool	is_empty () const
	Check if the automaton recognizes the empty language. More...
std::ostream &	print_dot (std::ostream &os, int index=-1, bool labels=true) const
	Print the states array of MTBDD in graphviz format. More...
twa_graph_ptr	as_twa (bool state_based=false, bool labels=true) const
	Convert this automaton to a spot::twa_graph. More...
mtdfa_stats	get_stats (bool nodes, bool paths) const
	Compute some statistics about the automaton. More...
bdd_dict_ptr	get_dict () const
	Get the bdd_dict associated to this automaton. More...
bdd	get_controllable_variables () const
	Returns the conjunction of controllable variables. More...
void	set_controllable_variables (const std::vector< std::string > &vars, bool ignore_non_registered_ap=false)
	Declare a list of controllable variables. More...
void	set_controllable_variables (bdd vars)
	Declare a list of controllable variables. More...

Public Attributes
std::vector< bdd >	states
	BDD transitions for each root state. More...
std::vector< formula >	names
std::vector< formula >	aps
	The list of atomic propositions possibly used by the automaton. More...

Detailed Description

A DFA represented using shared multi-terminal BDDs.

Such a DFA is represented by a vector of BDDs: one BDD per state. Each BDD encodes the set of outgoing transitions of a state. The of the transitions encoded naturally using BDD decision variables, and the destination state is stored as a "terminal" node.

Those DFA use transition-based acceptance, and that acceptance is represented by the last bit of the value stored in the terminal.

If a transition should reach state V, the terminal stores the value 2*V if the transition is rejecting, or 2*V+1 if the transition is accepting.

bddfalse and bddtrue terminals are used to represent rejecting and accepting sink states.

[duret.25.ciaa]

Constructor & Destructor Documentation

mtdfa()

spot::mtdfa::mtdfa ( const bdd_dict_ptr &  dict )

inlinenoexcept

Create an empty mtdfa.

The dict is used to record how BDD variables map to atomic propositions.

Member Function Documentation

as_twa()

twa_graph_ptr spot::mtdfa::as_twa	(	bool	state_based = false,
		bool	labels = true
	)		const

Convert this automaton to a spot::twa_graph.

The twa_graph class is not meant to represent finite automata, so this will actually abuse the twa_graph class by creating a deterministic Büchi automaton in which accepting transitions should be interpreted as final transitions. If state_based is set, then a DBA with state-based acceptance is created instead.

The conversion can be costly, since it requires creating BDD-labeled transitions for each path between a root and a leaf of the state array. However it can be useful to explain the MTDBA semantics.

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

get_controllable_variables()

bdd spot::mtdfa::get_controllable_variables ( ) const

inline

Returns the conjunction of controllable variables.

get_dict()

bdd_dict_ptr spot::mtdfa::get_dict ( ) const

inline

Get the bdd_dict associated to this automaton.

get_stats()

mtdfa_stats spot::mtdfa::get_stats	(	bool	nodes,
		bool	paths
	)		const

Compute some statistics about the automaton.

If nodes and paths are false, this only fetches statistics that are available in constant time.

If nodes is true, this will additionally count the number of internal nodes and leaves. It requires scanning the BDDs for the entire array of states, so this is linear in what the number of nodes involved.

If paths is true, this will additionally count the number of paths from roots to leaves. This is potentially exponential in the number of atomic propositions.

is_empty()

bool spot::mtdfa::is_empty

(

)

const

Check if the automaton recognizes the empty language.

num_roots()

unsigned spot::mtdfa::num_roots ( ) const

inline

The number of MTBDDs roots.

This is the size of the states array. It does not account for any bddfalse or bddtrue state.

num_states()

unsigned spot::mtdfa::num_states ( ) const

inline

The number of states in the automaton.

This counts the number of roots, plus one if the bddtrue state is reachable. This is therefore the size that the transition-based output of as_twa() would have.

print_dot()

std::ostream& spot::mtdfa::print_dot	(	std::ostream &	os,
		int	index = -1,
		bool	labels = true
	)		const

Print the states array of MTBDD in graphviz format.

If index is non-negative, print only the single state specified by index.

By default states will be named according to the formulas given in the names array, if available. Set labels to false (or clear names) if you prefer states to be numbered.

set_controllable_variables() [1/2]

void spot::mtdfa::set_controllable_variables

(

bdd

vars

)

Declare a list of controllable variables.

Doing so affect the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function is expected to be called after you have built the automaton, in some way (causing atomic propositions to be registered). If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

set_controllable_variables() [2/2]

void spot::mtdfa::set_controllable_variables	(	const std::vector< std::string > &	vars,
		bool	ignore_non_registered_ap = false
	)

Declare a list of controllable variables.

Doing so affect the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function is expected to be called after you have built the automaton, in some way (causing atomic propositions to be registered). If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

Member Data Documentation

aps

std::vector<formula> spot::mtdfa::aps

The list of atomic propositions possibly used by the automaton.

This is actually the list of atomic propositions that appeared in the formulas/automata that were used to build this automaton. The automaton itself may use fewer atomic propositions, for instance in case some of them cancel each other.

This vector is sorted by formula ID, to make it easy to merge with another sorted vector.

names

std::vector<formula> spot::mtdfa::names

Name formula for each root state.

states

std::vector<bdd> spot::mtdfa::states

BDD transitions for each root state.

---

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

• spot/twaalgos/ltlf2dfa.hh