Skip to content
This repository has been archived by the owner on Sep 16, 2024. It is now read-only.

Commit

Permalink
Fixed some minor assertions, and fixed the progress indication.
Browse files Browse the repository at this point in the history
  • Loading branch information
mlaveaux committed Sep 11, 2023
1 parent 96fdbad commit 98d22ee
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 4 deletions.
9 changes: 6 additions & 3 deletions libraries/lps/include/mcrl2/lps/explorer.h
Original file line number Diff line number Diff line change
Expand Up @@ -1074,7 +1074,7 @@ class explorer: public abortable
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
while (number_of_active_processes>0 || !todo->empty())
{
assert(thread_todo->empty());
assert(m_must_abort || thread_todo->empty());

if (!todo->empty())
{
Expand Down Expand Up @@ -1192,11 +1192,12 @@ class explorer: public abortable
// not empty, to take up more work.
number_of_active_processes--;
number_of_idle_processes++;
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads > 1) m_exclusive_state_access.lock();

assert(thread_todo->empty() || m_must_abort);
if (todo->empty())
{
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.unlock();
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads > 1) m_exclusive_state_access.unlock();
std::this_thread::sleep_for(std::chrono::milliseconds(100));
if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
}
Expand Down Expand Up @@ -1491,6 +1492,7 @@ class explorer: public abortable
{
throw mcrl2::runtime_error("Dfs exploration is not thread safe.");
}

for (const transition& tr: out_edges(s0, regular_summands, confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator))
{
if (m_must_abort)
Expand Down Expand Up @@ -1529,6 +1531,7 @@ class explorer: public abortable
}
}
gray.erase(s0);

finish_state(0, s0); // TODO MAKE THREAD SAFE
}

Expand Down
4 changes: 3 additions & 1 deletion libraries/lts/include/mcrl2/lts/state_space_generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -570,7 +570,8 @@ class progress_monitor
static std::mutex exclusive_print_mutex;
if (search_strategy == lps::es_breadth)
{
if (number_of_threads == 1 && ++count == level_up)
++count;
if (number_of_threads == 1 && count == level_up)
{
exclusive_print_mutex.lock();
mCRL2log(log::debug) << "Number of states at level " << level << " is " << state_count - last_state_count << "\n";
Expand All @@ -584,6 +585,7 @@ class progress_monitor
if (time(&new_log_time) > last_log_time.load(std::memory_order_relaxed))
{
exclusive_print_mutex.lock();

last_log_time = new_log_time;
std::size_t lvl_states = state_count - last_state_count;
std::size_t lvl_transitions = transition_count - last_transition_count;
Expand Down

0 comments on commit 98d22ee

Please sign in to comment.