genltl.cc 29.6 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
164
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
};
165
166
167
168
169
170
171
172
173

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

193

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

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

struct job
{
  int pattern;
271
  struct range range;
272
273
274
275
276
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;

277
278
279

const struct argp_child children[] =
  {
280
281
282
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
283
  };
284
285

static void
286
enqueue_job(int pattern, const char* range_str)
287
288
289
{
  job j;
  j.pattern = pattern;
290
  j.range = parse_range(range_str);
291
292
293
  jobs.push_back(j);
}

294
295
296
297
298
299
300
301
302
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

303
static int
304
parse_opt(int key, char* arg, struct argp_state*)
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
{
  // 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:
327
328
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
329
330
      enqueue_job(key, arg);
      break;
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
    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;
349
350
351
352
353
354
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

355
356
357
358
359
360
361
362
363
364
#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))
365
366

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
367
static formula
368
369
370
E_n(std::string name, int n)
{
  if (n <= 0)
371
    return formula::tt();
372

373
  formula result = nullptr;
374
375
376
377
378

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
379
      formula f = formula::ap(p.str());
380
      if (result)
381
        result = And_(f, result);
382
      else
383
        result = f;
384
385
386
387
388
389
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
390
static formula
391
392
393
phi_n(std::string name, int n)
{
  if (n <= 0)
394
    return formula::tt();
395

396
397
  formula result = nullptr;
  formula p = formula::ap(name);
398
399
400
  for (; n > 0; --n)
    {
      if (result)
401
        result = And_(p, X_(result));
402
      else
403
        result = p;
404
405
406
407
    }
  return result;
}

408
409
static formula
N_n(std::string name, int n)
410
{
411
  return formula::F(phi_n(name, n));
412
413
414
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
415
static formula
416
417
418
phi_prime_n(std::string name, int n)
{
  if (n <= 0)
419
    return formula::tt();
420

421
422
  formula result = nullptr;
  formula p = formula::ap(name);
423
424
425
  for (; n > 0; --n)
    {
      if (result)
426
427
428
429
        {
          p = X_(p);
          result = And_(result, p);
        }
430
      else
431
432
433
        {
          result = p;
        }
434
435
436
437
    }
  return result;
}

438
static formula
439
440
441
442
443
444
445
446
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
447
static formula
448
449
450
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
451
    return conj ? formula::tt() : formula::ff();
452

453
  formula result = nullptr;
454

455
  op o = conj ? op::And : op::Or;
456
457
458
459
460

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

      if (result)
464
        result = formula::multop(o, {f, result});
465
      else
466
        result = f;
467
468
469
470
471
472
    }
  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
473
static formula
474
475
476
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
477
    return conj ? formula::tt() : formula::ff();
478

479
  formula result = nullptr;
480

481
  op o = conj ? op::And : op::Or;
482
483
484
485
486

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

      if (result)
490
        result = formula::multop(o, {f, result});
491
      else
492
        result = f;
493
494
495
496
497
498
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
499
500
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
501
502
503
504
{
  if (n <= 0)
    n = 1;

505
  formula result = nullptr;
506
507
508
509
510

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
511
      formula f = formula::ap(p.str());
512
      if (!result)
513
        result = f;
514
      else if (right_assoc)
515
        result = formula::binop(o, f, result);
516
      else
517
        result = formula::binop(o, result, f);
518
519
520
521
522
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
523
static formula
524
525
526
R_n(std::string name, int n)
{
  if (n <= 0)
527
    return formula::tt();
528

529
  formula pi;
530
531
532
533

  {
    std::ostringstream p;
    p << name << 1;
534
    pi = formula::ap(p.str());
535
536
  }

537
  formula result = nullptr;
538
539
540

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

546
      formula fg = F_(G_(pi));
547

548
      formula f = Or_(gf, fg);
549
550

      if (result)
551
        result = And_(f, result);
552
      else
553
        result = f;
554
555
556
557
558
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
559
static formula
560
561
562
Q_n(std::string name, int n)
{
  if (n <= 0)
563
    return formula::tt();
564

565
  formula pi;
566
567
568
569

  {
    std::ostringstream p;
    p << name << 1;
570
    pi = formula::ap(p.str());
571
572
  }

573
  formula result = nullptr;
574
575
576

  for (int i = 1; i <= n; ++i)
    {
577
      formula f = F_(pi);
578
579
580

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

583
      formula g = G_(pi);
584
585
586
587

      f = Or_(f, g);

      if (result)
588
        result = And_(f, result);
589
      else
590
        result = f;
591
592
593
594
595
596
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
597
598
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
599
600
{
  if (n <= 0)
601
    return conj ? formula::tt() : formula::ff();
602

603
  formula result = nullptr;
604

605
  op cop = conj ? op::And : op::Or;
606
607
608
609
610

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

      if (result)
614
        result = formula::multop(cop, {f, result});
615
      else
616
        result = f;
617
618
619
620
621
622
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
623
static formula
624
625
fair_response(std::string p, std::string q, std::string r, int n)
{
626
627
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
628
629
630
631
632
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
633
634
static formula
X_n(formula p, int n)
635
636
{
  assert(n >= 0);
637
  formula res = p;
638
639
640
641
642
643
644
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
645
static formula
646
647
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
648
649
650
651
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
652

653
  std::vector<formula> res(4);
654
655
656
657
658
659

  // 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]
660
      std::vector<formula> v(n);
661
      for (int i = 0; i + 1 < n; ++i)
662
        v[i] = X_n(neg_m, i + 1);
663
664
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
665
666
667
668
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
669
      formula p = m;
670
      for (int i = n - 1; i > 0; --i)
671
        p = And_(neg_m, X_(p));
672
      res[0] = And_(m, G_(Implies_(m, X_(p))));
673
674
675
676
677
678
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
679
      std::vector<formula> v2(n);
680
      for (int i = 0; i < n; ++i)
681
        v2[i] = X_n(neg_b, i);
682
      res[1] = formula::And(std::move(v2));
683
684
685
686
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
687
      formula p = neg_b;
688
      for (int i = n - 1; i > 0; --i)
689
        p = And_(neg_b, X_(p));
690
      res[1] = p;
691
692
693
694
695
696
    }

#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.
697
698
699
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
700
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
701
702
703

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
704
705
706
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
707
708
709
710
711
712
713
                       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))))))));
714
  return formula::And(std::move(res));
715
716
}

