autfilt: fix --sat-minimize -B
Fixes #340. * bin/common_post.cc: -B implies -S. * tests/core/satmin2.test: Test this.
This commit is contained in:
parent
ee30f96676
commit
82796c04ae
3 changed files with 11 additions and 2 deletions
3
NEWS
3
NEWS
|
|
@ -35,6 +35,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:
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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`"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue