spot::mtdswa Struct Reference

MTBDD-based representation of a state-based ω-automaton. More...

#include <spot/twaalgos/mtdswa.hh>

Inheritance diagram for spot::mtdswa:

Collaboration diagram for spot::mtdswa:

Public Member Functions
	mtdswa (const bdd_dict_ptr &dict) noexcept
bdd_dict_ptr	get_dict () const
	get the bdd_dict associated to this automaton
unsigned	num_roots () const
unsigned	num_states () const
	The number of states in the automaton.
std::ostream &	print_dot (std::ostream &os, const char *opts=nullptr) const
	Print the MTBDD.
twa_graph_ptr	as_twa (bool state_based=false, bool labels=true, bool complete=false) const
	convert to twa
void	sinks_as_states ()
	convert bddtrue/bddfalse nodes to actual states
void	sinks_as_constants (bool keep_all_states=false)
	converse sink states to bddtrue/bddfalse constants
bdd	get_controllable_variables () const
	Returns the conjunction of controllable variables.
void	set_controllable_variables (const std::vector< std::string > &vars, bool ignore_non_registered_ap=false)
	declare a list of controllable variables
void	set_controllable_variables (bdd vars)
	declare a list of controllable variables

Public Attributes
std::vector< formula >	aps
	The list of atomic propositions possibly used by the automaton.
std::vector< bdd >	states
std::vector< formula >	names
std::vector< acc_cond::mark_t >	colors
acc_cond	acc
std::unordered_map< int, int >	terminal_to_state_map
std::unordered_map< int, unsigned >	highlight_nodes
std::unordered_map< int, int >	highlight_groups

Detailed Description

MTBDD-based representation of a state-based ω-automaton.

Member Function Documentation

as_twa()

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

convert to twa

get_controllable_variables()

bdd spot::mtdswa::get_controllable_variables ( ) const

inline

Returns the conjunction of controllable variables.

get_dict()

bdd_dict_ptr spot::mtdswa::get_dict ( ) const

inline

get the bdd_dict associated to this automaton

num_states()

unsigned spot::mtdswa::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::mtdswa::print_dot	(	std::ostream &	os,
		const char *	opts = nullptr
	)		const

Print the MTBDD.

Add opts="s" to show SCCs.

set_controllable_variables() [1/2]

void spot::mtdswa::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 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::mtdswa::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 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.

sinks_as_constants()

void spot::mtdswa::sinks_as_constants

(

bool

keep_all_states = false

)

converse sink states to bddtrue/bddfalse constants

This modifies the automaton in place so that any sink state is turned into bddtrue or bddfalse depending on its acceptance.

The original sink states will be removed and the other state will be renumbered, unless keep_all_states is set.

sinks_as_states()

void spot::mtdswa::sinks_as_states

(

)

convert bddtrue/bddfalse nodes to actual states

This modifies the automaton in place so that it does not use the bddtrue and bddfalse constants. Those will be replaced by accepting and rejecting sinks respectively. Those new states are introduced only if no existing state can serve the same purpose.

When the acceptance condition is always accepting, or when it is always rejecting, introducing a sink state might require changing the acceptance condition. When that happens, the acceptance will be set to Büchi.

If the automaton had named states, newly introduced sinks will be named as formula::tt() or formula::ff().

Member Data Documentation

aps

std::vector<formula> spot::mtdswa::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 cases some of them canceled each other.

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

---

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

• spot/twaalgos/mtdswa.hh