tostring.cc 15.6 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
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
// (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
// License for more details.
//
// You should have received a copy of the GNU General Public License
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

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

34

35
namespace spot
36
37
38
{
  namespace ltl
  {
39
    namespace
40
    {
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
      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,
63
	KOrRat,
64
	KAnd,
65
	KAndRat,
66
67
	KAndNLM,
	KConcat,
68
	KFusion,
69
70
71
72
73
74
75
76
77
78
79
80
81
      };

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

      const char* spin_kw[] = {
102
103
	"false", // 0 doesn't work from the command line
	"true",  // 1 doesn't work from the command line
104
105
	"[*0]",			// not supported
	" xor ",		// rewritten
106
107
	" -> ",			// rewritten, although supported
	" <-> ",		// rewritten, although supported
108
109
	" U ",
	" V ",
110
	" W ",			// rewritten, although supported
111
	" M ",			// rewritten
112
113
114
115
116
117
	"<>-> ",		// not supported
	"<>=> ",		// not supported
	"<>+> ",		// not supported
	"<>=+> ",		// not supported
	"[]-> ",		// not supported
	"[]=> ",		// not supported
118
	"!",
119
	"X",
120
121
122
	"<>",
	"[]",
	" || ",
123
	" || ",
124
125
126
	" && ",
	" && ",			// not supported
	" & ",			// not supported
127
128
	";",			// not supported
	":",			// not supported
129
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
      const char* utf8_kw[] = {
	"0",
	"1",
	"[*0]",
	"⊕",
	" → ",
	" ↔ ",
	" U ",
	" R ",
	" W ",
	" M ",
	"◇→ ",
	"◇⇒ ",
	"◇→̃ ",
	"◇⇒̃ ",
	"□→ ",
	"□⇒ ",
	"¬",
	"○",
	"◇",
	"□",
	"∨",
	" | ",
	"∧",
	" ∩ ",
	" & ",
	";",
	":",
      };

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

182
183
      // If the formula has the form (!b)[*], return b.
      static
184
      const formula*
185
186
      strip_star_not(const formula* f)
      {
187
188
	if (const bunop* s = is_Star(f))
	  if (const unop* n = is_Not(s->child()))
189
190
191
192
193
194
195
	    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
196
      const formula*
197
198
199
      match_goto(const multop *mo, unsigned i)
      {
	assert(i + 1 < mo->size());
200
	const formula* b = strip_star_not(mo->nth(i));
201
202
203
204
205
206
207
	if (!b || !b->is_boolean())
	  return 0;
	if (mo->nth(i + 1) == b)
	  return b;
	return 0;
      }

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

	virtual
	~to_string_visitor()
	{
	}

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

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

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

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

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

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

291
292
	  bool onelast = false;

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

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

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

377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
	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();
	}

395
396
397
	void
	visit(const bunop* bo)
	{
398
399
400
401
402
	  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
403
	  // Abbreviate "1[*]" as "[*]".
404
	  if (c != constant::true_instance())
405
	    {
406
407
408
409
	      bunop::type op = bo->op();
	      switch (op)
		{
		case bunop::Star:
410
		  if (const multop* mo = is_Concat(c))
411
412
413
		    {
		      unsigned s = mo->size();
		      if (s == 2)
414
			if (const formula* b = match_goto(mo, 0))
415
416
417
418
419
420
421
			  {
			    c = b;
			    sugar = Goto;
			  }
		    }
		  break;
		}
422

423
424
	      emit_bunop_child(c);
	    }
425

426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
	  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;
446
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
	  // 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_ << "]";
480
481
	}

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

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

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

500
501
502
503
	  switch (uo->op())
	    {
	    case unop::Not:
	      need_parent = false;
504
505
506
507
508
509
510
511
512
513
514
	      // If we negate a single letter in UTF-8, use a
	      // combining overline.
	      if (!full_parent_ && kw_ == utf8_kw)
		if (const ltl::atomic_prop* ap = is_atomic_prop(uo->child()))
		  if (ap->name().size() == 1
		      && is_bare_word(ap->name().c_str()))
		    {
		      overline = true;
		      break;
		    }
	      emit(KNot);
515
516
	      break;
	    case unop::X:
517
	      emit(KX);
518
519
	      break;
	    case unop::F:
520
	      emit(KF);
521
522
	      break;
	    case unop::G:
523
	      emit(KG);
524
	      break;
525
526
527
528
	    case unop::Finish:
	      os_ << "finish";
	      need_parent = true;
	      break;
529
530
	    case unop::Closure:
	      os_ << "{";
531
	      in_ratexp_ = true;
532
533
534
	      top_level_ = true;
	      break;
	    case unop::NegClosure:
535
536
	      emit(KNot);
	      os_ << "{";
537
538
	      in_ratexp_ = true;
	      top_level_ = true;
539
	      break;
540
541
542
543
544
545
	    case unop::NegClosureMarked:
	      emit(KNot);
	      os_ << (kw_ == utf8_kw ? "̃{": "+{");
	      in_ratexp_ = true;
	      top_level_ = true;
	      break;
546
547
	    }

548
	  if (need_parent || full_parent_)
549
	    openp();
550
	  uo->child()->accept(*this);
551
552
	  if (need_parent || full_parent_)
	    closep();
553

554
555
556
557
558
	  switch (uo->op())
	    {
	    case unop::Closure:
	    case unop::NegClosure:
	      os_ << "}";
559
	      in_ratexp_ = false;
560
561
562
563
564
565
	      top_level_ = false;
	      break;
	    default:
	      break;
	    }

566
	  if (full_parent_ && !top_level)
567
	    closep();
568
569
570
571
572
	  else if (overline)
	    // The following string contains only the character U+0305
	    // (a combining overline).  It looks better than U+0304 (a
	    // combining overbar).
	    os_ << "̅";
573
574
	}

575
576
577
	void
	visit(const automatop* ao)
	{
578
579
	  // Warning: this string isn't parsable because the automaton
	  // operators used may not be defined.
580
581
582
583
	  bool top_level = top_level_;
	  top_level_ = false;
	  if (!top_level)
	    os_ << "(";
584
	  os_ << ao->get_nfa()->get_name() << "(";
585
586
587
588
589
590
591
592
593
594
595
596
	  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_ << ")";
	}

597
598
599
600
601
602
603
604
605
606
607
608
	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
609
		  const formula* b = match_goto(mo, i);
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
		  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)[*]
629
630
631
632
		  if (const bunop* s = is_Star(mo->nth(i)))
		    if (const formula* b2 = strip_star_not(mo->nth(i + 1)))
		      if (const multop* sc = is_Concat(s->child()))
			if (const formula* b1 = match_goto(sc, 0))
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
			  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);
	    }
	}


