genltl.cc 40.3 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
#include "common_sys.hh"
138
139
140
141
142
143
144
145

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

146
#include "common_setup.hh"
147
#include "common_output.hh"
148
#include "common_range.hh"
149
#include "common_cout.hh"
150
151
152
153
154
155

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
156
#include <cmath>
157
158
#include <cstdlib>
#include <cstring>
159
160
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
161
#include <spot/tl/parse.hh>
162
#include <spot/tl/exclusive.hh>
163
164
165
166

using namespace spot;

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

169
enum {
170
171
  FIRST_CLASS = 256,
  OPT_AND_F = FIRST_CLASS,
172
173
174
175
176
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
177
178
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
179
180
181
  OPT_GH_Q,
  OPT_GH_R,
  OPT_GO_THETA,
182
183
  OPT_KR_N,
  OPT_KR_NLOGN,
184
  OPT_KV_PSI,
185
186
187
188
189
190
191
192
193
  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,
194
  OPT_SB_PATTERNS,
195
196
197
198
199
  OPT_TV_F1,
  OPT_TV_F2,
  OPT_TV_G1,
  OPT_TV_G2,
  OPT_TV_UU,
200
201
202
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
203
204
  OPT_POSITIVE,
  OPT_NEGATIVE,
205
};
206

207
const char* const class_name[LAST_CLASS - FIRST_CLASS] =
208
209
210
211
212
213
214
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
215
216
    "dac-patterns",
    "eh-patterns",
217
218
219
    "gh-q",
    "gh-r",
    "go-theta",
220
221
    "kr-n",
    "kr-nlogn",
222
    "kv-psi",
223
224
225
226
227
228
229
230
231
    "or-fg",
    "or-g",
    "or-gf",
    "or-r-left",
    "or-r-right",
    "rv-counter",
    "rv-counter-carry",
    "rv-counter-carry-linear",
    "rv-counter-linear",
232
    "sb-patterns",
233
234
235
236
237
    "tv-f1",
    "tv-f2",
    "tv-g1",
    "tv-g2",
    "tv-uu",
238
239
240
241
    "u-left",
    "u-right",
  };

242

243
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
244
245
246
247
248

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

