From d1aca565b5a73ff282d03d499145ecf47bd5e1d9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Jul 2016 18:11:21 +0200 Subject: [PATCH] remove the incorrect project_twa_run() It was bogus, and is better replaced by twa_run::project(). * NEWS, doc/org/upgrade2.org: Mention the removal. * spot/twaalgos/projrun.cc, spot/twaalgos/projrun.hh: Remove the files. * spot/twaalgos/Makefile.am: Adjust. --- NEWS | 4 ++++ doc/org/upgrade2.org | 2 +- spot/twaalgos/Makefile.am | 2 -- spot/twaalgos/projrun.cc | 44 ----------------------------------- spot/twaalgos/projrun.hh | 48 --------------------------------------- 5 files changed, 5 insertions(+), 95 deletions(-) delete mode 100644 spot/twaalgos/projrun.cc delete mode 100644 spot/twaalgos/projrun.hh diff --git a/NEWS b/NEWS index bb07e1899..595111478 100644 --- a/NEWS +++ b/NEWS @@ -93,6 +93,10 @@ New in spot 2.0.3a (not yet released) project a run found in a product onto one of the original operand. This is for instance used by autfilt --highlight-word. + The old spot::project_twa_run() function has been removed: it was + not used anywhere in Spot, and had an obvious bug in its + implementation, so it cannot be missed by anyone. + Python: * The __format__() method for formula support the same diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index e2618e4f5..8df4ff21c 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -286,7 +286,7 @@ that provide a function with a similar service. | ~tgbaalgos/neverclaim.hh~ | ~spot/twaalgos/neverclaim.hh~ | | | ~tgbaalgos/postproc.hh~ | ~spot/twaalgos/postproc.hh~ | | | ~tgbaalgos/powerset.hh~ | ~spot/twaalgos/powerset.hh~ | | -| ~tgbaalgos/projrun.hh~ | ~spot/twaalgos/projrun.hh~ | | +| ~tgbaalgos/projrun.hh~ | ~spot/twaalgos/emptiness.hh~ | use =twa_run::project()= since Spot 2.1 | | ~tgbaalgos/randomgraph.hh~ | ~spot/twaalgos/randomgraph.hh~ | | | ~tgbaalgos/reachiter.hh~ | ~spot/twaalgos/reachiter.hh~ | | | ~tgbaalgos/reducerun.hh~ | ~spot/twaalgos/emptiness.hh~ | now =twa_run::reduce()= | diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 48f0db39b..da694e374 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -59,7 +59,6 @@ twaalgos_HEADERS = \ postproc.hh \ powerset.hh \ product.hh \ - projrun.hh \ randomgraph.hh \ randomize.hh \ reachiter.hh \ @@ -115,7 +114,6 @@ libtwaalgos_la_SOURCES = \ postproc.cc \ powerset.cc \ product.cc \ - projrun.cc \ randomgraph.cc \ randomize.cc \ reachiter.cc \ diff --git a/spot/twaalgos/projrun.cc b/spot/twaalgos/projrun.cc deleted file mode 100644 index e8f1564db..000000000 --- a/spot/twaalgos/projrun.cc +++ /dev/null @@ -1,44 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include - -namespace spot -{ - - twa_run_ptr - project_twa_run(const const_twa_ptr& a_run, - const const_twa_ptr& a_proj, - const const_twa_run_ptr& run) - { - auto res = std::make_shared(a_proj); - for (auto& i: run->prefix) - res->prefix.emplace_back(a_run->project_state(i.s, a_proj), - i.label, i.acc); - for (auto& i: run->cycle) - res->prefix.emplace_back(a_run->project_state(i.s, a_proj), - i.label, i.acc); - return res; - } -} diff --git a/spot/twaalgos/projrun.hh b/spot/twaalgos/projrun.hh deleted file mode 100644 index c0db25177..000000000 --- a/spot/twaalgos/projrun.hh +++ /dev/null @@ -1,48 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include -#include -#include -#include - -namespace spot -{ - struct twa_run; - - /// \ingroup twa_run - /// \brief Project a twa_run on a tgba. - /// - /// If a twa_run has been generated on a product, or any other - /// on-the-fly algorithm with tgba operands, - /// - /// \param run the run to replay - /// \param a_run the automata on which the run was generated - /// \param a_proj the automata on which to project the run - /// \return true iff the run could be completed - SPOT_API twa_run_ptr - project_twa_run(const const_twa_ptr& a_run, - const const_twa_ptr& a_proj, - const const_twa_run_ptr& run); -}