FDR::LTS::Machine Class Reference

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

#include <machine.h>

List of all members.

Public Member Functions

 Machine (const Machine &)
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.
virtual std::vector
< CompiledEvent > 
alphabet (bool include_tau) const =0
 Returns the set of events used by this Machine.
virtual bool has_divergence_labellings () const =0
 Does this GLTS have explicit divergence labels.
virtual bool has_minimal_acceptance_labellings () const =0
 Does this GLTS have explicit minimal acceptance labels.
virtual std::vector
< CompiledEvent > 
initials (const Node &node) const =0
 The set of events that the node can perform immediately.
virtual bool is_divergent (const Node &node, Canceller *canceller) const =0
 True if the state is considered to diverge.
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.
Machineoperator= (const Machine &machine)
virtual std::shared_ptr< Noderoot_node () const =0
 Returns the root, i.e. initial, node of this state machine.
virtual std::vector< Transitiontransitions (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

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.
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.
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.

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.

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.
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.
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:
 All Classes Functions

Generated on 27 Oct 2017 for FDR by  doxygen 1.6.1