struct job
{
  int pattern;
341
  struct range range;
342
343
344
345
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
346
347
bool opt_positive = false;
bool opt_negative = false;
348
349
350

const struct argp_child children[] =
  {
351
352
353
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
354
  };
355
356

static void
357
enqueue_job(int pattern, const char* range_str)
358
359
360
{
  job j;
  j.pattern = pattern;
361
  j.range = parse_range(range_str);
362
363
364
  jobs.push_back(j);
}

365
366
367
368
369
370
371
372
373
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

374
static int
375
parse_opt(int key, char* arg, struct argp_state*)
376
377
378
379
380
381
382
383
384
385
386
387
388
{
  // 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:
389
390
    case OPT_KR_N:
    case OPT_KR_NLOGN:
391
    case OPT_KV_PSI:
392
393
394
395
396
397
398
399
400
    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:
401
402
403
404
405
    case OPT_TV_F1:
    case OPT_TV_F2:
    case OPT_TV_G1:
    case OPT_TV_G2:
    case OPT_TV_UU:
406
407
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
408
409
      enqueue_job(key, arg);
      break;
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
    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;
428
429
430
431
432
433
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
434
435
436
437
438
439
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

440
441
442
443
444
445
446
447
448
449
#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))
450
451

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
452
static formula
453
454
455
E_n(std::string name, int n)
{
  if (n <= 0)
456
    return formula::tt();
457

458
  formula result = nullptr;
459
460
461
462
463

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
464
      formula f = formula::ap(p.str());
465
      if (result)
466
        result = And_(f, result);
467
      else
468
        result = f;
469
470
471
472
473
474
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
475
static formula
476
477
phi_n(std::string name, int n,
      op oper = op::And)
478
479
{
  if (n <= 0)
480
    return formula::tt();
481

482
483
  formula result = nullptr;
  formula p = formula::ap(name);
484
485
486
  for (; n > 0; --n)
    {
      if (result)
487
        result = formula::multop(oper, {p, X_(result)});
488
      else
489
        result = p;
490
491
492
493
    }
  return result;
}

494
495
static formula
N_n(std::string name, int n)
496
{
497
  return formula::F(phi_n(name, n));
498
499
500
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
501
static formula
502
503
phi_prime_n(std::string name, int n,
            op oper = op::And)
504
505
{
  if (n <= 0)
506
    return formula::tt();
507

508
509
  formula result = nullptr;
  formula p = formula::ap(name);
510
511
512
  for (; n > 0; --n)
    {
      if (result)
513
514
        {
          p = X_(p);
515
          result = formula::multop(oper, {result, p});
516
        }
517
      else
518
519
520
        {
          result = p;
        }
521
522
523
524
    }
  return result;
}

525
static formula
526
527
528
529
530
531
532
533
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
534
static formula
535
536
537
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
538
    return conj ? formula::tt() : formula::ff();
539

540
  formula result = nullptr;
541

542
  op o = conj ? op::And : op::Or;
543
544
545
546
547

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

      if (result)
551
        result = formula::multop(o, {f, result});
552
      else
553
        result = f;
554
555
556
557
558
559
    }
  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
560
static formula
561
562
563
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
564
    return conj ? formula::tt() : formula::ff();
565

566
  formula result = nullptr;
567

568
  op o = conj ? op::And : op::Or;
569
570
571
572
573

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

      if (result)
577
        result = formula::multop(o, {f, result});
578
      else
579
        result = f;
580
581
582
583
584
585
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
586
587
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
588
589
590
591
{
  if (n <= 0)
    n = 1;

592
  formula result = nullptr;
593
594
595
596
597

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
598
      formula f = formula::ap(p.str());
599
      if (!result)
600
        result = f;
601
      else if (right_assoc)
602
        result = formula::binop(o, f, result);
603
      else
604
        result = formula::binop(o, result, f);
605
606
607
608
609
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
610
static formula
611
612
613
R_n(std::string name, int n)
{
  if (n <= 0)
614
    return formula::tt();
615

616
  formula pi;
617
618
619
620

  {
    std::ostringstream p;
    p << name << 1;
621
    pi = formula::ap(p.str());
622
623
  }

624
  formula result = nullptr;
625
626
627

  for (int i = 1; i <= n; ++i)
    {
628
      formula gf = G_(F_(pi));
629
630
      std::ostringstream p;
      p << name << i + 1;
631
      pi = formula::ap(p.str());
632

633
      formula fg = F_(G_(pi));
634

635
      formula f = Or_(gf, fg);
636
637

      if (result)
638
        result = And_(f, result);
639
      else
640
        result = f;
641
642
643
644
645
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
646
static formula
647
648
649
Q_n(std::string name, int n)
{
  if (n <= 0)
650
    return formula::tt();
651

652
  formula pi;
653
654
655
656

  {
    std::ostringstream p;
    p << name << 1;
657
    pi = formula::ap(p.str());
658
659
  }

660
  formula result = nullptr;
661
662
663

  for (int i = 1; i <= n; ++i)
    {
664
      formula f = F_(pi);
665
666
667

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

670
      formula g = G_(pi);
671
672
673
674

      f = Or_(f, g);

      if (result)
675
        result = And_(f, result);
676
      else
677
        result = f;
678
679
680
681
682
683
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
684
685
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
686
687
{
  if (n <= 0)
688
    return conj ? formula::tt() : formula::ff();
689

690
  formula result = nullptr;
691

692
  op cop = conj ? op::And : op::Or;
693
694
695
696
697

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

      if (result)
701
        result = formula::multop(cop, {f, result});
702
      else
703
        result = f;
704
705
706
707
708
709
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
710
static formula
711
712
fair_response(std::string p, std::string q, std::string r, int n)
{
713
714
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
715
716
717
718
719
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
720
721
static formula
X_n(formula p, int n)
722
723
{
  assert(n >= 0);
724
  formula res = p;
725
726
727
728
729
730
731
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
732
static formula
733
734
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
735
736
737
738
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
739

740
  std::vector<formula> res(4);
741
742
743
744
745
746

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

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

#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.
784
785
786
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
787
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
788
789
790

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
791
792
793
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
794
795
796
797
798
799
800
                       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))))))));
801
  return formula::And(std::move(res));
802
803
}

804
static formula
805
ltl_counter_carry(std::string bit, std::string marker,
806
                  std::string carry, int n, bool linear)
807
{
808
809
810
811
812
813
  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);
814

815
  std::vector<formula> res(6);
816
817
818
819
820
821

  // 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]
822
      std::vector<formula> v(n);
823
      for (int i = 0; i + 1 < n; ++i)
824
        v[i] = X_n(neg_m, i + 1);
825
826
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
827
828
829
830
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
831
      formula p = m;
832
      for (int i = n - 1; i > 0; --i)
833
        p = And_(neg_m, X_(p));
834
      res[0] = And_(m, G_(Implies_(m, X_(p))));
835
836
837
838
839
840
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
841
      std::vector<formula> v2(n);
842
      for (int i = 0; i < n; ++i)
843
        v2[i] = X_n(neg_b, i);
844
      res[1] = formula::And(std::move(v2));
845
846
847
848
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
849
      formula p = neg_b;
850
      for (int i = n - 1; i > 0; --i)
851
        p = And_(neg_b, X_(p));
852
      res[1] = p;
853
854
    }

855
856
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
857
858

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
862
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
863
864
865
866

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
872
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
873
874
875
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
876
877
878
879
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
880
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
881
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
882
883
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
884
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
885
                                      Implies_(b, And_(c, Xn_negb))))));
