mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Static Public Member Functions | Protected Attributes | Static Protected Attributes | List of all members
mcrl2::lts::detail::counter_example_constructor Class Reference

A class that can be used to store counterexample trees and. More...

#include <counter_example.h>

Public Types

using index_type = std::size_t
 

Public Member Functions

 counter_example_constructor (const std::string &name, const std::string &counter_example_file, bool structured_output)
 Constructor.
 
index_type add_transition (std::size_t label_index, index_type previous_entry)
 This function stores a label to the counterexample tree.
 
template<class LTS_TYPE >
void save_counter_example (index_type index, const LTS_TYPE &l, const std::vector< size_t > &extra_actions=std::vector< size_t >()) const
 
template<class LTS_TYPE >
trace get_trace (const LTS_TYPE &l, index_type index) const
 This function returns the trace from the root to the current index.
 
bool is_dummy () const
 This function indicates that this is not a dummy counterexample class and that a serious counterexample is required.
 
bool is_structured () const
 Returns whether this counter-example is printed in a machine-readable way to stdout If false is returned, the counter-example is written to a file.
 

Static Public Member Functions

static index_type root_index ()
 Return the index of the root.
 

Protected Attributes

std::deque< action_index_pair > m_backward_tree
 
const std::string m_name
 
const std::string m_counter_example_file
 
const bool m_structured_output = false
 

Static Protected Attributes

static const index_type m_root_index =-1
 

Detailed Description

A class that can be used to store counterexample trees and.

Definition at line 56 of file counter_example.h.

Member Typedef Documentation

◆ index_type

using mcrl2::lts::detail::counter_example_constructor::index_type = std::size_t

Definition at line 59 of file counter_example.h.

Constructor & Destructor Documentation

◆ counter_example_constructor()

mcrl2::lts::detail::counter_example_constructor::counter_example_constructor ( const std::string &  name,
const std::string &  counter_example_file,
bool  structured_output 
)
inline

Constructor.

Definition at line 78 of file counter_example.h.

Member Function Documentation

◆ add_transition()

index_type mcrl2::lts::detail::counter_example_constructor::add_transition ( std::size_t  label_index,
index_type  previous_entry 
)
inline

This function stores a label to the counterexample tree.

Definition at line 95 of file counter_example.h.

◆ get_trace()

template<class LTS_TYPE >
trace mcrl2::lts::detail::counter_example_constructor::get_trace ( const LTS_TYPE &  l,
index_type  index 
) const
inline

This function returns the trace from the root to the current index.

Definition at line 135 of file counter_example.h.

◆ is_dummy()

bool mcrl2::lts::detail::counter_example_constructor::is_dummy ( ) const
inline

This function indicates that this is not a dummy counterexample class and that a serious counterexample is required.

Definition at line 159 of file counter_example.h.

◆ is_structured()

bool mcrl2::lts::detail::counter_example_constructor::is_structured ( ) const
inline

Returns whether this counter-example is printed in a machine-readable way to stdout If false is returned, the counter-example is written to a file.

Definition at line 166 of file counter_example.h.

◆ root_index()

static index_type mcrl2::lts::detail::counter_example_constructor::root_index ( )
inlinestatic

Return the index of the root.

Definition at line 85 of file counter_example.h.

◆ save_counter_example()

template<class LTS_TYPE >
void mcrl2::lts::detail::counter_example_constructor::save_counter_example ( index_type  index,
const LTS_TYPE &  l,
const std::vector< size_t > &  extra_actions = std::vector<size_t>() 
) const
inline

Definition at line 103 of file counter_example.h.

Member Data Documentation

◆ m_backward_tree

std::deque< action_index_pair > mcrl2::lts::detail::counter_example_constructor::m_backward_tree
protected

Definition at line 66 of file counter_example.h.

◆ m_counter_example_file

const std::string mcrl2::lts::detail::counter_example_constructor::m_counter_example_file
protected

Definition at line 68 of file counter_example.h.

◆ m_name

const std::string mcrl2::lts::detail::counter_example_constructor::m_name
protected

Definition at line 67 of file counter_example.h.

◆ m_root_index

const index_type mcrl2::lts::detail::counter_example_constructor::m_root_index =-1
staticprotected

Definition at line 65 of file counter_example.h.

◆ m_structured_output

const bool mcrl2::lts::detail::counter_example_constructor::m_structured_output = false
protected

Definition at line 69 of file counter_example.h.

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