mCRL2
Loading...
Searching...
No Matches
counter_example.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
17
18#ifndef _LIBLTS_COUNTER_EXAMPLE_H
19#define _LIBLTS_COUNTER_EXAMPLE_H
20
21#include "mcrl2/lts/lts_lts.h"
22#include "mcrl2/lts/trace.h"
23
24
25namespace mcrl2
26{
27namespace lts
28{
29
30namespace detail
31{
32
33
35// to the counterexample three in the direction of the root.
37{
38 protected:
39 std::size_t m_label_index;
41
42 public:
46 {}
47
48 std::size_t label_index() const
49 {
50 return m_label_index;
51 }
52
53 std::size_t previous_entry_index() const
54 {
56 }
57};
58
60// from which a counterexample trace can be extracted.
62{
63 public:
64 typedef std::size_t index_type;
65
66 protected:
67 // The backward three is stored in a deque.
68 // The root has entry std::size_t(-1).
69
70 static const index_type m_root_index=-1;
71 std::deque< action_index_pair > m_backward_tree;
72 const std::string m_name;
73 const std::string m_counter_example_file;
75
76 public:
78 // \param name The name of the model that the counter example is for
79 // \param counter_example_file The name of the file to save the counter example to
80 // \param structured_output Whether the counterexample should be printed to std:cout
81 // \detail If structured_output=true, the counter example is not saved to file.
82 // If counter_example_file="", the name of the counter example file name is derived from name (the parameter)
83 counter_example_constructor(const std::string& name, const std::string& counter_example_file, bool structured_output)
84 : m_name(name)
85 , m_counter_example_file(counter_example_file)
86 , m_structured_output(structured_output)
87 {}
88
91 {
92 return m_root_index;
93 }
94
96 // \param label_index The label index is the label as used in transitions.
97 // \param previous_entry The index of the counterexample trace to which
98 // this action label must be attached.
99 // \ret It returns a new index which can be used to extend the counterexample.
100 index_type add_transition(std::size_t label_index, index_type previous_entry)
101 {
102 m_backward_tree.emplace_back(label_index, previous_entry);
103 return m_backward_tree.size()-1;
104 }
105
106 /* A trace to index is saved, followed by a list of actions in extra_actions. */
107 template < class LTS_TYPE >
108 void save_counter_example(index_type index, const LTS_TYPE& l, const std::vector<size_t>& extra_actions=std::vector<size_t>()) const
109 {
110 // We first store the label indices in reverse order in a stack.
111 std::stack< index_type > reversed_label_indices;
112 for(index_type current_index=index;
113 current_index!=m_root_index;
114 current_index=m_backward_tree[current_index].previous_entry_index())
115 {
116 reversed_label_indices.push(m_backward_tree[current_index].label_index());
117 }
118
119 trace result;
120 while (!reversed_label_indices.empty())
121 {
124 core::identifier_string(mcrl2::lts::pp(l.action_label(reversed_label_indices.top()))),
127 reversed_label_indices.pop();
128 }
129
130 /* Add the actions in extra actions. */
131 for(const size_t& a: extra_actions)
132 {
135 core::identifier_string(mcrl2::lts::pp(l.action_label(a))),
138 }
140 {
141 std::cout << m_name << ": ";
142 result.save("", mcrl2::lts::trace::tfLine); // Write to stdout.
143 }
144 else
145 {
146 std::string filename = m_name + ".trc";
147 if (!m_counter_example_file.empty())
148 {
149 filename = m_counter_example_file;
150 }
151 mCRL2log(log::verbose) << "Saved trace to file " + filename + "\n";
152 result.save(filename);
153 }
154 }
155
157 bool is_dummy() const
158 {
159 return false;
160 }
161
164 bool is_structured() const
165 {
166 return m_structured_output;
167 }
168};
169
170
172// counter example is desired. Its index_type is empty.
174{
175 public:
176 typedef dummy_counter_example_constructor index_type; // This yields an empty type.
177
179 {
180 return dummy_counter_example_constructor(); // This returns nothing.
181 }
182
183 index_type add_transition(std::size_t /* label_index*/, index_type /* previous_entry*/)
184 {
185 // This dummy counter example generator intentionally does nothing.
186 return *this;
187 }
188
189 template < class LTS_TYPE >
190 void save_counter_example(index_type /* index */, const LTS_TYPE& /*l*/, const std::vector<size_t>& /* extra_actions */ =std::vector<size_t>()) const
191 {
192 // This dummy counter example generator intentionally does not save anything.
193 }
194
196 bool is_dummy() const
197 {
198 return true;
199 }
200
203 bool is_structured() const
204 {
205 return false;
206 }
207};
208
209} // namespace detail
210} // namespace lts
211} // namespace mcrl2
212
213#endif // _LIBLTS_COUNTER_EXAMPLE_H
Term containing a string.
A list of aterm objects.
Definition aterm_list.h:23
\brief A timed multi-action
A simple class storing the index of a label and an index.
action_index_pair(std::size_t label_index, std::size_t previous_entry_index)
A class that can be used to store counterexample trees and.
void save_counter_example(index_type index, const LTS_TYPE &l, const std::vector< size_t > &extra_actions=std::vector< size_t >()) const
static index_type root_index()
Return the index of the root.
std::deque< action_index_pair > m_backward_tree
index_type add_transition(std::size_t label_index, index_type previous_entry)
This function stores a label to the counterexample tree.
bool is_dummy() const
This function indicates that this is not a dummy counterexample class and that a serious counterexamp...
bool is_structured() const
Returns whether this counter-example is printed in a machine-readable way to stdout If false is retur...
counter_example_constructor(const std::string &name, const std::string &counter_example_file, bool structured_output)
Constructor.
A class that can be used to construct counter examples if no.
bool is_dummy() const
This function indicates that this is a dummy counterexample class and that no counterexample is requi...
void save_counter_example(index_type, const LTS_TYPE &, const std::vector< size_t > &=std::vector< size_t >()) const
index_type add_transition(std::size_t, index_type)
bool is_structured() const
Returns whether this counter-example is printed in a machine-readable way to stdout If false is retur...
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
void save(const std::string &filename, trace_format tf=tfMcrl2) const
Output the trace into a file with the indicated name.
Definition trace.h:401
void add_action(const mcrl2::lps::multi_action &action)
Add an action to the current trace.
Definition trace.h:319
\brief An action label
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
std::string pp(const abstraction &x)
Definition data.cpp:39
@ verbose
Definition logger.h:35
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
This class allows to flexibly manipulate traces.