genltl.cc 39.7 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
122
//
// @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}
// }

123

124
#include "common_sys.hh"
125
126
127
128
129
130
131
132

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

133
#include "common_setup.hh"
134
#include "common_output.hh"
135
#include "common_range.hh"
136
#include "common_cout.hh"
137
138
139
140
141
142

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
143
#include <cmath>
144
145
#include <cstdlib>
#include <cstring>
146
147
#include <spot/tl/formula.hh>
#include <spot/tl/relabel.hh>
148
#include <spot/tl/parse.hh>
149
#include <spot/tl/exclusive.hh>
150
151
152
153

using namespace spot;

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

156
157
158
159
160
161
162
enum {
  OPT_AND_F = 1,
  OPT_AND_FG,
  OPT_AND_GF,
  OPT_CCJ_ALPHA,
  OPT_CCJ_BETA,
  OPT_CCJ_BETA_PRIME,
163
164
  OPT_DAC_PATTERNS,
  OPT_EH_PATTERNS,
165
166
167
  OPT_GH_Q,
  OPT_GH_R,
  OPT_GO_THETA,
168
169
170
  OPT_KR_N,
  OPT_KR_NLOGN,
  OPT_KV_PHI,
171
172
173
174
175
176
177
178
179
  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,
180
  OPT_SB_PATTERNS,
181
182
183
184
185
  OPT_TV_F1,
  OPT_TV_F2,
  OPT_TV_G1,
  OPT_TV_G2,
  OPT_TV_UU,
186
187
188
  OPT_U_LEFT,
  OPT_U_RIGHT,
  LAST_CLASS,
189
190
  OPT_POSITIVE,
  OPT_NEGATIVE,
191
};
192
193
194
195
196
197
198
199
200

const char* const class_name[LAST_CLASS] =
  {
    "and-f",
    "and-fg",
    "and-gf",
    "ccj-alpha",
    "ccj-beta",
    "ccj-beta-prime",
201
202
    "dac-patterns",
    "eh-patterns",
203
204
205
    "gh-q",
    "gh-r",
    "go-theta",
206
207
208
    "kr-n",
    "kr-nlogn",
    "kv-phi",
209
210
211
212
213
214
215
216
217
    "or-fg",
    "or-g",
    "or-gf",
    "or-r-left",
    "or-r-right",
    "rv-counter",
    "rv-counter-carry",
    "rv-counter-carry-linear",
    "rv-counter-linear",
218
    "sb-patterns",
219
220
221
222
223
    "tv-f1",
    "tv-f2",
    "tv-g1",
    "tv-g2",
    "tv-uu",
224
225
226
227
    "u-left",
    "u-right",
  };

228

229
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
230
231
232
233
234

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

