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

formula: avoid id clash for atomic propositions

Browse source 
This corrects a bug that has never been observed yet, has it would
require more than UINT_MAX formulas allocations.

* spot/tl/formula.cc, spot/tl/formula.hh: Bump the formula ID in the
unlikely case a new atomic proposition would receive the same id as a
previous one.
This commit is contained in:
Alexandre Duret-Lutz 2019-10-17 11:22:50 +02:00
parent f7bec7eae9
commit 64e3fcfb54
2 changed files with 28 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

33
spot/tl/formula.cc
View file

@ -1053,9 +1053,15 @@ namespace spot
auto ires = m.name2ap.emplace(name, nullptr);
if (!ires.second)
return ires.first->second->clone();
// Name the formula before creating it, because
// the constructor will call ap_name().
m.ap2name.emplace(next_id_, name);
// Name the formula before creating it, because the constructor
// will call ap_name().
//
// We plan to use next_id_ for identifier, but it is possible that
// next_id_ has already wrapped around 0 and that next_id_ is
// already the name of another atomic proposition. In that
// unlikely case, simply increment the id.
while (SPOT_UNLIKELY(!m.ap2name.emplace(next_id_, name).second))
bump_next_id();
// next_id_ is incremented by setup_props(), called by the
// constructor of fnode
return ires.first->second = new fnode(op::ap, {});
@ -1072,6 +1078,19 @@ namespace spot
}
size_t fnode::next_id_ = 0U;
size_t fnode::bump_next_id()
{
size_t id = next_id_++;
// If the counter of formulae ever loops, we want to skip the
// first three values, because they are permanently associated
// to constants, and it is convenient to have constants
// smaller than all other formulas.
if (SPOT_UNLIKELY(next_id_ == 0))
next_id_ = 3;
return id;
}
const fnode* fnode::ff_ = new fnode(op::ff, {});
const fnode* fnode::tt_ = new fnode(op::tt, {});
const fnode* fnode::ew_ = new fnode(op::eword, {});
@ -1079,13 +1098,7 @@ namespace spot
void fnode::setup_props(op o)
{
id_ = next_id_++;
// If the counter of formulae ever loops, we want to skip the
// first three values, because they are permanently associated
// to constants, and it is convenient to have constants
// smaller than all other formulas.
if (SPOT_UNLIKELY(next_id_ == 0))
next_id_ = 3;
id_ = bump_next_id();
switch (o)
{

9
spot/tl/formula.hh
View file

@ -504,6 +504,7 @@ namespace spot
}
private:
static size_t bump_next_id();
void setup_props(op o);
void destroy_aux() const;
@ -790,9 +791,9 @@ namespace spot
if (id() > other.id())
return false;
// The case where id()==other.id() but ptr_ != other.ptr_ is
// very unlikely (we would need to build more that UINT_MAX
// formulas), so let's just compare pointer, and ignore the fact
// that it may give some nondeterminism.
// very unlikely (we would need to build more than UINT_MAX
// formulas), so let's just compare pointers, and ignore the
// fact that it may introduce some nondeterminism.
return ptr_ < other.ptr_;
}
@ -1402,7 +1403,7 @@ namespace spot
/// Can be used as a hash number.
///
/// The id is almost unique as it is an unsigned number
/// incremented at each formula construction, and the unsigned may
/// incremented for each formula construction, and the number may
/// wrap around zero. If this is used for ordering, make sure to
/// deal with equality
size_t id() const