FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
A counterexample demonstrating how a trace refinement check failed. More...
#include <trace_counterexample.h>
Public Member Functions | |
TraceCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation) | |
LTS::CompiledEvent | error_event () const |
The event the implementation performed the specification could not. | |
![]() | |
const std::shared_ptr< Behaviour > & | implementation_behaviour () const |
The behaviour of the implementation process. | |
const std::shared_ptr< Behaviour > & | specification_behaviour () const |
The behaviour of the specification process. | |
![]() | |
Counterexample (const Counterexample &)=delete | |
Counterexample & | operator= (const Counterexample &)=delete |
Additional Inherited Members | |
![]() | |
RefinementCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation) | |
A counterexample demonstrating how a trace refinement check failed.
In this case the specification Behaviour is guaranteed to be a LTS::Behaviour::Irrelevant, whilst the implementation Behaviour is guaranteed to be a LTS::Behaviour::Trace.