basicreduce.cc 13.4 KB
Newer Older
1
2
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
// Copyright (C) 2004, 2007 Laboratoire d'Informatique de
4
5
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
martinez's avatar
martinez committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// 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.

24
#include "basicreduce.hh"
25
26
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
martinez's avatar
martinez committed
27
28
29
30
31
32
#include <cassert>

namespace spot
{
  namespace ltl
  {
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
    bool
    is_GF(const formula* f)
    {
      const unop* op = dynamic_cast<const unop*>(f);
      if (op && op->op() == unop::G)
	{
	  const unop* opchild = dynamic_cast<const unop*>(op->child());
	  if (opchild && opchild->op() == unop::F)
	    return true;
	}
      return false;
    }

    bool
    is_FG(const formula* f)
    {
      const unop* op = dynamic_cast<const unop*>(f);
      if (op && op->op() == unop::F)
	{
	  const unop* opchild = dynamic_cast<const unop*>(op->child());
	  if (opchild && opchild->op() == unop::G)
	    return true;
	}
      return false;
    }

59
    namespace
martinez's avatar
martinez committed
60
    {
61
62
63
      class basic_reduce_visitor: public visitor
      {
      public:
64

65
	basic_reduce_visitor(){}
66

67
	virtual ~basic_reduce_visitor(){}
martinez's avatar
martinez committed
68

69
70
71
72
73
	formula*
	result() const
	{
	  return result_;
	}
74

75
76
77
	void
	visit(atomic_prop* ap)
	{
78
	  formula* f = ap->clone();
79
80
	  result_ = f;
	}
81

82
83
84
85
86
	void
	visit(constant* c)
	{
	  result_ = c;
	}
87

88
89
90
91
92
93
94
95
96
	formula*
	param_case(multop* mo, unop::type op, multop::type op_child)
	{
	  formula* result;
	  multop::vec* res1 = new multop::vec;
	  multop::vec* resGF = new multop::vec;
	  unsigned mos = mo->size();
	  for (unsigned i = 0; i < mos; ++i)
	    if (is_GF(mo->nth(i)))
97
	      resGF->push_back(mo->nth(i)->clone());
98
	    else
99
	      res1->push_back(mo->nth(i)->clone());
100
	  mo->destroy();
101
102
103
104
	  multop::vec* res3 = new multop::vec;
	  if (!res1->empty())
	    res3->push_back(unop::instance(op,
					   multop::instance(op_child, res1)));
105
	  else
106
107
108
109
110
111
112
113
	    delete res1;
	  if (!resGF->empty())
	    res3->push_back(multop::instance(op_child, resGF));
	  else
	    delete resGF;
	  result = multop::instance(op_child, res3);
	  return result;
	}
114

115
116
117
118
119
120
121
122
123
124
125
126
	void
	visit(unop* uo)
	{
	  formula* f = uo->child();
	  result_ = basic_reduce(f);
	  multop* mo = 0;
	  unop* u = 0;
	  binop* bo = 0;
	  switch (uo->op())
	    {
	    case unop::Not:
	      result_ = unop::instance(unop::Not, result_);
127
	      return;
martinez's avatar
martinez committed
128

129
130
131
132
	    case unop::X:
	      // X(true) = true
	      // X(false) = false
	      if (dynamic_cast<constant*>(result_))
133
		return;
134

135
136
	      // XGF(f) = GF(f)
	      if (is_GF(result_))
137
		return;
138

139
140
141
142
143
144
145
146
	      // X(f1 & GF(f2)) = X(f1) & GF(F2)
	      // X(f1 | GF(f2)) = X(f1) | GF(F2)
	      mo = dynamic_cast<multop*>(result_);
	      if (mo)
		{
		  result_ = param_case(mo, unop::X, mo->op());
		  return;
		}
martinez's avatar
martinez committed
147

148
	      result_ = unop::instance(unop::X, result_);
martinez's avatar
martinez committed
149
150
	      return;

151
152
153
154
	    case unop::F:
	      // F(true) = true
	      // F(false) = false
	      if (dynamic_cast<constant*>(result_))
martinez's avatar
martinez committed
155
		return;
156

157
158
159
160
	      // FX(a) = XF(a)
	      u = dynamic_cast<unop*>(result_);
	      if (u && u->op() == unop::X)
		{
161
		  formula* res =
162
163
164
		    unop::instance(unop::X,
				   unop::instance(unop::F,
						  basic_reduce(u->child())));
165
		  u->destroy();
166
167
		  // FXX(a) = XXF(a) ...
		  result_ = basic_reduce(res);
168
		  res->destroy();
169
170
		  return;
		}
martinez's avatar
martinez committed
171

172
173
174
175
176
177
178
	      // F(f1 & GF(f2)) = F(f1) & GF(F2)
	      mo = dynamic_cast<multop*>(result_);
	      if (mo && mo->op() == multop::And)
		{
		  result_ = param_case(mo, unop::F, multop::And);
		  return;
		}
179

180
181
	      result_ = unop::instance(unop::F, result_);
	      return;
182

183
184
185
186
	    case unop::G:
	      // G(true) = true
	      // G(false) = false
	      if (dynamic_cast<constant*>(result_))
187
		return;
martinez's avatar
martinez committed
188

189
190
191
192
193
194
	      // G(a R b) = G(b)
	      bo = dynamic_cast<binop*>(result_);
	      if (bo && bo->op() == binop::R)
		{
		  result_ = unop::instance(unop::G,
					   basic_reduce(bo->second()));
195
		  bo->destroy();
196
197
198
199
200
201
202
		  return;
		}

	      // GX(a) = XG(a)
	      u = dynamic_cast<unop*>(result_);
	      if (u && u->op() == unop::X)
		{
203
		  formula* res =
204
205
206
		    unop::instance(unop::X,
				   unop::instance(unop::G,
						  basic_reduce(u->child())));
207
		  u->destroy();
208
209
210
		  // GXX(a) = XXG(a) ...
		  // GXF(a) = XGF(a) = GF(a) ...
		  result_ = basic_reduce(res);
211
		  res->destroy();
212
213
214
215
216
217
218
219
220
221
222
223
224
		  return;
		}

	      // G(f1 | GF(f2)) = G(f1) | GF(F2)
	      mo = dynamic_cast<multop*>(result_);
	      if (mo && mo->op() == multop::Or)
		{
		  result_ = param_case(mo, unop::G, multop::Or);
		  return;
		}

	      result_ = unop::instance(unop::G, result_);
	      return;
225
226
227
228

	    case unop::Finish:
	      result_ = unop::instance(unop::Finish, result_);
	      return;
martinez's avatar
martinez committed
229
	    }
230
231
232
	  /* Unreachable code.  */
	  assert(0);
	}
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
266
267
268
269
270
271
272
273
274
275
276
277
	void
	visit(binop* bo)
	{
	  formula* f1 = bo->first();
	  formula* f2 = bo->second();
	  unop* fu1;
	  unop* fu2;
	  switch (bo->op())
	    {
	    case binop::Xor:
	    case binop::Equiv:
	    case binop::Implies:
	      result_ = binop::instance(bo->op(),
					basic_reduce(f1),
					basic_reduce(f2));
	      return;
	    case binop::U:
	    case binop::R:
	      f2 = basic_reduce(f2);

	      // a U false = false
	      // a U true = true
	      // a R false = false
	      // a R true = true
	      if (dynamic_cast<constant*>(f2))
		{
		  result_ = f2;
		  return;
		}

	      f1 = basic_reduce(f1);

	      // X(a) U X(b) = X(a U b)
	      // X(a) R X(b) = X(a R b)
	      fu1 = dynamic_cast<unop*>(f1);
	      fu2 = dynamic_cast<unop*>(f2);
	      if (fu1 && fu2
		  && fu1->op() == unop::X
		  && fu2->op() == unop::X)
		{
		  formula* ftmp = binop::instance(bo->op(),
						  basic_reduce(fu1->child()),
						  basic_reduce(fu2->child()));
		  result_ = unop::instance(unop::X, basic_reduce(ftmp));
278
279
280
		  f1->destroy();
		  f2->destroy();
		  ftmp->destroy();
281
		  return;
martinez's avatar
martinez committed
282
	      }
283

284
285
286
287
288
289
290
	      result_ = binop::instance(bo->op(), f1, f2);
	      return;
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

291
292
293
294
295
296
	void
	visit(automatop*)
	{
	  assert(0);
	}

297
298
299
300
301
302
303
304
305
306
307
	void
	visit(multop* mo)
	{
	  multop::type op = mo->op();
	  unsigned mos = mo->size();
	  multop::vec* res = new multop::vec;

	  multop::vec* tmpX = new multop::vec;
	  multop::vec* tmpU = new multop::vec;
	  multop::vec* tmpR = new multop::vec;
	  multop::vec* tmpFG = new multop::vec;
308
	  multop::vec* tmpF = new multop::vec;
309
	  multop::vec* tmpGF = new multop::vec;
310
	  multop::vec* tmpG = new multop::vec;
311
312
313
314
315
316
317
318
319
320
321
322

	  multop::vec* tmpOther = new multop::vec;

	  for (unsigned i = 0; i < mos; ++i)
	    res->push_back(basic_reduce(mo->nth(i)));

	  switch (op)
	    {
	    case multop::And:

	      for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
		{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
323
324
		  // An iteration of the loop may zero some later elements
		  // of the vector to mark them as redundant.  Skip them.
325
326
327
328
329
330
		  if (!*i)
		    continue;
		  unop* uo = dynamic_cast<unop*>(*i);
		  binop* bo = dynamic_cast<binop*>(*i);
		  if (uo)
		    {
331
		      if (uo->op() == unop::X)
332
333
			{
			  // Xa & Xb = X(a & b)
334
			  tmpX->push_back(uo->child()->clone());
335
336
337
338
339
			}
		      else if (is_FG(*i))
			{
			  // FG(a) & FG(b) = FG(a & b)
			  unop* uo2 = dynamic_cast<unop*>(uo->child());
340
			  tmpFG->push_back(uo2->child()->clone());
341
			}
342
343
344
345
346
		      else if (uo->op() == unop::G)
			{
			  // G(a) | G(b) = G(a | b)
			  tmpG->push_back(uo->child()->clone());
			}
347
348
		      else
			{
349
			  tmpOther->push_back((*i)->clone());
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
			}
		    }
		  else if (bo)
		    {
		      if (bo->op() == binop::U)
			{
			  // (a U b) & (c U b) = (a & c) U b
			  formula* ftmp = dynamic_cast<binop*>(*i)->second();
			  multop::vec* tmpUright = new multop::vec;
			  for (multop::vec::iterator j = i; j != res->end();
			       j++)
			    {
			      if (!*j)
				continue;
			      binop* bo2 = dynamic_cast<binop*>(*j);
			      if (bo2 && bo2->op() == binop::U
				  && ftmp == bo2->second())
				{
				  tmpUright
369
				    ->push_back(bo2->first()->clone());
370
371
				  if (j != i)
				    {
372
				      (*j)->destroy();
373
374
375
376
377
378
379
380
381
382
				      *j = 0;
				    }
				}
			    }
			  tmpU
			    ->push_back(binop::instance(binop::U,
							multop::
							instance(multop::
								 And,
								 tmpUright),
383
							ftmp->clone()));
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
			}
		      else if (bo->op() == binop::R)
			{
			  // (a R b) & (a R c) = a R (b & c)
			  formula* ftmp = dynamic_cast<binop*>(*i)->first();
			  multop::vec* tmpRright = new multop::vec;
			  for (multop::vec::iterator j = i; j != res->end();
			       j++)
			    {
			      if (!*j)
				continue;
			      binop* bo2 = dynamic_cast<binop*>(*j);
			      if (bo2 && bo2->op() == binop::R
				  && ftmp == bo2->first())
				{
				  tmpRright
400
				    ->push_back(bo2->second()->clone());
401
402
				  if (j != i)
				    {
403
				      (*j)->destroy();
404
405
406
407
408
409
				      *j = 0;
				    }
				}
			    }
			  tmpR
			    ->push_back(binop::instance(binop::R,
410
							ftmp->clone(),
411
412
413
414
415
416
							multop::
							instance(multop::And,
								 tmpRright)));
			}
		      else
			{
417
			  tmpOther->push_back((*i)->clone());
418
419
420
421
			}
		    }
		  else
		    {
422
		      tmpOther->push_back((*i)->clone());
423
		    }
424
		  (*i)->destroy();
425
426
427
428
429
430
431
432
433
434
435
436
437
		}
	      break;

	    case multop::Or:

	      for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
		{
		  if (!*i)
		    continue;
		  unop* uo = dynamic_cast<unop*>(*i);
		  binop* bo = dynamic_cast<binop*>(*i);
		  if (uo)
		    {
438
		      if (uo->op() == unop::X)
439
440
			{
			  // Xa | Xb = X(a | b)
441
			  tmpX->push_back(uo->child()->clone());
442
443
444
445
446
			}
		      else if (is_GF(*i))
			{
			  // GF(a) | GF(b) = GF(a | b)
			  unop* uo2 = dynamic_cast<unop*>(uo->child());
447
			  tmpGF->push_back(uo2->child()->clone());
448
			}
449
		      else if (uo->op() == unop::F)
450
			{
451
452
			  // F(a) | F(b) = F(a | b)
			  tmpF->push_back(uo->child()->clone());
453
454
455
			}
		      else
			{
456
			  tmpOther->push_back((*i)->clone());
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
			}
		    }
		  else if (bo)
		    {
		      if (bo->op() == binop::U)
			{
			  // (a U b) | (a U c) = a U (b | c)
			  formula* ftmp = bo->first();
			  multop::vec* tmpUright = new multop::vec;
			  for (multop::vec::iterator j = i; j != res->end();
			       j++)
			    {
			      if (!*j)
				continue;
			      binop* bo2 = dynamic_cast<binop*>(*j);
			      if (bo2 && bo2->op() == binop::U
				  && ftmp == bo2->first())
				{
				  tmpUright
476
				    ->push_back(bo2->second()->clone());
477
478
				  if (j != i)
				    {
479
				      (*j)->destroy();
480
481
482
483
484
				      *j = 0;
				    }
				}
			    }
			  tmpU->push_back(binop::instance(binop::U,
485
							  ftmp->clone(),
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
							  multop::
							  instance(multop::Or,
								   tmpUright)));
			}
		      else if (bo->op() == binop::R)
			{
			  // (a R b) | (c R b) = (a | c) R b
			  formula* ftmp = dynamic_cast<binop*>(*i)->second();
			  multop::vec* tmpRright = new multop::vec;
			  for (multop::vec::iterator j = i; j != res->end();
			       j++)
			    {
			      if (!*j)
				continue;
			      binop* bo2 = dynamic_cast<binop*>(*j);
			      if (bo2 && bo2->op() == binop::R
				  && ftmp == bo2->second())
				{
				  tmpRright
505
				    ->push_back(bo2->first()->clone());
506
507
				  if (j != i)
				    {
508
				      (*j)->destroy();
509
510
511
512
513
514
				      *j = 0;
				    }
				}
			    }
			  tmpR
			    ->push_back(binop::instance(binop::R,
515
516
							multop::
							instance(multop::Or,
517
								 tmpRright),
518
							ftmp->clone()));
519
520
521
			}
		      else
			{
522
			  tmpOther->push_back((*i)->clone());
523
524
525
526
			}
		    }
		  else
		    {
527
		      tmpOther->push_back((*i)->clone());
528
		    }
529
		  (*i)->destroy();
530
531
532
533
		}

	      break;
	    }
534

535
536
	  res->clear();
	  delete res;
537

538

539
540
541
542
	  if (tmpX && !tmpX->empty())
	    tmpOther->push_back(unop::instance(unop::X,
					       multop::instance(mo->op(),
								tmpX)));
543
	  else
544
	    delete tmpX;
545

546
547
548
549
550
551
552
553
554
555
556
557
558
	  if (!tmpF->empty())
	    tmpOther->push_back(unop::instance(unop::F,
					       multop::instance(mo->op(),
								tmpF)));
	  else
	    delete tmpF;

	  if (!tmpG->empty())
	    tmpOther->push_back(unop::instance(unop::G,
					       multop::instance(mo->op(),
								tmpG)));
	  else
	    delete tmpG;
559

560
	  if (!tmpU->empty())
561
	    tmpOther->push_back(multop::instance(mo->op(), tmpU));
562
	  else
563
	    delete tmpU;
564

565

566
	  if (!tmpR->empty())
567
	    tmpOther->push_back(multop::instance(mo->op(), tmpR));
568
	  else
569
	    delete tmpR;
570

571
	  if (!tmpGF->empty())
572
573
574
575
576
577
578
579
	    {
	      formula* ftmp
		= unop::instance(unop::G,
				 unop::instance(unop::F,
						multop::instance(mo->op(),
								 tmpGF)));
	      tmpOther->push_back(ftmp);
	    }
580
	  else
581
	    delete tmpGF;
582
583


584
	  if (!tmpFG->empty())
585
586
587
588
589
590
591
592
593
594
595
596
597
598
	    {
	      formula* ftmp = 0;
	      if (mo->op() == multop::And)
		ftmp
		  = unop::instance(unop::F,
				   unop::instance(unop::G,
						  multop::instance(mo->op(),
								   tmpFG)));
	      else
		ftmp
		  = unop::instance(unop::F,
				   multop::instance(mo->op(), tmpFG));
	      tmpOther->push_back(ftmp);
	    }
599
	  else
600
	    delete tmpFG;
601

602

603
	  result_ = multop::instance(op, tmpOther);
martinez's avatar
martinez committed
604

605
606
	  return;
	}
607

608
609
610
611
      protected:
	formula* result_;
      };
    }
martinez's avatar
martinez committed
612

613
614
    formula*
    basic_reduce(const formula* f)
martinez's avatar
martinez committed
615
    {
616
      basic_reduce_visitor v;
martinez's avatar
martinez committed
617
618
619
620
621
622
      const_cast<formula*>(f)->accept(v);
      return v.result();
    }

  }
}