FDR::Assertions::PropertyAssertion Class Reference

An assertion about processes. More...

#include <property_assertion.h>

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

List of all members.

Public Member Functions

 PropertyAssertion (const PropertyAssertion &assertion)
std::shared_ptr< LTS::Machinemachine () const
 The process that this assertion is about.
PropertyAssertionoperator= (const PropertyAssertion &assertion)
LTS::SemanticModel semantic_model () const
 The semantic model this check has been performed in.

Friends

struct AssertionFactory

Detailed Description

An assertion about processes.


Member Function Documentation

std::shared_ptr<LTS::Machine> FDR::Assertions::PropertyAssertion::machine (  )  const

The process that this assertion is about.

This property is only available after the assertion has been compiled, which occurs during Assertion::execute().


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