genltl.cc 45.6 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
148
149
150
151
152
153
154
155
156
157
//
// @InProceedings{pelanek.07.spin,
//   author = {Radek Pel\'{a}nek},
//   title = {{BEEM}: benchmarks for explicit model checkers},
//   booktitle = {Proceedings of the 14th international SPIN conference on
//     Model checking software},
//   year = 2007,
//   pages = {263--267},
//   numpages = {5},
//   volume = {4595},
//   series = {Lecture Notes in Computer Science},
//   publisher = {Springer-Verlag}
// }
158

159

160
#include "common_sys.hh"
161
162
163
164
165
166
167
168

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

169
#include "common_setup.hh"
170
#include "common_output.hh"
171
#include "common_range.hh"
172
#include "common_cout.hh"
173
174
175
176
177
178

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
179
#include <cmath>
180
181
#include <cstdlib>
#include <cstring>
182
183
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
184
#include <spot/tl/parse.hh>
185
#include <spot/tl/exclusive.hh>
186
187
188
189

using namespace spot;

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

192
enum {
193
194
  FIRST_CLASS = 256,
  OPT_AND_F = FIRST_CLASS,
195
196
197
198
199
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
200
201
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
202
203
204
  OPT_GH_Q,
  OPT_GH_R,
  OPT_GO_THETA,
205
  OPT_HKRSS_PATTERNS,
206
207
  OPT_KR_N,
  OPT_KR_NLOGN,
208
  OPT_KV_PSI,
209
210
211
  OPT_OR_FG,
  OPT_OR_G,
  OPT_OR_GF,
212
  OPT_P_PATTERNS,
213
214
215
216
217
218
  OPT_R_LEFT,
  OPT_R_RIGHT,
  OPT_RV_COUNTER,
  OPT_RV_COUNTER_CARRY,
  OPT_RV_COUNTER_CARRY_LINEAR,
  OPT_RV_COUNTER_LINEAR,
219
  OPT_SB_PATTERNS,
220
221
222
223
224
  OPT_TV_F1,
  OPT_TV_F2,
  OPT_TV_G1,
  OPT_TV_G2,
  OPT_TV_UU,
225
226
227
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
228
229
  OPT_POSITIVE,
  OPT_NEGATIVE,
230
};
231

232
const char* const class_name[LAST_CLASS - FIRST_CLASS] =
233
234
235
236
237
238
239
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
240
241
    "dac-patterns",
    "eh-patterns",
242
243
244
    "gh-q",
    "gh-r",
    "go-theta",
245
    "hkrss-patterns",
246
247
    "kr-n",
    "kr-nlogn",
248
    "kv-psi",
249
250
251
    "or-fg",
    "or-g",
    "or-gf",
252
    "p-patterns",
253
254
    "r-left",
    "r-right",
255
256
257
258
    "rv-counter",
    "rv-counter-carry",
    "rv-counter-carry-linear",
    "rv-counter-linear",
259
    "sb-patterns",
260
261
262
263
264
    "tv-f1",
    "tv-f2",
    "tv-g1",
    "tv-g2",
    "tv-uu",
265
266
267
268
    "u-left",
    "u-right",
  };

269

270
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
271
272
273
274
275

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

