From c535871ffd641ad957dccab68ebebd36112343f0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 3 Jun 2018 19:35:02 +0200
Subject: [PATCH] genltl: --ms-example now has two arguments

* bin/genltl.cc, spot/gen/formulas.cc, tests/core/genltl.test: Adjust.
* NEWS: Mention it.
---
 NEWS                   |  3 ++
 bin/genltl.cc          |  4 +--
 spot/gen/formulas.cc   | 17 ++++-----
 tests/core/genltl.test | 80 ++++++++++++++++++++++++++----------------
 4 files changed, 62 insertions(+), 42 deletions(-)

diff --git a/NEWS b/NEWS
index e16cb623c..352d1694c 100644
--- a/NEWS
+++ b/NEWS
@@ -34,6 +34,9 @@ New in spot 2.5.3.dev  (not yet released)
       --sejk-patterns[=RANGE]   φ₁,φ₂,φ₃ from Sikert et al's [CAV'16]
                              paper (range should be included in 1..3)
 
+  - genltl --ms-example can now take a two-range argument,
+    (as --sejk-f above).
+
   Library:
 
   - spot::twa_graph::merge_states() is a new method that merges states
diff --git a/bin/genltl.cc b/bin/genltl.cc
index b3fd1ae9c..a4ad71fbe 100644
--- a/bin/genltl.cc
+++ b/bin/genltl.cc
@@ -110,8 +110,8 @@ static const argp_option options[] =
     { "kv-psi", gen::LTL_KV_PSI, "RANGE", 0,
       "quadratic formula with doubly exponential DBA", 0 },
     OPT_ALIAS(kr-n2),
-    { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE", 0,
-      "GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))", 0 },
+    { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE[,RANGE]", 0,
+      "GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))", 0 },
     { "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0,
       "FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...", 0 },
     { "ms-phi-r", gen::LTL_MS_PHI_R, "RANGE", 0,
diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc
index 6033112de..fd766d063 100644
--- a/spot/gen/formulas.cc
+++ b/spot/gen/formulas.cc
@@ -43,19 +43,14 @@ namespace spot
     namespace
     {
       static formula
-      ms_example(const char* a, const char* b, int n)
+      ms_example(const char* a, const char* b, int n, int m)
       {
         formula ax = formula::tt();
         formula fb = formula::tt();
         for (int i = n; i > 0; --i)
-          {
-            std::ostringstream ans;
-            ans << a << i;
-            ax = And_(formula::ap(ans.str()), X_(ax));
-            ans.str("");
-            ans << b << i;
-            fb = F_(And_(formula::ap(ans.str()), fb));
-          }
+          ax = And_(formula::ap(a + std::to_string(i)), X_(ax));
+        for (int i = m; i > 0; --i)
+          fb = F_(And_(formula::ap(b + std::to_string(i)), fb));
         return And_(G_(F_(ax)), fb);
       }
 
@@ -1255,7 +1250,7 @@ namespace spot
         case LTL_OR_GF:
           return GF_n("p", n, false);
         case LTL_MS_EXAMPLE:
-          return ms_example("a", "b", n);
+          return ms_example("a", "b", n, m);
         case LTL_MS_PHI_H:
           return ms_phi_h("a", "b", n);
         case LTL_MS_PHI_R:
@@ -1458,7 +1453,9 @@ namespace spot
         case LTL_KR_N:
         case LTL_KR_NLOGN:
         case LTL_KV_PSI:
+          return 1;
         case LTL_MS_EXAMPLE:
+          return 2;
         case LTL_MS_PHI_H:
         case LTL_MS_PHI_R:
         case LTL_MS_PHI_S:
diff --git a/tests/core/genltl.test b/tests/core/genltl.test
index 706ac92b4..3b73938d4 100755
--- a/tests/core/genltl.test
+++ b/tests/core/genltl.test
@@ -154,43 +154,63 @@ test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16
 test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16
 
 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
-       --gf-equiv=0..5 --gf-implies=0..5 --format=%F=%L,%f |
+       --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
     ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
-ms-example=0,1
-ms-example=1,2
-ms-example=2,4
-ms-example=3,7
-ms-example=4,12
-ms-phi-r=0,2
-ms-phi-r=1,16
-ms-phi-r=2,29
-ms-phi-s=0,5
-ms-phi-s=1,8
-ms-phi-s=2,497
-ms-phi-h=0,1
-ms-phi-h=1,3
-ms-phi-h=2,7
-ms-phi-h=3,15
-ms-phi-h=4,31
-gf-equiv=0,1
-gf-equiv=1,4
-gf-equiv=2,8
-gf-equiv=3,21
-gf-equiv=4,81
-gf-equiv=5,431
-gf-implies=0,1
-gf-implies=1,5
-gf-implies=2,12
-gf-implies=3,41
-gf-implies=4,186
-gf-implies=5,1047
+"ms-example=0,0",1
+"ms-example=0,1",2
+"ms-example=0,2",3
+"ms-example=0,3",4
+"ms-example=0,4",5
+"ms-example=1,0",1
+"ms-example=1,1",2
+"ms-example=1,2",3
+"ms-example=1,3",4
+"ms-example=1,4",5
+"ms-example=2,0",2
+"ms-example=2,1",3
+"ms-example=2,2",4
+"ms-example=2,3",5
+"ms-example=2,4",6
+"ms-example=3,0",4
+"ms-example=3,1",5
+"ms-example=3,2",6
+"ms-example=3,3",7
+"ms-example=3,4",8
+"ms-example=4,0",8
+"ms-example=4,1",9
+"ms-example=4,2",10
+"ms-example=4,3",11
+"ms-example=4,4",12
+"ms-phi-r=0",2
+"ms-phi-r=1",16
+"ms-phi-r=2",29
+"ms-phi-s=0",5
+"ms-phi-s=1",8
+"ms-phi-s=2",497
+"ms-phi-h=0",1
+"ms-phi-h=1",3
+"ms-phi-h=2",7
+"ms-phi-h=3",15
+"ms-phi-h=4",31
+"gf-equiv=0",1
+"gf-equiv=1",4
+"gf-equiv=2",8
+"gf-equiv=3",21
+"gf-equiv=4",81
+"gf-equiv=5",431
+"gf-implies=0",1
+"gf-implies=1",5
+"gf-implies=2",12
+"gf-implies=3",41
+"gf-implies=4",186
+"gf-implies=5",1047
 EOF
 diff out exp
 
 # Running ltl2tgba on one formula at a time should give the same results
 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
-       --gf-equiv=0..5 --gf-implies=0..5 --format=%F=%L,%f |
+       --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
     ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out
 diff out exp