fix some typos
* spot/graph/graph.hh, spot/ltsmin/spins_kripke.hxx, spot/mc/bloemen.hh, spot/mc/lpar13.hh, spot/twaalgos/determinize.cc: Here.
This commit is contained in:
parent
583ca38d91
commit
9de5455552
5 changed files with 25 additions and 25 deletions
|
|
@ -1295,10 +1295,10 @@ namespace spot
|
||||||
static std::vector<std::thread> tv;
|
static std::vector<std::thread> tv;
|
||||||
SPOT_ASSERT(tv.empty());
|
SPOT_ASSERT(tv.empty());
|
||||||
tv.resize(nthreads);
|
tv.resize(nthreads);
|
||||||
// FIXME: Due to the way these thread advence into the sate
|
// FIXME: Due to the way these thread advance into the state
|
||||||
// vectors, they access very close memory location. It
|
// vector, they access very close memory location. It would
|
||||||
// would seems more cache friendly to have thread work on
|
// seems more cache friendly to have threads work on blocks
|
||||||
// blocks of continuous states.
|
// of continuous states.
|
||||||
for (unsigned id = 0; id < nthreads; ++id)
|
for (unsigned id = 0; id < nthreads; ++id)
|
||||||
tv[id] = std::thread(
|
tv[id] = std::thread(
|
||||||
[bne, id, ns, &idx_list, p, nthreads]()
|
[bne, id, ns, &idx_list, p, nthreads]()
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et
|
||||||
// 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.
|
||||||
//
|
//
|
||||||
|
|
@ -400,10 +400,10 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// FIXME I think we only need visbles aps, i.e. if the system has
|
// FIXME: I think we only need visible aps. E.g., if the system has
|
||||||
// following variables, i.e. P_0.var1 and P_0.var2 but the property
|
// variables P_0.var1 and P_0.var2 but the property automaton only
|
||||||
// automaton only mention P_0.var2, we do not need to capture (in
|
// mentions P_0.var2, we do not need to capture (in the resulting
|
||||||
// the resulting cube) any atomic proposition for P_0.var1
|
// cube) any atomic proposition for P_0.var1
|
||||||
void
|
void
|
||||||
kripkecube<cspins_state,
|
kripkecube<cspins_state,
|
||||||
cspins_iterator>::match_aps(std::vector<std::string>& aps,
|
cspins_iterator>::match_aps(std::vector<std::string>& aps,
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et
|
// Copyright (C) 2015-2020, 2022 Laboratoire de Recherche et
|
||||||
// Developpement de l'Epita
|
// Developpement de l'Epita
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -127,7 +127,7 @@ namespace spot
|
||||||
bool b = it.isnew();
|
bool b = it.isnew();
|
||||||
|
|
||||||
// Insertion failed, delete element
|
// Insertion failed, delete element
|
||||||
// FIXME Should we add a local cache to avoid useless allocations?
|
// FIXME: Should we add a local cache to avoid useless allocations?
|
||||||
if (!b)
|
if (!b)
|
||||||
p_.deallocate(v);
|
p_.deallocate(v);
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015-2016, 2018-2021 Laboratoire de Recherche et
|
// Copyright (C) 2015-2016, 2018-, 20222022 Laboratoire de Recherche et
|
||||||
// Developpement de l'Epita
|
// Developpement de l'Epita
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -32,9 +32,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
/// \brief This class implements the sequential emptiness check as
|
/// \brief This class implements the sequential emptiness check as
|
||||||
/// presented in "Three SCC-based Emptiness Checks for Generalized
|
/// presented in "Three SCC-based Emptiness Checks for Generalized
|
||||||
/// B\¨uchi Automata" (Renault et al, LPAR 2013). Among the three
|
/// Büchi Automata" (Renault et al, LPAR 2013). Among the three
|
||||||
/// emptiness check that has been proposed we opted to implement
|
/// emptiness checks that have been proposed, we opted to implement
|
||||||
/// the Gabow's one.
|
/// yGabow's one.
|
||||||
template<typename State, typename SuccIterator,
|
template<typename State, typename SuccIterator,
|
||||||
typename StateHash, typename StateEqual>
|
typename StateHash, typename StateEqual>
|
||||||
class SPOT_API lpar13
|
class SPOT_API lpar13
|
||||||
|
|
@ -62,8 +62,8 @@ namespace spot
|
||||||
size_t
|
size_t
|
||||||
operator()(const product_state that) const noexcept
|
operator()(const product_state that) const noexcept
|
||||||
{
|
{
|
||||||
// FIXME! wang32_hash(that.st_prop) could have
|
// FIXME: wang32_hash(that.st_prop) could have been
|
||||||
// been pre-calculated!
|
// pre-calculated!
|
||||||
StateHash hasher;
|
StateHash hasher;
|
||||||
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
|
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
|
||||||
}
|
}
|
||||||
|
|
@ -135,7 +135,7 @@ namespace spot
|
||||||
map[newtop])))
|
map[newtop])))
|
||||||
{
|
{
|
||||||
sys_.recycle(todo.back().it_kripke, tid_);
|
sys_.recycle(todo.back().it_kripke, tid_);
|
||||||
// FIXME a local storage for twacube iterator?
|
// FIXME: a local storage for twacube iterator?
|
||||||
todo.pop_back();
|
todo.pop_back();
|
||||||
if (SPOT_UNLIKELY(found_))
|
if (SPOT_UNLIKELY(found_))
|
||||||
{
|
{
|
||||||
|
|
@ -346,7 +346,7 @@ namespace spot
|
||||||
ctrx_element* current = front;
|
ctrx_element* current = front;
|
||||||
while (current != nullptr)
|
while (current != nullptr)
|
||||||
{
|
{
|
||||||
// FIXME also display acc?
|
// FIXME: also display acc?
|
||||||
res = res + " " +
|
res = res + " " +
|
||||||
std::to_string(current->prod_st->st_prop) +
|
std::to_string(current->prod_st->st_prop) +
|
||||||
+ "*" +
|
+ "*" +
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015-2021 Laboratoire de Recherche et
|
// Copyright (C) 2015-2022 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -476,7 +476,7 @@ namespace spot
|
||||||
std::vector<int> tmp;
|
std::vector<int> tmp;
|
||||||
while (brace >= 0)
|
while (brace >= 0)
|
||||||
{
|
{
|
||||||
// FIXME is not there a smarter way?
|
// FIXME: is there a smarter way?
|
||||||
tmp.insert(tmp.begin(), brace);
|
tmp.insert(tmp.begin(), brace);
|
||||||
brace = s.braces_[brace];
|
brace = s.braces_[brace];
|
||||||
}
|
}
|
||||||
|
|
@ -781,7 +781,7 @@ namespace spot
|
||||||
bool
|
bool
|
||||||
safra_state::operator<(const safra_state& other) const
|
safra_state::operator<(const safra_state& other) const
|
||||||
{
|
{
|
||||||
// FIXME what is the right, if any, comparison to perform?
|
// FIXME: what is the right, if any, comparison to perform?
|
||||||
return braces_ == other.braces_ ? nodes_ < other.nodes_
|
return braces_ == other.braces_ ? nodes_ < other.nodes_
|
||||||
: braces_ < other.braces_;
|
: braces_ < other.braces_;
|
||||||
}
|
}
|
||||||
|
|
@ -887,7 +887,7 @@ namespace spot
|
||||||
// NB spot::simulation() does not remove unreachable states, as it
|
// NB spot::simulation() does not remove unreachable states, as it
|
||||||
// would invalidate the contents of 'implications'.
|
// would invalidate the contents of 'implications'.
|
||||||
// so we need to explicitly test for unreachable states
|
// so we need to explicitly test for unreachable states
|
||||||
// FIXME based on the scc_info, we could remove the unreachable
|
// FIXME: based on the scc_info, we could remove the unreachable
|
||||||
// states, both in the input automaton and in 'implications'
|
// states, both in the input automaton and in 'implications'
|
||||||
// to reduce the size of 'implies'.
|
// to reduce the size of 'implies'.
|
||||||
if (!scc.reachable_state(i))
|
if (!scc.reachable_state(i))
|
||||||
|
|
@ -922,7 +922,7 @@ namespace spot
|
||||||
std::vector<bdd> support(aut->num_states());
|
std::vector<bdd> support(aut->num_states());
|
||||||
if (use_stutter && aut->prop_stutter_invariant())
|
if (use_stutter && aut->prop_stutter_invariant())
|
||||||
{
|
{
|
||||||
// FIXME this could be improved
|
// FIXME: this could be improved
|
||||||
// supports of states should account for possible stuttering if we plan
|
// supports of states should account for possible stuttering if we plan
|
||||||
// to use stuttering invariance
|
// to use stuttering invariance
|
||||||
for (unsigned c = 0; c != scc.scc_count(); ++c)
|
for (unsigned c = 0; c != scc.scc_count(); ++c)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue