FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | List of all members
FDR::Assertions::MinAcceptanceCounterexample Class Reference

A counterexample demonstrating how a failures refinement check failed. More...

#include <min_acceptance_counterexample.h>

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

Public Member Functions

 MinAcceptanceCounterexample (const std::shared_ptr< Behaviour > &specification, const std::shared_ptr< Behaviour > &implementation)
 
const std::vector< LTS::CompiledEvent > & min_acceptance () const
 The set of events the implementation is guaranteed to be accepted. More...
 
- 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 how a failures refinement check failed.

In this case the specification Behaviour is guaranteed to be a LTS::Behaviour::Irrelevant, whilst the implementation Behaviour is guaranteed to be a LTS::Behaviour::MinAcceptance.

Member Function Documentation

◆ min_acceptance()

const std::vector<LTS::CompiledEvent>& FDR::Assertions::MinAcceptanceCounterexample::min_acceptance ( ) const

The set of events the implementation is guaranteed to be accepted.

The erroneous set of events that are accepted by the implementation, but is not a superset of any of the specification acceptances.


The documentation for this class was generated from the following file: