ltlcheck.cc 26.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.


#include "common_sys.hh"

#include <string>
#include <iostream>
#include <sstream>
26
#include <fstream>
27
28
29
#include <cstdlib>
#include <cstdio>
#include <argp.h>
30
31
32
#include <signal.h>
#include <unistd.h>
#include <sys/wait.h>
33
#include "error.h"
34
#include "gethrxtime.h"
35
36
37
38
39
40
41
42
43

#include "common_setup.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.hh"
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/lbt.hh"
44
#include "ltlvisit/relabel.hh"
45
#include "tgbaalgos/lbtt.hh"
46
47
48
49
50
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
51
#include "misc/formater.hh"
52
53
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
54
#include "misc/escape.hh"
55
#include "misc/hash.hh"
56

57
58
59
60
61
62
63
64
// Disable handling of timeout on systems that miss kill() or alarm().
// For instance MinGW.
#if HAVE_KILL && HAVE_ALARM
# define ENABLE_TIMEOUT 1
#else
# define ENABLE_TIMEOUT 0
#endif

65
66
const char argp_program_doc[] ="\
Call several LTL/PSL translators and cross-compare their output to detect \
67
bugs, or to gather statistics.  The list of formulas to use should be \
68
supplied on standard input, or using the -f or -F options.\v\
69
70
71
72
Exit status:\n\
  0  everything went fine (timeouts are OK too)\n\
  1  some translator failed to output something we understand, or failed\n\
     sanity checks (statistics were output nonetheless)\n\
73
74
  2  ltlcheck aborted on error\n\
";
75
76
77
78


#define OPT_STATES 1
#define OPT_DENSITY 2
79
80
#define OPT_JSON 3
#define OPT_CSV 4
81
#define OPT_DUPS 5
82
#define OPT_NOCHECKS 6
83
84
85
86
87
88
89

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Specifying translator to call:", 2 },
    { "translator", 't', "COMMANDFMT", 0,
      "register one translators to call", 0 },
90
    { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 },
