From 0b71df3fd32c7e60503e4b5ce3425b50f6e4d545 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 9 Jan 2018 10:59:10 +0100 Subject: [PATCH] genltl: add --gf-implies * spot/gen/formulas.cc, spot/gen/formulas.hh: Implement LTL_GF_IMPLIES. * bin/genltl.cc: Add --gf-implies. * NEWS: Mention it. * tests/core/genltl.test: Use it. --- NEWS | 5 +++-- bin/genltl.cc | 4 +++- spot/gen/formulas.cc | 32 ++++++++++++++++++-------------- spot/gen/formulas.hh | 3 ++- tests/core/genltl.test | 12 +++++++++--- 5 files changed, 35 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 7869ab85d..c4c5fe488 100644 --- a/NEWS +++ b/NEWS @@ -10,9 +10,10 @@ New in spot 2.4.4.dev (net yet released) Tools: - - genltl learned to generate a new family of formulas, taken from + - genltl learned to generate two new family of formulas, taken from the SYNTCOMP competition on reactive synthesis: - --gf-equiv=RANGE (GFa{1} & GFa{2} & ... & GFa{n}) <-> GFz + --gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz + --gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz - genltl learned to generate 4 new families of formulas, taken from Müller & Sickert's GandALF'17 paper: diff --git a/bin/genltl.cc b/bin/genltl.cc index edf79607f..4c37356bd 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015-2017 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2015-2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -88,6 +88,8 @@ static const argp_option options[] = "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0}, { "gf-equiv", gen::LTL_GF_EQUIV, "RANGE", 0, "(GFa1 & GFa2 & ... & GFan) <-> GFz", 0}, + { "gf-implies", gen::LTL_GF_IMPLIES, "RANGE", 0, + "(GFa1 & GFa2 & ... & GFan) -> GFz", 0}, { "gh-q", gen::LTL_GH_Q, "RANGE", 0, "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 }, { "gh-r", gen::LTL_GH_R, "RANGE", 0, diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index bed76a207..d9dd5eab9 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Developpement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Developpement // de l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -41,18 +41,6 @@ namespace spot { namespace { - static formula - LTL_GF_equiv(int n, const std::string& a, const std::string& z) - { - std::vector gfs; - for (int i = 0; i < n; ++i) - gfs.emplace_back(formula::G(formula::F( - formula::ap(a + std::to_string(i+1))))); - - return formula::Equiv(formula::And(gfs), - formula::G(formula::F(formula::ap(z)))); - } - static formula ms_example(const char* a, const char* b, int n) { @@ -272,6 +260,18 @@ namespace spot return result; } + static formula + LTL_GF_equiv_implies(int n, const std::string& a, const std::string& z, + bool equiv) + { + formula left = GF_n(a, n); + formula right = formula::G(formula::F(formula::ap(z))); + if (equiv) + return formula::Equiv(left, right); + else + return formula::Implies(left, right); + } + // (((p1 OP p2) OP p3)...OP pn) if right_assoc == false // (p1 OP (p2 OP (p3 OP (... pn) if right_assoc == true static formula @@ -1172,7 +1172,9 @@ namespace spot case LTL_FXG_OR: return FXG_or_n("p", n); case LTL_GF_EQUIV: - return LTL_GF_equiv(n, "a", "z"); + return LTL_GF_equiv_implies(n, "a", "z", true); + case LTL_GF_IMPLIES: + return LTL_GF_equiv_implies(n, "a", "z", false); case LTL_GH_Q: return Q_n("p", n); case LTL_GH_R: @@ -1254,6 +1256,7 @@ namespace spot "eh-patterns", "fxg-or", "gf-equiv", + "gf-implies", "gh-q", "gh-r", "go-theta", @@ -1312,6 +1315,7 @@ namespace spot return 12; case LTL_FXG_OR: case LTL_GF_EQUIV: + case LTL_GF_IMPLIES: case LTL_GH_Q: case LTL_GH_R: case LTL_GO_THETA: diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index 7ab7f9621..cff83aa50 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Developpement de +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -191,6 +191,7 @@ namespace spot LTL_EH_PATTERNS, LTL_FXG_OR, LTL_GF_EQUIV, + LTL_GF_IMPLIES, LTL_GH_Q, LTL_GH_R, LTL_GO_THETA, diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 0fb4d4b80..0250bd346 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -136,7 +136,7 @@ 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 --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< out diff out exp