ltl2tgba.cc 16 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/reduce.hh"
28
#include "ltlvisit/tostring.hh"
29
#include "ltlvisit/apcollect.hh"
30
31
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
32
#include "tgbaalgos/ltl2tgba_lacim.hh"
33
#include "tgbaalgos/ltl2tgba_fm.hh"
34
#include "tgba/bddprint.hh"
35
#include "tgbaalgos/dotty.hh"
36
#include "tgbaalgos/lbtt.hh"
37
#include "tgba/tgbatba.hh"
38
#include "tgbaalgos/magic.hh"
39
40
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
41
#include "tgbaparse/public.hh"
42
#include "tgbaalgos/dupexp.hh"
43
#include "tgbaalgos/neverclaim.hh"
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
martinez's avatar
martinez committed
54
	    << "  -a    display the acceptance_conditions BDD, not the "
55
	    << "reachability graph"
56
	    << std::endl
martinez's avatar
martinez committed
57
58
59
60
	    << "  -A    same as -a, but as a set" << std::endl
	    << "  -d    turn on traces during parsing" << std::endl
	    << "  -D    degeneralize the automaton" << std::endl
	    << "  -e    emptiness-check (Couvreur), expect and compute "
61
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
62
	    << "  -e2   emptiness-check (Couvreur variant), expect and compute "
63
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
64
	    << "  -E    emptiness-check (Couvreur), expect no counter-example "
65
	    << std::endl
martinez's avatar
martinez committed
66
	    << "  -E2   emptiness-check (Couvreur variant), expect no "
67
	    << "counter-example " << std::endl
martinez's avatar
martinez committed
68
69
70
71
72
73
74
75
            << "  -f    use Couvreur's FM algorithm for translation"
	    << std::endl
            << "  -F    read the formula from the file" << std::endl
            << "  -L    fair-loop approximation (implies -f)" << std::endl
	    << "  -m    magic-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -M    magic-search (implies -D), expect no counter-example"
	    << std::endl
martinez's avatar
martinez committed
76
77
78
79
	    << "  -n    same as -m, but display more counter-examples"
	    << std::endl
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
80
81
            << "  -p    branching postponement (implies -f)" << std::endl
	    << "  -r    display the relation BDD, not the reachability graph"
82
	    << std::endl
martinez's avatar
martinez committed
83
84
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
85
	    << "and universality" << std::endl
martinez's avatar
martinez committed
86
	    << "  -r3   reduce formula using implication between "
87
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
88
89
90
	    << "  -r4   reduce formula using all rules" << std::endl
	    << "  -rd   display the reduce formula" << std::endl
	    << "  -R    same as -r, but as a set" << std::endl
martinez's avatar
martinez committed
91
	    << "  -R1q  use direct simulation to merge some state "
martinez's avatar
martinez committed
92
	    << "(use -L for more reduction)"
93
	    << std::endl
martinez's avatar
martinez committed
94
	    << "  -R1t  use direct simulation to remove some transition "
martinez's avatar
martinez committed
95
	    << "(use -L for more reduction)"
96
	    << std::endl
martinez's avatar
martinez committed
97
98
99
100
101
102
	    << "  -R2q  use delayed simulation to merge some state "
	    << "(the automaton must be degeneralised)"
	    << std::endl
	    << "  -R2t  use delayed simulation to remove some transition "
	    << "(the automaton must be degeneralised)"
	    << std::endl
martinez's avatar
martinez committed
103
	    << "  -R3   use SCC to reduce the automata"
104
	    << std::endl
martinez's avatar
martinez committed
105
	    << "  -Rd   display the simulation relation"
106
	    << std::endl
martinez's avatar
martinez committed
107
	    << "  -RD   display the parity game (dot format)"
108
	    << std::endl
martinez's avatar
martinez committed
109
	    << "  -s    convert to explicit automata, and number states "
110
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
111
	    << "  -S    convert to explicit automata, and number states "
112
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
113
	    << "  -t    display reachable states in LBTT's format" << std::endl
114
115
            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
	    << "events (implies -f)" << std::endl
martinez's avatar
martinez committed
116
117
118
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
119
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
120
	    << "  -X    do not compute an automaton, read it from a file"
121
	    << std::endl
martinez's avatar
martinez committed
122
	    << "  -y    do not merge states with same symbolic representation "
123
	    << "(implies -f)" << std::endl;
124
125
126
127
128
129
130
131
  exit(2);
}

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

132
  bool debug_opt = false;
133
  bool degeneralize_opt = false;
134
  bool fm_opt = false;
135
  bool fm_exprop_opt = false;
136
  bool fm_symb_merge_opt = true;
137
  bool file_opt = false;
138
  int output = 0;
139
  int formula_index = 0;
