genltl.cc 30.3 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
#include "common_sys.hh"
111
112
113
114
115
116
117
118

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

119
#include "common_setup.hh"
120
#include "common_output.hh"
121
#include "common_range.hh"
122
123
124
125
126
127
128
129

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
#include <cstdlib>
#include <cstring>
130
131
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
132
#include <spot/tl/parse.hh>
133
134
135
136

using namespace spot;

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

139
140
141
142
143
144
145
enum {
  OPT_AND_F = 1,
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
146
147
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
148
149
150
151
152
153
154
155
156
157
158
159
  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,
160
  OPT_SB_PATTERNS,
161
162
163
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
164
165
  OPT_POSITIVE,
  OPT_NEGATIVE,
166
};
167
168
169
170
171
172
173
174
175

const char* const class_name[LAST_CLASS] =
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
176
177
    "dac-patterns",
    "eh-patterns",
178
179
180
181
182
183
184
185
186
187
188
189
    "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",
190
    "sb-patterns",
191
192
193
194
    "u-left",
    "u-right",
  };

195

196
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
197
198
199
200
201

static const argp_option options[] =
  {
    /**************************************************/
    // Keep this alphabetically sorted (expect for aliases).
202
    { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
203
204
205
206
207
208
209
210
211
212
213
214
215
216
    // 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 },
217
218
219
220
221
222
    { "dac-patterns", OPT_DAC_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Dwyer et al. [FMSP'98] Spec. Patterns for LTL "
      "(range should be included in 1..45)", 0 },
    { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Etessami and Holzmann [Concur'00] patterns "
      "(range should be included in 1..12)", 0 },
223
    { "gh-q", OPT_GH_Q, "RANGE", 0,
224
      "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 },
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
    { "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 },
245
246
247
    { "sb-patterns", OPT_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Somenzi and Bloem [CAV'00] patterns "
      "(range should be included in 1..27)", 0 },
248
249
250
251
252
    { "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),
253
    RANGE_DOC,
254
  /**************************************************/
255
    { nullptr, 0, nullptr, 0, "Output options:", -20 },
256
257
258
259
260
261
    { "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 },
262
    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
263
      "the following interpreted sequences:", -19 },
264
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
265
      "the formula (in the selected syntax)", 0 },
266
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
267
      "the name of the pattern", 0 },
268
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
269
      "the argument of the pattern", 0 },
270
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
271
      "a single %", 0 },
272
273
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
274
275
276
277
278
  };

struct job
{
  int pattern;
279
  struct range range;
280
281
282
283
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
284
285
bool opt_positive = false;
bool opt_negative = false;
286
287
288

const struct argp_child children[] =
  {
289
290
291
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
292
  };
293
294

static void
295
enqueue_job(int pattern, const char* range_str)
296
297
298
{
  job j;
  j.pattern = pattern;
299
  j.range = parse_range(range_str);
300
301
302
  jobs.push_back(j);
}

303
304
305
306
307
308
309
310
311
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

312
static int
313
parse_opt(int key, char* arg, struct argp_state*)
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
{
  // 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:
336
337
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
338
339
      enqueue_job(key, arg);
      break;
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
    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;
358
359
360
361
362
363
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
364
365
366
367
368
369
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

370
371
372
373
374
375
376
377
378
379
#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))
380
381

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
382
static formula
383
384
385
E_n(std::string name, int n)
{
  if (n <= 0)
386
    return formula::tt();
387

388
  formula result = nullptr;
389
390
391
392
393

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
394
      formula f = formula::ap(p.str());
395
      if (result)
396
        result = And_(f, result);
397
      else
398
        result = f;
399
400
401
402
403
404
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
405
static formula
406
407
408
phi_n(std::string name, int n)
{
  if (n <= 0)
409
    return formula::tt();
410

411
412
  formula result = nullptr;
  formula p = formula::ap(name);
413
414
415
  for (; n > 0; --n)
    {
      if (result)
416
        result = And_(p, X_(result));
417
      else
418
        result = p;
419
420
421
422
    }
  return result;
}

423
424
static formula
N_n(std::string name, int n)
425
{
426
  return formula::F(phi_n(name, n));
427
428
429
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
430
static formula
431
432
433
phi_prime_n(std::string name, int n)
{
  if (n <= 0)
434
    return formula::tt();
435

436
437
  formula result = nullptr;
  formula p = formula::ap(name);
438
439
440
  for (; n > 0; --n)
    {
      if (result)
441
442
443
444
        {
          p = X_(p);
          result = And_(result, p);
        }
445
      else
446
447
448
        {
          result = p;
        }
449
450
451
452
    }
  return result;
}

453
static formula
454
455
456
457
458
459
460
461
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
462
static formula
463
464
465
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
466
    return conj ? formula::tt() : formula::ff();
467

468
  formula result = nullptr;
469

470
  op o = conj ? op::And : op::Or;
471
472
473
474
475

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

      if (result)
479
        result = formula::multop(o, {f, result});
480
      else
481
        result = f;
482
483
484
485
486
487
    }
  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
488
static formula
489
490
491
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
492
    return conj ? formula::tt() : formula::ff();
493

494
  formula result = nullptr;
495

496
  op o = conj ? op::And : op::Or;
497
498
499
500
501

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

      if (result)
505
        result = formula::multop(o, {f, result});
506
      else
507
        result = f;
508
509
510
511
512
513
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
514
515
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
516
517
518
519
{
  if (n <= 0)
    n = 1;

520
  formula result = nullptr;
521
522
523
524
525

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
526
      formula f = formula::ap(p.str());
527
      if (!result)
528
        result = f;
529
      else if (right_assoc)
530
        result = formula::binop(o, f, result);
531
      else
532
        result = formula::binop(o, result, f);
533
534
535
536
537
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
538
static formula
539
540
541
R_n(std::string name, int n)
{
  if (n <= 0)
542
    return formula::tt();
543

544
  formula pi;
545
546
547
548

  {
    std::ostringstream p;
    p << name << 1;
549
    pi = formula::ap(p.str());
550
551
  }

552
  formula result = nullptr;
553
554
555

  for (int i = 1; i <= n; ++i)
    {
556
      formula gf = G_(F_(pi));
557
558
      std::ostringstream p;
      p << name << i + 1;
559
      pi = formula::ap(p.str());
560

561
      formula fg = F_(G_(pi));
562

563
      formula f = Or_(gf, fg);
564
565

      if (result)
566
        result = And_(f, result);
567
      else
568
        result = f;
569
570
571
572
573
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
574
static formula
575
576
577
Q_n(std::string name, int n)
{
  if (n <= 0)
578
    return formula::tt();
579

580
  formula pi;
581
582
583
584

  {
    std::ostringstream p;
    p << name << 1;
585
    pi = formula::ap(p.str());
586
587
  }

588
  formula result = nullptr;
589
590
591

  for (int i = 1; i <= n; ++i)
    {
592
      formula f = F_(pi);
593
594
595

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

598
      formula g = G_(pi);
599
600
601
602

      f = Or_(f, g);

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

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
612
613
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
614
615
{
  if (n <= 0)
616
    return conj ? formula::tt() : formula::ff();
617

618
  formula result = nullptr;
619

620
  op cop = conj ? op::And : op::Or;
621
622
623
624
625

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

      if (result)
629
        result = formula::multop(cop, {f, result});
630
      else
631
        result = f;
632
633
634
635
636
637
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
638
static formula
639
640
fair_response(std::string p, std::string q, std::string r, int n)
{
641
642
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
643
644
645
646
647
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
648
649
static formula
X_n(formula p, int n)
650
651
{
  assert(n >= 0);
652
  formula res = p;
653
654
655
656
657
658
659
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
660
static formula
661
662
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
663
664
665
666
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
667

668
  std::vector<formula> res(4);
669
670
671
672
673
674

  // 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]
675
      std::vector<formula> v(n);
676
      for (int i = 0; i + 1 < n; ++i)
677
        v[i] = X_n(neg_m, i + 1);
678
679
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
680
681
682
683
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
684
      formula p = m;
685
      for (int i = n - 1; i > 0; --i)
686
        p = And_(neg_m, X_(p));
687
      res[0] = And_(m, G_(Implies_(m, X_(p))));
688
689
690
691
692
693
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
694
      std::vector<formula> v2(n);
695
      for (int i = 0; i < n; ++i)
696
        v2[i] = X_n(neg_b, i);
697
      res[1] = formula::And(std::move(v2));
698
699
700
701
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
702
      formula p = neg_b;
703
      for (int i = n - 1; i > 0; --i)
704
        p = And_(neg_b, X_(p));
705
      res[1] = p;
706
707
708
709
710
711
    }

#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.
712
713
714
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
715
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
716
717
718

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
719
720
721
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
722
723
724
725
726
727
728
                       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))))))));
729
  return formula::And(std::move(res));
730
731
}

732
static formula
733
ltl_counter_carry(std::string bit, std::string marker,
734
                  std::string carry, int n, bool linear)
735
{
736
737
738
739
740
741
  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);
742

743
  std::vector<formula> res(6);
744
745
746
747
748
749

  // 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]
750
      std::vector<formula> v(n);
751
      for (int i = 0; i + 1 < n; ++i)
752
        v[i] = X_n(neg_m, i + 1);
753
754
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
755
756
757
758
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
759
      formula p = m;
760
      for (int i = n - 1; i > 0; --i)
761
        p = And_(neg_m, X_(p));
762
      res[0] = And_(m, G_(Implies_(m, X_(p))));
763
764
765
766
767
768
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
769
      std::vector<formula> v2(n);
770
      for (int i = 0; i < n; ++i)
771
        v2[i] = X_n(neg_b, i);
772
      res[1] = formula::And(std::move(v2));
773
774
775
776
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
777
      formula p = neg_b;
778
      for (int i = n - 1; i > 0; --i)
779
        p = And_(neg_b, X_(p));
780
      res[1] = p;
781
782
    }

783
784
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
785
786

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
790
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
791
792
793
794

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
800
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
801
802
803
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
804
805
806
807
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
808
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
809
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
810
811
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
812
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
813
                                      Implies_(b, And_(c, Xn_negb))))));
