FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
A counterexample demonstrating non determinism in a process. More...
#include <determinism_counterexample.h>
Public Member Functions | |
DeterminismCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation) | |
![]() | |
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 non determinism in a process.
A determinism assertion can fail for two reasons:
In this case the specification Behaviour is guaranteed to be a LTS::Behaviour::Irrelevant (since the specification is an internal FDR process), whilst the implementation Behaviour is guaranteed to be a LTS::Behaviour::MinAcceptance.