MTDSwA (MTBDD-based ω-automata)

Algorithms and data structures for MTBDD-based ω-automata. More...

Classes
struct	spot::mtdswa
	MTBDD-based representation of a state-based ω-automaton. More...
class	spot::simple_ltl_translator
	"Semi-internal" for translating LTL using MTBDDs More...
struct	spot::mtdtwa
	A multi-terminal decision diagram representation of a TωA. More...

Typedefs
typedef std::shared_ptr< mtdswa >	spot::mtdswa_ptr
	Shared pointer to an mtdswa.
typedef std::shared_ptr< const mtdswa >	spot::const_mtdswa_ptr
	Shared pointer to a const mtdswa.
typedef std::pair< acc_cond::mark_t, unsigned >	spot::terminal_data_t
	Data associated with a terminal BDD node.
typedef std::vector< terminal_data_t >	spot::terminal_data_map_t
	Map from terminal BDD values to terminal data.
typedef std::shared_ptr< mtdtwa >	spot::mtdtwa_ptr
	Shared pointer to an mtdtwa.
typedef std::shared_ptr< const mtdtwa >	spot::const_mtdtwa_ptr
	Shared pointer to a const mtdtwa.

Functions
mtdswa_ptr	spot::dtwa_to_mtdswa (const twa_graph_ptr &aut)
	Convert deterministic TwA to MTDSwA.
std::vector< int >	spot::scc_vector (const mtdswa_ptr &aut, std::vector< bool > *transient=nullptr, std::vector< std::vector< int > > *succs=nullptr)
	Find the SCC of each state.
std::vector< unsigned >	spot::loding_weak_ranking (const mtdswa_ptr &aut, bool fix=false)
	Preprocess a weak MTDSwA before minimization.
