FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
libfdr
include
fdr
assertions
divergence_free_assertion.h
1
#pragma once
2
3
#include <fdr/assertions/property_assertion.h>
4
5
namespace
FDR
6
{
7
namespace
Assertions
8
{
10
class
DivergenceFreeAssertion
:
public
PropertyAssertion
11
{
12
public
:
20
DivergenceFreeAssertion
(
const
std::shared_ptr<Session>& session,
const
std::shared_ptr<LTS::Machine>&
machine
,
21
const
LTS::SemanticModel model);
22
~
DivergenceFreeAssertion
();
23
24
DivergenceFreeAssertion
(
const
DivergenceFreeAssertion
& assertion) =
delete
;
25
DivergenceFreeAssertion
& operator=(
const
DivergenceFreeAssertion
& assertion) =
delete
;
26
27
private
:
28
DivergenceFreeAssertion
();
29
30
friend
struct
AssertionFactory;
31
};
32
33
}
// end Assertions
34
}
// end FDR
FDR::Assertions::PropertyAssertion::machine
std::shared_ptr< LTS::Machine > machine() const
The process that this assertion is about.
FDR::Assertions::DivergenceFreeAssertion
An assertion that the given machine is divergence free.
Definition:
divergence_free_assertion.h:11
FDR::Assertions::PropertyAssertion
An assertion about processes.
Definition:
property_assertion.h:13
FDR::Assertions::DivergenceFreeAssertion::DivergenceFreeAssertion
DivergenceFreeAssertion(const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model)
Construct a new divergence-freedom assertion.
Generated on Mon May 11 2020 18:30:17 for FDR by
1.8.18