struct job
{
  int pattern;
326
  struct range range;
327
328
329
330
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;
331
332
bool opt_positive = false;
bool opt_negative = false;
333
334
335

const struct argp_child children[] =
  {
336
337
338
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
339
  };
340
341

static void
342
enqueue_job(int pattern, const char* range_str)
343
344
345
{
  job j;
  j.pattern = pattern;
346
  j.range = parse_range(range_str);
347
348
349
  jobs.push_back(j);
}

350
351
352
353
354
355
356
357
358
static void
enqueue_job(int pattern, int min, int max)
{
  job j;
  j.pattern = pattern;
  j.range = {min, max};
  jobs.push_back(j);
}

359
static int
360
parse_opt(int key, char* arg, struct argp_state*)
361
362
363
364
365
366
367
368
369
370
371
372
373
{
  // 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:
374
375
376
    case OPT_KR_N:
    case OPT_KR_NLOGN:
    case OPT_KV_PHI:
377
378
379
380
381
382
383
384
385
    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:
386
387
388
389
390
    case OPT_TV_F1:
    case OPT_TV_F2:
    case OPT_TV_G1:
    case OPT_TV_G2:
    case OPT_TV_UU:
391
392
    case OPT_U_LEFT:
    case OPT_U_RIGHT:
393
394
      enqueue_job(key, arg);
      break;
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
    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;
413
414
415
416
417
418
    case OPT_POSITIVE:
      opt_positive = true;
      break;
    case OPT_NEGATIVE:
      opt_negative = true;
      break;
419
420
421
422
423
424
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

425
426
427
428
429
430
431
432
433
434
#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))
435
436

// F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
437
static formula
438
439
440
E_n(std::string name, int n)
{
  if (n <= 0)
441
    return formula::tt();
442

443
  formula result = nullptr;
444
445
446
447
448

  for (; n > 0; --n)
    {
      std::ostringstream p;
      p << name << n;
449
      formula f = formula::ap(p.str());
450
      if (result)
451
        result = And_(f, result);
452
      else
453
        result = f;
454
455
456
457
458
459
      result = F_(result);
    }
  return result;
}

// p & X(p & X(p & ... X(p)))
460
static formula
461
462
phi_n(std::string name, int n,
      op oper = op::And)
463
464
{
  if (n <= 0)
465
    return formula::tt();
466

467
468
  formula result = nullptr;
  formula p = formula::ap(name);
469
470
471
  for (; n > 0; --n)
    {
      if (result)
472
        result = formula::multop(oper, {p, X_(result)});
473
      else
474
        result = p;
475
476
477
478
    }
  return result;
}

479
480
static formula
N_n(std::string name, int n)
481
{
482
  return formula::F(phi_n(name, n));
483
484
485
}

// p & X(p) & XX(p) & XXX(p) & ... X^n(p)
486
static formula
487
488
phi_prime_n(std::string name, int n,
            op oper = op::And)
489
490
{
  if (n <= 0)
491
    return formula::tt();
492

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

510
static formula
511
512
513
514
515
516
517
518
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
519
static formula
520
521
522
GF_n(std::string name, int n, bool conj = true)
{
  if (n <= 0)
523
    return conj ? formula::tt() : formula::ff();
524

525
  formula result = nullptr;
526

527
  op o = conj ? op::And : op::Or;
528
529
530
531
532

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

      if (result)
536
        result = formula::multop(o, {f, result});
537
      else
538
        result = f;
539
540
541
542
543
544
    }
  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
545
static formula
546
547
548
FG_n(std::string name, int n, bool conj = false)
{
  if (n <= 0)
549
    return conj ? formula::tt() : formula::ff();
550

551
  formula result = nullptr;
552

553
  op o = conj ? op::And : op::Or;
554
555
556
557
558

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

      if (result)
562
        result = formula::multop(o, {f, result});
563
      else
564
        result = f;
565
566
567
568
569
570
    }
  return result;
}

//  (((p1 OP p2) OP p3)...OP pn)   if right_assoc == false
//  (p1 OP (p2 OP (p3 OP (... pn)  if right_assoc == true
571
572
static formula
bin_n(std::string name, int n, op o, bool right_assoc = false)
573
574
575
576
{
  if (n <= 0)
    n = 1;

577
  formula result = nullptr;
578
579
580
581
582

  for (int i = 1; i <= n; ++i)
    {
      std::ostringstream p;
      p << name << (right_assoc ? (n + 1 - i) : i);
583
      formula f = formula::ap(p.str());
584
      if (!result)
585
        result = f;
586
      else if (right_assoc)
587
        result = formula::binop(o, f, result);
588
      else
589
        result = formula::binop(o, result, f);
590
591
592
593
594
    }
  return result;
}

// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
595
static formula
596
597
598
R_n(std::string name, int n)
{
  if (n <= 0)
599
    return formula::tt();
600

601
  formula pi;
602
603
604
605

  {
    std::ostringstream p;
    p << name << 1;
606
    pi = formula::ap(p.str());
607
608
  }

609
  formula result = nullptr;
610
611
612

  for (int i = 1; i <= n; ++i)
    {
613
      formula gf = G_(F_(pi));
614
615
      std::ostringstream p;
      p << name << i + 1;
616
      pi = formula::ap(p.str());
617

618
      formula fg = F_(G_(pi));
619

620
      formula f = Or_(gf, fg);
621
622

      if (result)
623
        result = And_(f, result);
624
      else
625
        result = f;
626
627
628
629
630
    }
  return result;
}

// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
631
static formula
632
633
634
Q_n(std::string name, int n)
{
  if (n <= 0)
635
    return formula::tt();
636

637
  formula pi;
638
639
640
641

  {
    std::ostringstream p;
    p << name << 1;
642
    pi = formula::ap(p.str());
643
644
  }

645
  formula result = nullptr;
646
647
648

  for (int i = 1; i <= n; ++i)
    {
649
      formula f = F_(pi);
650
651
652

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

655
      formula g = G_(pi);
656
657
658
659

      f = Or_(f, g);

      if (result)
660
        result = And_(f, result);
661
      else
662
        result = f;
663
664
665
666
667
668
    }
  return result;
}

//  OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
//  OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
669
670
static formula
combunop_n(std::string name, int n, op o, bool conj = false)
671
672
{
  if (n <= 0)
673
    return conj ? formula::tt() : formula::ff();
674

675
  formula result = nullptr;
676

677
  op cop = conj ? op::And : op::Or;
678
679
680
681
682

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

      if (result)
686
        result = formula::multop(cop, {f, result});
687
      else
688
        result = f;
689
690
691
692
693
694
    }
  return result;
}

// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
695
static formula
696
697
fair_response(std::string p, std::string q, std::string r, int n)
{
698
699
  formula fair = GF_n(p, n);
  formula resp = G_(Implies_(formula::ap(q), F_(formula::ap(r))));
700
701
702
703
704
  return Not_(Implies_(fair, resp));
}


// Builds X(X(...X(p))) with n occurrences of X.
705
706
static formula
X_n(formula p, int n)
707
708
{
  assert(n >= 0);
709
  formula res = p;
710
711
712
713
714
715
716
  while (n--)
    res = X_(res);
  return res;
}

// Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
717
static formula
718
719
ltl_counter(std::string bit, std::string marker, int n, bool linear)
{
720
721
722
723
  formula b = formula::ap(bit);
  formula neg_b = Not_(b);
  formula m = formula::ap(marker);
  formula neg_m = Not_(m);
724

725
  std::vector<formula> res(4);
726
727
728
729
730
731

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

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

#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.
769
770
771
  formula Xnm1_b = X_n(b, n - 1);
  formula Xn_b = X_(Xnm1_b);
  res[2] = G_(Implies_(And_(m, neg_b),
772
                       AndX_(Xnm1_b, U_(And_(Not_(m), Equiv_(b, Xn_b)), m))));
773
774
775

  // From the least significant bit to the first 0, all the bits
  // are flipped on the next value.  Remaining bits are identical.
776
777
778
  formula Xnm1_negb = X_n(neg_b, n - 1);
  formula Xn_negb = X_(Xnm1_negb);
  res[3] = G_(Implies_(And_(m, b),
779
780
781
782
783
784
785
                       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))))))));
