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

#include <SymbolicStateDfa.h>

Public Member Functions
std::shared_ptr< VarMgr >	var_mgr () const
	Returns the variable manager.

std::size_t	automaton_id () const
	Returns the automaton ID. More...

std::vector< int >	initial_state () const
	Returns the bitvector representing the initial state of the DFA.

CUDD::BDD	initial_state_bdd () const
	Returns the BDD representing the initial state of the DFA.

CUDD::BDD	final_states () const
	Returns the BDD encoding the set of final states.

std::vector< CUDD::BDD >	transition_function () const
	Returns the transition function of the DFA as a vector of BDDs. More...

void	restrict_dfa_with_states (const CUDD::BDD &valid_states)
	Restrict a symbolic DFA with a given set of states. More...

void	restrict_dfa_with_transitions (const CUDD::BDD &feasible_moves)
	Restrict a symbolic DFA with a set of feasible moves. More...

void	dump_dot (const std::string &filename) const
	Saves the symbolic representation of the DFA in a .dot file. More...

void	new_sink_states (const CUDD::BDD &sink_states)
	Shrink a set of states to a sink state. More...

Static Public Member Functions
static SymbolicStateDfa	from_explicit (const ExplicitStateDfaAdd &explicit_dfa)
	Converts an explicit DFA to a symbolic representation. More...

static SymbolicStateDfa	from_predicates (std::shared_ptr< VarMgr > var_mgr, std::vector< CUDD::BDD > predicates)
	Creates a simple automaton that remembers the value of predicates. More...

static SymbolicStateDfa	product_AND (const std::vector< SymbolicStateDfa > &dfa_vector)
	Returns a product AND of two symbolic DFAs. More...

static std::vector< int >	state_to_binary (std::size_t state, std::size_t bit_count)
	Returns the binary encoding of a given state index. More...

static SymbolicStateDfa	product_OR (const std::vector< SymbolicStateDfa > &dfa_vector)
	Returns a product AND of two symbolic DFAs. More...

static SymbolicStateDfa	complement (const SymbolicStateDfa dfa)
	Returns the complement of a symbolic DFA. More...

Detailed Description

A DFA with symbolic states and transitions.

Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi: Symbolic LTLf Synthesis. IJCAI 2017: 1362-1369

Member Function Documentation

◆ automaton_id()

std::size_t Syft::SymbolicStateDfa::automaton_id ( ) const

Returns the automaton ID.

This ID can be used to retrieve the associated state variables from the variable manager.

◆ complement()

SymbolicStateDfa Syft::SymbolicStateDfa::complement ( const SymbolicStateDfa dfa )

static

Returns the complement of a symbolic DFA.

Parameters

dfa	The DFA to be complemented.

Returns: A symbolic DFA of the complement.

◆ dump_dot()

void Syft::SymbolicStateDfa::dump_dot ( const std::string & filename ) const

Saves the symbolic representation of the DFA in a .dot file.

The file includes both the BDDs representing the transition function and the BDD representing the final states.

Parameters

filename The name of the file to save the symbolic DFA to.

◆ from_explicit()

SymbolicStateDfa Syft::SymbolicStateDfa::from_explicit ( const ExplicitStateDfaAdd & explicit_dfa )

static

Converts an explicit DFA to a symbolic representation.

Encodes the state space of the DFA in a logarithmic number of state variables, using BDDs to represent the transition function and the set of final states.

Parameters

explicit_dfa The explicit DFA to be converted.

Returns: The symbolic representation of the DFA.

◆ from_predicates()

SymbolicStateDfa Syft::SymbolicStateDfa::from_predicates	(	std::shared_ptr< VarMgr >	var_mgr,
		std::vector< CUDD::BDD >	predicates
	)

static

Creates a simple automaton that remembers the value of predicates.

Parameters

var_mgr	The variable manager to use to create the state variables.
predicates	A vector of BDDs over named variables representing the predicates to remember.

Returns: A symbolic DFA with one state variable for each predicate. The i-th state variable records whether predicates[i] was true in the last step. The initial state has all state variables set to 0. All states are accepting states.

◆ new_sink_states()

void Syft::SymbolicStateDfa::new_sink_states ( const CUDD::BDD & sink_states )

Shrink a set of states to a sink state.

Parameters

sink_states The set of states to shrink.

◆ product_AND()

SymbolicStateDfa Syft::SymbolicStateDfa::product_AND ( const std::vector< SymbolicStateDfa > & dfa_vector )

static

Returns a product AND of two symbolic DFAs.

Parameters

first_dfa	The first DFA.
second_dfa	The second DFA.

Returns: A symbolic DFA of the product AND.

◆ product_OR()

SymbolicStateDfa Syft::SymbolicStateDfa::product_OR ( const std::vector< SymbolicStateDfa > & dfa_vector )

static

Returns a product AND of two symbolic DFAs.

Parameters

first_dfa	The first DFA.
second_dfa	The second DFA.

Returns: A symbolic DFA of the product OR.

◆ restrict_dfa_with_states()

void Syft::SymbolicStateDfa::restrict_dfa_with_states ( const CUDD::BDD & valid_states )

Restrict a symbolic DFA with a given set of states.

Basically restrict a DFA to a set of states from the DFA.

Parameters

valid_states The set of states to be kept.

Returns: The restricted symbolic DFA.

◆ restrict_dfa_with_transitions()

void Syft::SymbolicStateDfa::restrict_dfa_with_transitions ( const CUDD::BDD & feasible_moves )

Restrict a symbolic DFA with a set of feasible moves.

Parameters

feasible_moves The set of feasible moves to be kept.

Returns: The restricted symbolic DFA.

◆ state_to_binary()

std::vector< int > Syft::SymbolicStateDfa::state_to_binary	(	std::size_t	state,
		std::size_t	bit_count
	)

static

Returns the binary encoding of a given state index.

Parameters

state	The state index.
bit_count	The number of bits in the binary encoding DFA.

Returns: The binary encoding.

◆ transition_function()

std::vector< CUDD::BDD > Syft::SymbolicStateDfa::transition_function ( ) const

Returns the transition function of the DFA as a vector of BDDs.

The BDD in index i computes the value of state variable i in the next step, given the current values of the state and alphabet variables.

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

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

Public Member Functions

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ automaton_id()

◆ complement()

◆ dump_dot()

◆ from_explicit()

◆ from_predicates()

◆ new_sink_states()

◆ product_AND()

◆ product_OR()

◆ restrict_dfa_with_states()

◆ restrict_dfa_with_transitions()

◆ state_to_binary()

◆ transition_function()