886
    }
887
  return formula::And(std::move(res));
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
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));
}

934
935
static void
bad_number(const char* pattern, int n, int max = 0)
936
937
938
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
939
940
941
      << ", supported range is 1..";
  if (max)
    err << max;
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
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
  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);
}
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
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
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
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);

  formula fc = formula::ap(c);
  formula fd = formula::ap(d);

  formula* fa = new formula[n];
  formula* fb = new formula[n];

  for (int i = 0; i < n; i++)
    {
      fa[i] = formula::ap(a + std::to_string(i + 1));
      fb[i] = formula::ap(b + std::to_string(i + 1));
    }

  formula res = formula::And({ kr2_exp_1(fa, fb, fc, fd),
                               kr2_exp_2(n, fa, fb),
                               kr2_exp_3(n, fa, fb, fc, fd),
                               kr2_exp_4(n, fa, fb, fc, fd),
                               kr2_exp_5(n, fa, fb, fc, fd),
                               kr2_exp_mutex(n, fa, fb, fc, fd) });

  return res;
}

1339
1340
1341
static void
output_pattern(int pattern, int n)
{
1342
  formula f = nullptr;
1343
1344
1345
1346
  switch (pattern)
    {
      // Keep this alphabetically-ordered!
    case OPT_AND_F:
1347
      f = combunop_n("p", n, op::F, true);
1348
1349
1350
1351
1352
1353
1354
1355
      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:
1356
      f = formula::And({E_n("p", n), E_n("q", n)});
1357
1358
      break;
    case OPT_CCJ_BETA:
1359
      f = formula::And({N_n("p", n), N_n("q", n)});
1360
1361
      break;
    case OPT_CCJ_BETA_PRIME:
1362
      f = formula::And({N_prime_n("p", n), N_prime_n("q", n)});
1363
      break;
1364
1365
1366
1367
1368
1369
    case OPT_DAC_PATTERNS:
      f = dac_pattern(n);
      break;
    case OPT_EH_PATTERNS:
      f = eh_pattern(n);
      break;
1370
1371
1372
1373
1374
1375
1376
1377
1378
    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;
1379
1380
1381
1382
1383
1384