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

dbranch: fix handling of states without successors

Browse source 
Fixes #524, reported by Rüdiger Ehlers.

* spot/twaalgos/dbranch.cc: When merging an edge going to state
without successors simply delete it.
* bin/spot-x.cc: Typo in documentation.
* tests/core/ltlcross.test: Add a test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2023-01-23 11:59:49 +01:00
parent 39212bbcd2
commit 7e1d684797
4 changed files with 31 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

4
bin/spot-x.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -53,7 +53,7 @@ implication-based simplifications are attempted. Defaults to 16.") },
{ nullptr, 0, nullptr, 0, "Translation options:", 0 },
{ DOC("ltl-split", "Set to 0 to disable the translation of automata \
as product or sum of subformulas.") },
{ DOC("branch-prop", "Set to 0 to disable branching-postponement \
{ DOC("branch-post", "Set to 0 to disable branching-postponement \
(done during translation, may create more states) and delayed-branching \
(almost similar, but done after translation to only remove states). \
Set to 1 to force branching-postponement, and to 2 \