140
  enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
141
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
142
143
  bool magic_many = false;
  bool expect_counter_example = false;
144
  bool from_file = false;
145
  int reduc_aut = spot::Reduce_None;
146
  int redopt = spot::ltl::Reduce_None;
147
148
  bool display_reduce_form = false;
  bool display_rel_sim = false;
149
  bool display_parity_game = false;
150
  bool post_branching = false;
151
  bool fair_loop_approx = false;
152
153
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
154

155
  for (;;)
156
    {
157
      if (argc < formula_index + 2)
158
	syntax(argv[0]);
159
160
161

      ++formula_index;

162
163
164
165
166
167
168
169
170
      if (!strcmp(argv[formula_index], "-a"))
	{
	  output = 2;
	}
      else if (!strcmp(argv[formula_index], "-A"))
	{
	  output = 4;
	}
      else if (!strcmp(argv[formula_index], "-d"))
171
172
173
	{
	  debug_opt = true;
	}
174
175
176
177
      else if (!strcmp(argv[formula_index], "-D"))
	{
	  degeneralize_opt = true;
	}
178
179
180
181
182
183
      else if (!strcmp(argv[formula_index], "-e"))
	{
	  echeck = Couvreur;
	  expect_counter_example = true;
	  output = -1;
	}
184
185
186
187
188
189
      else if (!strcmp(argv[formula_index], "-e2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = true;
	  output = -1;
	}
190
191
192
193
194
195
      else if (!strcmp(argv[formula_index], "-E"))
	{
	  echeck = Couvreur;
	  expect_counter_example = false;
	  output = -1;
	}
196
197
198
199
200
201
      else if (!strcmp(argv[formula_index], "-E2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = false;
	  output = -1;
	}
202
203
204
205
206
207
208
209
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
210
211
212
213
214
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
martinez's avatar
martinez committed
215
      else if (!strcmp(argv[formula_index], "-m"))
martinez's avatar
martinez committed
216
	{
martinez's avatar
martinez committed
217
	  echeck = MagicSearch;
martinez's avatar
martinez committed
218
219
220
221
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
martinez's avatar
martinez committed
222
      else if (!strcmp(argv[formula_index], "-M"))
223
224
225
	{
	  echeck = MagicSearch;
	  degeneralize_opt = true;
martinez's avatar
martinez committed
226
	  expect_counter_example = false;
227
	  output = -1;
martinez's avatar
martinez committed
228
	}
martinez's avatar
martinez committed
229
230
      else if (!strcmp(argv[formula_index], "-n"))
	{
231
	  echeck = MagicSearch;
martinez's avatar
martinez committed
232
233
234
235
236
237
238
239
240
241
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	  magic_many = true;
	}
      else if (!strcmp(argv[formula_index], "-N"))
	{
	  degeneralize_opt = true;
	  output = 8;
	}
242
243
244
245
246
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
247
248
      else if (!strcmp(argv[formula_index], "-r"))
	{
249
250
	  output = 1;
	}
251
252
253
254
255
256
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
257
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
258
259
260
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
261
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
262
263
264
265
266
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
267
268
269
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
270
	}
martinez's avatar
martinez committed
271
272
273
274
275
276
277
278
279
      else if (!strcmp(argv[formula_index], "-R1q"))
	{
	  reduc_aut |= spot::Reduce_quotient_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R1t"))
	{
	  reduc_aut |= spot::Reduce_transition_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R2q"))
280
	{
martinez's avatar
martinez committed
281
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
282
	}
martinez's avatar
martinez committed
283
      else if (!strcmp(argv[formula_index], "-R2t"))
284
	{
martinez's avatar
martinez committed
285
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
	}
      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;
	}
      else if (!strcmp(argv[formula_index], "-RD"))
	{
	  display_parity_game = true;
	}
303
304
305
306
307
308
309
310
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
311
312
313
314
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
315
316
317
318
319
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
320
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
321
322
323
324
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
325
	      tok = strtok(0, ", \t;");
326
327
	    }
	}
328
329
330
331
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
332
333
334
335
336
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
337
338
339
340
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
341
342
343
344
345
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
346
347
348
349
      else
	{
	  break;
	}
350
351
    }

352
353
354
355
  std::string input;

  if (file_opt)
    {
356
      if (strcmp(argv[formula_index], "-"))
357
	{
358
	  std::ifstream fin(argv[formula_index]);
359
	  if (!fin)
360
361
362
363
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
364

365
	  if (!std::getline(fin, input, '\0'))
366
367
368
369
370
371
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
372
	{
373
	  std::getline(std::cin, input, '\0');
374
375
376
377
378
379
380
	}
    }
  else
    {
      input = argv[formula_index];
    }

381
  spot::bdd_dict* dict = new spot::bdd_dict();
382
383
384
385
386
387
388
389
390

  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)
391
    {
392
393
394
395
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

396
397
398
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
399
400
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
401
402
	  if (spot::format_tgba_parse_errors(std::cerr, pel))
	    return 2;
403
	  e->merge_transitions();
404
	}
405
      else
406
	{
407
	  if (redopt != spot::ltl::Reduce_None)
408
	    {
409
410
411
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
412
413
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
414
	    }
415

416
	  if (fm_opt)
417
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
418
					       fm_symb_merge_opt,
419
					       post_branching,
420
					       fair_loop_approx, unobservables);
421
422
423
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
424

425
426
427
428
      spot::tgba_tba_proxy* degeneralized = 0;
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

429
430
431
432
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
433
434
435
436

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

martinez's avatar
martinez committed
437
438
439
440
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
441
	    {
martinez's avatar
martinez committed
442
443
444
445
446
447
448
449
450
451
452
453
454
	      spot::direct_simulation_relation* rel_dir = 0;
	      spot::delayed_simulation_relation* rel_del = 0;

	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			       spot::Reduce_transition_Dir_Sim))
		rel_dir = spot::get_direct_relation_simulation(a,
							       std::cout,
							       display_parity_game);
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
		rel_del = spot::get_delayed_relation_simulation(a,
								std::cout,
								display_parity_game);
