genltl.cc 43.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2015, 2016, 2017 Laboratoire de Recherche et
3
// 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
//
// @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}
// }
122
123
124
125
126
127
128
129
130
131
132
133
134
//
// @InProceedings{kupferman.10.mochart,
//   author = {Orna Kupferman and And Rosenberg},
//   title = {The Blow-Up in Translating LTL do Deterministic Automata},
//   booktitle = {Proceedings of the 6th International Workshop on Model
//                Checking and Artificial Intelligence (MoChArt 2010)},
//   pages = {85--94},
//   year = 2011,
//   volume = {6572},
//   series = {Lecture Notes in Artificial Intelligence},
//   month = nov,
//   publisher = {Springer}
// }
135
136
137
138
139
140
141
142
143
144
//
// @techreport{holevek.04.tr,
//    title = {Verification Results in {Liberouter} Project},
//    author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak
//              and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek},
//    month = {September},
//    year = 2004,
//    number = 03,
//    institution = {CESNET}
// }
145

146

147
#include "common_sys.hh"
148
149
150
151
152
153
154
155

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

156
#include "common_setup.hh"
157
#include "common_output.hh"
158
#include "common_range.hh"
159
#include "common_cout.hh"
160
161
162
163
164
165

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
166
#include <cmath>
167
168
#include <cstdlib>
#include <cstring>
169
170
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
171
#include <spot/tl/parse.hh>
172
#include <spot/tl/exclusive.hh>
173
174
175
176

using namespace spot;

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

179
enum {
180
181
  FIRST_CLASS = 256,
  OPT_AND_F = FIRST_CLASS,
182
183
184
185
186
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
187
188
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
189
190
191
  OPT_GH_Q,
  OPT_GH_R,
  OPT_GO_THETA,
192
  OPT_HKRSS_PATTERNS,
193
194
  OPT_KR_N,
  OPT_KR_NLOGN,
195
  OPT_KV_PSI,
196
197
198
199
200
201
202
203
204
  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,
205
  OPT_SB_PATTERNS,
206
207
208
209
210
  OPT_TV_F1,
  OPT_TV_F2,
  OPT_TV_G1,
  OPT_TV_G2,
  OPT_TV_UU,
211
212
213
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
214
215
  OPT_POSITIVE,
  OPT_NEGATIVE,
216
};
217

218
const char* const class_name[LAST_CLASS - FIRST_CLASS] =
219
220
221
222
223
224
225
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
226
227
    "dac-patterns",
    "eh-patterns",
228
229
230
    "gh-q",
    "gh-r",
    "go-theta",
231
    "hkrss-patterns",
232
233
    "kr-n",
    "kr-nlogn",
234
    "kv-psi",
235
236
237
238
239
240
241
242
243
    "or-fg",
    "or-g",
    "or-gf",
    "or-r-left",
    "or-r-right",
    "rv-counter",
    "rv-counter-carry",
    "rv-counter-carry-linear",
    "rv-counter-linear",
244
    "sb-patterns",
245
246
247
248
249
    "tv-f1",
    "tv-f2",
    "tv-g1",
    "tv-g2",
    "tv-uu",
250
251
252
253
    "u-left",
    "u-right",
  };

254

255
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
256
257
258
259
260

