tostring.cc 14.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2010, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
7
8
9
10
11
12
13
14
15
16
// 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
17
// or FITNESS FOR A PARTICULAR PURPOSE.	 See the GNU General Public
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
18
19
20
21
22
23
24
// 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.

25
#include <cassert>
26
#include <sstream>
27
#include <ctype.h>
28
#include <ostream>
29
#include <cstring>
30
#include "ltlast/allnodes.hh"
31
32
33
#include "ltlast/visitor.hh"
#include "lunabbrev.hh"
#include "tostring.hh"
34

35

36
namespace spot
37
38
39
{
  namespace ltl
  {
40
    namespace
41
    {
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
      enum keyword {
	KFalse = 0,
	KTrue = 1,
	KEmptyWord = 2,
	KXor,
	KImplies,
	KEquiv,
	KU,
	KR,
	KW,
	KM,
	KEConcat,
	KEConcatNext,
	KEConcatMarked,
	KEConcatMarkedNext,
	KUConcat,
	KUConcatNext,
	KNot,
	KX,
	KF,
	KG,
	KOr,
64
	KOrRat,
65
	KAnd,
66
	KAndRat,
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
	KAndNLM,
	KConcat,
	KFusion
      };

      const char* spot_kw[] = {
	"0",
	"1",
	"[*0]",
	" xor ",
	" -> ",
	" <-> ",
	" U ",
	" R ",
	" W ",
	" M ",
83
84
85
86
87
88
	"<>-> ",
	"<>=> ",
	"<>+> ",
	"<>=+> ",
	"[]-> ",
	"[]=> ",
89
90
91
92
93
	"!",
	"X",
	"F",
	"G",
	" | ",
94
	" | ",
95
96
97
	" & ",
	" && ",
	" & ",
98
99
	";",
	":"
100
101
102
103
104
105
106
107
108
109
110
111
112
      };

      const char* spin_kw[] = {
	"0",
	"1",
	"[*0]",			// not supported
	" xor ",		// rewritten
	" -> ",			// rewritten
	" <-> ",		// rewritten
	" U ",
	" V ",
	" W ",			// not supported
	" M ",			// not supported
113
114
115
116
117
118
	"<>-> ",		// not supported
	"<>=> ",		// not supported
	"<>+> ",		// not supported
	"<>=+> ",		// not supported
	"[]-> ",		// not supported
	"[]=> ",		// not supported
119
120
121
122
123
	"!",
	"()",
	"<>",
	"[]",
	" || ",
124
	" || ",
125
126
127
	" && ",
	" && ",			// not supported
	" & ",			// not supported
128
129
	";",			// not supported
	":",			// not supported
130
131
      };

132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
      const char* utf8_kw[] = {
	"0",
	"1",
	"[*0]",
	"⊕",
	" → ",
	" ↔ ",
	" U ",
	" R ",
	" W ",
	" M ",
	"◇→ ",
	"◇⇒ ",
	"◇→̃ ",
	"◇⇒̃ ",
	"□→ ",
	"□⇒ ",
	"¬",
	"○",
	"◇",
	"□",
	"∨",
	" | ",
	"∧",
	" ∩ ",
	" & ",
	";",
	":",
      };

162
163
      static bool
      is_bare_word(const char* str)
164
      {
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
	// 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;
181
      }
182

183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
      // If the formula has the form (!b)[*], return b.
      static
      formula*
      strip_star_not(const formula* f)
      {
	if (bunop* s = is_Star(f))
	  if (unop* n = is_Not(s->child()))
	    return n->child();
	return 0;
      }

      // If the formula as position i in multop mo has the form
      // (!b)[*];b with b being a Boolean formula, return b.
      static
      formula*
      match_goto(const multop *mo, unsigned i)
      {
	assert(i + 1 < mo->size());
	formula* b = strip_star_not(mo->nth(i));
	if (!b || !b->is_boolean())
	  return 0;
	if (mo->nth(i + 1) == b)
	  return b;
	return 0;
      }

209
      class to_string_visitor: public const_visitor
210
      {
211
      public:
212
213
	to_string_visitor(std::ostream& os,
			  bool full_parent = false,
214
215
			  bool ratexp = false,
			  const char** kw = spot_kw)
216
	  : os_(os), top_level_(true),
217
218
	    full_parent_(full_parent), in_ratexp_(ratexp),
	    kw_(kw)
219
220
221
222
223
224
225
226
	{
	}

	virtual
	~to_string_visitor()
	{
	}

227
228
229
230
231
232
233
234
235
236
237
238
	void
	openp() const
	{
	  os_ << (in_ratexp_ ? "{" : "(");
	}

	void
	closep() const
	{
	  os_ << (in_ratexp_ ? "}" : ")");
	}

239
240
241
242
243
244
	std::ostream&
	emit(int symbol)
	{
	  return os_ << kw_[symbol];
	}

245
246
247
248
	void
	visit(const atomic_prop* ap)
	{
	  std::string str = ap->name();
249
250
	  if (full_parent_)
	    os_ << "(";
251
252
253
254
255
256
257
258
	  if (!is_bare_word(str.c_str()))
	    {
	      os_ << '"' << str << '"';
	    }
	  else
	    {
	      os_ << str;
	    }
259
260
	  if (full_parent_)
	    os_ << ")";
261
262
263
264
265
	}

	void
	visit(const constant* c)
	{
266
	  if (full_parent_)
267
	    openp();
268
269
270
271
272
273
274
275
276
277
278
279
	  switch (c->val())
	    {
	    case constant::False:
	      emit(KFalse);
	      break;
	    case constant::True:
	      emit(KTrue);
	      break;
	    case constant::EmptyWord:
	      emit(KEmptyWord);
	      break;
	    }
280
	  if (full_parent_)
281
	    closep();
282
283
284
285
286
287
	}

	void
	visit(const binop* bo)
	{
	  bool top_level = top_level_;
288
	  top_level_ = false;
289
	  if (!top_level)
290
	    openp();
291

292
293
	  bool onelast = false;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
294
295
296
297
	  switch (bo->op())
	    {
	    case binop::UConcat:
	    case binop::EConcat:
298
	    case binop::EConcatMarked:
299
300
	      os_ << "{";
	      in_ratexp_ = true;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
301
	      top_level_ = true;
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
	      {
		multop* m = is_multop(bo->first(), multop::Concat);
		if (m)
		  {
		    unsigned s = m->size();
		    if (m->nth(s - 1) == constant::true_instance())
		      {
			formula* tmp = m->all_but(s - 1);
			tmp->accept(*this);
			tmp->destroy();
			onelast = true;
			break;
		      }
		  }
	      }
317
	      // fall through
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
318
319
320
321
	    default:
	      bo->first()->accept(*this);
	      break;
	    }
322
323
324
325

	  switch (bo->op())
	    {
	    case binop::Xor:
326
	      emit(KXor);
327
328
	      break;
	    case binop::Implies:
329
	      emit(KImplies);
330
331
	      break;
	    case binop::Equiv:
332
	      emit(KEquiv);
333
334
	      break;
	    case binop::U:
335
	      emit(KU);
336
337
	      break;
	    case binop::R:
338
	      emit(KR);
339
	      break;
340
	    case binop::W:
341
	      emit(KW);
342
343
	      break;
	    case binop::M:
344
	      emit(KM);
345
	      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346
	    case binop::UConcat:
347
348
	      os_ << "}";
	      emit(onelast ? KUConcatNext : KUConcat);
349
350
	      in_ratexp_ = false;
	      top_level_ = top_level;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
351
352
	      break;
	    case binop::EConcat:
353
354
355
356
357
358
	      if (bo->second() == constant::true_instance())
		{
		  os_ << "}!";
		  in_ratexp_ = false;
		  goto second_done;
		}
359
360
	      os_ << "}";
	      emit(onelast ? KEConcatNext : KEConcat);
361
362
	      in_ratexp_ = false;
	      top_level_ = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
363
	      break;
364
	    case binop::EConcatMarked:
365
366
	      os_ << "}";
	      emit(onelast ? KEConcatMarkedNext : KEConcatMarked);
367
368
	      in_ratexp_ = false;
	      top_level_ = false;
369
	      break;
370
371
372
	    }

	  bo->second()->accept(*this);
373
	second_done:
374
	  if (!top_level)
375
	    closep();
376
377
	}

378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
	void
	emit_bunop_child(const formula* b)
	{
	  // b[*] is OK, no need to print {b}[*].  However want braces
	  // for {!b}[*], the only unary operator that can be nested
	  // with [*] or any other BUnOp like [->i..j] or [=i..j].
	  formula::opkind ck = b->kind();
	  bool need_parent = (full_parent_
			      || ck == formula::UnOp
			      || ck == formula::BinOp
			      || ck == formula::MultOp);
	  if (need_parent)
	    openp();
	  b->accept(*this);
	  if (need_parent)
	    closep();
	}

396
397
398
	void
	visit(const bunop* bo)
	{
399
400
401
402
403
	  const formula* c = bo->child();
	  enum { Star, Goto, Equal } sugar = Star;
	  unsigned default_min = 0;
	  unsigned default_max = bunop::unbounded;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
404
	  // Abbreviate "1[*]" as "[*]".
405
	  if (c != constant::true_instance())
406
	    {
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
	      bunop::type op = bo->op();
	      switch (op)
		{
		case bunop::Star:
		  if (multop* mo = is_Concat(c))
		    {
		      unsigned s = mo->size();
		      if (s == 2)
			if (formula* b = match_goto(mo, 0))
			  {
			    c = b;
			    sugar = Goto;
			  }
		    }
		  break;
		}
423

424
425
	      emit_bunop_child(c);
	    }
426

427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
	  unsigned min = bo->min();
	  unsigned max = bo->max();
	  switch (sugar)
	    {
	    case Star:
	      if (min == 1 && max == bunop::unbounded)
		{
		  os_ << "[+]";
		  return;
		}
	      os_ << "[*";
	      break;
	    case Equal:
	      os_ << "[=";
	      break;
	    case Goto:
	      os_ << "[->";
	      default_min = 1;
	      default_max = 1;
	      break;
447
448
	    }

449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
	  // Beware that the default parameters of the Goto operator are
	  // not the same as Star or Equal:
	  //
	  //   [->]   = [->1..1]
	  //   [->..] = [->1..unbounded]
	  //   [*]    = [*0..unbounded]
	  //   [*..]  = [*0..unbounded]
	  //   [=]    = [=0..unbounded]
	  //   [=..]  = [=0..unbounded]
	  //
	  // Strictly speaking [=] is not specified by PSL, and anyway we
	  // automatically rewrite Exp[=0..unbounded] as
	  // Exp[*0..unbounded], so we should never have to print [=]
	  // here.
	  //
	  // Also
	  //   [*..]  = [*0..unbounded]

	  if (min != default_min || max != default_max)
	    {
	      // Always print the min_, even when it is equal to
	      // default_min, this way we avoid ambiguities (like
	      // when reading [*..3] near [->..2])
	      os_ << min;
	      if (min != max)
		{
		  os_ << "..";
		  if (max != bunop::unbounded)
		    os_ << max;
		}
	    }
	  os_ << "]";
481
482
	}

483
484
485
	void
	visit(const unop* uo)
	{
486
	  top_level_ = false;
487
488
	  // The parser treats F0, F1, G0, G1, X0, and X1 as atomic
	  // propositions.  So make sure we output F(0), G(1), etc.
489
	  bool need_parent = (uo->child()->kind() == formula::Constant);
490
491
492
493
494
495
496
	  bool top_level = top_level_;

	  if (full_parent_)
	    {
	      need_parent = false; // These will be printed by each subformula

	      if (!top_level)
497
		openp();
498
499
	    }

500
501
502
	  switch (uo->op())
	    {
	    case unop::Not:
503
	      emit(KNot);
504
505
506
	      need_parent = false;
	      break;
	    case unop::X:
507
	      emit(KX);
508
509
	      break;
	    case unop::F:
510
	      emit(KF);
511
512
	      break;
	    case unop::G:
513
	      emit(KG);
514
	      break;
515
516
517
518
	    case unop::Finish:
	      os_ << "finish";
	      need_parent = true;
	      break;
519
520
	    case unop::Closure:
	      os_ << "{";
521
	      in_ratexp_ = true;
522
523
524
	      top_level_ = true;
	      break;
	    case unop::NegClosure:
525
526
	      emit(KNot);
	      os_ << "{";
527
528
	      in_ratexp_ = true;
	      top_level_ = true;
529
	      break;
530
531
	    }

532
	  if (need_parent || full_parent_)
533
	    openp();
534
	  uo->child()->accept(*this);
535
536
	  if (need_parent || full_parent_)
	    closep();
537

538
539
540
541
542
	  switch (uo->op())
	    {
	    case unop::Closure:
	    case unop::NegClosure:
	      os_ << "}";
543
	      in_ratexp_ = false;
544
545
546
547
548
549
	      top_level_ = false;
	      break;
	    default:
	      break;
	    }

550
	  if (full_parent_ && !top_level)
551
	    closep();
552
553
	}

554
555
556
	void
	visit(const automatop* ao)
	{
557
558
	  // Warning: this string isn't parsable because the automaton
	  // operators used may not be defined.
559
560
561
562
	  bool top_level = top_level_;
	  top_level_ = false;
	  if (!top_level)
	    os_ << "(";
563
	  os_ << ao->get_nfa()->get_name() << "(";
564
565
566
567
568
569
570
571
572
573
574
575
	  unsigned max = ao->size();
	  ao->nth(0)->accept(*this);
	  for (unsigned n = 1; n < max; ++n)
	    {
	      os_ << ",";
	      ao->nth(n)->accept(*this);
	    }
	  os_ << ")";
	  if (!top_level)
	    os_ << ")";
	}

576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
	void
	resugar_concat(const multop* mo)
	{
	  unsigned max = mo->size();

	  for (unsigned i = 0; i < max; ++i)
	    {
	      if (i > 0)
		emit(KConcat);
	      if (i + 1 < max)
		{
		  // Try to match (!b)[*];b
		  formula* b = match_goto(mo, i);
		  if (b)
		    {
		      emit_bunop_child(b);

		      // Wait... maybe we are looking at (!b)[*];b;(!b)[*]
		      // in which case it's b[=1].
		      if (i + 2 < max && mo->nth(i) == mo->nth(i + 2))
			{
			  os_ << "[=1]";
			  i += 2;
			}
		      else
			{
			  os_ << "[->]";
			  ++i;
			}
		      continue;
		    }
		  // Try to match ((!b)[*];b)[*i..j];(!b)[*]
		  if (bunop* s = is_Star(mo->nth(i)))
		    if (formula* b2 = strip_star_not(mo->nth(i + 1)))
		      if (multop* sc = is_Concat(s->child()))
			if (formula* b1 = match_goto(sc, 0))
			  if (b1 == b2)
			    {
			      emit_bunop_child(b1);
			      os_ << "[=";
			      unsigned min = s->min();
			      os_ << min;
			      unsigned max = s->max();
			      if (max != min)
				{
				  os_ << "..";
				  if (max != bunop::unbounded)
				    os_ << max;
				}
			      os_ << "]";
			      ++i;
			      continue;
			    }
		}
	      mo->nth(i)->accept(*this);
	    }
	}


635
636
637
638
639
640
	void
	visit(const multop* mo)
	{
	  bool top_level = top_level_;
	  top_level_ = false;
	  if (!top_level)
641
	    openp();
642
643
644
645
646
647
648
649
650
651
652
653
	  multop::type op = mo->op();

	  // Handle the concatenation separately, because we want to
	  // "resugar" some patterns.
	  if (op == multop::Concat)
	    {
	      resugar_concat(mo);
	      if (!top_level)
		closep();
	      return;
	    }

654
	  mo->nth(0)->accept(*this);
655
	  keyword k = KFalse;	// Initialize to something to please GCC.
656
	  switch (op)
657
658
	    {
	    case multop::Or:
659
	      k = KOr;
660
	      break;
661
662
663
	    case multop::OrRat:
	      k = KOrRat;
	      break;
664
	    case multop::And:
665
666
667
668
	      k = in_ratexp_ ? KAndRat : KAnd;
	      break;
	    case multop::AndRat:
	      k = KAndRat;
669
670
	      break;
	    case multop::AndNLM:
671
	      k = KAndNLM;
672
	      break;
673
	    case multop::Concat:
674
675
	      // Handled by resugar_concat.
	      assert(0);
676
	      break;
677
	    case multop::Fusion:
678
	      k = KFusion;
679
	      break;
680
	    }
681
	  assert(k != KFalse);
682

683
	  unsigned max = mo->size();
684
685
	  for (unsigned n = 1; n < max; ++n)
	    {
686
	      emit(k);
687
688
689
	      mo->nth(n)->accept(*this);
	    }
	  if (!top_level)
690
	    closep();
691
692
693
694
	}
      protected:
	std::ostream& os_;
	bool top_level_;
695
	bool full_parent_;
696
	bool in_ratexp_;
697
	const char** kw_;
698
699
700
      };

    } // anonymous
701

702
    std::ostream&
703
704
    to_string(const formula* f, std::ostream& os, bool full_parent,
	      bool ratexp)
705
    {
706
      to_string_visitor v(os, full_parent, ratexp, spot_kw);
707
      f->accept(v);
708
      return os;
709
710
    }

711
    std::string
712
    to_string(const formula* f, bool full_parent, bool ratexp)
713
714
    {
      std::ostringstream os;
715
      to_string(f, os, full_parent, ratexp);
716
717
      return os.str();
    }
718

719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
    std::ostream&
    to_utf8_string(const formula* f, std::ostream& os, bool full_parent,
	      bool ratexp)
    {
      to_string_visitor v(os, full_parent, ratexp, utf8_kw);
      f->accept(v);
      return os;
    }

    std::string
    to_utf8_string(const formula* f, bool full_parent, bool ratexp)
    {
      std::ostringstream os;
      to_utf8_string(f, os, full_parent, ratexp);
      return os.str();
    }

736
    std::ostream&
737
    to_spin_string(const formula* f, std::ostream& os, bool full_parent)
738
    {
739
740
741
742
743
      // Remove xor, ->, and <-> first.
      formula* fu = unabbreviate_logic(f);
      to_string_visitor v(os, full_parent, false, spin_kw);
      fu->accept(v);
      fu->destroy();
744
745
746
747
      return os;
    }

    std::string
748
    to_spin_string(const formula* f, bool full_parent)
749
750
    {
      std::ostringstream os;
751
      to_spin_string(f, os, full_parent);
752
753
      return os.str();
    }
754
755
  }
}