ltl2tgba.cc 14.2 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
95
96
97
98
99
100
	    << "  -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
101
102
103
104
	    << "  -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
105
	    << "  -t   display reachable states in LBTT's format" << std::endl
106
107
	    << "  -T   display reachable states in LBTT's format w/o "
	    << "acceptance conditions" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
108
	    << "  -v   display the BDD variables used by the automaton"
109
	    << std::endl
110
111
            << "  -x   try to produce a more deterministic automata "
	    << "(implies -f)" << std::endl
112
	    << "  -X   do not compute an automaton, read it from a file"
113
114
	    << std::endl
	    << "  -y   do not merge states with same symbolic representation "
115
	    << "(implies -f)" << 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
      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();
	    }
	}

430
      spot::tgba_tba_proxy* degeneralized = 0;
431
432
433
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

434
435
436
437
438
439
440
441
442
443
444
445
446
      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;
	}

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

493
494
495
496
497
      switch (echeck)
	{
	case None:
	  break;
	case Couvreur:
498
	case Couvreur2:
499
	  {
500
	    spot::emptiness_check* ec;
501
	    if (echeck == Couvreur)
502
	      ec = new spot::emptiness_check(a);
503
	    else
504
505
506
	      ec = new spot::emptiness_check_shy(a);

	    bool res = ec->check();
507

508
509
510
511
512
	    if (expect_counter_example)
	      {
		if (res)
		  {
		    exit_code = 1;
513
		    delete ec;
514
515
		    break;
		  }
516
		spot::counter_example ce(ec->result());
517
		ce.print_result(std::cout);
518
519
520
521
522
	      }
	    else
	      {
		exit_code = !res;
	      }
523
	    delete ec;
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
	  }
	  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;
	}

549
550
      if (f)
        spot::ltl::destroy(f);
551
552
      if (expl)
	delete expl;
553
554
      if (degeneralize_opt)
	delete degeneralized;
555
556
      if (aut_red)
	delete aut_red;
557

558
      delete to_free;
559
560
561
562
563
564
565
566
567
568
    }
  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);
569
  delete dict;
570
571
  return exit_code;
}