syntimpl.cc 10.7 KB
Newer Older
1
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
Guillaume Sadegh's avatar
Guillaume Sadegh committed
2
3
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
martinez's avatar
martinez committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// 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
// 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 "syntimpl.hh"
25
#include "ltlast/allnodes.hh"
martinez's avatar
martinez committed
26
27
28
#include <cassert>

#include "lunabbrev.hh"
29
#include "simpfg.hh"
martinez's avatar
martinez committed
30
31
32
33
34
35
#include "nenoform.hh"

namespace spot
{
  namespace ltl
  {
36
    namespace
martinez's avatar
martinez committed
37
    {
38

39
      class inf_right_recurse_visitor: public const_visitor
martinez's avatar
martinez committed
40
      {
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
      public:

	inf_right_recurse_visitor(const formula *f)
	  : result_(false), f(f)
	{
	}

	virtual
	~inf_right_recurse_visitor()
	{
	}

	int
	result() const
	{
	  return result_;
	}

	void
	visit(const atomic_prop* ap)
	{
	  if (dynamic_cast<const atomic_prop*>(f) == ap)
	    result_ = true;
	}
65

66
67
68
69
	void
	visit(const constant* c)
	{
	  switch (c->val())
70
	    {
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
	    case constant::True:
	      result_ = true;
	      return;
	    case constant::False:
	      result_ = false;
	      return;
	    }
	}

	void
	visit(const unop* uo)
	{
	  const formula* f1 = uo->child();
	  switch (uo->op())
	    {
	    case unop::Not:
	      if (uo == f)
		result_ = true;
	      return;
	    case unop::X:
	      {
		const unop* op = dynamic_cast<const unop*>(f);
		if (op && op->op() == unop::X)
		  result_ = syntactic_implication(op->child(), f1);
	      }
	      return;
	    case unop::F:
	      /* F(a) = true U a */
	      result_ = syntactic_implication(f, f1);
	      return;
	    case unop::G:
	      /* G(a) = false R a */
	      if (syntactic_implication(f, constant::false_instance()))
		result_ = true;
	      return;
106
107
	    case unop::Finish:
	      return;
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

	void
	visit(const binop* bo)
	{
	  const formula* f1 = bo->first();
	  const formula* f2 = bo->second();
	  const binop* fb = dynamic_cast<const binop*>(f);
	  const unop* fu = dynamic_cast<const unop*>(f);
	  switch (bo->op())
	    {
	    case binop::Xor:
	    case binop::Equiv:
	    case binop::Implies:
	      return;
	    case binop::U:
127
	    case binop::W:
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
	      if (syntactic_implication(f, f2))
		result_ = true;
	      return;
	    case binop::R:
	      if (fb && fb->op() == binop::R)
		if (syntactic_implication(fb->first(), f1) &&
		    syntactic_implication(fb->second(), f2))
		  {
		    result_ = true;
		    return;
		  }
	      if (fu && fu->op() == unop::G)
		if (f1 == constant::false_instance() &&
		    syntactic_implication(fu->child(), f2))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f, f1)
		  && syntactic_implication(f, f2))
		result_ = true;
	      return;
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
	    case binop::M:
	      if (fb && fb->op() == binop::M)
		if (syntactic_implication(fb->first(), f1) &&
		    syntactic_implication(fb->second(), f2))
		  {
		    result_ = true;
		    return;
		  }
	      if (fu && fu->op() == unop::F)
		if (f2 == constant::true_instance() &&
		    syntactic_implication(fu->child(), f1))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f, f1)
		  && syntactic_implication(f, f2))
		result_ = true;
	      return;
169
	    }
170
171
172
173
	  /* Unreachable code.  */
	  assert(0);
	}

174
175
176
177
178
179
	void
	visit(const automatop*)
	{
	  assert(0);
	}

180
181
182
183
184
185
	void
	visit(const multop* mo)
	{
	  multop::type op = mo->op();
	  unsigned mos = mo->size();
	  switch (op)
186
	    {
187
188
189
190
191
192
193
194
195
196
	    case multop::And:
	      for (unsigned i = 0; i < mos; ++i)
		if (!syntactic_implication(f, mo->nth(i)))
		  return;
	      result_ = true;
	      break;
	    case multop::Or:
	      for (unsigned i = 0; i < mos && !result_; ++i)
		if (syntactic_implication(f, mo->nth(i)))
		  result_ = true;
197
198
	      break;
	    }
199
200
201
202
203
204
205
206
207
208
	}

