From b4cced9ba8ccb95a2f44614460ec38191e137cc7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Jul 2019 16:26:53 +0200 Subject: [PATCH] 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 | 4 ++ bin/genltl.cc | 8 +++- bin/man/genltl.x | 4 ++ doc/spot.bib | 18 +++++++- spot/gen/formulas.cc | 94 +++++++++++++++++++++++++++++++++++++++++ spot/gen/formulas.hh | 8 ++++ tests/core/genltl.test | 6 ++- tests/core/ltlfilt.test | 5 +++ 8 files changed, 143 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index e65aa08b9..5806d5365 100644 --- a/NEWS +++ b/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 diff --git a/bin/genltl.cc b/bin/genltl.cc index 98854fb9b..c9f8374bd 100644 --- a/bin/genltl.cc +++ b/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 }, diff --git a/bin/man/genltl.x b/bin/man/genltl.x index a21b40083..6194ba8ab 100644 --- a/bin/man/genltl.x +++ b/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. diff --git a/doc/spot.bib b/doc/spot.bib index 173567c15..f777ed604 100644 --- a/doc/spot.bib +++ b/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, diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index fcb7f8e14..a94512970 100644 --- a/spot/gen/formulas.cc +++ b/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 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 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: diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index dcec6be14..ac5974e48 100644 --- a/spot/gen/formulas.hh +++ b/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)))` diff --git a/tests/core/genltl.test b/tests/core/genltl.test index c0078a3be..23d284ab3 100755 --- a/tests/core/genltl.test +++ b/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<exp <