From b0ba6190b7a4fd49e755823d036b7d4f97d08792 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Jan 2017 20:57:21 +0100 Subject: [PATCH] ltlcross: relabel unsupported atomic propisitions in %s * bin/ltlcross.cc: Do it. * bin/common_trans.cc: Adjust documentation. * tests/core/ltl3ba.test: Test it. * NEWS: Document it. --- NEWS | 6 +++++- bin/common_trans.cc | 9 +++++---- bin/ltlcross.cc | 8 +++++--- tests/core/ltl3ba.test | 17 ++++++++++++----- 4 files changed, 27 insertions(+), 13 deletions(-) diff --git a/NEWS b/NEWS index ca3e382fd..5734a7f33 100644 --- a/NEWS +++ b/NEWS @@ -130,7 +130,7 @@ New in spot 2.2.2.dev (Not yet released) * The new function mp_class(f) returns the class of the formula f in the temporal hierarchy of Manna & Pnueli. -Bug fixed: +Bugs fixed: * The minimize_wdba() function was not correctly minimizing automata with useless SCCs. This was not an issue for the LTL translation @@ -139,6 +139,10 @@ Bug fixed: consequence, some tricky safety or guarantee properties were only recognized as obligations. + * When ltlcross was running a translator taking the Spin syntax as + input (%s) it would not automatically relabel any unsupported + atomic propositions as ltldo already do. + New in spot 2.2.2 (2016-12-16) Build: diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 3c71ab719..a446f0545 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -642,13 +642,14 @@ static const argp_option options[] = { "%F,%S,%L,%W", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, { "%O", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "the automaton is output in HOA, never claim, LBTT, or ltl2dstar's " + "the automaton output in HOA, never claim, LBTT, or ltl2dstar's " "format", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { nullptr, 0, nullptr, 0, "If either %l, %L, or %T are used, any input formula that does " "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " - "relabeled automatically.\n" + "relabeled automatically. Likewise if %s or %S are used with " + "atomic proposition that compatible with Spin's syntax.\n" "The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\"" " by a bracketed sequence of operators to unabbreviate before outputing" " the formula. For instance %[MW]f will rewrite operators M and W" diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index edca1167e..7e22feff2 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -994,8 +994,10 @@ namespace // If we need LBT atomic proposition in any of the input or // output, relabel the formula. - if (!f.has_lbt_atomic_props() && - (runner.has('l') || runner.has('L') || runner.has('T'))) + if ((!f.has_lbt_atomic_props() && + (runner.has('l') || runner.has('L') || runner.has('T'))) + || (!f.has_spin_atomic_props() && + (runner.has('s') || runner.has('S')))) f = spot::relabel(f, spot::Pnn); // ---------- Positive Formula ---------- diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test index 348d67381..04c028bac 100755 --- a/tests/core/ltl3ba.test +++ b/tests/core/ltl3ba.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -30,9 +30,16 @@ set -e # The -H1 option will output alternating automata, so this tests # ltlcross's support in this area. -randltl -n 30 2 | -ltlcross 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' \ - --ambiguous --strength --csv=output.csv +# Using '_x' as first formula makes sure that ltlcross automatically +# relabels the input formula when the atomic propositions are not +# compatible with Spin's syntax. +( + echo _x + randltl -n 30 2 +) | ltlcross 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' \ + --ambiguous --strength --csv=output.csv + +grep _x output.csv && exit 1 # Make sure all lines in output.csv have the same number of comas sed 's/[^,]//g'