genltl.cc 32.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

// Families defined here come from the following papers:
//
// @InProceedings{cichon.09.depcos,
//   author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski},
//   title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas},
//   booktitle = {Proceedings of the Fourth International Conference on
//                Dependability of Computer Systems},
//   pages = {17--24},
//   year = 2009,
//   publisher = {IEEE Computer Society},
// }
//
// @InProceedings{geldenhuys.06.spin,
//   author = {Jaco Geldenhuys and Henri Hansen},
//   title = {Larger Automata and Less Work for LTL Model Checking},
//   booktitle = {Proceedings of the 13th International SPIN Workshop},
//   year = {2006},
//   pages = {53--70},
//   series = {Lecture Notes in Computer Science},
//   volume = {3925},
//   publisher = {Springer}
// }
//
// @InProceedings{gastin.01.cav,
//   author = {Paul Gastin and Denis Oddoux},
//   title = {Fast {LTL} to {B\"u}chi Automata Translation},
46
47
//   booktitle        = {Proceedings of the 13th International Conference on
//                   Computer Aided Verification (CAV'01)},
48
49
50
51
52
53
54
55
56
57
58
59
60
//   pages = {53--65},
//   year = 2001,
//   editor = {G. Berry and H. Comon and A. Finkel},
//   volume = {2102},
//   series = {Lecture Notes in Computer Science},
//   address = {Paris, France},
//   publisher = {Springer-Verlag}
// }
//
// @InProceedings{rozier.07.spin,
//   author = {Kristin Y. Rozier and Moshe Y. Vardi},
//   title = {LTL Satisfiability Checking},
//   booktitle = {Proceedings of the 12th International SPIN Workshop on
61
//                   Model Checking of Software (SPIN'07)},
62
63
64
65
66
67
//   pages = {149--167},
//   year = {2007},
//   volume = {4595},
//   series = {Lecture Notes in Computer Science},
//   publisher = {Springer-Verlag}
// }
68
69
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
106
107
108
//
// @InProceedings{dwyer.98.fmsp,
//   author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett},
//   title         = {Property Specification Patterns for Finite-state
//                   Verification},
//   booktitle     = {Proceedings of the 2nd Workshop on Formal Methods in
//                   Software Practice (FMSP'98)},
//   publisher     = {ACM Press},
//   address       = {New York},
//   editor        = {Mark Ardis},
//   month         = mar,
//   year          = {1998},
//   pages         = {7--15}
// }
//
// @InProceedings{etessami.00.concur,
//   author = {Kousha Etessami and Gerard J. Holzmann},
//   title = {Optimizing {B\"u}chi Automata},
//   booktitle = {Proceedings of the 11th International Conference on
//                Concurrency Theory (Concur'00)},
//   pages = {153--167},
//   year = {2000},
//   editor = {C. Palamidessi},
//   volume = {1877},
//   series = {Lecture Notes in Computer Science},
//   address = {Pennsylvania, USA},
//   publisher = {Springer-Verlag}
// }
//
// @InProceedings{somenzi.00.cav,
//   author = {Fabio Somenzi and Roderick Bloem},
//   title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
//   booktitle = {Proceedings of the 12th International Conference on
//                Computer Aided Verification (CAV'00)},
//   pages = {247--263},
//   year = {2000},
//   volume = {1855},
//   series = {Lecture Notes in Computer Science},
//   address = {Chicago, Illinois, USA},
//   publisher = {Springer-Verlag}
// }
109
110
111
112
113
114
115
116
117
118
119
120
121
122
//
// @InProceedings{tabakov.10.rv,
//   author = {Deian Tabakov and Moshe Y. Vardi},
//   title = {Optimized Temporal Monitors for {SystemC}},
//   booktitle = {Proceedings of the 1st International Conference on Runtime
// 		  Verification (RV'10)},
//   pages = {436--451},
//   year = 2010,
//   volume = {6418},
//   series = {Lecture Notes in Computer Science},
//   month = nov,
//   publisher = {Springer}
// }

123

124
#include "common_sys.hh"
125
126
127
128
129
130
131
132

#include <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
#include "error.h"
#include <vector>

133
#include "common_setup.hh"
134
#include "common_output.hh"
135
#include "common_range.hh"
136
#include "common_cout.hh"
137
138
139
140
141
142
143
144

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
#include <cstdlib>
#include <cstring>
145
146
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
147
#include <spot/tl/parse.hh>
148
149
150
151

using namespace spot;

const char argp_program_doc[] ="\
152
Generate temporal logic formulas from predefined patterns.";
153

