genltl.cc 40.2 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
268
269
    { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Etessami and Holzmann [Concur'00] patterns "
      "(range should be included in 1..12)", 0 },
270
    { "gh-q", OPT_GH_Q, "RANGE", 0,
271
      "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 },
272
    { "gh-r", OPT_GH_R, "RANGE", 0,
273
      "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0 },
274
275
    { "go-theta", OPT_GO_THETA, "RANGE", 0,
      "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 },
276
    { "kr-n", OPT_KR_N, "RANGE", 0,
277
      "linear formula with doubly exponential DBA", 0 },
278
    { "kr-nlogn", OPT_KR_NLOGN, "RANGE", 0,
279
      "quasilinear formula with doubly exponential DBA", 0 },
280
    { "kv-psi", OPT_KV_PSI, "RANGE", 0,
281
      "quadratic formula with doubly exponential DBA", 0 },
282
    OPT_ALIAS(kr-n2),
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
    { "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 },
299
300
301
    { "sb-patterns", OPT_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
      "Somenzi and Bloem [CAV'00] patterns "
      "(range should be included in 1..27)", 0 },
302
303
304
305
306
307
    { "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 },
308
309
310
311
312
    { "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),
313
    RANGE_DOC,
314
  /**************************************************/
315
    { nullptr, 0, nullptr, 0, "Output options:", -20 },
316
317
318
319
320
321
    { "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 },
322
    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
323
      "the following interpreted sequences:", -19 },
324
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
325
      "the formula (in the selected syntax)", 0 },
326
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
327
      "the name of the pattern", 0 },
328
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
329
      "the argument of the pattern", 0 },
330
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
331
      "a single %", 0 },
332
    COMMON_LTL_OUTPUT_SPECS,
333
334
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
335
336
337
338
339
  };

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

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

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

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

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

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

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

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

457
  formula result = nullptr;
458
459
460
461
462

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

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

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

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

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

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

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

539
  formula result = nullptr;
540

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

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

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

565
  formula result = nullptr;
566

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

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

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

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

591
  formula result = nullptr;
592
593
594
595
596

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

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

615
  formula pi;
616
617
618
619

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

623
  formula result = nullptr;
624
625
626

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

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

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

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

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

651
  formula pi;
652
653
654
655

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

659
  formula result = nullptr;
660
661
662

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

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

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

      f = Or_(f, g);

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

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

689
  formula result = nullptr;
690

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
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));
}

933
934
static void
bad_number(const char* pattern, int n, int max = 0)
935
936
937
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
938
939
940
      << ", supported range is 1..";
  if (max)
    err << max;
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
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
  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);
}
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
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
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;
}

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