FDR::Assertions::DeadlockFreeAssertion Class Reference

An assertion that a process is deadlock free. More...

#include <deadlock_free_assertion.h>

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

List of all members.

Public Member Functions

 DeadlockFreeAssertion (const DeadlockFreeAssertion &assertion)
 DeadlockFreeAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model)
 Construct a new deadlock-freedom assertion.
DeadlockFreeAssertionoperator= (const DeadlockFreeAssertion &assertion)

Friends

struct AssertionFactory

Detailed Description

An assertion that a process is deadlock free.


Constructor & Destructor Documentation

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

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