FDR::LTS::Machine Class Reference

A compiled state machine (a GLTS). More...

#include <machine.h>

Public Member Functions
	Machine (const Machine &)=delete
virtual std::vector< std::shared_ptr< Node > >	afters (const Node &node, const CompiledEvent event) const =0
	The set of states reachable from the given node via the given event. More...
virtual std::vector< CompiledEvent >	alphabet (bool include_tau) const =0
	Returns the set of events used by this Machine. More...
virtual bool	has_divergence_labellings () const =0
	Does this GLTS have explicit divergence labels. More...
virtual bool	has_minimal_acceptance_labellings () const =0
	Does this GLTS have explicit minimal acceptance labels. More...
virtual std::vector< CompiledEvent >	initials (const Node &node) const =0
	The set of events that the node can perform immediately. More...
virtual bool	is_divergent (const Node &node, Canceller *canceller) const =0
	True if the state is considered to diverge. More...
virtual bool	is_explicitly_divergent (const Node &node) const =0
	Is the state labelled as explicitly divergent.
virtual std::vector< std::vector< CompiledEvent > >	minimal_acceptances (const Node &node) const =0
	The set of minimal acceptances of the given node. More...
Machine &	operator= (const Machine &machine)=delete
virtual std::shared_ptr< Node >	root_node () const =0
	Returns the root, i.e. initial, node of this state machine.
virtual std::vector< Transition >	transitions (const Node &node) const =0
	The transitions available from the given node.

Detailed Description

A compiled state machine (a GLTS).

Note that the methods that are used to visit transitions of this machine are not high-performance. If you are interested in such an interface please contact us.

This MUST not be subclassed.

Member Function Documentation

afters()

virtual std::vector<std::shared_ptr<Node> > FDR::LTS::Machine::afters ( const Node &  node, const CompiledEvent  event  ) const

pure virtual

The set of states reachable from the given node via the given event.

Parameters

node	The node to return the afters of. If this node is not a node of this machine, the result is undefined.
event	The event for which destinations are required. Must not be LTS::INVALID_EVENT.

alphabet()

virtual std::vector<CompiledEvent> FDR::LTS::Machine::alphabet ( bool  include_tau ) const

pure virtual

Returns the set of events used by this Machine.

This set contains at least all of those events that are performable in some reachable state, but under some circumstances, may also include events that were in the definition of the machine, but are not performable in any reachable state.

Parameters

include_tau

If true tau will be included in the alphabet, if tau can be performed by this machine.

Returns

A set representing the alphabet.

has_divergence_labellings()

virtual bool FDR::LTS::Machine::has_divergence_labellings ( ) const

pure virtual

Does this GLTS have explicit divergence labels.

If this is false, is_explicitly_divergent will always be false.

has_minimal_acceptance_labellings()

virtual bool FDR::LTS::Machine::has_minimal_acceptance_labellings ( ) const

pure virtual

Does this GLTS have explicit minimal acceptance labels.

If this is false, minimal_acceptances will return {initials} if initials contains no tau, and {} otherwise.

initials()

virtual std::vector<CompiledEvent> FDR::LTS::Machine::initials ( const Node &  node ) const

pure virtual

The set of events that the node can perform immediately.

Parameters

node	The node to return the initials of. If this node is not a node of this machine, the result is undefined.

is_divergent()

virtual bool FDR::LTS::Machine::is_divergent ( const Node &  node, Canceller *  canceller  ) const

pure virtual

True if the state is considered to diverge.

This will either be because the node is explicitly divergent and this machine has divergence labellings, or because there is a cycle of taus reachable from this state via other taus.

Parameters

node	The node to test for divergence.
canceller	Since this is a long running operation, an optional canceller may be provided to prematurely terminate computation.

Exceptions

CancelledError

if the computation is cancelled before a result is computed.

minimal_acceptances()

virtual std::vector<std::vector<CompiledEvent> > FDR::LTS::Machine::minimal_acceptances ( const Node &  node ) const

pure virtual

The set of minimal acceptances of the given node.

Note that if has_minimal_acceptance_labellings() is false, then this is equal to {initials()} providing initials() does not contain a tau, and is equal to {} if it does contain a tau.

Parameters

node	The node to return the minimal acceptances of. If this node is not a node of this machine, the result is undefined.

---

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

• libfdr/include/fdr/lts/machine.h