FDR::Assertions::DeterministicAssertion Class Reference

An assertion that the given machine is deterministic. More...

#include <deterministic_assertion.h>

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

List of all members.

Public Member Functions

 DeterministicAssertion (const DeterministicAssertion &assertion)
 DeterministicAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model)
 Construct a new determinism assertion.
DeterministicAssertionoperator= (const DeterministicAssertion &assertion)

Friends

struct AssertionFactory

Detailed Description

An assertion that the given machine is deterministic.


Constructor & Destructor Documentation

FDR::Assertions::DeterministicAssertion::DeterministicAssertion ( const std::shared_ptr< Session > &  session,
const std::shared_ptr< LTS::Machine > &  machine,
const LTS::SemanticModel  model 
)

Construct a new determinism 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