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

remprop: reset no-terminal property

Browse source 
Reported by Yong Li.

* spot/twaalgos/remprop.cc: Here.
* tests/python/removeap.py: New test case.
* tests/Makefile.am: Add it.
* NEWS: Document the issue.
* THANKS: Add Yong Li.
This commit is contained in:
Alexandre Duret-Lutz 2019-06-02 09:00:08 +02:00
parent 03b8db0fed
commit 74786324f4
5 changed files with 46 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/twaalgos/remprop.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -162,6 +162,10 @@ namespace spot
}
}
if (res->prop_terminal().is_false())
// Non-terminal automata could become terminal.
res->prop_terminal(trival::maybe());
transform_accessible(aut, res, [&](unsigned, bdd& cond,
acc_cond::mark_t&, unsigned)
{