      protected:
	bool result_; /* true if f < f1, false otherwise. */
	const formula* f;
      };

      /////////////////////////////////////////////////////////////////////////

      class inf_left_recurse_visitor: public const_visitor
martinez's avatar
martinez committed
209
      {
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
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
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
      public:

	inf_left_recurse_visitor(const formula *f)
	  : result_(false), f(f)
	{
	}

	virtual
	~inf_left_recurse_visitor()
	{
	}

	bool
	special_case(const formula* f2)
	{
	  const binop* fb = dynamic_cast<const binop*>(f);
	  const binop* f2b = dynamic_cast<const binop*>(f2);
	  if (fb && f2b && fb->op() == f2b->op()
	      && syntactic_implication(f2b->first(), fb->first())
	      && syntactic_implication(f2b->second(), fb->second()))
	    return true;
	  return false;
	}

	int
	result() const
	{
	  return result_;
	}

	void
	visit(const atomic_prop* ap)
	{
	  inf_right_recurse_visitor v(ap);
	  const_cast<formula*>(f)->accept(v);
	  result_ = v.result();
	}

	void
	visit(const constant* c)
	{
	  inf_right_recurse_visitor v(c);
	  switch (c->val())
	    {
	    case constant::True:
	      const_cast<formula*>(f)->accept(v);
	      result_ = v.result();
	      return;
	    case constant::False:
	      result_ = true;
	      return;
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

	void
	visit(const unop* uo)
	{
	  const formula* f1 = uo->child();
	  inf_right_recurse_visitor v(uo);
	  switch (uo->op())
	    {
	    case unop::Not:
	      if (uo == f)
		result_ = true;
	      return;
	    case unop::X:
	      {
		const unop* op = dynamic_cast<const unop*>(f);
		if (op && op->op() == unop::X)
		  result_ = syntactic_implication(f1, op->child());
	      }
	      return;
	    case unop::F:
	      {
		/* F(a) = true U a */
		const formula* tmp = binop::instance(binop::U,
						     constant::true_instance(),
289
						     f1->clone());
290
291
292
		if (special_case(tmp))
		  {
		    result_ = true;
293
		    tmp->destroy();
294
295
296
297
		    return;
		  }
		if (syntactic_implication(tmp, f))
		  result_ = true;
298
		tmp->destroy();
299
300
301
302
303
304
305
		return;
	      }
	    case unop::G:
	      {
		/* G(a) = false R a */
		const formula* tmp = binop::instance(binop::R,
						     constant::false_instance(),
306
						     f1->clone());
307
308
309
		if (special_case(tmp))
		  {
		    result_ = true;
310
		    tmp->destroy();
311
312
313
314
		    return;
		  }
		if (syntactic_implication(tmp, f))
		  result_ = true;
315
		tmp->destroy();
316
317
		return;
	      }
318
319
	    case unop::Finish:
	      return;
320
321
322
323
324
325
326
327
328
329
330
331
332
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

	void
	visit(const binop* bo)
	{
	  if (special_case(bo))
	    {
	      result_ = true;
	      return;
	    }
martinez's avatar
martinez committed
333

334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
	  const formula* f1 = bo->first();
	  const formula* f2 = bo->second();
	  const binop* fb = dynamic_cast<const binop*>(f);
	  const unop* fu = dynamic_cast<const unop*>(f);
	  switch (bo->op())
	    {
	    case binop::Xor:
	    case binop::Equiv:
	    case binop::Implies:
	      return;
	    case binop::U:
	      /* (a < c) && (c < d) => a U b < c U d */
	      if (fb && fb->op() == binop::U)
		if (syntactic_implication(f1, fb->first()) &&
		    syntactic_implication(f2, fb->second()))
		  {
		    result_ = true;
		    return;
		  }
	      if (fu && fu->op() == unop::F)
		if (f1 == constant::true_instance() &&
		    syntactic_implication(f2, fu->child()))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f1, f)
		  && syntactic_implication(f2, f))
		result_ = true;
	      return;
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
	    case binop::W:
	      /* (a < c) && (c < d) => a W b < c W d */
	      if (fb && fb->op() == binop::W)
		if (syntactic_implication(f1, fb->first()) &&
		    syntactic_implication(f2, fb->second()))
		  {
		    result_ = true;
		    return;
		  }
	      if (fu && fu->op() == unop::G)
		if (f2 == constant::false_instance() &&
		    syntactic_implication(f1, fu->child()))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f1, f)
		  && syntactic_implication(f2, f))
		result_ = true;
	      return;
384
385
386
387
388
389
390
391
392
393
394
	    case binop::R:
	      if (fu && fu->op() == unop::G)
		if (f1 == constant::false_instance() &&
		    syntactic_implication(f2, fu->child()))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f2, f))
		result_ = true;
	      return;
395
396
397
398
399
400
401
402
403
404
405
	    case binop::M:
	      if (fu && fu->op() == unop::F)
		if (f2 == constant::true_instance() &&
		    syntactic_implication(f1, fu->child()))
		  {
		    result_ = true;
		    return;
		  }
	      if (syntactic_implication(f2, f))
		result_ = true;
	      return;
406
407
408
409
410
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

411
412
413
414
415
416
	void
	visit(const automatop*)
	{
	  assert(0);
	}

417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
	void
	visit(const multop* mo)
	{
	  multop::type op = mo->op();
	  unsigned mos = mo->size();
	  switch (op)
	    {
	    case multop::And:
	      for (unsigned i = 0; (i < mos) && !result_; ++i)
		if (syntactic_implication(mo->nth(i), f))
		  result_ = true;
	      break;
	    case multop::Or:
	      for (unsigned i = 0; i < mos; ++i)
		if (!syntactic_implication(mo->nth(i), f))
		  return;
	      result_ = true;
	      break;
	    }
	}
martinez's avatar
martinez committed
437

438
439
440
441
      protected:
	bool result_; /* true if f1 < f, 1 otherwise. */
	const formula* f;
      };
martinez's avatar
martinez committed
442

443
    } // anonymous
