ltl2tgba.cc 14.3 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// 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.

22
23
#include <iostream>
#include <cassert>
24
25
#include <fstream>
#include <string>
26
#include "ltlvisit/destroy.hh"
27
#include "ltlvisit/reducform.hh"
28
#include "ltlvisit/tostring.hh"
29
30
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
31
#include "tgbaalgos/ltl2tgba_lacim.hh"
32
#include "tgbaalgos/ltl2tgba_fm.hh"
33
#include "tgba/bddprint.hh"
34
#include "tgbaalgos/dotty.hh"
35
#include "tgbaalgos/lbtt.hh"
36
#include "tgba/tgbatba.hh"
37
#include "tgbaalgos/magic.hh"
38
39
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
40
#include "tgbaparse/public.hh"
41
#include "tgbaalgos/dupexp.hh"
42
#include "tgbaalgos/neverclaim.hh"
43

44
45
#include "tgbaalgos/reductgba_sim.hh"

46
47
48
void
syntax(char* prog)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
  std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
50
            << "       "<< prog << " -F [OPTIONS...] file" << std::endl
51
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
52
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
53
	    << "Options:" << std::endl
54
	    << "  -a   display the acceptance_conditions BDD, not the "
55
	    << "reachability graph"
56
	    << std::endl
57
	    << "  -A   same as -a, but as a set" << std::endl
58
	    << "  -d   turn on traces during parsing" << std::endl
59
	    << "  -D   degeneralize the automaton" << std::endl
60
61
	    << "  -e   emptiness-check (Couvreur), expect and compute "
	    << "a counter-example" << std::endl
62
63
	    << "  -e2  emptiness-check (Couvreur variant), expect and compute "
	    << "a counter-example" << std::endl
64
65
	    << "  -E   emptiness-check (Couvreur), expect no counter-example "
	    << std::endl
66
67
	    << "  -E2  emptiness-check (Couvreur variant), expect no "
	    << "counter-example " << std::endl
68
69
70
            << "  -f   use Couvreur's FM algorithm for translation"
	    << std::endl
            << "  -F   read the formula from the file" << std::endl
71
            << "  -L   fair-loop approximation (implies -f)" << std::endl
72
73
74
75
76
77
	    << "  -m   magic-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -M   magic-search (implies -D), expect no counter-example"
	    << std::endl
	    << "  -n   same as -m, but display more counter-examples"
	    << std::endl
78
79
	    << "  -N   display the never clain for Spin "
	    << "(implies -D)" << std::endl
80
            << "  -p   branching postponement (implies -f)" << std::endl
81
	    << "  -r   display the relation BDD, not the reachability graph"
82
	    << std::endl
83
84
85
86
87
88
	    << "  -r1  reduce formula using basic rewriting" << std::endl
	    << "  -r2  reduce formula using class of eventuality and "
	    << "and universality" << std::endl
	    << "  -r3  reduce formula using implication between "
	    << "sub-formulae" << std::endl
	    << "  -r4  reduce formula using all rules" << std::endl
89
	    << "  -rd  display the reduce formula" << std::endl
90
	    << "  -R   same as -r, but as a set" << std::endl
91
92
93
94
	    << "  -s   convert to explicit automata, and number states "
	    << "in DFS order" << std::endl
	    << "  -S   convert to explicit automata, and number states "
	    << "in BFS order" << std::endl
95
	    << "  -t   display reachable states in LBTT's format" << std::endl
96
97
	    << "  -T   display reachable states in LBTT's format w/o "
	    << "acceptance conditions" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
98
	    << "  -v   display the BDD variables used by the automaton"
99
	    << std::endl
100
101
            << "  -x   try to produce a more deterministic automata "
	    << "(implies -f)" << std::endl
102
	    << "  -X   do not compute an automaton, read it from a file"
103
104
	    << std::endl
	    << "  -y   do not merge states with same symbolic representation "
105
106
107
108
109
110
111
112
113
114
115
	    << "(implies -f)" << std::endl
	    << "  -R1  use direct simulation to reduce the automata "
	    << "(implies -L)"
	    << std::endl
	    << "  -R2  use delayed simulation to reduce the automata, incorrect"
	    << "(implies -L)"
	    << std::endl
	    << "  -R3  use SCC to reduce the automata"
	    << std::endl
	    << "  -Rd  to display simulation relation"
	    << std::endl;
116
117
118
119
120
121
122
123
  exit(2);
}