455
456

	      if (display_rel_sim)
martinez's avatar
martinez committed
457
458
459
460
461
462
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
463

martinez's avatar
martinez committed
464
465
466
467
468
469
470
471
472
473
474
475
476
	      if (reduc_aut & spot::Reduce_quotient_Dir_Sim)
		aut_red->quotient_state(rel_dir);
	      if (reduc_aut & spot::Reduce_transition_Dir_Sim)
		aut_red->delete_transitions(rel_dir);
	      if (reduc_aut & spot::Reduce_quotient_Del_Sim)
		aut_red->quotient_state(rel_del);
	      if (reduc_aut & spot::Reduce_transition_Del_Sim)
		aut_red->delete_transitions(rel_del);

	      if (rel_dir)
		spot::free_relation_simulation(rel_dir);
	      if (rel_del)
		spot::free_relation_simulation(rel_del);
477
478
479
	    }
	}

480
481
482
483
484
485
486
487
488
489
490
491
492
      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;
	}

493
494
      switch (output)
	{
495
496
497
	case -1:
	  /* No output.  */
	  break;
498
499
500
501
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
502
503
504
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
505
506
	  break;
	case 2:
507
508
509
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
510
				get_core_data().acceptance_conditions);
511
512
	  break;
	case 3:
513
514
515
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
516
517
	  break;
	case 4:
518
519
520
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
521
				get_core_data().acceptance_conditions);
522
	  break;
523
	case 5:
524
	  a->get_dict()->dump(std::cout);
525
	  break;
526
527
528
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
529
530
531
	case 8:
	  spot::never_claim_reachable(std::cout, degeneralized, f);
	  break;
532
533
534
	default:
	  assert(!"unknown output option");
	}
535

536
537
      spot::emptiness_check* ec = 0;
      spot::tgba* ec_a = 0;
538
539
540
541
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
542

543
	case Couvreur:
544
545
546
547
	  ec_a = a;
	  ec = new spot::couvreur99_check(a);
	  break;

548
	case Couvreur2:
549
550
	  ec_a = a;
	  ec = new spot::couvreur99_check_shy(a);
551
	  break;
martinez's avatar
martinez committed
552

553
	case MagicSearch:
554
555
	  ec_a = degeneralized;
	  ec = new spot::magic_search(degeneralized);
556
	  break;
557
	}
martinez's avatar
martinez committed
558

559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
      if (ec)
	{
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
	      if (expect_counter_example != !!res)
		exit_code = 1;

	      if (!res)
		{
		  std::cout << "no accepting run found" << std::endl;
		  break;
		}
	      else
		{

		  spot::tgba_run* run = res->accepting_run();
		  if (!run)
		    {
		      std::cout << "an accepting run exist" << std::endl;
		    }
		  else
		    {
		      spot::print_tgba_run(std::cout, run, ec_a);
		      delete run;
		    }
		}
	      delete res;
	    }
	  while (magic_many);
	  delete ec;
martinez's avatar
martinez committed
590
591
	}

592
593
      if (f)
        spot::ltl::destroy(f);
594
595
      if (expl)
	delete expl;
596
597
      if (degeneralize_opt)
	delete degeneralized;
598
599
      if (aut_red)
	delete aut_red;
600

601
      delete to_free;
602
603
604
605
606
607
608
609
610
611
    }
  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);
612
  delete dict;
613
614
  return exit_code;
}