154
155
156
157
158
159
160
enum {
  OPT_AND_F = 1,
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
161
162
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
163
164
165
166
167
168
169
170
171
172
173
174
  OPT_GH_Q,
  OPT_GH_R,
  OPT_GO_THETA,
  OPT_OR_FG,
  OPT_OR_G,
  OPT_OR_GF,
  OPT_R_LEFT,
  OPT_R_RIGHT,
  OPT_RV_COUNTER,
  OPT_RV_COUNTER_CARRY,
  OPT_RV_COUNTER_CARRY_LINEAR,
  OPT_RV_COUNTER_LINEAR,
175
  OPT_SB_PATTERNS,
176
177
178
179
180
  OPT_TV_F1,
  OPT_TV_F2,
  OPT_TV_G1,
  OPT_TV_G2,
  OPT_TV_UU,
181
182
183
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
184
185
  OPT_POSITIVE,
  OPT_NEGATIVE,
186
};
187
188
189
190
191
192
193
194
195

const char* const class_name[LAST_CLASS] =
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
196
197
    "dac-patterns",
    "eh-patterns",
198
199
200
201
202
203
204
205
206
207
208
209
    "gh-q",
    "gh-r",
    "go-theta",
    "or-fg",
    "or-g",
    "or-gf",
    "or-r-left",
    "or-r-right",
    "rv-counter",
    "rv-counter-carry",
    "rv-counter-carry-linear",
    "rv-counter-linear",
210
    "sb-patterns",
211
212
213
214
215
    "tv-f1",
    "tv-f2",
    "tv-g1",
    "tv-g2",
    "tv-uu",
216
217
218
219
    "u-left",
    "u-right",
  };

220

221
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
222
223
224
225
226

