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

sat_minimize: do not complete in the preproc step

Browse source 
Fixes #204.

* spot/twaalgos/dtwasat.cc (sat_minimize): Here.
* tests/core/satmin2.test: Add a test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-14 10:18:16 +01:00
parent 3ff2acb397
commit b210db8949
3 changed files with 99 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

16
spot/twaalgos/dtwasat.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -1446,9 +1446,7 @@ namespace spot
postprocessor post;
auto sba = (state_based && a->prop_state_acc()) ?
postprocessor::SBAcc : postprocessor::Any;
post.set_pref(postprocessor::Deterministic
| postprocessor::Complete
| sba);
post.set_pref(postprocessor::Deterministic | sba);
post.set_type(postprocessor::Generic);
postprocessor::optimization_level level;
switch (preproc)
@ -1477,10 +1475,10 @@ namespace spot
&& (target_is_buchi || !user_supplied_acc))
return a;
}
else
{
complete_here(a);
}
// We always complete ourself, and do not ask the above call to
// postprocessor to do it, because that extra state would be
// returned in the case of a WDBA.
complete_here(a);
if (states == -1 && max_states == -1)
{