91
92
93
94
95
96
97
98
    /**************************************************/
    { 0, 0, 0, 0,
      "COMMANDFMT should specify input and output arguments using the "
      "following character sequences:", 3 },
    { "%f,%s,%l", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a (quoted) string in Spot, Spin, or LBT's syntax", 0 },
    { "%F,%S,%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula as a file in Spot, Spin, or LBT's syntax", 0 },
99
100
    { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the output automaton as a Never claim, or in LBTT's format", 0 },
101
102
103
104
    { 0, 0, 0, 0,
      "If either %l, %L, or %T are used, any input formula that does "
      "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "
      "relabeled automatically.", 0 },
105
    /**************************************************/
106
107
108
109
110
111
112
113
    { 0, 0, 0, 0, "ltlcheck behavior:", 4 },
    { "allow-dups", OPT_DUPS, 0, 0,
      "translate duplicate formulas in input", 0 },
    { "no-checks", OPT_NOCHECKS, 0, 0,
      "do not perform any sanity checks (negated formulas "
      "will not be translated)", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "State-space generation:", 5 },
114
115
116
117
118
119
    { "states", OPT_STATES, "INT", 0,
      "number of the states in the state-spaces (200 by default)", 0 },
    { "density", OPT_DENSITY, "FLOAT", 0,
      "probability, between 0.0 and 1.0, to add a transition between "
      "two states (0.1 by default)", 0 },
    /**************************************************/
120
    { 0, 0, 0, 0, "Statistics output:", 6 },
121
122
123
124
125
    { "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL,
      "output statistics as JSON in FILENAME or on standard output", 0 },
    { "csv", OPT_CSV, "FILENAME", OPTION_ARG_OPTIONAL,
      "output statistics as CSV in FILENAME or on standard output", 0 },
    /**************************************************/
126
127
128
129
130
131
132
133
134
135
136
137
138
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
    { 0, 0, 0, 0 }
  };

spot::bdd_dict dict;
unsigned states = 200;
float density = 0.1;
139
unsigned timeout = 0;
140
141
142
const char* json_output = 0;
const char* csv_output = 0;
bool want_stats = false;
143
bool allow_dups = false;
144
bool no_checks = false;
145
146
147
148
149

typedef Sgi::hash_set<const spot::ltl::formula*,
		      const spot::ptr_hash<const spot::ltl::formula> > fset_t;

fset_t unique_set;
150
151

std::vector<char*> translators;
152
153
154
155
156
157
158
159
bool global_error_flag = false;

static std::ostream&
global_error()
{
  global_error_flag = true;
  return std::cerr;
}
160

161
162
163
164
165
166
167
168
169
170
struct statistics
{
  bool ok;
  unsigned states;
  unsigned edges;
  unsigned transitions;
  unsigned acc;
  unsigned scc;
  unsigned nondetstates;
  bool nondeterministic;
171
  double time;
172
173
174
175
176
177
178
  unsigned product_states;
  unsigned product_transitions;
  unsigned product_scc;

  static void
  fields(std::ostream& os)
  {
179
180
181
182
183
184
185
186
187
188
189
    os << (" \"states\","
	   " \"edges\","
	   " \"transitions\","
	   " \"acc\","
	   " \"scc\","
	   " \"nondetstates\","
	   " \"nondeterministic\","
	   " \"time\","
	   " \"product_states\","
	   " \"product_transitions\","
	   " \"product_scc\"");
190
191
192
193
194
195
196
197
198
199
200
201
  }

  void
  to_csv(std::ostream& os)
  {
    os << states << ", "
       << edges << ", "
       << transitions << ", "
       << acc << ", "
       << scc << ", "
       << nondetstates << ", "
       << nondeterministic << ", "
202
       << time << ", "
203
204
205
206
207
208
209
210
211
212
213
       << product_states << ", "
       << product_transitions << ", "
       << product_scc;
  }
};

typedef std::vector<statistics> statistics_formula;
typedef std::vector<statistics_formula> statistics_vector;
statistics_vector vstats;
std::vector<std::string> formulas;

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
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as an integer.", s);
  return res;
}

static int
to_pos_int(const char* s)
{
  int res = to_int(s);
  if (res < 0)
    error(2, 0, "%d is not positive", res);
  return res;
}

static float
to_float(const char* s)
{
  char* endptr;
  // Do not use strtof(), it does not exist on Solaris 9.
  float res = strtod(s, &endptr);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as a float.", s);
  return res;
}

static float
to_probability(const char* s)
{
  float res = to_float(s);
  if (res < 0.0 || res > 1.0)
    error(2, 0, "%f is not between 0 and 1.", res);
  return res;
}


static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case 't':
    case ARGP_KEY_ARG:
      translators.push_back(arg);
      break;
264
265
    case 'T':
      timeout = to_pos_int(arg);
266
267
268
269
#if !ENABLE_TIMEOUT
      std::cerr << "warning: setting a timeout is not supported "
		<< "on your platform" << std::endl;
#endif
270
      break;
271
272
273
274
    case OPT_CSV:
      want_stats = true;
      csv_output = arg ? arg : "-";
      break;
275
276
277
    case OPT_DENSITY:
      density = to_probability(arg);
      break;
278
279
280
    case OPT_DUPS:
      allow_dups = true;
      break;
281
282
283
284
    case OPT_JSON:
      want_stats = true;
      json_output = arg ? arg : "-";
      break;
285
286
287
    case OPT_NOCHECKS:
      no_checks = true;
      break;
