FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
A counterexample to a refinement assertion. More...
#include <refinement_counterexample.h>
Public Member Functions | |
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 |
Protected Member Functions | |
RefinementCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation) | |
A counterexample to a refinement assertion.
This has two behaviours. Generally, the specification behaviour is not of interest (the only exception is when the counterexample is a Counterexample::Divergence), whilst the implementation behaviour exhibits some behaviour of the implementation that is not allowed by the specification process (e.g. an event the implementation can perform that the specification cannot, in the case of a trace behaviour).