FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
A behaviour of a machine that has been executed several times. More...
#include <segmented_behaviour.h>
Public Member Functions | |
SegmentedBehaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &trace, const std::shared_ptr< Behaviour > &behaviour, const std::vector< std::shared_ptr< TraceBehaviour >> &prior_sections) | |
std::shared_ptr< Behaviour > | last () const |
The actual erroneous behaviour, which is the very last segment. | |
std::vector< std::shared_ptr< TraceBehaviour > > | prior_sections () const |
The segments that lead up to last(). More... | |
![]() | |
Behaviour (const Behaviour &)=delete | |
std::shared_ptr< LTS::Machine > | machine () 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... | |
Behaviour & | operator= (const Behaviour &)=delete |
const std::vector< LTS::CompiledEvent > & | trace () const |
Returns the sequence of events that led to this behaviour. More... | |
Additional Inherited Members | |
![]() | |
Behaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &events) | |
A behaviour of a machine that has been executed several times.
For example consider the process loop(P) where loop(P) = P ; loop(P). Clearly, it is possible for a Behaviour to require P to be executed multiple times. Any such Behaviour will be represented by a SegmentedBehaviour, where each segment is actually a TraceBehaviour, where TraceBehaviour::error_event() indicates the event that causes the next segment to be started (in the above case it would be tick, indicating termination). The actual erroroneous behaviour is stored in last(), which could be a MinAcceptanceBehaviour etc (but is guaranteed not to be a SegmentedBehaviour itself).
std::vector<std::shared_ptr<TraceBehaviour> > FDR::Assertions::SegmentedBehaviour::prior_sections | ( | ) | const |
The segments that lead up to last().
Each segment is a TraceBehaviour whose TraceBehaviour::error_event() indicates how the next segment is started.