288
289
290
291
292
293
294
295
296
297
    case OPT_STATES:
      states = to_pos_int(arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static int
298
create_tmpfile(char c, unsigned int n, std::string& name)
299
300
{
  char tmpname[30];
301
  snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
302
303
304
305
306
307
308
  int fd = mkstemp(tmpname);
  if (fd == -1)
    error(2, errno, "failed to create a temporary file");
  name = tmpname;
  return fd;
}

309
310

static volatile bool timed_out = false;
311
312
#if ENABLE_TIMEOUT
static volatile int alarm_on = 0;
313
314
315
316
317
318
319
320
321
322
323
324
325
326
static int child_pid = -1;

static void
sig_handler(int sig)
{
  if (child_pid == 0)
    error(2, 0, "child received signal %d before starting", sig);

  if (sig == SIGALRM && alarm_on)
    {
      timed_out = true;
      if (--alarm_on)
	{
	  // Send SIGTERM to children.
327
	  kill(-child_pid, SIGTERM);
328
329
330
331
332
333
334
	  // Try again later if it didn't work.  (alarm() will be reset
	  // if it did work and the call to wait() returns)
	  alarm(2);
	}
      else
	{
	  // After a few gentle tries, really kill that child.
335
	  kill(-child_pid, SIGKILL);
336
337
338
339
340
	}
    }
  else
    {
      // forward signal
341
      kill(-child_pid, sig);
342
343
      // and die verbosely
      error(2, 0, "received signal %d", sig);
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
    }
}

static void
setup_sig_handler()
{
  struct sigaction sa;
  sa.sa_handler = sig_handler;
  sigemptyset(&sa.sa_mask);
  sa.sa_flags = SA_RESTART; // So that wait() doesn't get aborted by SIGALRM.
  sigaction(SIGALRM, &sa, 0);
  // Catch termination signals, so we can kill the subprocess.
  sigaction(SIGHUP, &sa, 0);
  sigaction(SIGINT, &sa, 0);
  sigaction(SIGQUIT, &sa, 0);
  sigaction(SIGTERM, &sa, 0);
}

static int
exec_with_timeout(const char* cmd)
{
  int status;

  timed_out = false;

  child_pid = fork();
  if (child_pid == -1)
    error(2, errno, "failed to fork()");

  if (child_pid == 0)
    {
      setpgid(0, 0);
      execlp("sh", "sh", "-c", cmd, (char*)0);
      error(2, errno, "failed to run 'sh'");
    }
  else
    {
      alarm(timeout);
      // Upon SIGALRM, the child will receive up to 3
      // signals: SIGTERM, SIGTERM, SIGKILL.
      alarm_on = 3;
      int w = waitpid(child_pid, &status, 0);
      alarm_on = 0;

      if (w == -1)
	error(2, errno, "error during wait()");

      alarm(0);
    }
  return status;
}
395
396
397
398
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT
399

400
namespace
401
{
402
403
404
  struct quoted_string: public spot::printable_value<std::string>
  {
    using spot::printable_value<std::string>::operator=;
405

406
407
408
409
410
411
412
413
    void
    print(std::ostream& os, const char* pos) const
    {
      os << '\'';
      this->spot::printable_value<std::string>::print(os, pos);
      os << '\'';
    }
  };
414

415
416
417
418
419
  struct printable_result_filename: public spot::printable_value<std::string>
  {
    unsigned translator_num;
    enum output_format { None, Spin, Lbtt };
    mutable output_format format;
420

421
422
423
424
425
426
    void reset(unsigned n)
    {
      val_.clear();
      translator_num = n;
      format = None;
    }
427

428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
    void
    print(std::ostream& os, const char* pos) const
    {
      if (*pos == 'N')
	format = Spin;
      else
	format = Lbtt;
      if (!val_.empty())
	error(2, 0, "you may have only one %%N or %%T specifier: %s",
	      translators[translator_num]);
      close(create_tmpfile('o', translator_num,
			   const_cast<std::string&>(val_)));
      os << '\'' << val_ << '\'';
    }
  };
443

444
445
446
447
448
449
450
451
452
453
454
455
456
457
  class translator_runner: protected spot::formater
  {
  private:
    // Round-specific variables
    quoted_string string_ltl_spot;
    quoted_string string_ltl_spin;
    quoted_string string_ltl_lbt;
    quoted_string filename_ltl_spot;
    quoted_string filename_ltl_spin;
    quoted_string filename_ltl_lbt;
    std::list<std::string> toclean;
    // Run-specific variables
    printable_result_filename output;
  public:
458
459
    using spot::formater::has;

460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
    translator_runner()
    {
      declare('f', &string_ltl_spot);
      declare('s', &string_ltl_spin);
      declare('l', &string_ltl_lbt);
      declare('F', &filename_ltl_spot);
      declare('S', &filename_ltl_spin);
      declare('L', &filename_ltl_lbt);
      declare('N', &output);
      declare('T', &output);

      size_t s = translators.size();
      assert(s);
      for (size_t n = 0; n < s; ++n)
	prime(translators[n]);
475

476
477
478
    }

    // Cleanup temporary files.
479
480
    void
    round_cleanup()
481
    {
482
483
484
485
      for (std::list<std::string>::const_iterator i = toclean.begin();
	   i != toclean.end(); ++i)
	unlink(i->c_str());
      toclean.clear();
486
    }
487
488
489

    void
    string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
490
    {
491
492
493
494
495
496
497
      int fd = create_tmpfile('i', n, tmpname);
      write(fd, str.c_str(), str.size());
      write(fd, "\n", 1);
      close(fd);
      toclean.push_back(tmpname);
    }

498
499
    const std::string&
    formula() const
500
501
502
503
504
505
506
507
508
509
510
511
    {
      // Pick the most readable format we have...
      if (!string_ltl_spot.val().empty())
	return string_ltl_spot;
      if (!string_ltl_spin.val().empty())
	return string_ltl_spin;
      if (!string_ltl_lbt.val().empty())
	return string_ltl_lbt;
      error(2, 0, "None of the translators need the input formula?");
      return string_ltl_spot;
    }

512
513
    void
    round_formula(const spot::ltl::formula* f, unsigned serial)
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
    {
      if (has('f') || has('F'))
	string_ltl_spot = spot::ltl::to_string(f, true);
      if (has('s') || has('S'))
	string_ltl_spin = spot::ltl::to_spin_string(f, true);
      if (has('l') || has('L'))
	string_ltl_lbt = spot::ltl::to_lbt_string(f);
      if (has('F'))
	string_to_tmp(string_ltl_spot, serial, filename_ltl_spot);
      if (has('S'))
	string_to_tmp(string_ltl_spin, serial, filename_ltl_spin);
      if (has('L'))
	string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt);
    }

529
530
    const spot::tgba*
    translate(unsigned int translator_num, char l, statistics_formula* fstats)
531
532
533
534
535
536
    {
      output.reset(translator_num);

      std::ostringstream command;
      format(command, translators[translator_num]);
      toclean.push_back(output.val());
537
538
539
540
541

      if (output.format == printable_result_filename::None)
	error(2, 0, "no output sequence used in %s",
	      translators[translator_num]);

542
543
544
      std::string cmd = command.str();
      std::cerr << "Running [" << l << translator_num << "]: "
		<< cmd << std::endl;
545
      xtime_t before = gethrxtime();
546
      int es = exec_with_timeout(cmd.c_str());
547
      xtime_t after = gethrxtime();
548
549

      const spot::tgba* res = 0;
550
551
      if (timed_out)
	{
552
553
	  // This is not considered to be a global error.
	  std::cerr << "warning: timeout during execution of command\n";
554
555
556
	}
      else if (WIFSIGNALED(es))
	{
557
558
	  global_error() << "error: execution terminated by signal "
			 << WTERMSIG(es) << ".\n";
559
560
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
561
	{
562
563
	  global_error() << "error: execution returned exit code "
			 << WEXITSTATUS(es) << ".\n";
564
565
566
567
568
569
	}
      else
	{
	  switch (output.format)
	    {
	    case printable_result_filename::Spin:
570
	      {
571
572
573
574
		spot::neverclaim_parse_error_list pel;
		res = spot::neverclaim_parse(output, pel, &dict);
		if (!pel.empty())
		  {
575
576
577
		    std::ostream& err = global_error();
		    err << "error: failed to parse the produced neverclaim.\n";
		    spot::format_neverclaim_parse_errors(err, output, pel);
578
579
580
581
		    delete res;
		    res = 0;
		  }
		break;
582
	      }
583
	    case printable_result_filename::Lbtt:
584
	      {
585
		std::string error;
586
		std::ifstream f(output.val().c_str());
587
588
		if (!f)
		  {
589
590
591
		    global_error() << "Cannot open " << output.val()
				   << std::endl;
		    global_error_flag = true;
592
593
594
		  }
		else
		  {
595
		    res = spot::lbtt_parse(f, error, &dict);
596
		    if (!res)
597
598
599
		      global_error() << ("Failed error to parse output in "
					 "LBTT format: ")
				     << error << std::endl;
600
601
		  }
		break;
602
	      }
603
604
605
	    case printable_result_filename::None:
	      assert(!"unreachable code");
	    }
606
	}
607
      // Compute statistics.
608
      if (res && want_stats)
609
610
611
612
613
614
615
616
617
618
619
620
621
	{
	  statistics* st = &(*fstats)[translator_num];
	  st->ok = true;
	  spot::tgba_sub_statistics s = sub_stats_reachable(res);
	  st->states = s.states;
	  st->edges = s.transitions;
	  st->transitions = s.sub_transitions;
	  st->acc = res->number_of_acceptance_conditions();
	  spot::scc_map m(res);
	  m.build_map();
	  st->scc = m.scc_count();
	  st->nondetstates = spot::count_nondet_states(res);
	  st->nondeterministic = st->nondetstates != 0;
622
623
          double prec = XTIME_PRECISION;
	  st->time = (after - before) / prec;
624
	}
625
      return res;
626
    }
627
  };
628

629
630
631
632
633
634
635
636
637
638
639
640
641
642
  static bool
  is_empty(const spot::tgba* aut)
  {
    spot::emptiness_check* ec = spot::couvreur99(aut);
    spot::emptiness_check_result* res = ec->check();
    delete res;
    delete ec;
    return !res;
  }

  static void
  cross_check(const std::vector<spot::scc_map*>& maps, char l)
  {
    size_t m = maps.size();
643

644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
    std::vector<bool> res(m);
    unsigned verified = 0;
    unsigned violated = 0;
    for (size_t i = 0; i < m; ++i)
      if (spot::scc_map* m = maps[i])
	{
	  // r == true iff the automaton i is accepting.
	  bool r = false;
	  unsigned c = m->scc_count();
	  for (unsigned j = 0; (j < c) && !r; ++j)
	    r |= m->accepting(j);
	  res[i] = r;
	  if (r)
	    ++verified;
	  else
	    ++violated;
	}
    if (verified != 0 && violated != 0)
662
      {
663
664
	std::ostream& err = global_error();
	err << "error: {";
665
666
667
668
669
670
671
	bool first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && res[i])
	    {
	      if (first)
		first = false;
	      else
672
673
		err << ",";
	      err << l << i;
674
	    }
675
	err << "} disagree with {";
676
677
678
679
680
681
682
	first = true;
	for (size_t i = 0; i < m; ++i)
	  if (maps[i] && !res[i])
	    {
	      if (first)
		first = false;
	      else
683
684
		err << ",";
	      err << l << i;
685
	    }
686
	err << "} when evaluating the state-space\n";
687
      }
688
  }
689

690
  typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
691

692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
  // Collect all the states of SSPACE that appear in the accepting SCCs
  // of PROD.
  static void
  states_in_acc(const spot::scc_map* m, const spot::tgba* sspace,
		state_set& s)
  {
    const spot::tgba* aut = m->get_aut();
    unsigned c = m->scc_count();
    for (unsigned n = 0; n < c; ++n)
      if (m->accepting(n))
	{
	  const std::list<const spot::state*>& l = m->states_of(n);
	  for (std::list<const spot::state*>::const_iterator i = l.begin();
	       i != l.end(); ++i)
	    {
	      spot::state* x = aut->project_state(*i, sspace);
	      if (!s.insert(x).second)
		x->destroy();
	    }
	}
  }
713

714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
  static bool
  consistency_check(const spot::scc_map* pos, const spot::scc_map* neg,
		    const spot::tgba* sspace)
  {
    // the states of SSPACE should appear in the accepting SCC of at
    // least one of POS or NEG.  Maybe both.
    state_set s;
    states_in_acc(pos, sspace, s);
    states_in_acc(neg, sspace, s);
    bool res = s.size() == states;
    state_set::iterator it;
    for (it = s.begin(); it != s.end(); it++)
      (*it)->destroy();
    return res;
  }
729
730
731

  class processor: public job_processor
  {
732
733
    translator_runner runner;

734
735
736
737
738
739
740
  public:
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
      (void) filename;
      (void) linenum;
741
      static unsigned round = 0;
742

743
744
745
746
747
748
749
750
751
752
      // If we need LBT atomic proposition in any of the input or
      // output, relabel the formula.
      if (!f->has_lbt_atomic_props() &&
	  (runner.has('l') || runner.has('L') || runner.has('T')))
	{
	  const spot::ltl::formula* g = spot::ltl::relabel(f, spot::ltl::Pnn);
	  f->destroy();
	  f = g;
	}

753
754
      // ---------- Positive Formula ----------

755
      runner.round_formula(f, round);
756

757
758
759
      // Call formula() before printing anything else, in case it
      // complains.
      std::string fstr = runner.formula();
760
761
762
763
764
765
      if (filename)
	std::cerr << filename << ":";
      if (linenum)
	std::cerr << linenum << ":";
      if (filename || linenum)
	std::cerr << " ";
766
      std::cerr << fstr << "\n";
767

768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
      // Make sure we do not translate the same formula twice.
      if (!allow_dups)
	{
	  if (unique_set.insert(f).second)
	    {
	      f->clone();
	    }
	  else
	    {
	      std::cerr
		<< ("warning: This formula or its negation has already"
		    " been checked.\n         Use --allow-dups if it "
		    "should not be ignored.\n")
		<< std::endl;
	      f->destroy();
	      return 0;
	    }
	}

      size_t m = translators.size();
      std::vector<const spot::tgba*> pos(m);
      std::vector<const spot::tgba*> neg(m);


      unsigned n = vstats.size();
793
      vstats.resize(n + (no_checks ? 1 : 2));
794
      statistics_formula* pstats = &vstats[n];
795
      statistics_formula* nstats = 0;
796
      pstats->resize(m);
797
798
      formulas.push_back(fstr);

799
      for (size_t n = 0; n < m; ++n)
800
801
802
	pos[n] = runner.translate(n, 'P', pstats);

      // ---------- Negative Formula ----------
803

804
805
806
      // The negative formula is only needed when checks are
      // activated.
      if (!no_checks)
807
	{
808
809
	  nstats = &vstats[n + 1];
	  nstats->resize(m);
810

811
812
	  const spot::ltl::formula* nf =
	    spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
813

814
815
816
817
818
819
820
821
822
	  if (!allow_dups)
	    {
	      bool res = unique_set.insert(nf->clone()).second;
	      // It is not possible to discover that nf has already been
	      // translated, otherwise that would mean that f had been
	      // translated too and we would have caught it before.
	      assert(res);
	      (void) res;
	    }
823

824
825
	  runner.round_formula(nf, round);
	  formulas.push_back(runner.formula());
826

827
828
829
830
	  for (size_t n = 0; n < m; ++n)
	    neg[n] = runner.translate(n, 'N', nstats);
	  nf->destroy();
	}
831

832
833
834
      f->destroy();
      runner.round_cleanup();
      ++round;
835

836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
      if (!no_checks)
	{
	  std::cerr << "Performing sanity checks and gathering statistics..."
		    << std::endl;

	  // intersection test
	  for (size_t i = 0; i < m; ++i)
	    if (pos[i])
	      for (size_t j = 0; j < m; ++j)
		if (neg[j])
		  {
		    spot::tgba_product* prod =
		      new spot::tgba_product(pos[i], neg[j]);
		    if (!is_empty(prod))
		      global_error() << "error: P" << i << "*N" << j
				     << " is nonempty\n";
		    delete prod;
		  }
	}
      else
	{
	  std::cerr << "Gathering statistics..." << std::endl;
	}
859
860

      // build products with a random state-space.
861
      spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
862
      spot::tgba* statespace = spot::random_graph(states, density, ap, &dict);
863
      delete ap;
864
865
866
867
868
869
870
871
872
873
874
875
876

      std::vector<spot::tgba*> pos_prod(m);
      std::vector<spot::tgba*> neg_prod(m);
      std::vector<spot::scc_map*> pos_map(m);
      std::vector<spot::scc_map*> neg_map(m);
      for (size_t i = 0; i < m; ++i)
	if (pos[i])
	  {
	    spot::tgba* p = new spot::tgba_product(pos[i], statespace);
	    pos_prod[i] = p;
	    spot::scc_map* sm = new spot::scc_map(p);
	    sm->build_map();
	    pos_map[i] = sm;
877
878

	    // Statistics
879
880
881
882
883
884
885
	    if (want_stats)
	      {
		(*pstats)[i].product_scc = sm->scc_count();
		spot::tgba_statistics s = spot::stats_reachable(p);
		(*pstats)[i].product_states = s.states;
		(*pstats)[i].product_transitions = s.transitions;
	      }
886
	  }
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
      if (!no_checks)
	for (size_t i = 0; i < m; ++i)
	  if (neg[i])
	    {
	      spot::tgba* p = new spot::tgba_product(neg[i], statespace);
	      neg_prod[i] = p;
	      spot::scc_map* sm = new spot::scc_map(p);
	      sm->build_map();
	      neg_map[i] = sm;

	      // Statistics
	      if (want_stats)
		{
		  (*nstats)[i].product_scc = sm->scc_count();
		  spot::tgba_statistics s = spot::stats_reachable(p);
		  (*nstats)[i].product_states = s.states;
		  (*nstats)[i].product_transitions = s.transitions;
		}
	    }
906

907
908
909
910
911
912
913
914
915
916
917
918
919
      if (!no_checks)
	{
	  // cross-comparison test
	  cross_check(pos_map, 'P');
	  cross_check(neg_map, 'N');

	  // consistency check
	  for (size_t i = 0; i < m; ++i)
	    if (pos_map[i] && neg_map[i] &&
		!(consistency_check(pos_map[i], neg_map[i], statespace)))
	      global_error() << "error: inconsistency between P" << i
			     << " and N" << i << "\n";
	}
920
921
922

      // Cleanup.

923
924
      if (!no_checks)
	for (size_t n = 0; n < m; ++n)
925
926
927
	{
	  delete neg_map[n];
	  delete neg_prod[n];
928
	  delete neg[n];
929
930
931
	}
      for (size_t n = 0; n < m; ++n)
	{
932
933
	  delete pos_map[n];
	  delete pos_prod[n];
934
935
	  delete pos[n];
	}
936
      delete statespace;
937
      std::cerr << std::endl;
938
939
940
941
942
      return 0;
    }
  };
}