444

445
446
    // This is called by syntactic_implication() after the
    // formulae have been normalized.
447
    bool
448
    syntactic_implication(const formula* f1, const formula* f2)
martinez's avatar
martinez committed
449
    {
450
451
452
453
454
      if (f1 == f2)
	return true;
      if (f2 == constant::true_instance()
	  || f1 == constant::false_instance())
	return true;
455

456
457
458
      inf_left_recurse_visitor v1(f2);
      inf_right_recurse_visitor v2(f1);

martinez's avatar
martinez committed
459
      const_cast<formula*>(f1)->accept(v1);
460
      if (v1.result())
martinez's avatar
martinez committed
461
462
463
	return true;

      const_cast<formula*>(f2)->accept(v2);
464
      if (v2.result())
martinez's avatar
martinez committed
465
	return true;
466

martinez's avatar
martinez committed
467
468
      return false;
    }
469

470
    bool
471
    syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
martinez's avatar
martinez committed
472
    {
473
474
      formula* l = f1->clone();
      formula* r = f2->clone();
475
      if (right)
476
	r = unop::instance(unop::Not, r);
477
      else
478
479
480
	l = unop::instance(unop::Not, l);

      formula* tmp = unabbreviate_logic(l);
481
      l->destroy();
482
      l = simplify_f_g(tmp);
483
      tmp->destroy();
484
      tmp = negative_normal_form(l);
485
      l->destroy();
486
487
488
      l = tmp;

      tmp = unabbreviate_logic(r);
489
      r->destroy();
490
      r = simplify_f_g(tmp);
491
      tmp->destroy();
492
      tmp = negative_normal_form(r);
493
      r->destroy();
494
495
496
      r = tmp;

      bool result = syntactic_implication(l, r);
497
498
      l->destroy();
      r->destroy();
499
      return result;
martinez's avatar
martinez committed
500
501
502
    }
  }
}