717
static formula
718
ltl_counter_carry(std::string bit, std::string marker,
719
                  std::string carry, int n, bool linear)
720
{
721
722
723
724
725
726
  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);
727

728
  std::vector<formula> res(6);
729
730
731
732
733
734

  // 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]
735
      std::vector<formula> v(n);
736
      for (int i = 0; i + 1 < n; ++i)
737
        v[i] = X_n(neg_m, i + 1);
738
739
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
740
741
742
743
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
744
      formula p = m;
745
      for (int i = n - 1; i > 0; --i)
746
        p = And_(neg_m, X_(p));
747
      res[0] = And_(m, G_(Implies_(m, X_(p))));
748
749
750
751
752
753
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
754
      std::vector<formula> v2(n);
755
      for (int i = 0; i < n; ++i)
756
        v2[i] = X_n(neg_b, i);
757
      res[1] = formula::And(std::move(v2));
758
759
760
761
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
762
      formula p = neg_b;
763
      for (int i = n - 1; i > 0; --i)
764
        p = And_(neg_b, X_(p));
765
      res[1] = p;
766
767
    }

768
769
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
770
771

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
775
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
776
777
778
779

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
785
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
786
787
788
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
789
790
791
792
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
793
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
794
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
795
796
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
797
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
798
                                      Implies_(b, And_(c, Xn_negb))))));
799
    }
800
  return formula::And(std::move(res));
801
802
}

803
804
805
806
807
808
809
810
811
812
813
814
815
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
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);
}
959
960
961
962

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

1040
1041
  // Make sure we use only "p42"-style of atomic propositions
  // in lbt's output.
1042
1043
  if (output_format == lbt_output && !f.has_lbt_atomic_props())
    f = relabel(f, Pnn);
1044

1045
  output_formula_checked(f, class_name[pattern - 1], n);
1046
1047
1048
1049
1050
}

static void
run_jobs()
{
1051
  for (auto& j: jobs)
1052
    {
1053
1054
      int inc = (j.range.max < j.range.min) ? -1 : 1;
      int n = j.range.min;
1055
      for (;;)
1056
1057
1058
1059
1060
1061
        {
          output_pattern(j.pattern, n);
          if (n == j.range.max)
            break;
          n += inc;
        }
1062
1063
1064
1065
1066
1067
1068
    }
}


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

1071
  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
1072
                    children, nullptr, nullptr };
1073

1074
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
1075
1076
1077
1078
    exit(err);

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

1081
1082
1083
1084
1085
1086
1087
1088
1089
  try
    {
      run_jobs();
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }

1090
1091
  return 0;
}