tostring.cc 6.71 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14
// or FITNESS FOR A PARTICULAR PURPOSE.	 See the GNU General Public
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
15
16
17
18
19
20
21
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
#include <cassert>
23
#include <sstream>
24
#include <ctype.h>
25
#include <ostream>
26
27
28
29
30
#include "tostring.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"


31
namespace spot
32
33
34
35
{
  namespace ltl
  {

36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
    static bool
    is_bare_word(const char* str)
    {
      // Bare words cannot be empty, start with the letter of a unary
      // operator, or be the name of an existing constant.  Also they
      // should start with an letter.
      if (!*str
	  || *str == 'F'
	  || *str == 'G'
	  || *str == 'X'
	  || !(isalpha(*str) || *str == '_')
	  || !strcasecmp(str, "true")
	  || !strcasecmp(str, "false"))
	return false;
      // The remaining of the word must be alphanumeric.
      while (*++str)
	if (!(isalnum(*str) || *str == '_'))
	  return false;
      return true;
    }

57
    class to_string_visitor : public const_visitor
58
59
    {
    public:
60
      to_string_visitor(std::ostream& os)
61
	: os_(os), top_level_(true)
62
63
      {
      }
64
65

      virtual
66
67
68
      ~to_string_visitor()
      {
      }
69
70

      void
71
      visit(const atomic_prop* ap)
72
      {
73
	std::string str = ap->name();
74
	if (!is_bare_word(str.c_str()))
75
76
77
78
79
80
81
	  {
	    os_ << '"' << str << '"';
	  }
	else
	  {
	    os_ << str;
	  }
82
83
84
      }

      void
85
      visit(const constant* c)
86
87
      {
	os_ << c->val_name();
88
89
      }

90
      void
91
      visit(const binop* bo)
92
      {
93
94
95
96
97
	bool top_level = top_level_;
	top_level_ = false;
	if (!top_level)
	  os_ << "(";

98
	bo->first()->accept(*this);
99

100
	switch (bo->op())
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
	  {
	  case binop::Xor:
	    os_ << " ^ ";
	    break;
	  case binop::Implies:
	    os_ << " => ";
	    break;
	  case binop::Equiv:
	    os_ << " <=> ";
	    break;
	  case binop::U:
	    os_ << " U ";
	    break;
	  case binop::R:
	    os_ << " R ";
	    break;
	  }
118

119
	bo->second()->accept(*this);
120
121
	if (!top_level)
	  os_ << ")";
122
      }
123

124
      void
125
      visit(const unop* uo)
126
      {
127
128
	// The parser treats F0, F1, G0, G1, X0, and X1 as atomic
	// propositions.  So make sure we output F(0), G(1), etc.
129
	bool need_parent = !!dynamic_cast<const constant*>(uo->child());
130
	switch (uo->op())
131
132
133
	  {
	  case unop::Not:
	    os_ << "!";
134
	    need_parent = false;
135
136
137
138
139
140
141
142
143
144
145
	    break;
	  case unop::X:
	    os_ << "X";
	    break;
	  case unop::F:
	    os_ << "F";
	    break;
	  case unop::G:
	    os_ << "G";
	    break;
	  }
146

147
	top_level_ = false;
148
149
	if (need_parent)
	  os_ << "(";
150
	uo->child()->accept(*this);
151
152
	if (need_parent)
	  os_ << ")";
153
      }
154

155
      void
156
      visit(const multop* mo)
157
      {
158
159
160
161
	bool top_level = top_level_;
	top_level_ = false;
	if (!top_level)
	  os_ << "(";
162
163
	unsigned max = mo->size();
	mo->nth(0)->accept(*this);
164
	const char* ch = " ";
165
	switch (mo->op())
166
167
168
	  {
	  case multop::Or:
	    ch = " | ";
169
	    break;
170
171
172
173
	  case multop::And:
	    ch = " & ";
	    break;
	  }
174

175
176
177
178
179
	for (unsigned n = 1; n < max; ++n)
	  {
	    os_ << ch;
	    mo->nth(n)->accept(*this);
	  }
180
181
	if (!top_level)
	  os_ << ")";
182
      }
183
    protected:
184
      std::ostream& os_;
185
      bool top_level_;
186
    };
187

188
    std::ostream&
189
    to_string(const formula* f, std::ostream& os)
190
191
    {
      to_string_visitor v(os);
192
      f->accept(v);
193
      return os;
194
195
    }

196
197
    std::string
    to_string(const formula* f)
198
199
200
201
202
    {
      std::ostringstream os;
      to_string(f, os);
      return os.str();
    }
203
204
205
206

    class to_spin_string_visitor : public to_string_visitor
    {
    public:
207
    to_spin_string_visitor(std::ostream& os)
208
209
210
211
212
213
214
215
216
217
218
219
      : to_string_visitor(os)
      {
      }

      virtual
      ~to_spin_string_visitor()
      {
      }

      void
      visit(const binop* bo)
      {
220
221
222
223
	bool top_level = top_level_;
	top_level_ = false;
	if (!top_level)
	  os_ << "(";
224

225
	switch (bo->op())
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
	  {
	  case binop::Xor:
	    os_ << "(!";
	    bo->first()->accept(*this);
	    os_ << " && ";
	    bo->second()->accept(*this);
	    os_ << ") || (";
	    bo->first()->accept(*this);
	    os_ << " && !";
	    bo->second()->accept(*this);
	    os_ << ")";
	    break;
	  case binop::Implies:
	    os_ << "!";
	    bo->first()->accept(*this);
	    os_ << " || ";
	    bo->second()->accept(*this);
	    break;
	  case binop::Equiv:
	    os_ << "(";
	    bo->first()->accept(*this);
	    os_ << " && ";
	    bo->second()->accept(*this);
	    os_ << ") || (!";
	    bo->first()->accept(*this);
	    os_ << " && !";
	    bo->second()->accept(*this);
	    os_ << ")";
	  case binop::U:
	    bo->first()->accept(*this);
	    os_ << " U ";
	    bo->second()->accept(*this);
	    break;
	  case binop::R:
	    bo->first()->accept(*this);
	   os_ << " V ";
	    bo->second()->accept(*this);
	    break;
	  }

266
267
	if (!top_level)
	  os_ << ")";
268
269
270
271
272
273
274
275
      }

      void
      visit(const unop* uo)
      {
	// The parser treats X0, and X1 as atomic propositions.	 So
	// make sure we output X(0) and X(1).
	bool need_parent = false;
276
	switch (uo->op())
277
278
279
280
281
	  {
	  case unop::Not:
	    os_ << "!";
	    break;
	  case unop::X:
282
	    need_parent = !!dynamic_cast<const constant*>(uo->child());
283
284
285
286
287
288
289
290
291
292
	    os_ << "X";
	    break;
	  case unop::F:
	    os_ << "<>";
	    break;
	  case unop::G:
	    os_ << "[]";
	    break;
	  }

293
	top_level_ = false;
294
295
296
297
298
299
300
301
302
303
	if (need_parent)
	  os_ << "(";
	uo->child()->accept(*this);
	if (need_parent)
	  os_ << ")";
      }

      void
      visit(const multop* mo)
      {
304
305
306
307
	bool top_level = top_level_;
	top_level_ = false;
	if (!top_level)
	  os_ << "(";
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
	unsigned max = mo->size();
	mo->nth(0)->accept(*this);
	const char* ch = " ";
	switch (mo->op())
	  {
	  case multop::Or:
	    ch = " || ";
	    break;
	  case multop::And:
	    ch = " && ";
	    break;
	  }

	for (unsigned n = 1; n < max; ++n)
	  {
	    os_ << ch;
	    mo->nth(n)->accept(*this);
	  }
326
327
	if (!top_level)
	  os_ << ")";
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
      }
    };

    std::ostream&
    to_spin_string(const formula* f, std::ostream& os)
    {
      to_spin_string_visitor v(os);
      f->accept(v);
      return os;
    }

    std::string
    to_spin_string(const formula* f)
    {
      std::ostringstream os;
      to_spin_string(f, os);
      return os.str();
    }
346
347
  }
}