From 1c96afb1d0aec3a146322c59bded27a2c2cb8517 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 18 Feb 2017 09:59:00 +0100
Subject: [PATCH] genltl: --kv-phi is in fact --kv-psi

* bin/genltl.cc: Change the name and add the bibtex entry.
* bin/man/genltl.x: Replace LNCS by LNAI.
* tests/core/genltl.test: Also test the %F output.
---
 bin/genltl.cc          | 23 ++++++++++++++++++-----
 bin/man/genltl.x       |  2 +-
 tests/core/genltl.test | 15 ++++++++++++---
 3 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/bin/genltl.cc b/bin/genltl.cc
index e4bb1f7c2..8fc105046 100644
--- a/bin/genltl.cc
+++ b/bin/genltl.cc
@@ -119,6 +119,19 @@
 //   month = nov,
 //   publisher = {Springer}
 // }
+//
+// @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}
+// }
 
 
 #include "common_sys.hh"
@@ -167,7 +180,7 @@ enum {
   OPT_GO_THETA,
   OPT_KR_N,
   OPT_KR_NLOGN,
-  OPT_KV_PHI,
+  OPT_KV_PSI,
   OPT_OR_FG,
   OPT_OR_G,
   OPT_OR_GF,
@@ -205,7 +218,7 @@ const char* const class_name[LAST_CLASS] =
     "go-theta",
     "kr-n",
     "kr-nlogn",
-    "kv-phi",
+    "kv-psi",
     "or-fg",
     "or-g",
     "or-gf",
@@ -263,7 +276,7 @@ static const argp_option options[] =
       "linear formula with doubly exponential DBA", 0 },
     { "kr-nlogn", OPT_KR_NLOGN, "RANGE", 0,
       "quasilinear formula with doubly exponential DBA", 0 },
-    { "kv-phi", OPT_KV_PHI, "RANGE", 0,
+    { "kv-psi", OPT_KV_PSI, "RANGE", 0,
       "quadratic formula with doubly exponential DBA", 0 },
     OPT_ALIAS(kr-n2),
     { "or-fg", OPT_OR_FG, "RANGE", 0, "FG(p1)|FG(p2)|...|FG(pn)", 0 },
@@ -373,7 +386,7 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_GO_THETA:
     case OPT_KR_N:
     case OPT_KR_NLOGN:
-    case OPT_KV_PHI:
+    case OPT_KV_PSI:
     case OPT_OR_FG:
     case OPT_OR_G:
     case OPT_OR_GF:
@@ -1367,7 +1380,7 @@ output_pattern(int pattern, int n)
     case OPT_KR_NLOGN:
       f = kr1_exp(n, "a", "b", "c", "d", "y", "z");
       break;
-    case OPT_KV_PHI:
+    case OPT_KV_PSI:
       f = kv_exp(n, "a", "b", "c", "d");
       break;
     case OPT_OR_FG:
diff --git a/bin/man/genltl.x b/bin/man/genltl.x
index c51121d9c..6272f4ac2 100644
--- a/bin/man/genltl.x
+++ b/bin/man/genltl.x
@@ -48,7 +48,7 @@ Proceedings of RV'10.  LNCS 6418.
 kr
 O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic
 Automata.
-Proceedings of MoChArt'10.  LNCS 6572.
+Proceedings of MoChArt'10.  LNAI 6572.
 .TP
 rv
 O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time.
diff --git a/tests/core/genltl.test b/tests/core/genltl.test
index 8c1b6add2..67b30fe8c 100755
--- a/tests/core/genltl.test
+++ b/tests/core/genltl.test
@@ -101,9 +101,18 @@ tv-uu,3,G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U p4))))))
 EOF
 diff output expected
 
-test $(genltl --kr-n2=2 | ltl2tgba --low -D --stats=%s) -ge 16
-test $(genltl --kr-nlogn=2 | ltl2tgba --low -D --stats=%s) -ge 16
-test $(genltl --kr-n=2 | ltl2tgba --low -D --stats=%s) -ge 16
+
+genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --format=%F=%L,%f |
+    ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
+cat >exp<<EOF
+kv-psi=1,15
+kv-psi=2,106
+kr-nlogn=1,19
+kr-nlogn=2,147
+kr-n=1,12
+kr-n=2,82
+EOF
+diff out exp
 
 test $(genltl --kr-n2=4 | ltl2tgba --low --stats=%s) -ge 16
 test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16