From 68ad39194823f9c08fa474e3cc7a2cdac2942f34 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Feb 2017 16:39:54 +0100 Subject: [PATCH] correct handling of --stats=%P Fixes #236. * bin/common_aoutput.cc: Fix it. * tests/core/format.test: Improve test cases. * NEWS: Mention the bug. --- NEWS | 3 +++ bin/common_aoutput.cc | 2 +- tests/core/format.test | 18 +++++++++++++----- 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index a51d8561e..0c48e5f8e 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 2.3.1.dev (not yet released) - The tests using LTSmin's patched version of divine would fail if the current (non-patched) version of divine was installed. + - Because of a typo, the output of --stats='...%P...' was correct + only if %p was used as well. + New in spot 2.3.1 (2017-02-20) Tools: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index e8011b30f..c1805f3c7 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, haut_deterministic_ = is_deterministic(haut->aut); } - if (has('p')) + if (has('P')) haut_complete_ = is_complete(haut->aut); if (has('G')) diff --git a/tests/core/format.test b/tests/core/format.test index 67a7ce0b3..a91026130 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -51,11 +51,19 @@ for i in 1 2 3 4 5 6; do cmp ap-$i.ltl ap-$i.ltl2 || exit 1 done -out=`ltl2tgba -f 'GFa' | autfilt --stats='%W,%w' --complement` +ltl2tgba GFa > GFa +out=` FGa +test "0,1,0,1" = "`