LTS< Tran > Class Template Reference

Class of labeled transition systems. More...

#include <LTS.hh>

Classes
class	PartitionRefinement
	Class to compute partition refinement for the states of an LTS. More...
class	SccAnalyzer
	Class to compute the (maximal) SCCs of the LTS. More...
class	SubsetConstruction
	Helper class to perform Rabin-Scott subset construction. More...

Public Types
using	Transition = Tran
using	Edge = std::pair< State, Transition >
using	EdgeSet = std::set< Edge >
using	Delta = std::vector< Transition >
using	PairsStateBdd = std::set< std::pair< State, BDD >, Util::PairWithBddCompare< State > >
	Type of sets of pairs of state and BDD.
using	const_iterator = std::vector< State >::const_iterator
	Constant iterator type.
using	SCCs = std::vector< StateSet >
	Type of the collection of SCCs.

Public Member Functions
const_iterator	cbegin ()
	Returns a const_iterator pointing to the first state.
const_iterator	cend ()
	Returns a const_iterator pointing "just past the last" state.
	LTS (Cudd mgr)
	Constructor.
size_t	numStates (void) const
	Returns the number of states in the LTS.
Cudd	getManager (void) const
	Returns the BDD manager of the LTS.
void	addState (State s, Delta delta=Delta{})
	Adds a state to the LTS.
void	addTransition (State source, State destination, BDD const &label)
	Adds a transition to a state of the LTS.
void	makeInitial (State s)
	Makes a state initial.
State	getInitial (void) const
	Returns the initial state of the LTS.
void	addAtomicProposition (BDD proposition, std::string name)
	Adds atomic proposition to model.
std::string	getPropositionName (BDD proposition) const
	Returns name of an atomic proposition.
std::set< BDD, Util::BddCompare >	getAtomicPropositions (void) const
	Returns the set of atomic propositions.
State	getSuccessor (State source, BDD letter) const
	Returns successor of source state for input letter in deterministic LTS.
StateSet	getSuccessors (State source, BDD letter) const
	Returns states reachable from source for input letter.
StateSet	getEpsilonSuccessors (State source) const
	Returns states reachable from source via epsilon transitions.
bool	checkTransitions (void) const
	Checks sanity of transitions.
void	print (std::ostream &os=std::cout) const
	Stream insertion operator helper function.
void	letters (StateSet const &stateset, std::vector< BDD > &lv) const
	Returns the letters in the labels of a set of states. More...
std::vector< BDD >	getLetters (std::vector< State > const &statevec) const
	Alternate interface to letters.
int	readVerbosity (void) const
	Returns the verbosity level of the LTS.
void	setVerbosity (int v)
	Sets the verbosity level of the LTS.
bool	isDeterministic (bool complete=true) const
	Checks whether the LTS is deterministic.
bool	isComplete (void) const
	Checks whether the LTS is complete.
SCCs	getSCCs (StateSet const &init, StateSet const &restriction, EdgeSet const &forbiddenEdges) const
	Computes the SCCs reachable from init and contained in restriction.
SCCs	getSCCs (StateSet const &init, StateSet const &restriction) const
	Computes the SCCs reachable from init and contained in restriction.
SCCs	getSCCs (StateSet const &restriction) const
	Computes the SCCs of the LTS contained in restriction.
SCCs	getSCCs (void) const
	Computes the SCCs of the LTS.
void	findTransient (std::vector< State > &transient, StateSet const &init, StateSet const &restriction) const
	Finds transient states of LTS reachable from init and contained in restriction.
void	findTransient (std::vector< State > &transient, StateSet const &restriction) const
	Finds transient states of LTS contained in restriction.
void	findTransient (std::vector< State > &transient) const
	Finds transient states of LTS.
std::map< State, State >	stateEquivalence (std::map< State, unsigned > const &outputClass) const
	Returns state equivalence relation.
void	trim (StateSet const &targets)
	Removes states with no path to target states.
void	trim (StateSet const &targets, SCCs const &sccs)
	Removes states with no path to target states. More...
void	printDot (std::string graphname=std::string("LTS")) const
	Writes LTS in dot format.
LTS	subsetsLTS (std::map< State, StateSet > &subsets) const
	Returns the result of the Rabin-Scott subset construction.
void	setEpsilonBDD (BDD const &e)
	Sets the epsilon proposition for LDBWs.
const BDD &	getEpsilonBDD (void) const
	Gets the epsilon proposition for LDBWs.
bool	hasEpsilonTransitions (void) const
	Checks whether there exist epsilon transitions.
LTS	product (LTS const &second)
	Returns the synchronous product of two LTSs.

Protected Types
using	TransitionMap = std::map< State, Delta >

Protected Member Functions
void	mergeTransitions (void)
	Merge transitions that differ at most in their labels.
bool	isTrivial (StateSet const &scc, EdgeSet const &forbidden=EdgeSet{}) const
	Check whether an SCC is trivial.
void	pruneVarSet (void)
	Prune the variable set of unused atomic propositions.

Protected Attributes
Cudd	mgr
int	verbosity
std::vector< State >	states
State	initialState
TransitionMap	transitions
std::set< BDD, Util::BddCompare >	varSet
BDD	epsilon

Detailed Description

template<typename Tran>
class LTS< Tran >

Class of labeled transition systems.

Automata classes extend this class by adding an acceptance condition.

Member Function Documentation

letters()

template<typename Tran >

void LTS< Tran >::letters	(	StateSet const &	stateset,
		std::vector< BDD > &	lv
	)		const

Returns the letters in the labels of a set of states.

Extract the letters of the transitions out of a set of states.

The objective is to find the letters from the smallest possible alphabet. If the automaton has inputs p, q, and r, it may still be that no transition out of the given states depends on r. Besides, all transitions may have labels of the forms (p&q) or !(p&q).

trim()

template<typename Tran >

void LTS< Tran >::trim	(	StateSet const &	targets,
		SCCs const &	sccs
	)

Removes states with no path to target states.

Uses previously computed SCCs.

---

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

• LTS/LTS.hh
• LTS/LTS.cc