FDR::Assertions::DeterminismCounterexample Class Reference

A counterexample demonstrating non determinism in a process. More...

#include <determinism_counterexample.h>

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

List of all members.

Public Member Functions

 DeterminismCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation)

Detailed Description

A counterexample demonstrating non determinism in a process.

A determinism assertion can fail for two reasons:

1. If a semantic model that involves Divergences is used, because the implementation diverges. In this case, the implementation behaviour will be a LTS::Behaviour::Loop or LTS::Behaviour::ExplicitDivergence, whilst the specification behaviour will be a LTS::Behaviour::Irrelevant. 2. Because the process can both perform a trace tr^<a>, and refuse a after performing the trace tr. In this case, the implementation will be a LTS::Behaviour::Trace, whilst the specification behaviour will be a LTS::Behaviour::MinAcceptance that are of the above form.

In this case the specification Behaviour is guaranteed to be a LTS::Behaviour::Irrelevant (since the specification is an internal FDR process), whilst the implementation Behaviour is guaranteed to be a LTS::Behaviour::MinAcceptance.


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