Commit 8abe78a7 authored by Thibault Allançon's avatar Thibault Allançon

mc: bitstate: fix sanity checks

* spot/mc/bitstate.hh: use pre-increment style
* spot/mc/mc.hh,
  tests/ltsmin/modelcheck.cc: fix > 80 columns
* spot/misc/hashfunc.hh: missing space before comma
parent ad75a210
Pipeline #17029 failed with stage
in 113 minutes and 23 seconds
......@@ -69,7 +69,7 @@ namespace spot
{
todo_.push_back(neighbor);
seen_.insert(neighbor);
state_number++;
++state_number;
}
}
}
......@@ -97,7 +97,7 @@ namespace spot
{
todo_.push_back(neighbor);
bf_->insert(state_hash(neighbor));
state_number++;
++state_number;
}
}
}
......
......@@ -425,7 +425,7 @@ namespace spot
std::cout << "\nBitstate hashing:\n";
std::cout << "DFS: " << s->dfs() << '\n';
std::cout << "DFS (bitstate hashing): " << s->dfs_bitstate_hashing() << '\n';
std::cout << "DFS (with BH): " << s->dfs_bitstate_hashing() << '\n';
delete s;
}
}
......@@ -67,7 +67,7 @@ namespace spot
/// \brief Jenkins lookup3 hash function.
///
/// https://burtleburtle.net/bob/c/lookup3.c
#define _jenkins_rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
#define _jenkins_rot(x, k) (((x)<<(k)) | ((x)>>(32-(k))))
inline size_t
lookup3_hash(size_t key)
{
......
......@@ -334,11 +334,11 @@ static int checked_main()
int memused = spot::memusage();
tm.start("deadlock check");
spot::bitstate_hashing<spot::ltsmin_kripkecube_ptr,
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>
(modelcube, mc_options.bitstate_mem_size);
spot::cspins_state,
spot::cspins_iterator,
spot::cspins_state_hash,
spot::cspins_state_equal>
(modelcube, mc_options.bitstate_mem_size);
tm.stop("deadlock check");
memused = spot::memusage() - memused;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment