mCRL2
Loading...
Searching...
No Matches
aterm_io_binary.cpp
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//
9
12
13
14namespace atermpp
15{
16using namespace mcrl2::utilities;
17
21static constexpr std::uint16_t BAF_MAGIC = 0x8baf;
22
39static constexpr std::uint16_t BAF_VERSION = 0x8307;
40
43enum class packet_type
44{
46 aterm,
49};
50
52static constexpr unsigned int packet_bits = 2;
53
54binary_aterm_ostream::binary_aterm_ostream(std::shared_ptr<mcrl2::utilities::obitstream> stream)
55 : m_stream(stream)
56{
57 // The term with function symbol index 0 indicates the end of the stream, its actual value does not matter.
58 m_function_symbols.insert(function_symbol("end_of_stream", 0));
60
61 // Write the header of the binary aterm format.
62 m_stream->write_bits(0, 8);
63 m_stream->write_bits(BAF_MAGIC, 16);
64 m_stream->write_bits(BAF_VERSION, 16);
65}
66
68 : binary_aterm_ostream(std::make_shared<mcrl2::utilities::obitstream>(stream))
69{}
70
72{
73 // Write the end of the stream.
74 m_stream->write_bits(static_cast<std::size_t>(packet_type::aterm), packet_bits);
75 m_stream->write_bits(0, function_symbol_index_width());
76}
77
80{
82 bool write = false;
83
85 : term(term)
86 {}
87
88 void mark(std::stack<std::reference_wrapper<detail::_aterm>>& todo) const
89 {
90 term.mark(todo);
91 }
92};
93
95{
96 // Traverse the term bottom up and store the subterms (and function symbol) before the actual term.
98 stack.emplace(static_cast<const aterm&>(term));
99
100 do
101 {
102 write_todo& current = stack.top();
103 aterm transformed = m_transformer(static_cast<const aterm&>(static_cast<const aterm&>(current.term)));
104
105 // Indicates that this term is output and not a subterm, these should always be written.
106 bool is_output = stack.size() == 1;
107 if (m_terms.index(current.term) >= m_terms.size() || is_output)
108 {
109 if (current.write)
110 {
111 if (transformed.type_is_int())
112 {
113 if (is_output)
114 {
115 // If the integer is output, write the header and just an integer
116 m_stream->write_bits(static_cast<std::size_t>(packet_type::aterm_int_output), packet_bits);
117 m_stream->write_integer(static_cast<const aterm_int&>(static_cast<const aterm&>(current.term)).value());
118 }
119 else
120 {
121 std::size_t symbol_index = write_function_symbol(transformed.function());
122
123 // Write the packet identifier of an aterm_int followed by its value.
124 m_stream->write_bits(static_cast<std::size_t>(packet_type::aterm), packet_bits);
125 m_stream->write_bits(symbol_index, function_symbol_index_width());
126 m_stream->write_integer(static_cast<const aterm_int&>(static_cast<const aterm&>(current.term)).value());
127 }
128 }
129 else
130 {
131 std::size_t symbol_index = write_function_symbol(transformed.function());
132
133 // Write the packet identifier, followed by the indices of its function symbol and arguments.
134 m_stream->write_bits(static_cast<std::size_t>(is_output ? packet_type::aterm_output : packet_type::aterm), packet_bits);
135 m_stream->write_bits(symbol_index, function_symbol_index_width());
136
137 for (const aterm& argument : transformed)
138 {
139 std::size_t index = m_terms.index(argument);
140 assert(index < m_terms.size()); // Every argument must already be written.
141 m_stream->write_bits(index, term_index_width());
142 }
143 }
144
145 if (!is_output)
146 {
147 // Only regular terms (not output) are shared and as such need a unique index.
148 bool assigned = m_terms.insert(current.term).second;
149 assert(assigned); mcrl2_unused(assigned); // This term should have a new index assigned.
150 m_term_index_width = static_cast<std::uint8_t>(std::log2(m_terms.size()) + 1);
151 }
152
153 stack.pop();
154 }
155 else
156 {
157 // Add all the arguments to the stack; to be processed first.
158 for (const aterm& argument : transformed)
159 {
160 const aterm& term = static_cast<const aterm&>(argument);
161 if (m_terms.index(term) >= m_terms.size())
162 {
163 // Only add arguments that have not been written before.
164 stack.emplace(term);
165 }
166 }
167
168 current.write = true;
169 }
170 }
171 else
172 {
173 stack.pop(); // This term was already written and as such should be skipped. This can happen if
174 // one term has two equal subterms.
175 }
176 }
177 while (!stack.empty());
178}
179
181{
182 assert(m_term_index_width == static_cast<unsigned int>(std::log2(m_terms.size()) + 1));
183 return m_term_index_width;
184}
185
187{
188 assert(m_function_symbol_index_width == static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1));
190}
191
192binary_aterm_istream::binary_aterm_istream(std::shared_ptr<mcrl2::utilities::ibitstream> stream)
193 : m_stream(stream)
194{
195 // The term with function symbol index 0 indicates the end of the stream.
196 m_function_symbols.emplace_back();
198
199 // Read the binary aterm format header.
200 if (m_stream->read_bits(8) != 0 || m_stream->read_bits(16) != BAF_MAGIC)
201 {
202 throw mcrl2::runtime_error("Error while reading: missing the BAF_MAGIC control sequence.");
203 }
204
205 std::size_t version = m_stream->read_bits(16);
206 if (version != BAF_VERSION)
207 {
208 throw mcrl2::runtime_error("The BAF version (" + std::to_string(version) + ") of the input file is incompatible with the version (" + std::to_string(BAF_VERSION) +
209 ") of this tool. The input file must be regenerated. ");
210 }
211}
212
214 : binary_aterm_istream(std::make_shared<mcrl2::utilities::ibitstream>(is))
215{}
216
218{
219 std::size_t result = m_function_symbols.index(symbol);
220
221 if (result < m_function_symbols.size())
222 {
223 return result;
224 }
225 else
226 {
227 // The function symbol has not been written yet, write it now and return its index.
228 m_stream->write_bits(static_cast<std::size_t>(packet_type::function_symbol), packet_bits);
229 m_stream->write_string(symbol.name());
230 m_stream->write_integer(symbol.arity());
231
232 auto result = m_function_symbols.insert(symbol);
233 m_function_symbol_index_width = static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1);
234
235 return result.first;
236 }
237}
238
240{
241 while(true)
242 {
243 // Determine the type of the next packet.
244 std::size_t header = m_stream->read_bits(packet_bits);
245 packet_type packet = static_cast<packet_type>(header);
246
247 if (packet == packet_type::function_symbol)
248 {
249 // Read a single function symbol and insert it into the already read function symbols.
250 std::string name = m_stream->read_string();
251 std::size_t arity = m_stream->read_integer();
252 m_function_symbols.emplace_back(name, arity);
253 m_function_symbol_index_width = static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1);
254 }
255 else if (packet == packet_type::aterm_int_output)
256 {
257 // Read the integer from the stream and construct an aterm_int.
258 std::size_t value = m_stream->read_integer();
259 make_aterm_int(static_cast<aterm_int&>(t), value);
260 return;
261 }
262 else if (packet == packet_type::aterm || packet == packet_type::aterm_output)
263 {
264 // First read the function symbol of the following term.
266
267 if (!symbol.defined())
268 {
269 // The term with function symbol zero marks the end of the stream.
270 t=aterm();
271 return;
272 }
273 else if (symbol == detail::g_as_int)
274 {
275 // Read the integer from the stream and construct a shared aterm_int in the index.
276 std::size_t value = m_stream->read_integer();
277 m_terms.emplace_back(aterm_int(value));
278 m_term_index_width = static_cast<unsigned int>(std::log2(m_terms.size()) + 1);
279 }
280 else
281 {
282 // Read arity number of arguments from the stream and search them in the already defined set of terms.
283 std::vector<aterm> arguments(symbol.arity());
284 for (std::size_t argument = 0; argument < symbol.arity(); ++argument)
285 {
286 arguments[argument] = m_terms[m_stream->read_bits(term_index_width())];
287 }
288
289 // Transform the resulting term.
290 aterm transformed = m_transformer(aterm(symbol, arguments.begin(), arguments.end()));
291
292 if (packet == packet_type::aterm_output)
293 {
294 // This aterm was marked as output in the file so return it.
295 t=transformed;
296 return;
297 }
298 else
299 {
300 // Construct the term appl from the function symbol and the already read arguments and insert it.
301 m_terms.emplace_back(transformed);
302 m_term_index_width = static_cast<unsigned int>(std::log2(m_terms.size()) + 1);
303 }
304 }
305 }
306 }
307}
308
310{
311 assert(m_term_index_width == static_cast<unsigned int>(std::log2(m_terms.size()) + 1));
312 return m_term_index_width;
313}
314
316{
317 assert(m_function_symbol_index_width == static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1));
319}
320
321void write_term_to_binary_stream(const aterm& t, std::ostream& os)
322{
323 binary_aterm_ostream(os) << t;
324}
325
326void read_term_from_binary_stream(std::istream& is, aterm& t)
327{
329}
330
331} // namespace atermpp
An integer term stores a single std::size_t value. It carries no arguments.
Definition aterm_int.h:26
std::size_t value() const noexcept
Provide the value stored in an aterm.
Definition aterm_int.h:54
aterm_transformer * m_transformer
Definition aterm_io.h:42
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
Reads terms from a stream in the steamable binary aterm format.
std::shared_ptr< mcrl2::utilities::ibitstream > m_stream
unsigned int m_function_symbol_index_width
caches the result of function_symbol_index_width().
atermpp::deque< aterm > m_terms
An index of read terms.
binary_aterm_istream(std::istream &is)
Provide the input stream from which terms are read.
unsigned int m_term_index_width
caches the result of term_index_width().
void get(aterm &t) override
Reads an aterm from this stream.
std::deque< function_symbol > m_function_symbols
An index of read function symbols.
Writes terms in a streamable binary aterm format to an output stream.
unsigned int m_term_index_width
caches the result of term_index_width().
std::size_t write_function_symbol(const function_symbol &symbol)
Write a function symbol to the output stream.
binary_aterm_ostream(std::ostream &os)
Provide the output stream to which the terms are written.
std::shared_ptr< mcrl2::utilities::obitstream > m_stream
unsigned int m_function_symbol_index_width
caches the result of function_symbol_index_width().
atermpp::indexed_set< aterm > m_terms
An index of already written terms.
void put(const aterm &term) override
Writes an aterm in a compact binary format where subterms are shared. The term that is written itself...
mcrl2::utilities::indexed_set< function_symbol > m_function_symbols
An index of already written function symbols.
Base class that should not be used.
std::size_t arity() const
Return the arity (number of arguments) of the function symbol (function_symbol).
const std::string & name() const
Return the name of the function_symbol.
A deque class in which aterms can be stored.
Definition stack.h:34
bool empty() const
Definition stack.h:124
size_type size() const
Definition stack.h:129
void pop()
Definition stack.h:150
void emplace(Args &&... args)
Definition stack.h:145
reference top()
Definition stack.h:114
bool type_is_int() const noexcept
Dynamic check whether the term is an aterm_int.
Definition aterm_core.h:63
Standard exception class for reporting runtime errors.
Definition exception.h:27
The counterpart of obitstream, guarantees that the same data is read as has been written when calling...
Definition bitstream.h:72
A bitstream provides per bit writing of data to any stream (including stdout).
Definition bitstream.h:32
function_symbol g_as_int
These function symbols are used to indicate integer, list and empty list terms.
The main namespace for the aterm++ library.
Definition algorithm.h:21
void write_term_to_binary_stream(const aterm &t, std::ostream &os)
Writes term t to a stream in binary aterm format.
static constexpr std::uint16_t BAF_VERSION
The BAF_VERSION constant is the version number of the ATerms written in BAF format....
void read_term_from_binary_stream(std::istream &is, aterm &t)
Reads a term from a stream in binary aterm format.
packet_type
Each packet has a header consisting of a type.
void make_aterm_int(aterm_int &target, std::size_t value)
Constructs an integer term from a value.
Definition aterm_int.h:69
static constexpr unsigned int packet_bits
The number of bits needed to store an element of packet_type.
static constexpr std::uint16_t BAF_MAGIC
The magic value for a binary aterm format stream.
void mcrl2_unused(T &&...)
Function that can be used to silence unused parameter warnings.
Definition unused.h:20
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
Keep track of whether the term can be written to the stream.
void mark(std::stack< std::reference_wrapper< detail::_aterm > > &todo) const
write_todo(const aterm &term)
detail::reference_aterm< aterm > term