FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
property_counterexample.h
1 #pragma once
2 
3 #include <fdr/assertions/counterexample/counterexample.h>
4 #include <fdr/assertions/behaviour/behaviour.h>
5 
6 namespace FDR
7 {
8 namespace Assertions
9 {
15 {
16 public:
18  const std::shared_ptr<Behaviour>& behaviour() const;
19 
20 protected:
21  PropertyCounterexample(const std::shared_ptr<Behaviour>& behaviour);
22 
23 private:
24  std::shared_ptr<Behaviour> behaviour_;
25 };
26 
27 } // end Assertions
28 } // end FDR
FDR::Assertions::PropertyCounterexample
A counterexample to a property assertion, such as deadlock freedom.
Definition: property_counterexample.h:15
FDR::Assertions::PropertyCounterexample::behaviour
const std::shared_ptr< Behaviour > & behaviour() const
The prohibited behaviour.
FDR::Assertions::Counterexample
A reason why an Assertion fails.
Definition: counterexample.h:16