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

complete: do not force Büchi on universal automata

Browse source 
* spot/twaalgos/complete.hh: Adjust documentation.
* spot/twaalgos/complete.cc: If the acceptance condition is a
tautology, delay the forcing of Büchi acceptance until we are sure it
is needed.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2022-05-19 16:38:02 +02:00
parent 3b8e11322b
commit f784e40548
3 changed files with 27 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -82,6 +82,9 @@ New in spot 2.10.6.dev (not yet released)
averted in the parser by delaying the construction of such n-ary
nodes until all children are known.
- complement() used to always turn tautological acceptance conditions
into Büchi. It now only does that if the automaton is modified.
New in spot 2.10.6 (2022-05-18)
Bugs fixed:

24
spot/twaalgos/complete.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2013-2018, 2022 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -29,6 +29,8 @@ namespace spot
return;
unsigned n = aut->num_states();
bool need_acc_fix = false;
// UM is a pair (bool, mark). If the Boolean is false, the
// acceptance is always satisfiable. Otherwise, MARK is an
// example of unsatisfiable mark.
@ -36,10 +38,11 @@ namespace spot
if (!um.first)
{
// We cannot safely complete an automaton if its
// acceptance is always satisfiable.
auto acc = aut->set_buchi();
for (auto& t: aut->edge_vector())
t.acc = acc;
// acceptance is always satisfiable, so we will
// have to fix the acceptance automaton. However
// postpone that until we are sure that the
// automaton really need to be completed.
need_acc_fix = true;
}
else
{
@ -129,6 +132,8 @@ namespace spot
// acceptance sets as the last outgoing edge of the
// state.
acc = t.acc;
// If a state already has a edge to a sink, remember it
// so we can add the missing conditions to it.
if (t.dst == sink)
edge_to_sink = aut->edge_number(t);
}
@ -136,6 +141,15 @@ namespace spot
// edge to some sink state.
if (missingcond != bddfalse)
{
if (need_acc_fix)
{
auto a = aut->set_buchi();
for (auto& t: aut->edge_vector())
t.acc = a;
if (aut->num_edges())
acc = a;
need_acc_fix = false;
}
// If we haven't found any sink, simply add one.
if (sink == -1U)
{

9
spot/twaalgos/complete.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
// Copyright (C) 2013-2015, 2017, 2022 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -25,12 +25,13 @@ namespace spot
{
/// \brief Complete a twa_graph in place.
///
/// If the TωA has an acceptance condition that is a tautology,
/// it will be changed into a Büchi automaton.
/// If the TωA is incomplete and has an acceptance condition that is
/// a tautology, it will be changed into a Büchi automaton.
SPOT_API void complete_here(twa_graph_ptr aut);
/// \brief Clone a twa and complete it.
///
/// If the twa has no acceptance set, one will be added.
/// If the TωA is incomplete and has an acceptance condition that is
/// a tautology, it will be changed into a Büchi automaton.
SPOT_API twa_graph_ptr complete(const const_twa_ptr& aut);
}