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

mc: rename ec_renault13lpar into lpar13

Browse source 
* 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
This commit is contained in:
Etienne Renault 2020-05-13 11:13:17 +02:00
parent b32e451292
commit ee01fdf209
4 changed files with 7 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/mc/Makefile.am
View file

@ -1,5 +1,5 @@
## -*- coding: utf-8 -*- ## -*- 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). ## Développement de l'Epita (LRDE).
## ##
## This file is part of Spot, a model checking library. ## 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) AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc 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 mc.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la noinst_LTLIBRARIES = libmc.la

6
spot/mc/ec.hh → spot/mc/lpar13.hh
View file

@ -33,7 +33,7 @@ namespace spot
/// the Gabow's one. /// the Gabow's one.
template<typename State, typename SuccIterator, template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual> typename StateHash, typename StateEqual>
class SPOT_API ec_renault13lpar class SPOT_API lpar13
{ {
struct product_state struct product_state
{ {
@ -75,7 +75,7 @@ namespace spot
return nullptr; // Useless return nullptr; // Useless
} }
ec_renault13lpar(kripkecube<State, SuccIterator>& sys, lpar13(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa, twacube_ptr twa,
shared_map& map, /* useless here */ shared_map& map, /* useless here */
shared_struct*, /* useless here */ shared_struct*, /* useless here */
@ -89,7 +89,7 @@ namespace spot
"error: does not match the kripkecube requirements"); "error: does not match the kripkecube requirements");
} }
virtual ~ec_renault13lpar() virtual ~lpar13()
{ {
map.clear(); map.clear();
} }

4
spot/mc/mc_instanciator.hh
View file

@ -25,7 +25,7 @@
#include <utility> #include <utility>
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/mc/mc.hh> #include <spot/mc/mc.hh>
#include <spot/mc/ec.hh> #include <spot/mc/lpar13.hh>
#include <spot/mc/deadlock.hh> #include <spot/mc/deadlock.hh>
#include <spot/mc/cndfs.hh> #include <spot/mc/cndfs.hh>
#include <spot/mc/bloemen.hh> #include <spot/mc/bloemen.hh>
@ -191,7 +191,7 @@ namespace spot
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::SWARMING: case mc_algorithm::SWARMING:
return instanciate<spot::ec_renault13lpar<State, Iterator, Hash, Equal>, return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
} }
} }

1
tests/ltsmin/modelcheck.cc
View file

@ -44,7 +44,6 @@
#include <thread> #include <thread>
#include <spot/twacube/twacube.hh> #include <spot/twacube/twacube.hh>
#include <spot/twacube_algos/convert.hh> #include <spot/twacube_algos/convert.hh>
#include <spot/mc/ec.hh>
const char argp_program_doc[] = const char argp_program_doc[] =
"Process model and formula to check wether a " "Process model and formula to check wether a "