656
657
658
659
660
661
	void
	visit(const multop* mo)
	{
	  bool top_level = top_level_;
	  top_level_ = false;
	  if (!top_level)
662
	    openp();
663
664
665
666
667
668
669
670
671
672
673
674
	  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;
	    }

675
	  mo->nth(0)->accept(*this);
676
	  keyword k = KFalse;	// Initialize to something to please GCC.
677
	  switch (op)
678
679
	    {
	    case multop::Or:
680
	      k = KOr;
681
	      break;
682
683
684
	    case multop::OrRat:
	      k = KOrRat;
	      break;
685
	    case multop::And:
686
687
688
689
	      k = in_ratexp_ ? KAndRat : KAnd;
	      break;
	    case multop::AndRat:
	      k = KAndRat;
690
691
	      break;
	    case multop::AndNLM:
692
	      k = KAndNLM;
693
	      break;
694
	    case multop::Concat:
695
696
	      // Handled by resugar_concat.
	      assert(0);
697
	      break;
698
	    case multop::Fusion:
699
	      k = KFusion;
700
	      break;
701
	    }
702
	  assert(k != KFalse);
703

704
	  unsigned max = mo->size();
705
706
	  for (unsigned n = 1; n < max; ++n)
	    {
707
	      emit(k);
708
709
710
	      mo->nth(n)->accept(*this);
	    }
	  if (!top_level)
711
	    closep();
712
713
714
715
	}
      protected:
	std::ostream& os_;
	bool top_level_;
716
	bool full_parent_;
717
	bool in_ratexp_;
718
	const char** kw_;
719
720
721
      };

    } // anonymous
722

723
    std::ostream&
724
725
    to_string(const formula* f, std::ostream& os, bool full_parent,
	      bool ratexp)
726
    {
727
      to_string_visitor v(os, full_parent, ratexp, spot_kw);
728
      f->accept(v);
729
      return os;
730
731
    }

732
    std::string
733
    to_string(const formula* f, bool full_parent, bool ratexp)
734
735
    {
      std::ostringstream os;
736
      to_string(f, os, full_parent, ratexp);
737
738
      return os.str();
    }
739

740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
    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();
    }

757
    std::ostream&
758
    to_spin_string(const formula* f, std::ostream& os, bool full_parent)
759
    {
760
      // Remove xor, ->, and <-> first.
761
      const formula* fu = unabbreviate_logic(f);
762
763
      // Also remove W and M.
      f = unabbreviate_wm(fu);
764
      fu->destroy();
765
766
767
      to_string_visitor v(os, full_parent, false, spin_kw);
      f->accept(v);
      f->destroy();
768
769
770
771
      return os;
    }

    std::string
772
    to_spin_string(const formula* f, bool full_parent)
773
774
    {
      std::ostringstream os;
775
      to_spin_string(f, os, full_parent);
776
777
      return os.str();
    }
778
779
  }
}