From ee01fdf20974de2218c2c0be4ff42d4c3bbc52af Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Wed, 13 May 2020 11:13:17 +0200 Subject: [PATCH] mc: rename ec_renault13lpar into lpar13 * spot/mc/ec.hh: Rename to ... * spot/mc/lpar13.hh: ... this. * spot/mc/Makefile.am, spot/mc/mc_instanciator.hh, tests/ltsmin/modelcheck.cc: Here --- spot/mc/Makefile.am | 4 ++-- spot/mc/{ec.hh => lpar13.hh} | 6 +++--- spot/mc/mc_instanciator.hh | 4 ++-- tests/ltsmin/modelcheck.cc | 1 - 4 files changed, 7 insertions(+), 8 deletions(-) rename spot/mc/{ec.hh => lpar13.hh} (99%) diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index 5307399bc..d0eb7fe68 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2015, 2016, 2017, 2019 Laboratoire de Recherche et +## Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -21,7 +21,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc -mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\ +mc_HEADERS = reachability.hh intersect.hh lpar13.hh unionfind.hh utils.hh\ mc.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh noinst_LTLIBRARIES = libmc.la diff --git a/spot/mc/ec.hh b/spot/mc/lpar13.hh similarity index 99% rename from spot/mc/ec.hh rename to spot/mc/lpar13.hh index 8f1b7e1cb..3c3f83fd4 100644 --- a/spot/mc/ec.hh +++ b/spot/mc/lpar13.hh @@ -33,7 +33,7 @@ namespace spot /// the Gabow's one. template - class SPOT_API ec_renault13lpar + class SPOT_API lpar13 { struct product_state { @@ -75,7 +75,7 @@ namespace spot return nullptr; // Useless } - ec_renault13lpar(kripkecube& sys, + lpar13(kripkecube& sys, twacube_ptr twa, shared_map& map, /* useless here */ shared_struct*, /* useless here */ @@ -89,7 +89,7 @@ namespace spot "error: does not match the kripkecube requirements"); } - virtual ~ec_renault13lpar() + virtual ~lpar13() { map.clear(); } diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh index 5f9267235..f89e9dae3 100644 --- a/spot/mc/mc_instanciator.hh +++ b/spot/mc/mc_instanciator.hh @@ -25,7 +25,7 @@ #include #include #include -#include +#include #include #include #include @@ -191,7 +191,7 @@ namespace spot kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); case mc_algorithm::SWARMING: - return instanciate, + return instanciate, kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); } } diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 55e474d97..acf35c447 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -44,7 +44,6 @@ #include #include #include -#include const char argp_program_doc[] = "Process model and formula to check wether a "