int
main(int argc, char** argv)
{
  int exit_code = 0;

124
  bool debug_opt = false;
125
  bool degeneralize_opt = false;
126
  bool fm_opt = false;
127
  bool fm_exprop_opt = false;
128
  bool fm_symb_merge_opt = true;
129
  bool file_opt = false;
130
  int output = 0;
131
  int formula_index = 0;
132
  enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
133
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
134
135
  bool magic_many = false;
  bool expect_counter_example = false;
136
  bool from_file = false;
137
  int reduc_aut = spot::Reduce_None;
138
  int redopt = spot::ltl::Reduce_None;
139
140
  bool display_reduce_form = false;
  bool display_rel_sim = false;
141
  bool post_branching = false;
142
  bool fair_loop_approx = false;
143

144
  for (;;)
145
    {
146
      if (argc < formula_index + 2)
147
	syntax(argv[0]);
148
149
150

      ++formula_index;

151
152
153
154
155
156
157
158
159
      if (!strcmp(argv[formula_index], "-a"))
	{
	  output = 2;
	}
      else if (!strcmp(argv[formula_index], "-A"))
	{
	  output = 4;
	}
      else if (!strcmp(argv[formula_index], "-d"))
160
161
162
	{
	  debug_opt = true;
	}
163
164
165
166
      else if (!strcmp(argv[formula_index], "-D"))
	{
	  degeneralize_opt = true;
	}
167
168
169
170
171
172
      else if (!strcmp(argv[formula_index], "-e"))
	{
	  echeck = Couvreur;
	  expect_counter_example = true;
	  output = -1;
	}
173
174
175
176
177
178
      else if (!strcmp(argv[formula_index], "-e2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = true;
	  output = -1;
	}
179
180
181
182
183
184
      else if (!strcmp(argv[formula_index], "-E"))
	{
	  echeck = Couvreur;
	  expect_counter_example = false;
	  output = -1;
	}
185
186
187
188
189
190
      else if (!strcmp(argv[formula_index], "-E2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = false;
	  output = -1;
	}
191
192
193
194
195
196
197
198
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
199
200
201
202
203
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
      else if (!strcmp(argv[formula_index], "-m"))
	{
	  echeck = MagicSearch;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-M"))
	{
	  echeck = MagicSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-n"))
	{
	  echeck = MagicSearch;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	  magic_many = true;
	}
226
227
228
229
230
      else if (!strcmp(argv[formula_index], "-N"))
	{
	  degeneralize_opt = true;
	  output = 8;
	}
231
232
233
234
235
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
236
237
      else if (!strcmp(argv[formula_index], "-r"))
	{
238
239
	  output = 1;
	}
240
241
242
243
244
245
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
246
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
247
248
249
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
250
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
251
252
253
254
255
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
256
257
258
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
259
	}
260
261
262
263
264
265
266
267
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
268
269
270
271
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
272
273
274
275
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  output = 7;
	}
276
277
278
279
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
280
281
282
283
284
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
285
286
287
288
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
289
290
291
292
293
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
      else if (!strcmp(argv[formula_index], "-R1"))
	{
	  reduc_aut |= spot::Reduce_Dir_Sim;
	  fair_loop_approx = true;
	}
      else if (!strcmp(argv[formula_index], "-R2"))
	{
	  reduc_aut |= spot::Reduce_Del_Sim;
	  fair_loop_approx = true;
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	}
      else if (!strcmp(argv[formula_index], "-rd"))
	{
	  display_reduce_form = true;
	}
      else if (!strcmp(argv[formula_index], "-Rd"))
	{
	  display_rel_sim = true;
	}
316
317
318
319
      else
	{
	  break;
	}
320
321
    }

322
323
324
325
  std::string input;

  if (file_opt)
    {
326
      if (strcmp(argv[formula_index], "-"))
327
	{
328
	  std::ifstream fin(argv[formula_index]);
329
	  if (!fin)
330
331
332
333
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
334

335
	  if (!std::getline(fin, input, '\0'))
336
337
338
339
340
341
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
342
	{
343
	  std::getline(std::cin, input, '\0');
344
345
346
347
348
349
350
	}
    }
  else
    {
      input = argv[formula_index];
    }

351
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
352
  spot::bdd_dict* dict = new spot::bdd_dict();
353
354
355
356
357
358
359
360
361

  spot::ltl::formula* f = 0;
  if (!from_file)
    {
      spot::ltl::parse_error_list pel;
      f = spot::ltl::parse(input, pel, env, debug_opt);
      exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
    }
  if (f || from_file)
362
    {
363
364
365
366
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

367
368
369
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
370
371
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
372
373
	  if (spot::format_tgba_parse_errors(std::cerr, pel))
	    return 2;
374
	  e->merge_transitions();
375
	}
376
      else
377
	{
378
	  if (redopt != spot::ltl::Reduce_None)
379
	    {
380
381
382
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
383
384
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
385
	    }
386

387
	  if (fm_opt)
388
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
389
					       fm_symb_merge_opt,
390
391
					       post_branching,
					       fair_loop_approx);
392
393
394
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
395

396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
      /*
	spot::tgba* aut_red = 0;
	if (reduc_aut != spot::Reduce_None)
	a = aut_red = spot::reduc_tgba_sim(a, reduc_aut);
      */

      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
	  if ((reduc_aut & spot::Reduce_Dir_Sim) ||
	      (reduc_aut & spot::Reduce_Del_Sim))
	    {
	      spot::simulation_relation* rel;
	      if (reduc_aut & spot::Reduce_Dir_Sim)
		rel = spot::get_direct_relation_simulation(a);
	      else if (reduc_aut & spot::Reduce_Del_Sim)
		rel = spot::get_delayed_relation_simulation(a, 1);
	      else
		assert(0);

	      if (display_rel_sim)
		aut_red->display_rel_sim(rel, std::cout);

	      if (reduc_aut & spot::Reduce_Dir_Sim)
		aut_red->prune_automata(rel);
	      else if (reduc_aut & spot::Reduce_Del_Sim)
		aut_red->quotient_state(rel);
	      else
		assert(0);

	      spot::free_relation_simulation(rel);
	    }

	  if (reduc_aut & spot::Reduce_Scc)
	    {
	      aut_red->prune_scc();
	    }
	}

436
      spot::tgba_tba_proxy* degeneralized = 0;
437
438
439
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

440
441
442
443
444
445
446
447
448
449
450
451
452
      spot::tgba_explicit* expl = 0;
      switch (dupexp)
	{
	case NoneDup:
	  break;
	case BFS:
	  a = expl = tgba_dupexp_bfs(a);
	  break;
	case DFS:
	  a = expl = tgba_dupexp_dfs(a);
	  break;
	}

453
454
      switch (output)
	{
455
456
457
	case -1:
	  /* No output.  */
	  break;
458
459
460
461
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
462
463
464
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
465
466
	  break;
	case 2:
467
468
469
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
470
				get_core_data().acceptance_conditions);
471
472
	  break;
	case 3:
473
474
475
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
476
477
	  break;
	case 4:
478
479
480
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
481
				get_core_data().acceptance_conditions);
482
	  break;
483
	case 5:
484
	  a->get_dict()->dump(std::cout);
485
	  break;
486
487
488
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
489
490
491
	case 7:
	  spot::nonacceptant_lbtt_reachable(std::cout, a);
	  break;
492
493
494
	case 8:
	  spot::never_claim_reachable(std::cout, degeneralized, f);
	  break;
495
496
497
	default:
	  assert(!"unknown output option");
	}
498

499
500
501
502
503
      switch (echeck)
	{
	case None:
	  break;
	case Couvreur:
504
	case Couvreur2:
505
	  {
506
	    spot::emptiness_check* ec;
507
	    if (echeck == Couvreur)
508
	      ec = new spot::emptiness_check(a);
509
	    else
510
511
512
	      ec = new spot::emptiness_check_shy(a);

	    bool res = ec->check();
513

514
515
516
517
518
	    if (expect_counter_example)
	      {
		if (res)
		  {
		    exit_code = 1;
519
		    delete ec;
520
521
		    break;
		  }
522
		spot::counter_example ce(ec->result());
523
		ce.print_result(std::cout);
524
525
526
527
528
	      }
	    else
	      {
		exit_code = !res;
	      }
529
	    delete ec;
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
	  }
	  break;
	case MagicSearch:
	  {
	    spot::magic_search ms(degeneralized);
	    bool res = ms.check();
	    if (expect_counter_example)
	      {
		if (!res)
		  {
		    exit_code = 1;
		    break;
		  }
		do
		  ms.print_result(std::cout);
		while (magic_many && ms.check());
	      }
	    else
	      {
		exit_code = res;
	      }
	  }
	  break;
	}

555
556
      if (f)
        spot::ltl::destroy(f);
557
558
      if (expl)
	delete expl;
559
560
      if (degeneralize_opt)
	delete degeneralized;
561
562
      if (aut_red)
	delete aut_red;
563

564
      delete to_free;
565
566
567
568
569
570
571
572
573
574
    }
  else
    {
      exit_code = 1;
    }

  assert(spot::ltl::atomic_prop::instance_count() == 0);
  assert(spot::ltl::unop::instance_count() == 0);
  assert(spot::ltl::binop::instance_count() == 0);
  assert(spot::ltl::multop::instance_count() == 0);
575
  delete dict;
576
577
  return exit_code;
}