Commit fb59cab0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

emptiness: allow twa_run::as_twa to preserve names

* spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh: Here.
* tests/python/ltsmin-dve.ipynb: Add a test.
* NEWS: Mention the change.
parent 3f547089
......@@ -6,6 +6,10 @@ New in spot 2.3.0.dev (not yet released)
will select the best output automaton for each formula translated.
See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples.
Library:
- spot::twa_run::as_twa() has an option to preserve state names.
Bugs fixed:
- spot::otf_product() was incorrectly registering atomic
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -752,13 +752,20 @@ namespace spot
}
twa_graph_ptr
twa_run::as_twa() const
twa_run::as_twa(bool preserve_names) const
{
auto d = aut->get_dict();
auto res = make_twa_graph(d);
res->copy_ap_of(aut);
res->copy_acceptance_of(aut);
std::vector<std::string>* names= nullptr;
if (preserve_names)
{
names = new std::vector<std::string>;
res->set_named_prop("state-names", names);
}
const state* s = aut->get_init_state();
unsigned src;
unsigned dst;
......@@ -777,6 +784,8 @@ namespace spot
assert(s->compare(i->s) == 0);
src = res->new_state();
seen.emplace(i->s, src);
if (names)
names->push_back(aut->format_state(s));
for (; i != l->end();)
{
......@@ -826,7 +835,15 @@ namespace spot
auto p = seen.emplace(next, 0);
if (p.second)
p.first->second = res->new_state();
{
unsigned ns = res->new_state();
p.first->second = ns;
if (names)
{
assert(ns = names->size());
names->push_back(aut->format_state(next));
}
}
dst = p.first->second;
res->new_edge(src, dst, label, acc);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -438,7 +438,10 @@ namespace spot
/// \brief Return a twa_graph_ptr corresponding to \a run
///
/// Identical states are merged.
twa_graph_ptr as_twa() const;
///
/// If \a preserve_names is set, the created states are named
/// using the format_state() result from the original state.
twa_graph_ptr as_twa(bool preserve_names = false) const;
/// \brief Display a twa_run.
///
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment