genltl: add --pps-arbiter-{strict,standard}

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
this.
* NEWS, bin/man/genltl.x, doc/spot.bib: Add documentation.
* tests/core/genltl.test, tests/core/ltlfilt.test: Add some tests.

NEWS

@@ -1,5 +1,9 @@
 New in spot 2.8.0.dev (not yet released)
 
+  Command-line tools:
+
+  - genltl learned --pps-arbiter-standard and --pps-arbiter-strict.
+
   Bugs fixed:
 
   - When complement() was called with an output_aborter, it could

bin/genltl.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2015-2018 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2015-2019 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -133,6 +133,12 @@ static const argp_option options[] =
       "(range should be included in 1..20)", 0 },
     OPT_ALIAS(beem-patterns),
     OPT_ALIAS(p),
+    { "pps-arbiter-standard", gen::LTL_PPS_ARBITER_STANDARD, "RANGE", 0,
+      "Arbiter with n clients that sent requests (ri) and "
+      "receive grants (gi).  Standard semantics.", 0 },
+    { "pps-arbiter-strict", gen::LTL_PPS_ARBITER_STRICT, "RANGE", 0,
+      "Arbiter with n clients that sent requests (ri) and "
+      "receive grants (gi).  Strict semantics.", 0 },
     { "r-left", gen::LTL_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 },
     { "r-right", gen::LTL_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 },
     { "rv-counter", gen::LTL_RV_COUNTER, "RANGE", 0, "n-bit counter", 0 },

bin/man/genltl.x

@@ -54,6 +54,10 @@ p
 R. Pelánek: BEEM: benchmarks for explicit model checkers
 Proceedings of Spin'07.  LNCS 4595.
 .TP
+pps
+N. Piterman, A. Pnueli, and Y. Sa'ar: Synthesis of Reactive(1) Designs.
+Proceedings of VMCAI'06.  LNCS 3855.
+.TP
 rv
 K. Rozier and M. Vardi: LTL Satisfiability Checking.
 Proceedings of Spin'07.  LNCS 4595.

doc/spot.bib

@@ -564,6 +564,20 @@
   publisher	= {Springer-Verlag}
 }
 