943
static void
944
print_stats_csv(const char* filename)
945
{
946
947
948
949
950
951
952
953
954
955
956
957
958
959
  std::ofstream* outfile = 0;
  std::ostream* out;
  if (!strncmp(filename, "-", 2))
    {
      out = &std::cout;
    }
  else
    {
      out = outfile = new std::ofstream(filename);
      if (!outfile)
	error(2, errno, "cannot open '%s'", filename);
    }

  unsigned ntrans = translators.size();
960
  unsigned rounds = vstats.size();
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
  assert(rounds = formulas.size());

  *out << "\"formula\", \"tool\", ";
  statistics::fields(*out);
  *out << "\n";
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  *out << "\"";
	  spot::escape_str(*out, formulas[r]);
	  *out << "\", \"";
	  spot::escape_str(*out, translators[t]);
	  *out << "\", ";
	  vstats[r][t].to_csv(*out);
	  *out << "\n";
	}
  delete outfile;
}

static void
print_stats_json(const char* filename)
{
  std::ofstream* outfile = 0;
  std::ostream* out;
  if (!strncmp(filename, "-", 2))
    {
      out = &std::cout;
    }
  else
    {
      out = outfile = new std::ofstream(filename);
      if (!outfile)
	error(2, errno, "cannot open '%s'", filename);
    }

997
  unsigned ntrans = translators.size();
998
  unsigned rounds = vstats.size();
999
1000
  assert(rounds = formulas.size());

1001
1002
  *out << "{\n  \"tools\": [\n    \"";
  spot::escape_str(*out, translators[0]);
1003
  for (unsigned t = 1; t < ntrans; ++t)
1004
1005
1006
1007
1008
1009
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, translators[t]);
    }
  *out << "\"\n  ],\n  \"inputs\": [\n    \"";
  spot::escape_str(*out, formulas[0]);
