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. |
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.