mtdswa_ptr	spot::product (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to intersect their languages.
mtdswa_ptr	spot::product_or (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to sum their languages.
mtdswa_ptr	spot::product_xor (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to build the exclusive sum of their languages.
mtdswa_ptr	spot::product_xnor (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to keep words that are handled similarly in both operands.
mtdswa_ptr	spot::product_implies (const mtdswa_ptr &swa1, const mtdswa_ptr &swa2)
	Combine two MTDSwAs to build an implication.
mtdswa_ptr	spot::complement (const mtdswa_ptr &swa)
	Complement an MTDSwA.
mtdswa_ptr	spot::obligation_to_mtdswa (formula f, const bdd_dict_ptr &dict, bool fuse_same_bdds=true, bool simplify_terms=true)
	Convert a syntactic-obligation to an MTDSwA.
mtdswa_ptr	spot::obligation_synthesis (formula f, const bdd_dict_ptr &dict, const std::vector< std::string > &outvars, bool realizability=false, bool simplify_terms=true, int debug=-1)
	Reactive synthesis of syntactic-obligations.
twa_graph_ptr	spot::mtdswa_strategy_to_mealy (mtdswa_ptr strategy, bool labels=true, bool loop=false)
	Convert a strategy represented as MTDSwA into a Mealy machine.
void	spot::trim (mtdswa_ptr swa, bool trim_useless_sccs_too=false)
	Remove unnecessary states from an MTDSwA.
mtdtwa_ptr	spot::dtwa_to_mtdtwa (const twa_graph_ptr &aut)
	Convert a deterministic TωA to an MTDTwA.
mtdswa_ptr	spot::minimize_mtdswa (const mtdswa_ptr &dfa)
	Minimization of MTDSwA.
mtdswa_ptr	spot::minimize_mtdswa (const mtdswa_ptr &dfa, const std::vector< unsigned > &initial_partition)
	Minimization of MTDSwA.
mtdswa_ptr	spot::quantify_exists (const mtdswa_ptr &swa, bdd vars, bool trim=true)
	Existentially quantify variables in a weak MTDSwA.
mtdswa_ptr	spot::quantify_exists (const mtdswa_ptr &swa, const formula &ap, bool trim=true)
	Existentially quantify variables in a weak MTDSwA.
mtdswa_ptr	spot::quantify_exists (const mtdswa_ptr &swa, const std::vector< formula > &aps, bool trim=true)
	Existentially quantify variables in a weak MTDSwA.
mtdswa_ptr	spot::quantify_forall (const mtdswa_ptr &swa, bdd vars, bool trim=true)
	Universally quantify variables in a weak MTDSwA.
mtdswa_ptr	spot::quantify_forall (const mtdswa_ptr &swa, const formula &ap, bool trim=true)
	Universally quantify variables in a weak MTDSwA.
mtdswa_ptr	spot::quantify_forall (const mtdswa_ptr &swa, const std::vector< formula > &aps, bool trim=true)
	Universally quantify variables in a weak MTDSwA.

Detailed Description

Algorithms and data structures for MTBDD-based ω-automata.

Typedef Documentation

const_mtdswa_ptr

typedef std::shared_ptr<const mtdswa> spot::const_mtdswa_ptr

#include <spot/twaalgos/mtdswa.hh>

Shared pointer to a const mtdswa.

const_mtdtwa_ptr

typedef std::shared_ptr<const mtdtwa> spot::const_mtdtwa_ptr

#include <spot/twaalgos/mtdtwa.hh>

Shared pointer to a const mtdtwa.

mtdswa_ptr

typedef std::shared_ptr< mtdswa > spot::mtdswa_ptr

#include <spot/twaalgos/mtdswa.hh>

Shared pointer to an mtdswa.

mtdtwa_ptr

typedef std::shared_ptr<mtdtwa> spot::mtdtwa_ptr

#include <spot/twaalgos/mtdtwa.hh>

Shared pointer to an mtdtwa.

terminal_data_map_t

typedef std::vector<terminal_data_t> spot::terminal_data_map_t

#include <spot/twaalgos/mtdtwa.hh>

Map from terminal BDD values to terminal data.

terminal_data_t

typedef std::pair<acc_cond::mark_t, unsigned> spot::terminal_data_t

#include <spot/twaalgos/mtdtwa.hh>

Data associated with a terminal BDD node.

Function Documentation

complement()

mtdswa_ptr spot::complement

(

const mtdswa_ptr &

swa

)

#include <spot/twaalgos/mtdswa.hh>

Complement an MTDSwA.

dtwa_to_mtdswa()

mtdswa_ptr spot::dtwa_to_mtdswa

(

const twa_graph_ptr &

aut

)

#include <spot/twaalgos/mtdswa.hh>

Convert deterministic TwA to MTDSwA.

dtwa_to_mtdtwa()

mtdtwa_ptr spot::dtwa_to_mtdtwa

(

const twa_graph_ptr &

aut

)

#include <spot/twaalgos/mtdtwa.hh>

Convert a deterministic TωA to an MTDTwA.

loding_weak_ranking()

std::vector< unsigned > spot::loding_weak_ranking	(	const mtdswa_ptr &	aut,
		bool	fix = false
	)

#include <spot/twaalgos/mtdswa.hh>

Preprocess a weak MTDSwA before minimization.

This implements Löding's ranking function [loding.01.ipl] that can be used to decide which transient states (i.e., states that are not part of any cycles) should be marked as accepting or rejecting in order to guarantee minimality after the automaton is minimized like a DFA.

Contrary to Löding's paper, we use a ranking function that is decreasing. A state can only go to another state with a rank that is equal or smaller. Even ranks designate rejecting states, and odd ranks designate accepting states.

The function returns a vector that gives the rank of each state. If the MTDSwA uses constants bddfalse and bddtrue as terminals, those can be assumed to have rank 0 and 1 respectively.

If fix is set, the acceptance of the states of the input automaton will be fixed according to the computed ranks.

The returned ranking vector can be passed minimize_mtdswa() to be used as initial partition.

minimize_mtdswa() [1/2]

mtdswa_ptr spot::minimize_mtdswa

(

const mtdswa_ptr &

dfa

)

#include <spot/twaalgos/mtdswa.hh>

Minimization of MTDSwA.

This is called minimization because it implements a variant of Moore's partition-refinement algorithms (that is normally used to minimize DFAs). However for general deterministic ω-automata, this does not guarantee minimality.

One exception is weak deterministic ω-automata, which can be minimized precisely if they are first preprocessed with loding_weak_ranking().

The implementation of this minimization currently is unable to merge states with any bddfalse or bddtrue constant. You can work around this by converting constants to states before minimizing, and possibly back to constants afterwards:

dfa->sinks_as_states();
dfa = minimize_mtdsw(dfa);
dfa->sinks_as_constants();  // if really needed

By default, the initial partition is based on the colors that label each state. If you know a better one, you can pass it as initial_partition.

minimize_mtdswa() [2/2]

mtdswa_ptr spot::minimize_mtdswa	(	const mtdswa_ptr &	dfa,
		const std::vector< unsigned > &	initial_partition
	)

#include <spot/twaalgos/mtdswa.hh>

Minimization of MTDSwA.

This is called minimization because it implements a variant of Moore's partition-refinement algorithms (that is normally used to minimize DFAs). However for general deterministic ω-automata, this does not guarantee minimality.

One exception is weak deterministic ω-automata, which can be minimized precisely if they are first preprocessed with loding_weak_ranking().

The implementation of this minimization currently is unable to merge states with any bddfalse or bddtrue constant. You can work around this by converting constants to states before minimizing, and possibly back to constants afterwards:

dfa->sinks_as_states();
dfa = minimize_mtdsw(dfa);
dfa->sinks_as_constants();  // if really needed

By default, the initial partition is based on the colors that label each state. If you know a better one, you can pass it as initial_partition.

mtdswa_strategy_to_mealy()

twa_graph_ptr spot::mtdswa_strategy_to_mealy	(	mtdswa_ptr	strategy,
		bool	labels = true,
		bool	loop = false
	)

#include <spot/twaalgos/mtdswa.hh>

Convert a strategy represented as MTDSwA into a Mealy machine.

If loop is set, a strategy reaching bddtrue will instead loop on the last assignment.

obligation_synthesis()

mtdswa_ptr spot::obligation_synthesis	(	formula	f,
		const bdd_dict_ptr &	dict,
		const std::vector< std::string > &	outvars,
		bool	realizability = false,
		bool	simplify_terms = true,
		int	debug = -1
	)

#include <spot/twaalgos/mtdswa.hh>

Reactive synthesis of syntactic-obligations.

The dictionary passed to this function should have variables registered in the order needed by the semantics you wish to use. For Mealy semantics, input variables should be registered before output variables. For Moore semantics, output variables should be registered before input variables.

This function will register any missing variable, so it is actually enough to pre-register input variables for Mealy, and pre-register output variables for Moore.

The formula may also use quantified atomic propositions (∀ or ∃). The quantified variables should not be pre-registered in the dictionary.

The main translation and synthesis techniques is described by [duret.26.cav] and the support for quantification uses the technique described in [alon.26.kr]

obligation_to_mtdswa()

mtdswa_ptr spot::obligation_to_mtdswa	(	formula	f,
		const bdd_dict_ptr &	dict,
		bool	fuse_same_bdds = true,
		bool	simplify_terms = true
	)

#include <spot/twaalgos/mtdswa.hh>

Convert a syntactic-obligation to an MTDSwA.

The formula may use quantified atomic propositions (∀ or ∃).

The main translation (without quantification) is described by [duret.26.cav] and the support for quantification uses the technique described in [alon.26.kr]

product()

mtdswa_ptr spot::product	(	const mtdswa_ptr &	swa1,
		const mtdswa_ptr &	swa2
	)

#include <spot/twaalgos/mtdswa.hh>

Combine two MTDSwAs to intersect their languages.

product_implies()

mtdswa_ptr spot::product_implies	(	const mtdswa_ptr &	swa1,
		const mtdswa_ptr &	swa2
	)

#include <spot/twaalgos/mtdswa.hh>

Combine two MTDSwAs to build an implication.

The results will recognize words that are rejected by swa1 or accepted by swa2.

product_or()

mtdswa_ptr spot::product_or	(	const mtdswa_ptr &	swa1,
		const mtdswa_ptr &	swa2
	)

#include <spot/twaalgos/mtdswa.hh>

Combine two MTDSwAs to sum their languages.

product_xnor()

mtdswa_ptr spot::product_xnor	(	const mtdswa_ptr &	swa1,
		const mtdswa_ptr &	swa2
	)

#include <spot/twaalgos/mtdswa.hh>

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

The results will recognize words that are recognized by swa1 and swa2, or that are rejected by both.

product_xor()

mtdswa_ptr spot::product_xor	(	const mtdswa_ptr &	swa1,
		const mtdswa_ptr &	swa2
	)

#include <spot/twaalgos/mtdswa.hh>

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

The results will recognize words that are there only in one of swa1 or swa2. If the resulting automaton has an empty language, then the two input automata were equivalent.

quantify_exists() [1/3]

mtdswa_ptr spot::quantify_exists	(	const mtdswa_ptr &	swa,
		bdd	vars,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Existentially quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

quantify_exists() [2/3]

mtdswa_ptr spot::quantify_exists	(	const mtdswa_ptr &	swa,
		const formula &	ap,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Existentially quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

quantify_exists() [3/3]

mtdswa_ptr spot::quantify_exists	(	const mtdswa_ptr &	swa,
		const std::vector< formula > &	aps,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Existentially quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

quantify_forall() [1/3]

mtdswa_ptr spot::quantify_forall	(	const mtdswa_ptr &	swa,
		bdd	vars,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Universally quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

quantify_forall() [2/3]

mtdswa_ptr spot::quantify_forall	(	const mtdswa_ptr &	swa,
		const formula &	ap,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Universally quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

quantify_forall() [3/3]

mtdswa_ptr spot::quantify_forall	(	const mtdswa_ptr &	swa,
		const std::vector< formula > &	aps,
		bool	trim = true
	)

#include <spot/twaalgos/mtdswa.hh>

Universally quantify variables in a weak MTDSwA.

The second argument can be a positive cube of BDD variables, a single atomic proposition, or a vector of atomic propositions to remove from the automaton. Atomic propositions that are not registered in the automaton are silently ignored; if all of them are ignored, the automaton is returned unchanged.

scc_vector()

std::vector< int > spot::scc_vector	(	const mtdswa_ptr &	aut,
		std::vector< bool > *	transient = nullptr,
		std::vector< std::vector< int > > *	succs = nullptr
	)

#include <spot/twaalgos/mtdswa.hh>

Find the SCC of each state.

This builds a vector as large as the number of states in aut, and giving the SCC number each state belongs to. SCC are numbered in reverse topological order (the SCC of the initial state has the highest number among the reachable SCCs, and SCC with number 0 is a terminal/leaf SCC).

If transient is not null, it receives one entry per SCC number: TRANSIENT[S] is set iff SCC S is transient, i.e., it consists of a single state that has no successor inside the SCC.

If succs is not null, it receives one entry per SCC number: SUCCS[S] is the sorted list of the successors of SCC S, without duplicates. Successors are represented by their SCC number, except for the implicit sinks bddfalse and bddtrue, which are represented by ~bddfalse.id() and ~bddtrue.id() (i.e., -1 and -2).

trim()

void spot::trim	(	mtdswa_ptr	swa,
		bool	trim_useless_sccs_too = false
	)

#include <spot/twaalgos/mtdswa.hh>

Remove unnecessary states from an MTDSwA.

By default, this removes states that are unreachable from the initial state, and renumbers the remaining states. This is what one expects from a trim function.

If trim_useless_sccs_too is set, states from which acceptance or rejection is inevitable are also replaced by bddtrue or bddfalse respectively. In that case, the set of accessible states is deduced from the SCC numbers returned by bdd_mt_sccs: the SCC of state 0 has the largest index among the SCCs reachable from it, so any SCC with a larger index is unreachable. No separate reachability pass is needed.

This modifies the automaton in place.