1010
  for (unsigned r = 1; r < rounds; ++r)
1011
1012
1013
1014
1015
1016
1017
    {
      *out << "\",\n    \"";
      spot::escape_str(*out, formulas[r]);
    }
  *out << ("\"\n  ],\n  \"fields\": [\n    \"input\", \"tool\",");
  statistics::fields(*out);
  *out << "\n  ],\n  \"results\": [";
1018
1019
1020
1021
1022
1023
  bool notfirst = false;
  for (unsigned r = 0; r < rounds; ++r)
    for (unsigned t = 0; t < ntrans; ++t)
      if (vstats[r][t].ok)
	{
	  if (notfirst)
1024
	    *out << ",";
1025
	  notfirst = true;
1026
1027
1028
	  *out << "\n    [ " << r << ", " << t << ", ";
	  vstats[r][t].to_csv(*out);
	  *out << " ]";
1029
	}
1030
1031
1032
  *out << "\n  ]\n}\n";

  delete outfile;
1033
}
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052

int
main(int argc, char** argv)
{
  setup(argv);

  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
		    argp_program_doc, children, 0, 0 };

  if (int err = argp_parse(&ap, argc, argv, 0, 0, 0))
    exit(err);

  if (jobs.empty())
    jobs.push_back(job("-", 1));

  if (translators.empty())
    error(2, 0, "No translator to run?  Run '%s --help' for usage.",
	  program_name);

1053
1054
  setup_sig_handler();

1055
1056
1057
  processor p;
  if (p.run())
    return 2;
1058

1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
  if (formulas.empty())
    {
      error(2, 0, "no formula to translate");
    }
  else
    {
      if (global_error_flag)
	std::cerr
	  << ("error: some error was detected during the above runs,\n"
	      "       please search for 'error:' messages in the above trace.")
	  << std::endl;
	else
	  std::cerr << "no problem detected" << std::endl;
    }

  if (json_output)
    print_stats_json(json_output);
  if (csv_output)
    print_stats_csv(csv_output);

1079
  return global_error_flag;
1080
}