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

ltsmin: remove useless code

Browse source 
* spot/ltsmin/spins_kripke.hh: here.
This commit is contained in:
Etienne Renault 2018-10-25 16:30:57 +02:00
parent d1200cb579
commit 7aa2d292cf
1 changed files with 1 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

19
spot/ltsmin/spins_kripke.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de // Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// l'Epita (LRDE) // l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -62,23 +62,6 @@ namespace spot
} }
}; };
/// \brief This class provides a hasher as required by the bricks classes
struct cspins_state_hasher
{
cspins_state_hasher(cspins_state&) { }
cspins_state_hasher() = default;
brick::hash::hash128_t hash(cspins_state t) const
{
// FIXME we should compute a better hash value for this particular
// case. Shall we use two differents hash functions?
return std::make_pair(t[0], t[0]);
}
bool equal(cspins_state lhs, cspins_state rhs) const
{
return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
}
};
/// \brief The management of states (i.e. allocation/deallocation) can /// \brief The management of states (i.e. allocation/deallocation) can
/// be painless since every time we have to consider wether the state will /// be painless since every time we have to consider wether the state will
/// be compressed or not. This class aims to simplify this management /// be compressed or not. This class aims to simplify this management