Skip to content

Commit

Permalink
Print the number of nodes of the LDD of the state space
Browse files Browse the repository at this point in the history 
*) In verbose mode the number of nodes is printed, and the variable
order that was used
  • Loading branch information
@wiegerw
wiegerw committed Feb 22, 2021
1 parent a7b0c36 commit f5989c9
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 13 deletions.
7 changes: 7 additions & 0 deletions 3rd-party/sylvan/src/sylvan_ldd.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -409,6 +409,13 @@ inline double satcount(const ldd& A)
return lddmc_satcount(A.get());
}

// nodecount(A) = the number of nodes of the LDD A
inline
std::size_t nodecount(const ldd& A)
{
return lddmc_nodecount(A.get());
}

// sat_one(A) = an arbitrary vector from the set A
// returns the value of the leaf node (0 or 1)
template <typename OutputIterator>
Expand Down
15 changes: 9 additions & 6 deletions libraries/lps/include/mcrl2/lps/lpsreach.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,7 @@ class lpsreach_algorithm
data::data_expression_list m_initial_state;
std::vector<boost::dynamic_bitset<>> m_summand_patterns;
std::vector<boost::dynamic_bitset<>> m_group_patterns;
std::vector<std::size_t> m_variable_order;

ldd state2ldd(const data::data_expression_list& x)
{
Expand Down Expand Up @@ -219,13 +220,13 @@ class lpsreach_algorithm
m_summand_patterns = compute_read_write_patterns(lpsspec_);
lps::adjust_read_write_patterns(m_summand_patterns, m_options);

std::vector<std::size_t> variable_order = lps::compute_variable_order(m_options.variable_order, m_summand_patterns);
mCRL2log(log::debug) << "variable order = " << core::detail::print_list(variable_order) << std::endl;
m_summand_patterns = lps::reorder_read_write_patterns(m_summand_patterns, variable_order);
m_variable_order = lps::compute_variable_order(m_options.variable_order, m_summand_patterns);
mCRL2log(log::debug) << "variable order = " << core::detail::print_list(m_variable_order) << std::endl;
m_summand_patterns = lps::reorder_read_write_patterns(m_summand_patterns, m_variable_order);
mCRL2log(log::debug) << lps::print_read_write_patterns(m_summand_patterns);

m_process_parameters = permute_copy(m_process_parameters, variable_order);
m_initial_state = permute_copy(m_initial_state, variable_order);
m_process_parameters = permute_copy(m_process_parameters, m_variable_order);
m_initial_state = permute_copy(m_initial_state, m_variable_order);
mCRL2log(log::debug) << "process parameters = " << core::detail::print_list(m_process_parameters) << std::endl;
mCRL2log(log::debug) << "initial state = " << core::detail::print_list(m_initial_state) << std::endl;

Expand All @@ -242,7 +243,7 @@ class lpsreach_algorithm
m_group_patterns = lps::compute_summand_group_patterns(m_summand_patterns, groups);
for (std::size_t j = 0; j < m_group_patterns.size(); j++)
{
m_summand_groups.emplace_back(lpsspec_, m_process_parameters, groups[j], m_group_patterns[j], m_summand_patterns, variable_order);
m_summand_groups.emplace_back(lpsspec_, m_process_parameters, groups[j], m_group_patterns[j], m_summand_patterns, m_variable_order);
}

for (std::size_t i = 0; i < m_summand_groups.size(); i++)
Expand Down Expand Up @@ -300,6 +301,8 @@ class lpsreach_algorithm

elapsed_seconds = std::chrono::steady_clock::now() - start;
std::cout << "number of states = " << satcount(visited) << " (time = " << std::setprecision(2) << std::fixed << elapsed_seconds.count() << "s)" << std::endl;
mCRL2log(log::verbose) << "LDD size = " << nodecount(visited) << std::endl;
mCRL2log(log::verbose) << "used variable order = " << core::detail::print_list(m_variable_order) << std::endl;

return visited;
}
Expand Down
17 changes: 10 additions & 7 deletions libraries/pbes/include/mcrl2/pbes/pbesreach.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,7 @@ class pbesreach_algorithm
data::data_expression_list m_initial_state;
std::vector<boost::dynamic_bitset<>> m_summand_patterns;
std::vector<boost::dynamic_bitset<>> m_group_patterns;
std::vector<std::size_t> m_variable_order;

ldd state2ldd(const data::data_expression_list& x)
{
Expand Down Expand Up @@ -307,14 +308,14 @@ class pbesreach_algorithm
m_summand_patterns = compute_read_write_patterns(m_pbes, m_process_parameters);
lps::adjust_read_write_patterns(m_summand_patterns, m_options);

std::vector<std::size_t> variable_order = lps::compute_variable_order(m_options.variable_order, m_summand_patterns, true);
assert(variable_order[0] == 0); // It is required that the propositional variable name stays up front
mCRL2log(log::debug) << "variable order = " << core::detail::print_list(variable_order) << std::endl;
m_summand_patterns = lps::reorder_read_write_patterns(m_summand_patterns, variable_order);
m_variable_order = lps::compute_variable_order(m_options.variable_order, m_summand_patterns, true);
assert(m_variable_order[0] == 0); // It is required that the propositional variable name stays up front
mCRL2log(log::debug) << "variable order = " << core::detail::print_list(m_variable_order) << std::endl;
m_summand_patterns = lps::reorder_read_write_patterns(m_summand_patterns, m_variable_order);
mCRL2log(log::debug) << lps::print_read_write_patterns(m_summand_patterns);

m_process_parameters = lps::permute_copy(m_process_parameters, variable_order);
m_initial_state = lps::permute_copy(m_initial_state, variable_order);
m_process_parameters = lps::permute_copy(m_process_parameters, m_variable_order);
m_initial_state = lps::permute_copy(m_initial_state, m_variable_order);
mCRL2log(log::debug) << "process parameters = " << core::detail::print_list(m_process_parameters) << std::endl;
mCRL2log(log::debug) << "initial state = " << core::detail::print_list(m_initial_state) << std::endl;

Expand All @@ -326,7 +327,7 @@ class pbesreach_algorithm
m_group_patterns = lps::compute_summand_group_patterns(m_summand_patterns, groups);
for (std::size_t j = 0; j < m_group_patterns.size(); j++)
{
m_summand_groups.emplace_back(m_pbes, m_process_parameters, propvar_map, groups[j], m_group_patterns[j], m_summand_patterns, variable_order);
m_summand_groups.emplace_back(m_pbes, m_process_parameters, propvar_map, groups[j], m_group_patterns[j], m_summand_patterns, m_variable_order);
}

for (std::size_t i = 0; i < m_summand_groups.size(); i++)
Expand Down Expand Up @@ -401,6 +402,8 @@ class pbesreach_algorithm
{
mCRL2log(log::verbose) << "number of states = " << satcount(visited) << " (time = " << std::setprecision(2) << std::fixed << elapsed_seconds.count() << "s)" << std::endl;
}
mCRL2log(log::verbose) << "LDD size = " << nodecount(visited) << std::endl;
mCRL2log(log::verbose) << "used variable order = " << core::detail::print_list(m_variable_order) << std::endl;

if (!m_options.srf.empty())
{
Expand Down

0 comments on commit f5989c9

Please sign in to comment.