FDR::Assertions::DivergenceFreeAssertion Class Reference

An assertion that the given machine is divergence free. More...

#include <divergence_free_assertion.h>

Inheritance diagram for FDR::Assertions::DivergenceFreeAssertion:
Inheritance graph
[legend]
Collaboration diagram for FDR::Assertions::DivergenceFreeAssertion:
Collaboration graph
[legend]

List of all members.

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.
DivergenceFreeAssertionoperator= (const DivergenceFreeAssertion &assertion)

Friends

struct AssertionFactory

Detailed Description

An assertion that the given machine is divergence free.


Constructor & Destructor Documentation

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.

Parameters:
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.

The documentation for this class was generated from the following file:
 All Classes Functions

Generated on 27 Oct 2017 for FDR by  doxygen 1.6.1