static const argp_option options[] =
  {
    /**************************************************/
    // Keep this alphabetically sorted (expect for aliases).
261
    { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
262
263
264
265
266
267
268
269
270
271
272
273
274
275
    // 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 },
276
277
    { "dac-patterns", OPT_DAC_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Dwyer et al. [FMSP'98] Spec. Patterns for LTL "
278
      "(range should be included in 1..55)", 0 },
279
    OPT_ALIAS(spec-patterns),
280
281
282
    { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Etessami and Holzmann [Concur'00] patterns "
      "(range should be included in 1..12)", 0 },
283
    { "gh-q", OPT_GH_Q, "RANGE", 0,
284
      "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 },
285
    { "gh-r", OPT_GH_R, "RANGE", 0,
286
      "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0 },
287
288
    { "go-theta", OPT_GO_THETA, "RANGE", 0,
      "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 },
289
290
291
292
    { "hkrss-patterns", OPT_HKRSS_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Holeček et al. patterns from the Liberouter project "
      "(range should be included in 1..55)", 0 },
    OPT_ALIAS(liberouter-patterns),
293
    { "kr-n", OPT_KR_N, "RANGE", 0,
294
      "linear formula with doubly exponential DBA", 0 },
295
    { "kr-nlogn", OPT_KR_NLOGN, "RANGE", 0,
296
      "quasilinear formula with doubly exponential DBA", 0 },
297
    { "kv-psi", OPT_KV_PSI, "RANGE", 0,
298
      "quadratic formula with doubly exponential DBA", 0 },
299
    OPT_ALIAS(kr-n2),
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
    { "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 },
316
317
318
    { "sb-patterns", OPT_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Somenzi and Bloem [CAV'00] patterns "
      "(range should be included in 1..27)", 0 },
319
320
321
322
323
324
    { "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 },
325
326
327
328
329
    { "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),
330
    RANGE_DOC,
331
  /**************************************************/
332
    { nullptr, 0, nullptr, 0, "Output options:", -20 },
333
334
335
336
337
338
    { "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 },
339
    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
340
      "the following interpreted sequences:", -19 },
341
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
342
      "the formula (in the selected syntax)", 0 },
343
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
344
      "the name of the pattern", 0 },
345
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
346
      "the argument of the pattern", 0 },
347
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
348
      "a single %", 0 },
349
    COMMON_LTL_OUTPUT_SPECS,
350
351
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
352
353
354
355
356
  };

struct job
{
  int pattern;
357
  struct range range;
358
359
360
361
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
362
363
bool opt_positive = false;
bool opt_negative = false;
364
365
366

const struct argp_child children[] =
  {
367
368
369
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
370
  };
371
372

static void
373
enqueue_job(int pattern, const char* range_str)
374
375
376
{
  job j;
  j.pattern = pattern;
377
  j.range = parse_range(range_str);
378
379
380
  jobs.push_back(j);
}

381
382
383
384
385
386
387
388
389
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

390
static int
391
parse_opt(int key, char* arg, struct argp_state*)
392
393
394
395
396
397
398
399
400
401
402
403
404
{
  // 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:
405
406
    case OPT_KR_N:
    case OPT_KR_NLOGN:
407
    case OPT_KV_PSI:
408
409
410
411
412
413
414
415
416
    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:
417
418
419
420
421
    case OPT_TV_F1:
    case OPT_TV_F2:
    case OPT_TV_G1:
    case OPT_TV_G2:
    case OPT_TV_UU:
422
423
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
424
425
      enqueue_job(key, arg);
      break;
426
    case OPT_DAC_PATTERNS:
427
    case OPT_HKRSS_PATTERNS:
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
      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;
445
446
447
448
449
450
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
451
452
453
454
455
456
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

457
458
459
460
461
462
463
464
465
466
#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))
467
468

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
469
static formula
470
471
472
E_n(std::string name, int n)
{
  if (n <= 0)
473
    return formula::tt();
474

475
  formula result = nullptr;
476
477
478
479
480

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
481
      formula f = formula::ap(p.str());
482
      if (result)
483
        result = And_(f, result);
484
      else
485
        result = f;
486
487
488
489
490
491
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
492
static formula
493
494
phi_n(std::string name, int n,
      op oper = op::And)
495
496
{
  if (n <= 0)
497
    return formula::tt();
498

499
500
  formula result = nullptr;
  formula p = formula::ap(name);
501
502
503
  for (; n > 0; --n)
    {
      if (result)
504
        result = formula::multop(oper, {p, X_(result)});
505
      else
506
        result = p;
507
508
509
510
    }
  return result;
}

511
512
static formula
N_n(std::string name, int n)
513
{
514
  return formula::F(phi_n(name, n));
515
516
517
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
518
static formula
519
520
phi_prime_n(std::string name, int n,
            op oper = op::And)
521
522
{
  if (n <= 0)
523
    return formula::tt();
524

525
526
  formula result = nullptr;
  formula p = formula::ap(name);
527
528
529
  for (; n > 0; --n)
    {
      if (result)
530
531
        {
          p = X_(p);
532
          result = formula::multop(oper, {result, p});
533
        }
534
      else
535
536
537
        {
          result = p;
        }
538
539
540
541
    }
  return result;
}

542
static formula
543
544
545
546
547
548
549
550
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
551
static formula
552
553
554
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
555
    return conj ? formula::tt() : formula::ff();
556

557
  formula result = nullptr;
558

559
  op o = conj ? op::And : op::Or;
560
561
562
563
564

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

      if (result)
568
        result = formula::multop(o, {f, result});
569
      else
570
        result = f;
571
572
573
574
575
576
    }
  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
577
static formula
578
579
580
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
581
    return conj ? formula::tt() : formula::ff();
582

583
  formula result = nullptr;
584

585
  op o = conj ? op::And : op::Or;
586
587
588
589
590

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

      if (result)
594
        result = formula::multop(o, {f, result});
595
      else
596
        result = f;
597
598
599
600
601
602
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
603
604
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
605
606
607
608
{
  if (n <= 0)
    n = 1;

609
  formula result = nullptr;
610
611
612
613
614

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
615
      formula f = formula::ap(p.str());
616
      if (!result)
617
        result = f;
618
      else if (right_assoc)
619
        result = formula::binop(o, f, result);
620
      else
621
        result = formula::binop(o, result, f);
622
623
624
625
626
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
627
static formula
628
629
630
R_n(std::string name, int n)
{
  if (n <= 0)
631
    return formula::tt();
632

633
  formula pi;
634
635
636
637

  {
    std::ostringstream p;
    p << name << 1;
638
    pi = formula::ap(p.str());
639
640
  }

641
  formula result = nullptr;
642
643
644

  for (int i = 1; i <= n; ++i)
    {
645
      formula gf = G_(F_(pi));
646
647
      std::ostringstream p;
      p << name << i + 1;
648
      pi = formula::ap(p.str());
649

650
      formula fg = F_(G_(pi));
651

652
      formula f = Or_(gf, fg);
653
654

      if (result)
655
        result = And_(f, result);
656
      else
657
        result = f;
658
659
660
661
662
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
663
static formula
664
665
666
Q_n(std::string name, int n)
{
  if (n <= 0)
667
    return formula::tt();
668

669
  formula pi;
670
671
672
673

  {
    std::ostringstream p;
    p << name << 1;
674
    pi = formula::ap(p.str());
675
676
  }

677
  formula result = nullptr;
678
679
680

  for (int i = 1; i <= n; ++i)
    {
681
      formula f = F_(pi);
682
683
684

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

687
      formula g = G_(pi);
688
689
690
691

      f = Or_(f, g);

      if (result)
692
        result = And_(f, result);
693
      else
694
        result = f;
695
696
697
698
699
700
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
701
702
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
703
704
{
  if (n <= 0)
705
    return conj ? formula::tt() : formula::ff();
706

707
  formula result = nullptr;
708

709
  op cop = conj ? op::And : op::Or;
710
711
712
713
714

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

      if (result)
718
        result = formula::multop(cop, {f, result});
719
      else
720
        result = f;
721
722
723
724
725
726
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
727
static formula
728
729
fair_response(std::string p, std::string q, std::string r, int n)
{
730
731
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
732
733
734
735
736
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
737
738
static formula
X_n(formula p, int n)
739
740
{
  assert(n >= 0);
741
  formula res = p;
742
743
744
745
746
747
748
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
749
static formula
750
751
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
752
753
754
755
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
756

757
  std::vector<formula> res(4);
758
759
760
761
762
763

  // 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]
764
      std::vector<formula> v(n);
765
      for (int i = 0; i + 1 < n; ++i)
766
        v[i] = X_n(neg_m, i + 1);
767
768
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
769
770
771
772
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
773
      formula p = m;
774
      for (int i = n - 1; i > 0; --i)
775
        p = And_(neg_m, X_(p));
776
      res[0] = And_(m, G_(Implies_(m, X_(p))));
777
778
779
780
781
782
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
783
      std::vector<formula> v2(n);
784
      for (int i = 0; i < n; ++i)
785
        v2[i] = X_n(neg_b, i);
786
      res[1] = formula::And(std::move(v2));
787
788
789
790
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
791
      formula p = neg_b;
792
      for (int i = n - 1; i > 0; --i)
793
        p = And_(neg_b, X_(p));
794
      res[1] = p;
795
796
797
798
799
800
    }

#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.
801
802
803
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
804
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
805
806
807

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
808
809
810
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
811
812
813
814
815
816
817
                       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))))))));
818
  return formula::And(std::move(res));
819
820
}

821
static formula
822
ltl_counter_carry(std::string bit, std::string marker,
823
                  std::string carry, int n, bool linear)
824
{
825
826
827
828
829
830
  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);
831

832
  std::vector<formula> res(6);
833
834
835
836
837
838

  // 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]
839
      std::vector<formula> v(n);
840
      for (int i = 0; i + 1 < n; ++i)
841
        v[i] = X_n(neg_m, i + 1);
842
843
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
844
845
846
847
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
848
      formula p = m;
849
      for (int i = n - 1; i > 0; --i)
850
        p = And_(neg_m, X_(p));
851
      res[0] = And_(m, G_(Implies_(m, X_(p))));
852
853
854
855
856
857
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
858
      std::vector<formula> v2(n);
859
      for (int i = 0; i < n; ++i)
860
        v2[i] = X_n(neg_b, i);
861
      res[1] = formula::And(std::move(v2));
862
863
864
865
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
866
      formula p = neg_b;
867
      for (int i = n - 1; i > 0; --i)
868
        p = And_(neg_b, X_(p));
869
      res[1] = p;
870
871
    }

872
873
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
874
875

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
879
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
880
881
882
883

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
889
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
890
891
892
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
893
894
895
896
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
897
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
898
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
899
900
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
901
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
902
                                      Implies_(b, And_(c, Xn_negb))))));
903
    }
904
  return formula::And(std::move(res));
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
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));
}