+@InProceedings{	  piterman.06.vmcai,
+  author	= {Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
+  editor	= {E. Allen Emerson and Kedar S. Namjoshi"},
+  title		= {Synthesis of Reactive(1) Designs},
+  booktitle	= {Proceedings of the 7th International Conference on
+		  Verification, Model Checking, and Abstract Interpretation
+		  (VMCAI'06)},
+  year		= {2006},
+  publisher	= {Springer},
+  pages		= {364--380},
+  volume	= {3855},
+  series	= {Lecture Notes in Computer Science}
+}
+
 @Book{		  psl.04.lrm,
   title		= {Property Specification Language Reference Manual v1.1},
   publisher	= {Accellera},
@@ -671,11 +685,11 @@
 
 @Book{		  systemverilog.18.std,
   title		= {1800-2017 - IEEE Standard for SystemVerilog--Unified
-                   Hardware Design, Specification, and Verification Language},
+		  Hardware Design, Specification, and Verification Language},
   publisher	= {IEEE},
   year		= {2018},
   month		= feb,
-  doi           = {10.1109/IEEESTD.2018.8299595}
+  doi		= {10.1109/IEEESTD.2018.8299595}
 }
 
 @InProceedings{	  tabakov.10.rv,

spot/gen/formulas.cc

@@ -1197,6 +1197,90 @@ namespace spot
       }
     }
 
+    static formula
+    pps_arbiter(std::string r_, std::string g_, int n, bool strict_)
+    {
+      formula* r = new formula[n];
+      formula* g = new formula[n];
+      std::vector<formula> res;
+
+      for (int i = 0; i < n; ++i)
+        {
+          r[i] = formula::ap(r_ + std::to_string(i + 1));
+          g[i] = formula::ap(g_ + std::to_string(i + 1));
+        }
+
+      formula theta_e;
+      formula theta_s;
+      formula psi_e;
+      formula psi_s;
+      formula phi_e;
+      formula phi_s;
+      {
+        std::vector<formula> res;
+        for (int i = 0; i < n; ++i)
+          res.push_back(formula::Not(r[i]));
+        theta_e = formula::And(res);
+
+        res.clear();
+        for (int i = 0; i < n; ++i)
+          res.push_back(formula::Not(g[i]));
+        theta_s = formula::And(res);
+
+        res.clear();
+        for (int i = 0; i < n; ++i)
+          {
+            formula left = formula::Xor(r[i], g[i]);
+            formula right = formula::Equiv(r[i], formula::X(r[i]));
+            res.push_back(formula::Implies(left, right));
+          }
+        psi_e = formula::And(res);
+
+        res.clear();
+        for (int i = 0; i < n; ++i)
+          {
+            for (int j = 0; j < i; ++j)
+              res.push_back(formula::Not(formula::And({g[i], g[j]})));
+            formula left = formula::Equiv(r[i], g[i]);
+            formula right = formula::Equiv(g[i], formula::X(g[i]));
+            res.push_back(formula::Implies(left, right));
+          }
+        psi_s = formula::And(res);
+
+        res.clear();
+        for (int i = 0; i < n; ++i)
+          {
+            formula f = formula::Not(formula::And({r[i], g[i]}));
+            res.push_back(formula::G(formula::F(f)));
+          }
+        phi_e = formula::And(res);
+
+        res.clear();
+        for (int i = 0; i < n; ++i)
+          {
+            res.push_back(formula::G(formula::F(formula::Equiv(r[i], g[i]))));
+          }
+        phi_s = formula::And(res);
+      }
+      delete[] r;
+      delete[] g;
+
+      if (!strict_)
+        {
+          formula imp =
+            formula::Implies(formula::And({formula::G(psi_e), phi_e}),
+                             formula::And({formula::G(psi_s), phi_s}));
+          return formula::Implies(theta_e, formula::And({theta_s, imp}));
+        }
+      else
+        {
+          formula e = formula::W(psi_s, formula::Not(psi_e));
+          formula imp =
+            formula::Implies(formula::And({formula::G(psi_e), phi_e}), phi_s);
+          return formula::Implies(theta_e, formula::And({theta_s, e, imp}));
+        }
+    }
+
     formula ltl_pattern(ltl_pattern_id pattern, int n, int m)
     {
       if (n < 0)
@@ -1275,6 +1359,10 @@ namespace spot
           return ms_phi_rs("a", "b", n, false);
         case LTL_P_PATTERNS:
           return p_pattern(n);
+        case LTL_PPS_ARBITER_STANDARD:
+          return pps_arbiter("r", "g", n, false);
+        case LTL_PPS_ARBITER_STRICT:
+          return pps_arbiter("r", "g", n, true);
         case LTL_R_LEFT:
           return bin_n("p", n, op::R, false);
         case LTL_R_RIGHT:
@@ -1351,6 +1439,8 @@ namespace spot
           "or-g",
           "or-gf",
           "p-patterns",
+          "pps-arbiter-standard",
+          "pps-arbiter-strict",
           "r-left",
           "r-right",
           "rv-counter",
@@ -1420,6 +1510,8 @@ namespace spot
           return 0;
         case LTL_P_PATTERNS:
           return 20;
+        case LTL_PPS_ARBITER_STANDARD:
+        case LTL_PPS_ARBITER_STRICT:
         case LTL_R_LEFT:
         case LTL_R_RIGHT:
         case LTL_RV_COUNTER_CARRY:
@@ -1485,6 +1577,8 @@ namespace spot
         case LTL_OR_G:
         case LTL_OR_GF:
         case LTL_P_PATTERNS:
+        case LTL_PPS_ARBITER_STANDARD:
+        case LTL_PPS_ARBITER_STRICT:
         case LTL_R_LEFT:
         case LTL_R_RIGHT:
         case LTL_RV_COUNTER_CARRY:

spot/gen/formulas.hh

@@ -114,6 +114,14 @@ namespace spot
       /// 20 formulas from BEEM.
       /// \cite pelanek.07.spin
       LTL_P_PATTERNS,
+      /// Arbiter for n clients sending requests, and receiving
+      /// grants. \cite piterman.06.vmcai using standard
+      /// semantics from \cite jacobs.16.synt .
+      LTL_PPS_ARBITER_STANDARD,
+      /// Arbiter for n clients sending requests, and receiving
+      /// grants. \cite piterman.06.vmcai using strict
+      /// semantics from \cite jacobs.16.synt .
+      LTL_PPS_ARBITER_STRICT,
       /// `(((p1 R p2) R p3) ... R pn)`
       LTL_R_LEFT,
       /// `(p1 R (p2 R (... R pn)))`

tests/core/genltl.test

@@ -129,7 +129,7 @@ EOF
 diff output expected
 
 genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
-       --format=%F=%L,%f |
+       --pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f |
     ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
 kv-psi=1,15
@@ -146,6 +146,10 @@ fxg-or=0,2
 fxg-or=1,3
 fxg-or=2,4
 fxg-or=3,5
+pps-arbiter-standard=2,15
+pps-arbiter-standard=3,23
+pps-arbiter-strict=2,37
+pps-arbiter-strict=3,82
 EOF
 diff out exp
 

tests/core/ltlfilt.test

@@ -534,3 +534,8 @@ cat >exp <<EOF
 F
 EOF
 diff out exp
+
+f1=`genltl --pps-arbiter-standard=2`
+f2=`genltl --pps-arbiter-strict=2`
+run 1 ltlfilt -f "$f2" --implied-by "$f1"
+run 0 ltlfilt -f "$f1" --implied-by "$f2"