struct job
{
  int pattern;
377
  struct range range;
378
379
380
381
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
382
383
bool opt_positive = false;
bool opt_negative = false;
384
385
386

const struct argp_child children[] =
  {
387
388
389
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
390
  };
391
392

static void
393
enqueue_job(int pattern, const char* range_str)
394
395
396
{
  job j;
  j.pattern = pattern;
397
  j.range = parse_range(range_str);
398
399
400
  jobs.push_back(j);
}

401
402
403
404
405
406
407
408
409
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

410
static int
411
parse_opt(int key, char* arg, struct argp_state*)
412
413
414
415
416
417
418
419
420
421
422
423
424
{
  // 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:
425
426
    case OPT_KR_N:
    case OPT_KR_NLOGN:
427
    case OPT_KV_PSI:
428
429
430
431
432
433
434
435
436
    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:
437
438
439
440
441
    case OPT_TV_F1:
    case OPT_TV_F2:
    case OPT_TV_G1:
    case OPT_TV_G2:
    case OPT_TV_UU:
442
443
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
444
445
      enqueue_job(key, arg);
      break;
446
    case OPT_DAC_PATTERNS:
447
    case OPT_HKRSS_PATTERNS:
448
449
450
451
452
453
454
455
456
457
458
      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;
459
460
461
462
463
464
    case OPT_P_PATTERNS:
      if (arg)
        enqueue_job(key, arg);
      else
        enqueue_job(key, 1, 20);
      break;
465
466
467
468
469
470
    case OPT_SB_PATTERNS:
      if (arg)
        enqueue_job(key, arg);
      else
        enqueue_job(key, 1, 27);
      break;
471
472
473
474
475
476
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
477
478
479
480
481
482
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

483
484
485
486
487
488
489
490
491
492
#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))
493
494

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
495
static formula
496
497
498
E_n(std::string name, int n)
{
  if (n <= 0)
499
    return formula::tt();
500

501
  formula result = nullptr;
502
503
504
505
506

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
507
      formula f = formula::ap(p.str());
508
      if (result)
509
        result = And_(f, result);
510
      else
511
        result = f;
512
513
514
515
516
517
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
518
static formula
519
520
phi_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
        result = formula::multop(oper, {p, X_(result)});
531
      else
532
        result = p;
533
534
535
536
    }
  return result;
}

537
538
static formula
N_n(std::string name, int n)
539
{
540
  return formula::F(phi_n(name, n));
541
542
543
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
544
static formula
545
546
phi_prime_n(std::string name, int n,
            op oper = op::And)
547
548
{
  if (n <= 0)
549
    return formula::tt();
550

551
552
  formula result = nullptr;
  formula p = formula::ap(name);
553
554
555
  for (; n > 0; --n)
    {
      if (result)
556
557
        {
          p = X_(p);
558
          result = formula::multop(oper, {result, p});
559
        }
560
      else
561
562
563
        {
          result = p;
        }
564
565
566
567
    }
  return result;
}

568
static formula
569
570
571
572
573
574
575
576
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
577
static formula
578
579
580
GF_n(std::string name, int n, bool conj = true)
{
  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 = G_(F_(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;
}

// FG(p_1) | FG(p_2) | ... | FG(p_n)   if conj == false
// FG(p_1) & FG(p_2) & ... & FG(p_n)   if conj == true
603
static formula
604
605
606
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
607
    return conj ? formula::tt() : formula::ff();
608

609
  formula result = nullptr;
610

611
  op o = conj ? op::And : op::Or;
612
613
614
615
616

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

      if (result)
620
        result = formula::multop(o, {f, result});
621
      else
622
        result = f;
623
624
625
626
627
628
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
629
630
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
631
632
633
634
{
  if (n <= 0)
    n = 1;

635
  formula result = nullptr;
636
637
638
639
640

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
641
      formula f = formula::ap(p.str());
642
      if (!result)
643
        result = f;
644
      else if (right_assoc)
645
        result = formula::binop(o, f, result);
646
      else
647
        result = formula::binop(o, result, f);
648
649
650
651
652
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
653
static formula
654
655
656
R_n(std::string name, int n)
{
  if (n <= 0)
657
    return formula::tt();
658

659
  formula pi;
660
661
662
663

  {
    std::ostringstream p;
    p << name << 1;
664
    pi = formula::ap(p.str());
665
666
  }

667
  formula result = nullptr;
668
669
670

  for (int i = 1; i <= n; ++i)
    {
671
      formula gf = G_(F_(pi));
672
673
      std::ostringstream p;
      p << name << i + 1;
674
      pi = formula::ap(p.str());
675

676
      formula fg = F_(G_(pi));
677

678
      formula f = Or_(gf, fg);
679
680

      if (result)
681
        result = And_(f, result);
682
      else
683
        result = f;
684
685
686
687
688
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
689
static formula
690
691
692
Q_n(std::string name, int n)
{
  if (n <= 0)
693
    return formula::tt();
694

695
  formula pi;
696
697
698
699

  {
    std::ostringstream p;
    p << name << 1;
700
    pi = formula::ap(p.str());
701
702
  }

703
  formula result = nullptr;
704
705
706

  for (int i = 1; i <= n; ++i)
    {
707
      formula f = F_(pi);
708
709
710

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

713
      formula g = G_(pi);
714
715
716
717

      f = Or_(f, g);

      if (result)
718
        result = And_(f, result);
719
      else
720
        result = f;
721
722
723
724
725
726
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
727
728
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
729
730
{
  if (n <= 0)
731
    return conj ? formula::tt() : formula::ff();
732

733
  formula result = nullptr;
734

735
  op cop = conj ? op::And : op::Or;
736
737
738
739
740

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

      if (result)
744
        result = formula::multop(cop, {f, result});
745
      else
746
        result = f;
747
748
749
750
751
752
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
753
static formula
754
755
fair_response(std::string p, std::string q, std::string r, int n)
{
756
757
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
758
759
760
761
762
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
763
764
static formula
X_n(formula p, int n)
765
766
{
  assert(n >= 0);
767
  formula res = p;
768
769
770
771
772
773
774
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
775
static formula
776
777
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
778
779
780
781
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
782

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

  // 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]
790
      std::vector<formula> v(n);
791
      for (int i = 0; i + 1 < n; ++i)
792
        v[i] = X_n(neg_m, i + 1);
793
794
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
795
796
797
798
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
799
      formula p = m;
800
      for (int i = n - 1; i > 0; --i)
801
        p = And_(neg_m, X_(p));
802
      res[0] = And_(m, G_(Implies_(m, X_(p))));
803
804
805
806
807
808
    }

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

#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.
827
828
829
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
830
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
831
832
833

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
834
835
836
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
837
838
839
840
841
842
843
                       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))))))));
844
  return formula::And(std::move(res));
845
846
}

847
static formula
848
ltl_counter_carry(std::string bit, std::string marker,
849
                  std::string carry, int n, bool linear)
850
{
851
852
853
854
855
856
  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);
857

858
  std::vector<formula> res(6);
859
860
861
862
863
864

  // 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]
865
      std::vector<formula> v(n);
866
      for (int i = 0; i + 1 < n; ++i)
867
        v[i] = X_n(neg_m, i + 1);
868
869
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
870
871
872
873
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
874
      formula p = m;
875
      for (int i = n - 1; i > 0; --i)
876
        p = And_(neg_m, X_(p));
877
      res[0] = And_(m, G_(Implies_(m, X_(p))));
878
879
880
881
882
883
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
884
      std::vector<formula> v2(n);
885
      for (int i = 0; i < n; ++i)
886
        v2[i] = X_n(neg_b, i);
887
      res[1] = formula::And(std::move(v2));
888
889
890
891
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
892
      formula p = neg_b;
893
      for (int i = n - 1; i > 0; --i)
894
        p = And_(neg_b, X_(p));
895
      res[1] = p;
896
897
    }

898
899
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
900
901

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
905
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
906
907
908
909

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
915
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
916
917
918
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
919
920
921
922
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
923
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
924
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
925
926
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
927
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
928
                                      Implies_(b, And_(c, Xn_negb))))));