951
952
static void
bad_number(const char* pattern, int n, int max = 0)
953
954
955
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
956
957
958
      << ", supported range is 1..";
  if (max)
    err << max;
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
  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);
}

1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
static formula
hkrss_pattern(int n)
{
  static const char* formulas[] = {
    "G(Fp0 & F!p0)",
    "GFp0 & GF!p0",
    "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0))",
    "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3))",
    "G!p0",
    "G((p0 -> F!p0) & (!p0 -> Fp0))",
    "G(p0 -> F(p0 & p1))",
    "G(p0 -> F((!p0 & p1 & p2 & p3) -> Fp4))",
    "G(p0 -> F!p1)",
    "G(p0 -> Fp1)",
    "G(p0 -> F(p1 -> Fp2))",
    "G(p0 -> F((p1 & p2) -> Fp3))",
    "G((p0 -> Fp1) & (p2 -> Fp3) & (p4 -> Fp5) & (p6 -> Fp7))",
    "G(!p0 & !p1)",
    "G!(p0 & p1)",
    "G(p0 -> p1)",
    "G((p0 -> !p1) & (p1 -> !p0))",
    "G(!p0 -> (p1 <-> !p2))",
    "G((!p0 & (p1 | p2 | p3)) -> p4)",
    "G((p0 & p1) -> (p2 | !(p3 & p4)))",
    "G((!p0 & p1 & !p2 & !p3 & !p4) -> F(!p5 & !p6 & !p7 & !p8))",
    "G((p0 & p1 & !p2 & !p3 & !p4) -> F(p5 & !p6 & !p7 & !p8))",
    "G(!p0 -> !(p1 & p2 & p3 & p4 & p5))",
    "G(!p0 -> ((p1 & p2 & p3 & p4) -> !p5))",
    "G((p0 & p1) -> (p2 | p3 | !(p4 & p5)))",
    "G((!p0 & (p1 | p2 | p3 | p4)) -> (!p5 <-> p6))",
    "G((p0 & p1) -> (p2 | p3 | p4 | !(p5 & p6)))",
    "G((p0 & p1) -> (p2 | p3 | p4 | p5 | !(p6 & p7)))",
    "G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))",
    "G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3))))))",
    "G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3)))))",
    "G(p0 -> (p1 U (!p1 U (!p2 | p3))))",
    "G(p0 -> (p1 U (!p1 U (p2 | p3))))",
    "G((!p0 & p1) -> Xp2)",
    "G(p0 -> X(p0 | p1))",
    ("G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) -> "
     "(X!p4 & X(!(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | "
     "!(p3 <-> Xp3)) U p4)))"),
    "G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))",
    "G(p0 -> X(!p0 U p1))",
    "G((!p0 & Xp0) -> X((p0 U p1) | Gp0))",
    "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))",
    ("G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 & (p0 U (p0 & !p1 & "
     "X(p0 & p1)))))))"),
    ("G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 "
     "& X(!p0 & p1)))))))"),
    ("G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & "
     "X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1))))))))))"),
    "G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))",
    ("G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | "
     "X(!p0 | X(!p0 | X!p0)))))))))))"),
    "G((Xp0 -> p0) -> (p1 <-> Xp1))",
    "G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))",
    ("!p0 U G!((p1 & p2) | (p3 & p4) | (p2 & p3) | (p2 & p4) | (p1 & p4) | "
     "(p1 & p3))"),
    "!p0 U p1",
    "(p0 U p1) | Gp0",
    "p0 & XG!p0",
    "XG(p0 -> (G!p1 | (!Xp1 U p2)))",
    "XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))",
    "XG((p0 & p1) -> ((p1 U p2) | Gp1))",
    "Xp0 & G((!p0 & Xp0) -> XXp0)",
  };

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

1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
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);
}
1184

