Classes
class	AdequateOrder

class	BoundedNet
	n-bounded Petri nets More...

class	BranchingProcess
	This class implements a branching process of a Net (see Esparza 2002). More...

class	Chronicle

class	Configuration
	A Configuration caracterises a configuration of a BranchingProcess. More...

class	DdNet

class	Diagnosis

class	Extension

class	ExtensionEquality

class	Extensions
	list of Extension objects More...

class	LabelledNet

class	LabelledPrioritizedNet

class	LabelledPrioritizedTimeNet

class	Marking

class	MarkingGraph

class	MarkingTable

class	Net
	1-bounded Petri nets More...

class	Observations

class	ObservedSystem

class	Pattern

class	PetriEventManager

class	PriorityPetriNet

class	ReachabilityGraph

class	RealTimeSystem

class	RealTimeSystemPattern

class	System

class	SystemPattern

class	TimeDecomposedTransition

class	TimeNet

class	TimeReachabilityGraph

class	TwinPattern

class	TwinRealTimeSystemPattern

class	Vdd

class	VddFactory

class	VddInvalid

class	Zsl

class	ZslFactory

class	ZslInvalid

Typedefs
typedef Diades::Graph::Node	Place

typedef Diades::Graph::Node	Transition

typedef Diades::Graph::Edge	Arc

Functions
void	automataConversion (const std::vector< std::reference_wrapper< const ObservableComponent > > &automata, const SynchronisationRules &sync, Net &result)

template<typename ConstReferenceIterator >
void	automataConversion (ConstReferenceIterator begin, ConstReferenceIterator end, const SynchronisationRules &sync, Net &result)

bool	loadDdNet (const string &filename, DdNet &net)

bool	loadLabelledPrioritizedNet (const string &filename, LabelledPrioritizedNet &net)

template<typename Minimal >
void	unfold (const Net &netSystem, Net &completePrefix)

template<typename Minimal >
Transition &	next (const Net &netSystem, Net &completePrefix)

Typedef Documentation

◆ Arc

typedef Diades::Graph::Edge Diades::Petri::Arc

An PetriNet Arc is encoded as an Diades::Graph::Edge in a Diades::Graph::Graph

Definition at line 39 of file BoundedNet.hh.

◆ Place

typedef Diades::Graph::Node Diades::Petri::Place

A Place is encoded as a Diades::Graph::Node in a Diades::Graph::Graph

Definition at line 24 of file BoundedNet.hh.

◆ Transition

typedef Diades::Graph::Node Diades::Petri::Transition

A Transition is encoded as a Diades::Graph::Node in a Diades::Graph::Graph

Definition at line 31 of file BoundedNet.hh.

Function Documentation

◆ automataConversion() [1/2]

void Diades::Petri::automataConversion	(	const std::vector< std::reference_wrapper< const ObservableComponent > > &	automata,
		const SynchronisationRules &	sync,
		Net &	result
	)

Parameters

automata	vector of ObservableComponent references
sync	synchronisation rules to synchronize the range of components
result	a marked Petri net whose marking graph is equivalent to the synchronized product of the range of components.

Referenced by automataConversion().

◆ automataConversion() [2/2]

template<typename ConstReferenceIterator >

void Diades::Petri::automataConversion	(	ConstReferenceIterator	begin,
		ConstReferenceIterator	end,
		const SynchronisationRules &	sync,
		Net &	result
	)

Automata conversion

Parameters

begin	beginning of the automata range
end	end of the automata range
sync	synchronisation rules to synchronize the range of automata [begin,end(
result	a marked Petri net whose marking graph is equivalent to the synchronized product of the range of automata.

Definition at line 52 of file AutomataConversion.hh.

References automataConversion().

◆ loadDdNet()

bool Diades::Petri::loadDdNet	(	const string &	filename,
		DdNet &	net
	)

◆ loadLabelledPrioritizedNet()

bool Diades::Petri::loadLabelledPrioritizedNet	(	const string &	filename,
		LabelledPrioritizedNet &	net
	)

◆ next()

template<typename Minimal >

Transition& Diades::Petri::next	(	const Net &	netSystem,
		Net &	completePrefix
	)

Definition at line 24 of file Unfolding.hh.

Referenced by Diades::Petri::Zsl::valid().

◆ unfold()