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 09bbaa1e41
commit a9c457f93f
4 changed files with 31 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -24,6 +24,10 @@ New in spot 2.11.3.dev (not yet released)
multiple initial states (because Spot supports only one), the HOA
parser could break state-based acceptance. (Issue #522.)
- delay_branching_here(), a new optimization of Spot 2.11 had an
incorrectly handling of states without successors, causing some
segfaults. (Issue #524.)
New in spot 2.11.3 (2022-12-09)
Bug fixes:

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 \

39
spot/twaalgos/dbranch.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2022 Laboratoire de Recherche et Développement
// Copyright (C) 2022-2023 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -118,27 +118,30 @@ namespace spot
continue;
}
unsigned mergedst = it2->second;
// we have to merge canddst into mergedst. This is as
// simple as:
// we have to merge canddst into mergedst.
// This is as simple as:
// 1) connecting their list of transitions
unsigned& mergedfirst = g.state_storage(mergedst).succ;
unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
unsigned& candfirst = g.state_storage(canddst).succ;
unsigned& candlast = g.state_storage(canddst).succ_tail;
if (mergedlast)
aut->edge_storage(mergedlast).next_succ = candfirst;
else // mergedst had now successor
mergedfirst = candfirst;
mergedlast = candlast;
// 2) updating the source of the merged transitions
for (unsigned e2 = candfirst; e2 != 0;)
if (candlast)
{
auto& edge = aut->edge_storage(e2);
edge.src = mergedst;
e2 = edge.next_succ;
unsigned& mergedfirst = g.state_storage(mergedst).succ;
unsigned& mergedlast = g.state_storage(mergedst).succ_tail;
unsigned& candfirst = g.state_storage(canddst).succ;
if (mergedlast)
aut->edge_storage(mergedlast).next_succ = candfirst;
else // mergedst had no successor
mergedfirst = candfirst;
mergedlast = candlast;
// 2) updating the source of the merged transitions
for (unsigned e2 = candfirst; e2 != 0;)
{
auto& edge = aut->edge_storage(e2);
edge.src = mergedst;
e2 = edge.next_succ;
}
// 3) deleting the edge to canddst.
candfirst = candlast = 0;
}
// 3) deleting the edge to canddst.
candfirst = candlast = 0;
it.erase();
// 4) updating succ_cand
succ_cand[mergedst] += succ_cand[canddst];

5
tests/core/ltlcross.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012-2014, 2016, 2019 Laboratoire de Recherche et
# Copyright (C) 2012-2014, 2016, 2019, 2023 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -65,3 +65,6 @@ ltlcross -D \
# Spot 2.8. We use ltl2tgba twice so ltlcross build cross-products.
ltlcross --verbose ltl2tgba ltl2tgba \
-f '(G(F((a1)&(X(X(b1))))))&(G(F((a2)&(X(X(b2))))))&(G(F((a3)&(X(X(b3))))))'
# Issue #524.
ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))'