814
    }
815
  return formula::And(std::move(res));
816
817
}

818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
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
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
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);
}
974
975
976
977

static void
output_pattern(int pattern, int n)
{
978
  formula f = nullptr;
979
980
981
982
  switch (pattern)
    {
      // Keep this alphabetically-ordered!
    case OPT_AND_F:
983
      f = combunop_n("p", n, op::F, true);
984
985
986
987
988
989
990
991
      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:
992
      f = formula::And({E_n("p", n), E_n("q", n)});
993
994
      break;
    case OPT_CCJ_BETA:
995
      f = formula::And({N_n("p", n), N_n("q", n)});
996
997
      break;
    case OPT_CCJ_BETA_PRIME:
998
      f = formula::And({N_prime_n("p", n), N_prime_n("q", n)});
999
      break;
1000
1001
1002
1003
1004
1005
    case OPT_DAC_PATTERNS:
      f = dac_pattern(n);
      break;
    case OPT_EH_PATTERNS:
      f = eh_pattern(n);
      break;
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
    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:
1019
      f = combunop_n("p", n, op::G, false);
1020
1021
1022
1023
1024
      break;
    case OPT_OR_GF:
      f = GF_n("p", n, false);
      break;
    case OPT_R_LEFT:
1025
      f = bin_n("p", n, op::R, false);
1026
1027
      break;
    case OPT_R_RIGHT:
1028
      f = bin_n("p", n, op::R, true);
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
      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;
1042
1043
1044
    case OPT_SB_PATTERNS:
      f = sb_pattern(n);
      break;
1045
    case OPT_U_LEFT:
1046
      f = bin_n("p", n, op::U, false);
1047
1048
      break;
    case OPT_U_RIGHT:
1049
      f = bin_n("p", n, op::U, true);
1050
1051
1052
1053
1054
      break;
    default:
      error(100, 0, "internal error: pattern not implemented");
    }

1055
1056
  // Make sure we use only "p42"-style of atomic propositions
  // in lbt's output.
1057
1058
  if (output_format == lbt_output && !f.has_lbt_atomic_props())
    f = relabel(f, Pnn);
1059

1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
  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);
    }
1070
1071
1072
1073
1074
}

static void
run_jobs()
{
1075
  for (auto& j: jobs)
1076
    {
1077
1078
      int inc = (j.range.max < j.range.min) ? -1 : 1;
      int n = j.range.min;
1079
      for (;;)
1080
1081
1082
1083
1084
1085
        {
          output_pattern(j.pattern, n);
          if (n == j.range.max)
            break;
          n += inc;
        }
1086
1087
1088
1089
1090
1091
1092
    }
}


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

1095
  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
1096
                    children, nullptr, nullptr };
1097

1098
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
1099
1100
1101
1102
    exit(err);

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

1105
1106
1107
1108
1109
1110
1111
1112
1113
  try
    {
      run_jobs();
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }

1114
1115
  return 0;
}