A DFA with explicit states and symbolic transitions. More...

#include <ExplicitStateDfa.h>

Inheritance diagram for Syft::ExplicitStateDfa:

Collaboration diagram for Syft::ExplicitStateDfa:

Public Member Functions
	ExplicitStateDfa (DFA *dfa, int nb_variables)
	Create an explicit-state DFA from an Lydia DFA structure and the number of variables. More...

	ExplicitStateDfa (DFA *dfa, const std::vector< std::string > &names)
	Create an explicit-state DFA from an Lydia DFA structure and the names of variables. More...

	ExplicitStateDfa (const ExplicitStateDfa &other)
	Create an explicit-state DFA from an existing one.

ExplicitStateDfa &	operator= (ExplicitStateDfa other)
	Create an explicit-state DFA from an existing one using the opeartor =.

int	get_nb_variables ()
	Get the number of variables.

void	dfa_print ()
	Print the explicit-state DFA.

Static Public Member Functions
static ExplicitStateDfa	dfa_of_formula (const whitemech::lydia::LTLfFormula &formula)
	Construct an explicit-state DFA from a given formula using Lydia. More...

static ExplicitStateDfa	dfa_product_and (const std::vector< ExplicitStateDfa > &dfa_vector)
	Take the product AND of a sequence of explicit-state DFAs. More...

static ExplicitStateDfa	dfa_product_or (const std::vector< ExplicitStateDfa > &dfa_vector)
	Take the product OR of a sequence of explicit-state DFAs. More...

static ExplicitStateDfa	dfa_minimize (const ExplicitStateDfa &d)
	Minimize a given explicit-state DFA. More...

static ExplicitStateDfa	restrict_dfa_with_states (ExplicitStateDfa &d, std::vector< size_t > states)
	Restrict an explicit-state DFA with a given set of states. More...

static ExplicitStateDfa	restrict_dfa_with_transitions (ExplicitStateDfa &d, std::unordered_map< size_t, CUDD::BDD > transitions, std::shared_ptr< VarMgr > var_mgr)
	Restrict a DFA with a given set of transitions. More...

static ExplicitStateDfa	dfa_complement (ExplicitStateDfa &d)
	Complement a DFA. More...

Detailed Description

A DFA with explicit states and symbolic transitions.

The LTLf-to-DFA construction utilizes Lydia. Giuseppe De Giacomo, Marco Favorito: Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata. ICAPS 2021: 122-130

Constructor & Destructor Documentation

◆ ExplicitStateDfa() [1/2]

Syft::ExplicitStateDfa::ExplicitStateDfa	(	DFA *	dfa,
		int	nb_variables
	)

inline

Create an explicit-state DFA from an Lydia DFA structure and the number of variables.

Parameters

dfa	A Lydia DFA structure.
nb_variables	The number of variables in the Lydia DFA.

◆ ExplicitStateDfa() [2/2]

Syft::ExplicitStateDfa::ExplicitStateDfa	(	DFA *	dfa,
		const std::vector< std::string > &	names
	)

inline

Create an explicit-state DFA from an Lydia DFA structure and the names of variables.

Parameters

dfa	A Lydia DFA structure.
names	The names of the variables in the Lydia DFA.

Member Function Documentation

◆ dfa_complement()

ExplicitStateDfa Syft::ExplicitStateDfa::dfa_complement ( ExplicitStateDfa & d )

static

Complement a DFA.

Basically exchange the accepting states and the non-accepting states.

Parameters

d	The DFA to be complemented.

Returns: The complement DFA.

◆ dfa_minimize()

ExplicitStateDfa Syft::ExplicitStateDfa::dfa_minimize ( const ExplicitStateDfa & d )

static

Minimize a given explicit-state DFA.

Parameters

d	The DFA to be minimized.

Returns: The minimal explicit-state DFA.

◆ dfa_of_formula()

ExplicitStateDfa Syft::ExplicitStateDfa::dfa_of_formula ( const whitemech::lydia::LTLfFormula & formula )

static

Construct an explicit-state DFA from a given formula using Lydia.

Parameters

formula An LTLf formula.

Returns: The corresponding explicit-state DFA.

◆ dfa_product_and()

ExplicitStateDfa Syft::ExplicitStateDfa::dfa_product_and ( const std::vector< ExplicitStateDfa > & dfa_vector )

static

Take the product AND of a sequence of explicit-state DFAs.

Parameters

dfa_vector The DFAs to be processed.

Returns: The product explicit-state DFA, which is also minimized.

◆ dfa_product_or()

ExplicitStateDfa Syft::ExplicitStateDfa::dfa_product_or ( const std::vector< ExplicitStateDfa > & dfa_vector )

static

Take the product OR of a sequence of explicit-state DFAs.

Parameters

dfa_vector The DFAs to be processed.

Returns: The product explicit-state DFA, which is also minimized.

◆ restrict_dfa_with_states()

ExplicitStateDfa Syft::ExplicitStateDfa::restrict_dfa_with_states	(	ExplicitStateDfa &	d,
		std::vector< size_t >	states
	)

static

Restrict an explicit-state DFA with a given set of states.

Basically restrict a DFA to a set of states from the DFA, and return a minimized one.

Parameters

d	The DFA to be restricted.
states	The set of states to be kept.

Returns: The restricted explicit-state DFA, which is also minimized.

◆ restrict_dfa_with_transitions()

ExplicitStateDfa Syft::ExplicitStateDfa::restrict_dfa_with_transitions	(	ExplicitStateDfa &	d,
		std::unordered_map< size_t, CUDD::BDD >	transitions,
		std::shared_ptr< VarMgr >	var_mgr
	)

static

Restrict a DFA with a given set of transitions.

Basically restrict a DFA to a set of transitions, and return a minimized one.

Parameters

d	The DFA to be restricted.
transitions	The set of transitions to be kept.

Returns: The restricted explicit-state DFA, which is also minimized.

The documentation for this class was generated from the following files:

src/synthesis/header/automata/ExplicitStateDfa.h
src/synthesis/source/automata/ExplicitStateDfa.cpp

Public Member Functions

Static Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ ExplicitStateDfa() [1/2]

◆ ExplicitStateDfa() [2/2]

Member Function Documentation

◆ dfa_complement()

◆ dfa_minimize()

◆ dfa_of_formula()

◆ dfa_product_and()

◆ dfa_product_or()

◆ restrict_dfa_with_states()

◆ restrict_dfa_with_transitions()