786
  return formula::And(std::move(res));
787
788
}

789
static formula
790
ltl_counter_carry(std::string bit, std::string marker,
791
                  std::string carry, int n, bool linear)
792
{
793
794
795
796
797
798
  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);
799

800
  std::vector<formula> res(6);
801
802
803
804
805
806

  // 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]
807
      std::vector<formula> v(n);
808
      for (int i = 0; i + 1 < n; ++i)
809
        v[i] = X_n(neg_m, i + 1);
810
811
      v[n - 1] = X_n(m, n);
      res[0] = And_(m, G_(Implies_(m, formula::And(std::move(v)))));
812
813
814
815
    }
  else
    {
      // G(m -> X(!m & X(!m X(m))))          [if n = 3]
816
      formula p = m;
817
      for (int i = n - 1; i > 0; --i)
818
        p = And_(neg_m, X_(p));
819
      res[0] = And_(m, G_(Implies_(m, X_(p))));
820
821
822
823
824
825
    }

  // All bits are initially zero.
  if (!linear)
    {
      // !b & X(!b) & XX(!b)    [if n = 3]
826
      std::vector<formula> v2(n);
827
      for (int i = 0; i < n; ++i)
828
        v2[i] = X_n(neg_b, i);
829
      res[1] = formula::And(std::move(v2));
830
831
832
833
    }
  else
    {
      // !b & X(!b & X(!b))     [if n = 3]
834
      formula p = neg_b;
835
      for (int i = n - 1; i > 0; --i)
836
        p = And_(neg_b, X_(p));
837
      res[1] = p;
838
839
    }