1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
static formula
X_n_kv_exp(formula a, int n, formula b)
{
  formula f = X_n(a, n);
  return And_(f, G_(Implies_(b, f)));
}

static formula
kv_exp(int n, std::string a, std::string b, std::string c, std::string d)
{
  formula fa = formula::ap(a);
  formula fb = formula::ap(b);
  formula fc = formula::ap(c);
  formula fd = formula::ap(d);

  exclusive_ap m;
  m.add_group({ fa, fb, fc, fd });

  formula xn = X_(G_(fc));
  for (int i = 0; i < n; i++)
    xn = X_(And_(Or_(fa, fb), xn));
  formula f1 = U_(Not_(fd), And_(fd, xn));

  formula f_and = nullptr;
  for (int i = 1; i <= n; i++)
    f_and = And_(f_and, Or_(X_n_kv_exp(fa, i, fd), X_n_kv_exp(fb, i, fd)));

  formula f2 = F_(And_(fc, And_(f_and, X_n(fc, n + 1))));

  return m.constrain(And_(f1, f2));
}

static formula
bit_ni(unsigned i, unsigned j, formula fbin[2])
{
  return fbin[((1u << j) & (i - 1)) != 0];
}

static formula
binary_ki(int k, unsigned i, formula fbin[2])
{
  formula res = bit_ni(i, k - 1, fbin);
  for (int j = k - 1; j >= 1; j--)
    res = And_(bit_ni(i, j - 1, fbin), X_(res));
  return res;
}

