FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
libfdr
include
fdr
assertions
counterexample
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
{
14
class
PropertyCounterexample
:
public
Counterexample
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
Generated on Mon May 11 2020 18:30:17 for FDR by
1.8.18