840
841
  formula Xn_b = X_n(b, n);
  formula Xn_negb = X_n(neg_b, n);
842
843

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

  // If m is 1 and b is 1 then c is 1 and n steps later b is 0.
847
  res[3] = G_(Implies_(And_(m, b), And_(c, Xn_negb)));
848
849
850
851

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

      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
857
      res[5] = G_(Implies_(c, And_(Implies_(X_(neg_b),
858
859
860
                                            And_(X_(neg_c), X_(Xn_b))),
                                   Implies_(X_(b),
                                            And_(X_(c), X_(Xn_negb))))));
861
862
863
864
    }
  else
    {
      // If there's no carry, then all of the bits stay the same n steps later.
865
      res[4] = G_(Implies_(And_(neg_c, X_(neg_m)),
866
                           X_(And_(Not_(c), Equiv_(b, Xn_b)))));
867
868
      // If there's a carry, then add one: flip the bits of b and
      // adjust the carry.
869
      res[5] = G_(Implies_(c, X_(And_(Implies_(neg_b, And_(neg_c, Xn_b)),
870
                                      Implies_(b, And_(c, Xn_negb))))));
871
    }
872
  return formula::And(std::move(res));
873
874
}

875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
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));
}

919
920
static void
bad_number(const char* pattern, int n, int max = 0)
921
922
923
{
  std::ostringstream err;
  err << "no pattern " << n << " for " << pattern
924
925
926
      << ", supported range is 1..";
  if (max)
    err << max;
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
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
  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);
}
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
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
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;
}

1324
1325
1326
static void
output_pattern(int pattern, int n)
{
1327
  formula f = nullptr;
1328
1329
1330
1331
  switch (pattern)
    {
      // Keep this alphabetically-ordered!
    case OPT_AND_F:
1332
      f = combunop_n("p", n, op::F, true);
1333
1334
1335
1336
1337
1338
1339
1340
      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:
1341
      f = formula::And({E_n("p", n), E_n("q", n)});
1342
1343
      break;
    case OPT_CCJ_BETA:
1344
      f = formula::And({N_n("p", n), N_n("q", n)});
1345
1346
      break;
    case OPT_CCJ_BETA_PRIME:
1347
      f = formula::And({N_prime_n("p", n), N_prime_n("q", n)});
1348
      break;
1349
1350
1351
1352
1353
1354
    case OPT_DAC_PATTERNS:
      f = dac_pattern(n);
      break;
    case OPT_EH_PATTERNS:
      f = eh_pattern(n);
      break;
1355
1356
1357
1358
1359
1360
1361
1362
1363
    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;
1364
1365
1366
1367
1368
1369
1370
1371
1372
    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;
    case OPT_KV_PHI:
      f = kv_exp(n, "a", "b", "c", "d");
      break;
1373
1374
1375
1376
    case OPT_OR_FG:
      f = FG_n("p", n, false);
      break;
    case OPT_OR_G:
1377
      f = combunop_n("p", n, op::G, false);
1378
1379
1380
1381
1382
      break;
    case OPT_OR_GF:
      f = GF_n("p", n, false);
      break;
    case OPT_R_LEFT:
1383
      f = bin_n("p", n, op::R, false);
1384
1385
      break;
    case OPT_R_RIGHT:
1386
      f = bin_n("p", n, op::R, true);
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
      break;
    case OPT_RV_COUNTER_CARRY:
      f = ltl_counter_carry("b", "m", "c", n, false);
      break;
    case OPT_RV_COUNTER_CARRY_LINEAR:
      f = ltl_counter_carry("b", "m", "c", n, true);
      break;
    case OPT_RV_COUNTER:
      f = ltl_counter("b", "m", n, false);
      break;
    case OPT_RV_COUNTER_LINEAR:
      f = ltl_counter("b", "m", n, true);
      break;
1400
1401
1402
    case OPT_SB_PATTERNS:
      f = sb_pattern(n);
      break;
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
    case OPT_TV_F1:
      f = tv_f1("p", "q", n