929
    }
930
  return formula::And(std::move(res));
931
932
}

933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
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));
}

977
978
static void
bad_number(const char* pattern, int n, int max = 0)
979
980
981
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
982
983
984
      << ", supported range is 1..";
  if (max)
    err << max;
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
  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);
}

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
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
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);
}

1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
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);
}

1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
static formula
p_pattern(int n)
{
  static const char* formulas[] = {
    "G(p0 -> Fp1)",
    "(GFp1 & GFp0) -> GFp2",
    "G(p0 -> (p1 & (p2 U p3)))",
    "F(p0 | p1)",
    "GF(p0 | p1)",
    "(p0 U p1) -> ((p2 U p3) | Gp2)",
    "G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))",
    "G(p0 -> (p1 R !p2))",
    "G(!p0 -> Fp0)",
    "G(p0 -> F(p1 | p2))",
    "!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))",
    "G!p0 -> G!p1",
    "G(p0 -> (G!p1 | (!p2 U p1)))",
    "G(p0 -> (p1 R (p1 | !p2)))",
    "G((p0 & p1) -> (!p1 R (p0 | !p1)))",
    "G(p0 -> F(p1 & p2))",
    "G(p0 -> (!p1 U (p1 U (p1 & p2))))",
    "G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))",
    "GFp0 -> GFp1",
    "GF(p0 | p1) & GF(p1 | p2)",
  };

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

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
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);
}
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
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
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(