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

A Behaviour that indicates the machine performed a prohibited event. More...

#include <trace_behaviour.h>

Inheritance diagram for FDR::Assertions::TraceBehaviour:
Inheritance graph
[legend]
Collaboration diagram for FDR::Assertions::TraceBehaviour:
Collaboration graph
[legend]

Public Member Functions

 TraceBehaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &trace, const LTS::CompiledEvent error_event)
 
LTS::CompiledEvent error_event () const
 The event considered to be disallowed. More...
 
- Public Member Functions inherited from FDR::Assertions::Behaviour
 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...
 

Additional Inherited Members

- Protected Member Functions inherited from FDR::Assertions::Behaviour
 Behaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &events)
 

Detailed Description

A Behaviour that indicates the machine performed a prohibited event.

In this case, after performing trace(), the state machine can perform error_event() which was not allowed according to the current specification.

Member Function Documentation

◆ error_event()

LTS::CompiledEvent FDR::Assertions::TraceBehaviour::error_event ( ) const

The event considered to be disallowed.

This is an event that can be performed by the machine in the last node of node_path(). It is guaranteed not to be LTS::INVALID_EVENT.


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