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

tgba_complete: rename as complete and export in Python

Browse source 
* src/twaalgos/complete.cc, src/twaalgos/complete.hh
(tgba_complete, tgba_complete_here): Rename as...
(complete, complete_here): ... these.  Also fix useless output of
acceptance marks on transition leading to the sink when the automaton
does not use state-based acceptance.
* src/tests/ikwiad.cc, src/twaalgos/dtgbacomp.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/postproc.cc,
src/twaalgos/product.cc: Adjust.
* wrap/python/spot_impl.i: Export these function.
* wrap/python/tests/automata.ipynb: Test spot.complete().
This commit is contained in:
Alexandre Duret-Lutz 2015-10-02 16:45:39 +02:00
parent afe5b2a1c0
commit 5e07e8384d
9 changed files with 257 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/twaalgos/complete.cc
View file

@ -21,7 +21,7 @@
namespace spot
{
unsigned tgba_complete_here(twa_graph_ptr aut)
unsigned complete_here(twa_graph_ptr aut)
{
unsigned n = aut->num_states();
unsigned sink = -1U;
@ -104,6 +104,8 @@ namespace spot
}
// In case the automaton use state-based acceptance, propagate
// the acceptance of the first edge to the one we add.
if (!aut->has_state_based_acc())
acc = 0U;
aut->new_edge(i, sink, missingcond, acc);
}
}
@ -117,7 +119,7 @@ namespace spot
return sink;
}
twa_graph_ptr tgba_complete(const const_twa_ptr& aut)
twa_graph_ptr complete(const const_twa_ptr& aut)
{
auto res = make_twa_graph(aut, {
true, // state based
@ -125,7 +127,7 @@ namespace spot
true, // deterministic
true, // stutter inv.
});
tgba_complete_here(res);
complete_here(res);
return res;
}

14
src/twaalgos/complete.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -25,15 +25,15 @@ namespace spot
{
/// \brief Complete a twa_graph in place.
///
/// If the tgba has no acceptance set, one will be added. The
/// If the TωA has no acceptance set, one will be added. The
/// returned value is the number of the sink state (it can be a new
/// state added for completion, or an existing non-accepting state
/// that has been reused as sink state because it had no outgoing
/// transitions apart from self-loops.)
SPOT_API unsigned tgba_complete_here(twa_graph_ptr aut);
SPOT_API unsigned complete_here(twa_graph_ptr aut);
/// \brief Clone a tgba and complete it.
/// \brief Clone a twa and complete it.
///
/// If the tgba has no acceptance set, one will be added.
SPOT_API twa_graph_ptr tgba_complete(const const_twa_ptr& aut);
/// If the twa has no acceptance set, one will be added.
SPOT_API twa_graph_ptr complete(const const_twa_ptr& aut);
}

2
src/twaalgos/dtgbacomp.cc
View file

@ -178,7 +178,7 @@ namespace spot
{
// Simply complete the automaton, and complement its
// acceptance.
auto res = cleanup_acceptance_here(tgba_complete(aut));
auto res = cleanup_acceptance_here(complete(aut));
res->set_acceptance(res->num_sets(),
res->get_acceptance().complement());
return res;

2
src/twaalgos/dtgbasat.cc
View file

@ -1339,7 +1339,7 @@ namespace spot
}
else
{
tgba_complete_here(a);
complete_here(a);
}
if (states == -1 && max_states == -1)

10
src/twaalgos/postproc.cc
View file

@ -156,7 +156,7 @@ namespace spot
|| (type_ == Monitor && a->num_sets() == 0))
{
if (COMP_)
a = tgba_complete(a);
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
@ -207,7 +207,7 @@ namespace spot
a = m;
}
if (COMP_)
a = tgba_complete(a);
a = complete(a);
return a;
}
@ -216,7 +216,7 @@ namespace spot
if (type_ == BA)
a = do_degen(a);
if (COMP_)
a = tgba_complete(a);
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
@ -380,7 +380,7 @@ namespace spot
in = dba;
}
const_twa_graph_ptr res = tgba_complete(in);
const_twa_graph_ptr res = complete(in);
if (target_acc == 1)
{
if (sat_states_ != -1)
@ -457,7 +457,7 @@ namespace spot
sim = dba ? dba : sim;
if (COMP_)
sim = tgba_complete(sim);
sim = complete(sim);
if (SBACC_)
sim = sbacc(sim);

4
src/twaalgos/product.cc
View file

@ -136,8 +136,8 @@ namespace spot
unsigned left_state,
unsigned right_state)
{
return product_aux(tgba_complete(left),
tgba_complete(right),
return product_aux(complete(left),
complete(right),
left_state, right_state, false);
}