static formula
kr1_exp_1(int k, formula fc, formula fd, formula fbin[2])
{
    return And_(fc, X_(Or_(binary_ki(k, 1, fbin), fd)));
}

static formula
kr1_exp_2(int n, int k, formula fa, formula fb, formula fbin[2])
{
  formula res = formula::tt();
  for (int i = 1; i <= n - 1; i++)
    res = And_(res,
               Implies_(binary_ki(k, i, fbin),
                        X_n(And_(Or_(fa, fb),
                            X_(binary_ki(k, i + 1, fbin))), k)));

  return G_(res);
}

static formula
kr1_exp_3(int n, int k, formula fa, formula fb, formula fc, formula fd,
          formula fbin[2])
{
  return G_(Implies_(binary_ki(k, n, fbin),
                     X_n(And_(Or_(fa, fb),
                              X_(And_(fc,
                                      X_(Or_(binary_ki(k, 1, fbin),
                                             Or_(fd,
                                                 G_(fc))))))), k)));
}

static formula
kr1_exp_4(int n, int k, formula fc, formula fd, formula fbin[2])
{
  return U_(Not_(fd),
            And_(fd,
                 X_(And_(binary_ki(k, 1, fbin), X_n(G_(fc),  n * (k + 1))))));
}

static formula
kr1_exp_5_r(int k, int i, formula fr, formula fd, formula fbin[2])
{
  return And_(fr, F_(And_(fd, F_(And_(binary_ki(k, i, fbin), X_n(fr, k))))));
}

