FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | Protected Member Functions | Friends | List of all members
FDR::Assertions::Behaviour Class Reference

A particular path through a Machine, often leading to an interesting state. More...

#include <behaviour.h>

Inheritance diagram for FDR::Assertions::Behaviour:
Inheritance graph
[legend]

Public Member Functions

 Behaviour (const Behaviour &)=delete
 
std::shared_ptr< LTS::Machinemachine () const
 The machine in which the behaviour occurs.
 
const std::vector< std::shared_ptr< LTS::Node > > & node_path () const
 The sequence of nodes leading to the behaviour. More...
 
Behaviouroperator= (const Behaviour &)=delete
 
const std::vector< LTS::CompiledEvent > & trace () const
 Returns the sequence of events that led to this behaviour. More...
 

Protected Member Functions

 Behaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &events)
 

Friends

struct BehaviourFactory
 
class DebugContext
 

Detailed Description

A particular path through a Machine, often leading to an interesting state.

A behaviour represents a single path in the state machine such that the last state exhibits something interesting. For example, if this Behaviour is actually a TraceBehaviour, then this means that last state can perform a particular event. If this TraceBehaviour came from a trace refinement assertion, then this means that the event was not allowed by the specification.

Member Function Documentation

◆ node_path()

const std::vector<std::shared_ptr<LTS::Node> >& FDR::Assertions::Behaviour::node_path ( ) const

The sequence of nodes leading to the behaviour.

This includes the node at which the behaviour occurs. If node_path()[i] is null there are three possible reasons:

  1. The machine did not perform an event, i.e. trace()[i-1] == LTS::INVALID_EVENT.
  2. The node cannot be represented. This can occasionally happen when unwinding compressions.
  3. The machine has not been turned on yet. For example, consider the process P = Q ; R. A behaviour of P has two sub-behaviours, and the behaviour for R will start with a null node because R is inactive (formally, off) until Q has terminated. In this case, trace()[j] == LTS::INVALID_EVENT for all j < i.

◆ trace()

const std::vector<LTS::CompiledEvent>& FDR::Assertions::Behaviour::trace ( ) const

Returns the sequence of events that led to this behaviour.

These are the events that cause transitions between different nodes in node_path(). Note that this can include LTS::INVALID_EVENT, which indicates that the machine did not perform any event.


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