An assertion that the given machine is divergence free. More...
#include <divergence_free_assertion.h>
Public Member Functions | |
DivergenceFreeAssertion (const DivergenceFreeAssertion &assertion) | |
DivergenceFreeAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model) | |
Construct a new divergence-freedom assertion. | |
DivergenceFreeAssertion & | operator= (const DivergenceFreeAssertion &assertion) |
Friends | |
struct | AssertionFactory |
An assertion that the given machine is divergence free.
FDR::Assertions::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.
session | The session associated with machine | |
machine | The machine to check. | |
model | The semantic model in which to perform the check. An exception may be thrown in Assertion::execute() if this is not a valid model for this assertion. |