FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | List of all members
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]

Public Member Functions

 DeterminismCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation)
 
- Public Member Functions inherited from FDR::Assertions::RefinementCounterexample
const std::shared_ptr< Behaviour > & implementation_behaviour () const
 The behaviour of the implementation process.
 
const std::shared_ptr< Behaviour > & specification_behaviour () const
 The behaviour of the specification process.
 
- Public Member Functions inherited from FDR::Assertions::Counterexample
 Counterexample (const Counterexample &)=delete
 
Counterexampleoperator= (const Counterexample &)=delete
 

Additional Inherited Members

- Protected Member Functions inherited from FDR::Assertions::RefinementCounterexample
 RefinementCounterexample (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: