From fc786d401a91cfece5b7685453fdfd9db626aca6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 28 Mar 2018 14:08:35 +0200 Subject: [PATCH] autfilt: fix --sat-minimize -B Fixes #340. * bin/common_post.cc: -B implies -S. * tests/core/satmin2.test: Test this. --- NEWS | 3 +++ bin/common_post.cc | 1 + tests/core/satmin2.test | 9 +++++++-- 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 171742626..88c28a167 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,9 @@ New in spot 2.5.2.dev (not yet released) - Fix cryptic error message from Python's spot.translate() and spot.postprocess() when supplying conflicting arguments. + - "autfilt -B --sat-minimize" was incorrectly producing + transition-based automata. + New in spot 2.5.2 (2018-03-25) Bugs fixed: diff --git a/bin/common_post.cc b/bin/common_post.cc index 2b07de609..ef97b0a26 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -164,6 +164,7 @@ parse_opt_post(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; colored = spot::postprocessor::Any; + sbacc = spot::postprocessor::SBAcc; break; case 'C': comp = spot::postprocessor::Complete; diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test index 3a5cbe150..d7c7e0b27 100755 --- a/tests/core/satmin2.test +++ b/tests/core/satmin2.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015, 2017 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2015, 2017, 2018 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -520,3 +520,8 @@ test "`cat out`" = 1 # Make sure no extra state are added. See issue #204 test 2 = `ltl2tgba a | autfilt --sat-minimize --stats=%s` + +# Make sure -B implies -S even for --sat-minimize. See issue #340. +ltl2tgba -G -D -f 'GF(a <-> XXb)' > aut +test 6 = "`autfilt -B --sat-minimize --stats=%s aut`" +test 6 = "`autfilt -B -S --sat-minimize --stats=%s aut`"