static const argp_option options[] =
  {
    /**************************************************/
    // Keep this alphabetically sorted (expect for aliases).
227
    { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
228
229
230
231
232
233
234
235
236
237
238
239
240
241
    // J. Geldenhuys and H. Hansen (Spin'06): Larger automata and less
    // work for LTL model checking.
    { "and-f", OPT_AND_F, "RANGE", 0, "F(p1)&F(p2)&...&F(pn)", 0 },
    OPT_ALIAS(gh-e),
    { "and-fg", OPT_AND_FG, "RANGE", 0, "FG(p1)&FG(p2)&...&FG(pn)", 0 },
    { "and-gf", OPT_AND_GF, "RANGE", 0, "GF(p1)&GF(p2)&...&GF(pn)", 0 },
    OPT_ALIAS(ccj-phi),
    OPT_ALIAS(gh-c2),
    { "ccj-alpha", OPT_CCJ_ALPHA, "RANGE", 0,
      "F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))", 0 },
    { "ccj-beta", OPT_CCJ_BETA, "RANGE", 0,
      "F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))", 0 },
    { "ccj-beta-prime", OPT_CCJ_BETA_PRIME, "RANGE", 0,
      "F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))", 0 },
242
243
    { "dac-patterns", OPT_DAC_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Dwyer et al. [FMSP'98] Spec. Patterns for LTL "
244
      "(range should be included in 1..55)", 0 },
245
246
247
    { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Etessami and Holzmann [Concur'00] patterns "
      "(range should be included in 1..12)", 0 },
248
    { "gh-q", OPT_GH_Q, "RANGE", 0,
249
      "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 },
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
    { "gh-r", OPT_GH_R, "RANGE", 0,
      "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0},
    { "go-theta", OPT_GO_THETA, "RANGE", 0,
      "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 },
    { "or-fg", OPT_OR_FG, "RANGE", 0, "FG(p1)|FG(p2)|...|FG(pn)", 0 },
    OPT_ALIAS(ccj-xi),
    { "or-g", OPT_OR_G, "RANGE", 0, "G(p1)|G(p2)|...|G(pn)", 0 },
    OPT_ALIAS(gh-s),
    { "or-gf", OPT_OR_GF, "RANGE", 0, "GF(p1)|GF(p2)|...|GF(pn)", 0 },
    OPT_ALIAS(gh-c1),
    { "r-left", OPT_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 },
    { "r-right", OPT_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 },
    { "rv-counter", OPT_RV_COUNTER, "RANGE", 0,
      "n-bit counter", 0 },
    { "rv-counter-carry", OPT_RV_COUNTER_CARRY, "RANGE", 0,
      "n-bit counter w/ carry", 0 },
    { "rv-counter-carry-linear", OPT_RV_COUNTER_CARRY_LINEAR, "RANGE", 0,
      "n-bit counter w/ carry (linear size)", 0 },
    { "rv-counter-linear", OPT_RV_COUNTER_LINEAR, "RANGE", 0,
      "n-bit counter (linear size)", 0 },
270
271
272
    { "sb-patterns", OPT_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Somenzi and Bloem [CAV'00] patterns "
      "(range should be included in 1..27)", 0 },
273
274
275
276
277
278
    { "tv-f1", OPT_TV_F1, "RANGE", 0, "G(p -> (q | Xq | ... | XX...Xq)", 0 },
    { "tv-f2", OPT_TV_F2, "RANGE", 0, "G(p -> (q | X(q | X(... | Xq)))", 0 },
    { "tv-g1", OPT_TV_G1, "RANGE", 0, "G(p -> (q & Xq & ... & XX...Xq)", 0 },
    { "tv-g2", OPT_TV_G2, "RANGE", 0, "G(p -> (q & X(q & X(... & Xq)))", 0 },
    { "tv-uu", OPT_TV_UU, "RANGE", 0,
      "G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...))))))", 0 },
279
280
281
282
283
    { "u-left", OPT_U_LEFT, "RANGE", 0, "(((p1 U p2) U p3) ... U pn)", 0 },
    OPT_ALIAS(gh-u),
    { "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 },
    OPT_ALIAS(gh-u2),
    OPT_ALIAS(go-phi),
284
    RANGE_DOC,
285
  /**************************************************/
286
    { nullptr, 0, nullptr, 0, "Output options:", -20 },
287
288
289
290
291
292
    { "negative", OPT_NEGATIVE, nullptr, 0,
      "output the negated versions of all formulas", 0 },
    OPT_ALIAS(negated),
    { "positive", OPT_POSITIVE, nullptr, 0,
      "output the positive versions of all formulas (done by default, unless"
      " --negative is specified without --positive)", 0 },
293
    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
294
      "the following interpreted sequences:", -19 },
295
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
296
      "the formula (in the selected syntax)", 0 },
297
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
298
      "the name of the pattern", 0 },
299
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
300
      "the argument of the pattern", 0 },
301
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
302
      "a single %", 0 },
303
    COMMON_LTL_OUTPUT_SPECS,
304
305
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
306
307
308
309
310
  };

struct job
{
  int pattern;
311
  struct range range;
312
313
314
315
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
316
317
bool opt_positive = false;
bool opt_negative = false;
318
319
320

const struct argp_child children[] =
  {
321
322
323
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
324
  };
325
326

static void
327
enqueue_job(int pattern, const char* range_str)
328
329
330
{
  job j;
  j.pattern = pattern;
331
  j.range = parse_range(range_str);
332
333
334
  jobs.push_back(j);
}

335
336
337
338
339
340
341
342
343
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

344
static int
345
parse_opt(int key, char* arg, struct argp_state*)
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case OPT_AND_F:
    case OPT_AND_FG:
    case OPT_AND_GF:
    case OPT_CCJ_ALPHA:
    case OPT_CCJ_BETA:
    case OPT_CCJ_BETA_PRIME:
    case OPT_GH_Q:
    case OPT_GH_R:
    case OPT_GO_THETA:
    case OPT_OR_FG:
    case OPT_OR_G:
    case OPT_OR_GF:
    case OPT_R_LEFT:
    case OPT_R_RIGHT:
    case OPT_RV_COUNTER:
    case OPT_RV_COUNTER_CARRY:
    case OPT_RV_COUNTER_CARRY_LINEAR:
    case OPT_RV_COUNTER_LINEAR:
368
369
370
371
372
    case OPT_TV_F1:
    case OPT_TV_F2:
    case OPT_TV_G1:
    case OPT_TV_G2:
    case OPT_TV_UU:
373
374
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
375
376
      enqueue_job(key, arg);
      break;
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
    case OPT_DAC_PATTERNS:
      if (arg)
        enqueue_job(key, arg);
      else
        enqueue_job(key, 1, 55);
      break;
    case OPT_EH_PATTERNS:
      if (arg)
        enqueue_job(key, arg);
      else
        enqueue_job(key, 1, 12);
      break;
    case OPT_SB_PATTERNS:
      if (arg)
        enqueue_job(key, arg);
      else
        enqueue_job(key, 1, 27);
      break;
395
396
397
398
399
400
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
401
402
403
404
405
406
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

407
408
409
410
411
412
413
414
415
416
#define G_(x) formula::G(x)
#define F_(x) formula::F(x)
#define X_(x) formula::X(x)
#define Not_(x) formula::Not(x)

#define Implies_(x, y) formula::Implies((x), (y))
#define Equiv_(x, y) formula::Equiv((x), (y))
#define And_(x, y) formula::And({(x), (y)})
#define Or_(x, y) formula::Or({(x), (y)})
#define U_(x, y) formula::U((x), (y))
417
418

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
419
static formula
420
421
422
E_n(std::string name, int n)
{
  if (n <= 0)
423
    return formula::tt();
424

425
  formula result = nullptr;
426
427
428
429
430

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
431
      formula f = formula::ap(p.str());
432
      if (result)
433
        result = And_(f, result);
434
      else
435
        result = f;
436
437
438
439
440
441
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
442
static formula
443
444
phi_n(std::string name, int n,
      op oper = op::And)
445
446
{
  if (n <= 0)
447
    return formula::tt();
448

449
450
  formula result = nullptr;
  formula p = formula::ap(name);
451
452
453
  for (; n > 0; --n)
    {
      if (result)
454
        result = formula::multop(oper, {p, X_(result)});
455
      else
456
        result = p;
457
458
459
460
    }
  return result;
}

461
462
static formula
N_n(std::string name, int n)
463
{
464
  return formula::F(phi_n(name, n));
465
466
467
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
468
static formula
469
470
phi_prime_n(std::string name, int n,
            op oper = op::And)
471
472
{
  if (n <= 0)
473
    return formula::tt();
474

475
476
  formula result = nullptr;
  formula p = formula::ap(name);
477
478
479
  for (; n > 0; --n)
    {
      if (result)
480
481
        {
          p = X_(p);
482
          result = formula::multop(oper, {result, p});
483
        }
484
      else
485
486
487
        {
          result = p;
        }
488
489
490
491
    }
  return result;
}

492
static formula
493
494
495
496
497
498
499
500
N_prime_n(std::string name, int n)
{
  return F_(phi_prime_n(name, n));
}


// GF(p_1) & GF(p_2) & ... & GF(p_n)   if conj == true
// GF(p_1) | GF(p_2) | ... | GF(p_n)   if conj == false
501
static formula
502
503
504
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
505
    return conj ? formula::tt() : formula::ff();
506

507
  formula result = nullptr;
508

509
  op o = conj ? op::And : op::Or;
510
511
512
513
514

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << i;
515
      formula f = G_(F_(formula::ap(p.str())));
516
517

      if (result)
518
        result = formula::multop(o, {f, result});
519
      else
520
        result = f;
521
522
523
524
525
526
    }
  return result;
}

// FG(p_1) | FG(p_2) | ... | FG(p_n)   if conj == false
// FG(p_1) & FG(p_2) & ... & FG(p_n)   if conj == true
527
static formula
528
529
530
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
531
    return conj ? formula::tt() : formula::ff();
532

533
  formula result = nullptr;
534

535
  op o = conj ? op::And : op::Or;
536
537
538
539
540

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << i;
541
      formula f = F_(G_(formula::ap(p.str())));
542
543

      if (result)
544
        result = formula::multop(o, {f, result});
545
      else
546
        result = f;
547
548
549
550
551
552
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
553
554
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
555
556
557
558
{
  if (n <= 0)
    n = 1;

559
  formula result = nullptr;
560
561
562
563
564

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
565
      formula f = formula::ap(p.str());
566
      if (!result)
567
        result = f;
568
      else if (right_assoc)
569
        result = formula::binop(o, f, result);
570
      else
571
        result = formula::binop(o, result, f);
572
573
574
575
576
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
577
static formula
578
579
580
R_n(std::string name, int n)
{
  if (n <= 0)
581
    return formula::tt();
582

583
  formula pi;
584
585
586
587

  {
    std::ostringstream p;
    p << name << 1;
588
    pi = formula::ap(p.str());
589
590
  }

591
  formula result = nullptr;
592
593
594

  for (int i = 1; i <= n; ++i)
    {
595
      formula gf = G_(F_(pi));
596
597
      std::ostringstream p;
      p << name << i + 1;
598
      pi = formula::ap(p.str());
599

600
      formula fg = F_(G_(pi));
601

602
      formula f = Or_(gf, fg);
603
604

      if (result)
605
        result = And_(f, result);
606
      else
607
        result = f;
608
609
610
611
612
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
613
static formula
614
615
616
Q_n(std::string name, int n)
{
  if (n <= 0)
617
    return formula::tt();
618

619
  formula pi;
620
621
622
623

  {
    std::ostringstream p;
    p << name << 1;
624
    pi = formula::ap(p.str());
625
626
  }

627
  formula result = nullptr;
628
629
630

  for (int i = 1; i <= n; ++i)
    {
631
      formula f = F_(pi);
632
633
634

      std::ostringstream p;
      p << name << i + 1;
635
      pi = formula::ap(p.str());
636

637
      formula g = G_(pi);
638
639
640
641

      f = Or_(f, g);

      if (result)
642
        result = And_(f, result);
643
      else
644
        result = f;
645
646
647
648
649
650
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
651
652
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
653
654
{
  if (n <= 0)
655
    return conj ? formula::tt() : formula::ff();
656

657
  formula result = nullptr;
658

659
  op cop = conj ? op::And : op::Or;
660
661
662
663
664

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << i;
665
      formula f = formula::unop(o, formula::ap(p.str()));
666
667

      if (result)
668
        result = formula::multop(cop, {f, result});
669
      else
670
        result = f;
671
672
673
674
675
676
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
677
static formula
678
679
fair_response(std::string p, std::string q, std::string r, int n)
{
680
681
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
682
683
684
685
686
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
687
688
static formula
X_n(formula p, int n)
689
690
{
  assert(n >= 0);
691
  formula res = p;
692
693
694
695
696
697
698
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
699
static formula
700
701
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
702
703
704
705
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
706

707
  std::vector<formula> res(4);
708
709
710
711
712
713

  // The marker starts with "1", followed by n-1 "0", then "1" again,
  // n-1 "0", etc.
  if (!linear)
    {
      // G(m -> X(!m)&XX(!m)&XXX(m))          [if n = 3]
714
      std::vector<formula> v(n);
715
      for (int i = 0; i + 1 < n; ++i)
716
        v[i] = X_n(neg_m, i + 1);
717
718
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
719
720
721
722
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
723
      formula p = m;
724
      for (int i = n - 1; i > 0; --i)
725
        p = And_(neg_m, X_(p));
726
      res[0] = And_(m, G_(Implies_(m, X_(p))));
727
728
729
730
731
732
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
733
      std::vector<formula> v2(n);
734
      for (int i = 0; i < n; ++i)
735
        v2[i] = X_n(neg_b, i);
736
      res[1] = formula::And(std::move(v2));
737
738
739
740
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
741
      formula p = neg_b;
742
      for (int i = n - 1; i > 0; --i)
743
        p = And_(neg_b, X_(p));
744
      res[1] = p;
745
746
747
748
749
750
    }

#define AndX_(x, y) (linear ? X_(And_((x), (y))) : And_(X_(x), X_(y)))

  // If the least significant bit is 0, it will be 1 at the next time,
  // and other bits stay the same.
751
752
753
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
754
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
755
756
757

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
758
759
760
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
761
762
763
764
765
766
767
                       AndX_(Xnm1_negb,
                             U_(And_(And_(b, neg_m), Xn_negb),
                                Or_(m, And_(And_(neg_m, neg_b),
                                            AndX_(Xnm1_b,
                                                  U_(And_(neg_m,
                                                          Equiv_(b, Xn_b)),
                                                     m))))))));
768
  return formula::And(std::move(res));
769
770
}

771
static formula
772
ltl_counter_carry(std::string bit, std::string marker,
773
                  std::string carry, int n, bool linear)
774
{
775
776
777
778
779
780
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
  formula c = formula::ap(carry);
  formula neg_c = Not_(c);
781

782
  std::vector<formula> res(6);
783
784
785
786
787
788

  // The marker starts with "1", followed by n-1 "0", then "1" again,
  // n-1 "0", etc.
  if (!linear)
    {
      // G(m -> X(!m)&XX(!m)&XXX(m))          [if n = 3]
789
      std::vector<formula> v(n);
790
      for (int i = 0; i + 1 < n; ++i)
791
        v[i] = X_n(neg_m, i + 1);
792
793
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
794
795
796
797
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
798
      formula p = m;
799
      for (int i = n - 1; i > 0; --i)
800
        p = And_(neg_m, X_(p));
801
      res[0] = And_(m, G_(Implies_(m, X_(p))));
802
803
804
805
806
807
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
808
      std::vector<formula> v2(n);
809
      for (int i = 0; i < n; ++i)
810
        v2[i] = X_n(neg_b, i);
811
      res[1] = formula::And(std::move(v2));
812
813
814
815
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
816
      formula p = neg_b;
817
      for (int i = n - 1; i > 0; --i)
818
        p = And_(neg_b, X_(p));
819
      res[1] = p;
820
821
    }

822
823
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
824
825

  // If m is 1 and b is 0 then c is 0 and n steps later b is 1.
826
  res[2] = G_(Implies_(And_(m, neg_b), And_(neg_c, Xn_b)));
827
828

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
829
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
830
831
832
833

  if (!linear)
    {
      // If there's no carry, then all of the bits stay the same n steps later.
834
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
835
                           And_(X_(Not_(c)), Equiv_(X_(b), X_(Xn_b)))));
836
837
838

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
839
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
840
841
842
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
843
844
845
846
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
847
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
848
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
849
850
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
851
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
852
                                      Implies_(b, And_(c, Xn_negb))))));
853
    }
854
  return formula::And(std::move(res));
855
856
}

857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
static formula
tv_f1(std::string p, std::string q, int n)
{
  return G_(Implies_(formula::ap(p), phi_prime_n(q, n, op::Or)));
}

static formula
tv_f2(std::string p, std::string q, int n)
{
  return G_(Implies_(formula::ap(p), phi_n(q, n, op::Or)));
}

static formula
tv_g1(std::string p, std::string q, int n)
{
  return G_(Implies_(formula::ap(p), phi_prime_n(q, n)));
}

static formula
tv_g2(std::string p, std::string q, int n)
{
  return G_(Implies_(formula::ap(p), phi_n(q, n)));
}

static formula
tv_uu(std::string name, int n)
{
  std::ostringstream p;
  p << name << n + 1;
  formula q = formula::ap(p.str());
  formula f = q;

  for (int i = n; i > 0; --i)
    {
      p.str("");
      p << name << i;
      q = formula::ap(p.str());
      f = U_(q, f);
      if (i > 1)
        f = And_(q, f);
    }
  return G_(Implies_(q,  f));
}

901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
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
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
static void bad_number(const char* pattern, int n, int max)
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
      << ", supported range is 1.." << max;
  throw std::runtime_error(err.str());
}

static formula
dac_pattern(int n)
{
  static const char* formulas[] = {
    "[](!p0)",
    "<>p2 -> (!p0 U p2)",
    "[](p1 -> [](!p0))",
    "[]((p1 & !p2 & <>p2) -> (!p0 U p2))",
    "[](p1 & !p2 -> (!p0 W p2))",

    "<>(p0)",
    "!p2 W (p0 & !p2)",
    "[](!p1) | <>(p1 & <>p0)",
    "[](p1 & !p2 -> (!p2 W (p0 & !p2)))",
    "[](p1 & !p2 -> (!p2 U (p0 & !p2)))",

    "(!p0 W (p0 W (!p0 W (p0 W []!p0))))",
    "<>p2 -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 |"
    " ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | (!p0 U p2)))))))))",
    "<>p1 -> (!p1 U (p1 & (!p0 W (p0 W (!p0 W (p0 W []!p0))))))",
    "[]((p1 & <>p2) -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 |"
    "((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | (!p0 U p2))))))))))",
    "[](p1 -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | ((!p0 & !p2) U"
    "(p2 | ((p0 & !p2) U (p2 | (!p0 W p2) | []p0)))))))))",

    "[](p0)",
    "<>p2 -> (p0 U p2)",
    "[](p1 -> [](p0))",
    "[]((p1 & !p2 & <>p2) -> (p0 U p2))",
    "[](p1 & !p2 -> (p0 W p2))",

    "!p0 W p3",
    "<>p2 -> (!p0 U (p3 | p2))",
    "[]!p1 | <>(p1 & (!p0 W p3))",
    "[]((p1 & !p2 & <>p2) -> (!p0 U (p3 | p2)))",
    "[](p1 & !p2 -> (!p0 W (p3 | p2)))",

    "[](p0 -> <>p3)",
    "<>p2 -> (p0 -> (!p2 U (p3 & !p2))) U p2",
    "[](p1 -> [](p0 -> <>p3))",
    "[]((p1 & !p2 & <>p2) -> ((p0 -> (!p2 U (p3 & !p2))) U p2))",
    "[](p1 & !p2 -> ((p0 -> (!p2 U (p3 & !p2))) W p2))",

    "<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))",
    "<>p2 -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4))))",
    "([]!p1) | (!p1 U (p1 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))",
    "[]((p1 & <>p2) -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4)))))",
    "[](p1 -> (<>p0 -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4))))))",

    "(<>(p3 & X<>p4)) -> ((!p3) U p0)",
    "<>p2 -> ((!(p3 & (!p2) & X(!p2 U (p4 & !p2)))) U (p2 | p0))",
    "([]!p1) | ((!p1) U (p1 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))",
    "[]((p1 & <>p2) -> ((!(p3 & (!p2) & X(!p2 U (p4 & !p2)))) U (p2 | p0)))",
    "[](p1 -> (!(p3 & (!p2) & X(!p2 U (p4 & !p2))) U (p2 | p0) |"
    " [](!(p3 & X<>p4))))",

    "[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))",
    "<>p2 -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U p2",
    "[] (p1 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))",
    "[] ((p1 & <>p2) -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U p2)",
    "[] (p1 -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U (p2 |"
    "[] (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0)))))",

    "[] (p0 -> <>(p3 & X<>p4))",
    "<>p2 -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U p2",
    "[] (p1 -> [] (p0 -> (p3 & X<> p4)))",
    "[] ((p1 & <>p2) -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U p2)",
    "[] (p1 -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U (p2 | []"
    "(p0 -> (p3 & X<> p4))))",

    "[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))",
    "<>p2 -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U p4)))) U p2",
    "[] (p1 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))",
    "[] ((p1 & <>p2) -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U"
    " p4)))) U p2)",
    "[] (p1 -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U p4)))) U (p2 |"
    "[] (p0 -> (p3 & !p5 & X(!p5 U p4)))))",
  };

  constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
  if (n < 1 || (unsigned) n > max)
    bad_number("--dac-patterns", n, max);
  return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}

static formula
eh_pattern(int n)
{
  static const char* formulas[] = {
    "p0 U (p1 & G(p2))",
    "p0 U (p1 & X(p2 U p3))",
    "p0 U (p1 & X(p2 & (F(p3 & X(F(p4 & X(F(p5 & X(F(p6))))))))))",
    "F(p0 & X(G(p1)))",
    "F(p0 & X(p1 & X(F(p2))))",
    "F(p0 & X(p1 U p2))",
    "(F(G(p0))) | (G(F(p1)))",
    "G(p0 -> (p1 U p2))",
    "G(p0 & X(F(p1 & X(F(p2 & X(F(p3)))))))",
    "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))) & (G(F(p4)))",
    "(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))",
    "G(p0 -> (p1 U ((G(p2)) | (G(p3)))))",
  };

  constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
  if (n < 1 || (unsigned) n > max)
    bad_number("--eh-patterns", n, max);
  return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}

static formula
sb_pattern(int n)
{
  static const char* formulas[] = {
    "p0 U p1",
    "p0 U (p1 U p2)",
    "!(p0 U (p1 U p2))",
    "G(F(p0)) -> G(F(p1))",
    "(F(p0)) U (G(p1))",
    "(G(p0)) U p1",
    "!((F(F(p0))) <-> (F(p)))",
    "!((G(F(p0))) -> (G(F(p))))",
    "!((G(F(p0))) <-> (G(F(p))))",
    "p0 R (p0 | p1)",
    "(Xp0 U Xp1) | !X(p0 U p1)",
    "(Xp0 U p1) | !X(p0 U (p0 & p1))",
    "G(p0 -> F(p1)) & (((X(p0)) U p1) | !X(p0 U (p0 & p1)))",
    "G(p0 -> F(p1)) & (((X(p0)) U X(p1)) | !X(p0 U p1))",
    "G(p0 -> F(p1))",
    "!G(p0 -> X(p1 R p2))",
    "!(F(G(p0)) | F(G(p1)))",
    "G(F(p0) & F(p1))",
    "F(p0) & F(!p0)",
    "(X(p1) & p2) R X(((p3 U p0) R p2) U (p3 R p2))",
    "(G(p1 | G(F(p0))) & G(p2 | G(F(!p0)))) | G(p1) | G(p2)",
    "(G(p1 | F(G(p0))) & G(p2 | F(G(!p0)))) | G(p1) | G(p2)",
    "!((G(p1 | G(F(p0))) & G(p2 | G(F(!p0)))) | G(p1) | G(p2))",
    "!((G(p1 | F(G(p0))) & G(p2 | F(G(!p0)))) | G(p1) | G(p2))",
    "(G(p1 | X(G p0))) & (G (p2 | X(G !p0)))",
    "G(p1 | (Xp0 & X!p0))",
    // p0 U p0 can't be represented other than as p0 in Spot
    "(p0 U p0) | (p1 U p0)",
  };

  constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
  if (n < 1 || (unsigned) n > max)
    bad_number("--sb-patterns", n, max);
  return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}
1057
1058
1059
1060

static void
output_pattern(int pattern, int n)
{
1061
  formula f = nullptr;
1062
1063
1064
1065
  switch (pattern)
    {
      // Keep this alphabetically-ordered!
    case OPT_AND_F:
1066
      f = combunop_n("p", n, op::F, true);
1067
1068
1069
1070
1071
1072
1073
1074
      break;
    case OPT_AND_FG:
      f = FG_n("p", n, true);
      break;
    case OPT_AND_GF:
      f = GF_n("p", n, true);
      break;
    case OPT_CCJ_ALPHA:
1075
      f = formula::And({E_n("p", n), E_n("q", n)});
1076
1077
      break;
    case OPT_CCJ_BETA:
1078
      f = formula::And({N_n("p", n), N_n("q", n)});
1079
1080
      break;
    case OPT_CCJ_BETA_PRIME:
1081
      f = formula::And({N_prime_n("p", n), N_prime_n("q", n)});
1082
      break;
1083
1084
1085
1086
1087
1088
    case OPT_DAC_PATTERNS:
      f = dac_pattern(n);
      break;
    case OPT_EH_PATTERNS:
      f = eh_pattern(n);
      break;
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
    case OPT_GH_Q:
      f = Q_n("p", n);
      break;
    case OPT_GH_R:
      f = R_n("p", n);
      break;
    case OPT_GO_THETA:
      f = fair_response("p", "q", "r", n);
      break;
    case OPT_OR_FG:
      f = FG_n("p", n, false);
      break;
    case OPT_OR_G:
1102
      f = combunop_n("p", n, op::G, false);
1103
1104
1105
1106
1107
      break;
    case OPT_OR_GF:
      f = GF_n("p", n, false);
      break;
    case OPT_R_LEFT:
1108
      f = bin_n("p", n, op::R, false);
1109
1110
      break;
    case OPT_R_RIGHT:
1111
      f = bin_n("p", n, op::R, true);
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
      break;
    case OPT_RV_COUNTER_CARRY:
      f = ltl_counter_carry("b", "m", "c", n, false);
      break;
    case OPT_RV_COUNTER_CARRY_LINEAR:
      f = ltl_counter_carry("b", "m", "c", n, true);
      break;
    case OPT_RV_COUNTER:
      f = ltl_counter("b", "m", n, false);
      break;
    case OPT_RV_COUNTER_LINEAR:
      f = ltl_counter("b", "m", n, true);
      break;
1125
1126
1127
    case OPT_SB_PATTERNS:
      f = sb_pattern(n);
      break;
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
    case OPT_TV_F1:
      f = tv_f1("p", "q", n);
      break;
    case OPT_TV_F2:
      f = tv_f2("p", "q", n);
      break;
    case OPT_TV_G1:
      f = tv_g1("p", "q", n);
      break;
    case OPT_TV_G2:
      f = tv_g2("p", "q", n);
      break;
    case OPT_TV_UU:
      f = tv_uu("p", n);
      break;
1143
    case OPT_U_LEFT:
1144
      f = bin_n("p", n, op::U, false);
1145
1146
      break;
    case OPT_U_RIGHT:
1147
      f = bin_n("p", n, op::U, true);
1148
1149
1150
1151
1152
      break;
    default:
      error(100, 0, "internal error: pattern not implemented");
    }

1153
1154
  // Make sure we use only "p42"-style of atomic propositions
  // in lbt's output.
1155
1156
  if (output_format == lbt_output && !f.has_lbt_atomic_props())
    f = relabel(f, Pnn);
1157

1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
  if (opt_positive || !opt_negative)
    {
      output_formula_checked(f, class_name[pattern - 1], n);
    }
  if (opt_negative)
    {
      std::string tmp = "!";
      tmp += class_name[pattern - 1];
      output_formula_checked(spot::formula::Not(f), tmp.c_str(), n);
    }
1168
1169
1170
1171
1172
}

static void
run_jobs()
{
1173
  for (auto& j: jobs)
1174
    {
1175
1176
      int inc = (j.range.max < j.range.min) ? -1 : 1;
      int n = j.range.min;
1177
      for (;;)
1178
1179
1180
1181
1182
1183
        {
          output_pattern(j.pattern, n);
          if (n == j.range.max)
            break;
          n += inc;
        }
1184
1185
1186
1187
1188
1189
1190
    }
}


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

1193
  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
1194
                    children, nullptr, nullptr };
1195

1196
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
1197
1198
1199
1200
    exit(err);

  if (jobs.empty())
    error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
1201
          program_name);
1202

1203
1204
1205
1206
1207
1208
1209
1210
1211
  try
    {
      run_jobs();
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }

1212
  flush_cout();
1213
1214
  return 0;
}