A counterexample demonstrating how a process can diverge during a refinement check. More...
#include <refinement_divergence_counterexample.h>
Public Member Functions | |
RefinementDivergenceCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation) |
A counterexample demonstrating how a process can diverge during a refinement check.
In this case the specification behaviour is guaranteed to be a IrrelevantBehaviour (ending in a non-divergent state of the specification), whilst the implementation behaviour is guaranteed to be a ExplicitDivergenceBehaviour or LoopBehaviour.