alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: relabel unsupported atomic propisitions in %s

Browse source 
* bin/ltlcross.cc: Do it.
* bin/common_trans.cc: Adjust documentation.
* tests/core/ltl3ba.test: Test it.
* NEWS: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-13 20:57:21 +01:00
parent 8754cea2ca
commit b0ba6190b7
4 changed files with 27 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -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 * The new function mp_class(f) returns the class of the formula
f in the temporal hierarchy of Manna & Pnueli. f in the temporal hierarchy of Manna & Pnueli.
Bug fixed: Bugs fixed:
* The minimize_wdba() function was not correctly minimizing automata * The minimize_wdba() function was not correctly minimizing automata
with useless SCCs. This was not an issue for the LTL translation 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 consequence, some tricky safety or guarantee properties were only
recognized as obligations. 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) New in spot 2.2.2 (2016-12-16)
Build: Build:

9
bin/common_trans.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
// l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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, { "%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 }, "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
{ "%O", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%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 }, "format", 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
{ nullptr, 0, nullptr, 0, { nullptr, 0, nullptr, 0,
"If either %l, %L, or %T are used, any input formula that does " "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 " "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\"" "The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\""
" by a bracketed sequence of operators to unabbreviate before outputing" " by a bracketed sequence of operators to unabbreviate before outputing"
" the formula. For instance %[MW]f will rewrite operators M and W" " the formula. For instance %[MW]f will rewrite operators M and W"

8
bin/ltlcross.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 // If we need LBT atomic proposition in any of the input or
// output, relabel the formula. // output, relabel the formula.
if (!f.has_lbt_atomic_props() && if ((!f.has_lbt_atomic_props() &&
(runner.has('l') || runner.has('L') || runner.has('T'))) (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); f = spot::relabel(f, spot::Pnn);
// ---------- Positive Formula ---------- // ---------- Positive Formula ----------

17
tests/core/ltl3ba.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de # Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # 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 # The -H1 option will output alternating automata, so this tests
# ltlcross's support in this area. # ltlcross's support in this area.
randltl -n 30 2 | # Using '_x' as first formula makes sure that ltlcross automatically
ltlcross 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' \ # relabels the input formula when the atomic propositions are not
--ambiguous --strength --csv=output.csv # 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 # Make sure all lines in output.csv have the same number of comas
sed 's/[^,]//g' <output.csv | sed 's/[^,]//g' <output.csv |