static formula
kr1_exp_5(int n, int k, formula fa, formula fb, formula fc, formula fd,
          formula fbin[2])
{
  formula fand = formula::tt();
  for (int i = 1; i <= n; i++)
    {
      formula for1 = kr1_exp_5_r(k, i, fa, fd, fbin);
      formula for2 = kr1_exp_5_r(k, i, fb, fd, fbin);
      fand = And_(fand, Implies_(binary_ki(k, i, fbin), X_n(Or_(for1,
                  for2), k)));
    }

    return F_(And_(fc,
                   X_(And_(Not_(fc),
                           U_(fand, fc)))));
}

static formula
kr1_exp(int n, std::string a, std::string b, std::string c, std::string d,
        std::string bin0, std::string bin1)
{
  int k = ceil(log2(n)) + (n == 1);

  if (n <= 0)
    bad_number("--kr1-exp", n);

  formula fa = formula::ap(a);
  formula fb = formula::ap(b);
  formula fc = formula::ap(c);
  formula fd = formula::ap(d);

  formula fbin0 = formula::ap(bin0);
  formula fbin1 = formula::ap(bin1);

  exclusive_ap m;
  m.add_group({ fa, fb, fc, fd, fbin0, fbin1 });

  formula fbin[2] = { fbin0, fbin1 };

  formula res = formula::And({ kr1_exp_1(k, fc, fd, fbin),
                               kr1_exp_2(n, k, fa, fb, fbin),
                               kr1_exp_3(n, k, fa, fb, fc, fd, fbin),
                               kr1_exp_4(n, k, fc, fd, fbin),
                               kr1_exp_5(n, k, fa, fb, fc, fd, fbin) });

  return m.constrain(res);
}

static formula
kr2_exp_1(formula* fa, formula* fb, formula fc, formula fd)
{
  (void) fd;
  return And_(fc,
              X_(Or_(fa[0],
                 Or_(fb[0], fd))));
}

static formula
kr2_exp_2(int n, formula* fa, formula* fb)
{
  formula res = formula::tt();
  for (int i = 1; i <= n - 1; i++)
    res = And_(res, Implies_(Or_(fa[i - 1], fb[i - 1]),
          X_(Or_(fa[i], fb[i]))));

  return G_(res);
}

static formula
kr2_exp_3(int n, formula* fa, formula* fb, formula fc, formula fd)
{
  return G_(Implies_(Or_(fa[n - 1], fb[n - 1]),
                     X_(And_(fc,
                             X_(Or_(fa[0],
                                    Or_(fb[0],
                                        Or_(fd, G_(fc)))))))));
}

static formula
kr2_exp_4(int n, formula* fa, formula* fb, formula fc, formula fd)
{
  return U_(Not_(fd), And_(fd, X_(And_(Or_(fa[0], fb[0]), X_n(G_(fc), n)))));
}

static formula
kr2_exp_5_r(int i, formula* fr, formula fd)
{
  return And_(fr[i - 1], F_(And_(fd, F_(fr[i - 1]))));
}

static formula
kr2_exp_5(int n, formula* fa, formula* fb, formula fc, formula fd)
{
  formula facc = formula::ff();
  for (int i = 1; i <= n; i++)
    {
      formula for1 = kr2_exp_5_r(i, fa, fd);
      formula for2 = kr2_exp_5_r(i, fb, fd);
      facc = Or_(facc, (Or_(for1, for2)));
    }

  return F_(And_(fc,
                 X_(And_(Not_(fc), U_(facc, fc)))));
}

static formula
kr2_exp_mutex(int n, formula* fa, formula* fb, formula fc, formula fd)
{
  formula f1or = formula::ff();
  formula f3and = formula::tt();

  for (int i = 1; i <= n; i++)
    {
      f1or = Or_(f1or, Or_(fa[i - 1], fb[i - 1]));
      f3and = And_(f3and, Implies_(fa[i - 1], Not_(fb[i - 1])));
    }

  formula f1 = G_(Implies_(Or_(fc, fd), Not_(f1or)));
  formula f2 = G_(Implies_(fc, Not_(fd)));
  formula f3 = G_(f3and);

  return And_(f1, And_(f2, f3));
}

static formula
kr2_exp(int n, std::string a, std::string b, std::string c, std::string d)
{
  if (n <= 0)
    bad_number("--kr-n", n);

  form