An assertion that the given machine is deterministic. More...
#include <deterministic_assertion.h>
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. | |
DeterministicAssertion & | operator= (const DeterministicAssertion &assertion) |
Friends | |
struct | AssertionFactory |
An assertion that the given machine is deterministic.
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.
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. |