FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
A path that is irrelevant to debugging the current counterexample. More...
#include <irrelevant_behaviour.h>
Public Member Functions | |
IrrelevantBehaviour (const std::shared_ptr< LTS::Machine > &machine, const std::vector< std::shared_ptr< LTS::Node >> &node_path, const std::vector< LTS::CompiledEvent > &trace) | |
![]() | |
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 path that is irrelevant to debugging the current counterexample.
For example, in assert STOP [T= STOP ||| a -> STOP, the STOP on the left hand side of the interleave is irrelevant to the failure of the assertion, and thus is represented using an IrrelevantBehaviour.
This also comes up as the beahviour of the specification process.