Skip to content

Commit

Permalink
Applied a fix to the copy information in union_cube
Browse files Browse the repository at this point in the history 
*) It turned out that the settings in the copy parameter of union_cube
were still wrong. This wasn't detected due to insufficient testing.
Again with the help of Jeroen Meijer this problem has been fixed now.
  • Loading branch information
@wiegerw
wiegerw committed Feb 9, 2021
1 parent 3e0b721 commit 86e903e
Show file tree
Hide file tree
Showing 3 changed files with 46 additions and 20 deletions.
9 changes: 8 additions & 1 deletion libraries/lps/include/mcrl2/lps/symbolic_reachability.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,12 @@ std::vector<T> as_vector(const atermpp::term_list<T>& x)
return std::vector<T>(x.begin(), x.end());
}

template <typename T>
std::vector<T> as_vector(const std::set<T>& x)
{
return std::vector<T>(x.begin(), x.end());
}

template <typename T>
std::set<T> as_set(const atermpp::term_list<T>& x)
{
Expand Down Expand Up @@ -414,6 +420,7 @@ std::ostream& operator<<(std::ostream& out, const summand_group& x)
out << "condition = " << smd.condition << std::endl;
out << "variables = " << core::detail::print_list(smd.variables) << std::endl;
out << "next state = " << core::detail::print_list(smd.next_state) << std::endl;
out << "copy = " << core::detail::print_list(smd.copy) << std::endl;
std::vector<std::string> assignments;
auto vi = x.write_parameters.begin();
auto ni = smd.next_state.begin();
Expand Down Expand Up @@ -718,7 +725,7 @@ void learn_successors_callback(WorkerP*, Task*, std::uint32_t* x, std::size_t n,
}
mCRL2log(log::debug) << " " << print_transition(data_index, xy, group.read, group.write) << std::endl;
group.Ldomain = union_cube(group.Ldomain, x, x_size);
group.L = union_cube_copy(group.L, xy, smd.copy.data(), xy_size);
group.L = algorithm.m_options.no_relprod ? union_cube(group.L, xy, xy_size) : union_cube_copy(group.L, xy, smd.copy.data(), xy_size);
return false;
},
data::is_false
Expand Down
32 changes: 21 additions & 11 deletions tools/developer/lpsreach/lpsreach.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,24 +98,34 @@ std::vector<boost::dynamic_bitset<>> read_write_patterns(const lps::specificatio

struct summand_group: public lps::summand_group
{
summand_group(const lps::specification& lpsspec, const std::set<std::size_t>& summand_indices, const boost::dynamic_bitset<>& read_write_pattern, const std::vector<boost::dynamic_bitset<>>& read_write_patterns)
: lps::summand_group(lpsspec.process().process_parameters(), read_write_pattern)
summand_group(const lps::specification& lpsspec, const std::set<std::size_t>& group_indices, const boost::dynamic_bitset<>& group_pattern, const std::vector<boost::dynamic_bitset<>>& read_write_patterns)
: lps::summand_group(lpsspec.process().process_parameters(), group_pattern)
{
using lps::project;
using utilities::as_vector;
using utilities::as_set;
using utilities::detail::set_union;

std::set<std::size_t> used;
for (std::size_t j: read)
{
used.insert(2*j);
}
for (std::size_t j: write)
{
used.insert(2*j + 1);
}

const auto& lps_summands = lpsspec.process().action_summands();
const auto& process_parameters = lpsspec.process().process_parameters();
for (std::size_t i: summand_indices)

for (std::size_t i: group_indices)
{
std::vector<int> copy(read.size(), 0);
for (std::size_t j = 0; j < write.size(); j++)
std::vector<int> copy;
for (std::size_t j: used)
{
bool r = read_write_pattern[2*j];
bool w = read_write_pattern[2*j+1];
bool ri = read_write_patterns[i][2*j];
bool wi = read_write_patterns[i][2*j+1];
copy.push_back(!ri && !wi && !r && w);
bool b = read_write_patterns[i][j];
copy.push_back(b ? 0 : 1);
}
const auto& smd = lps_summands[i];
summands.emplace_back(smd.condition(), smd.summation_variables(), project(as_vector(smd.next_state(process_parameters)), write), copy);
Expand Down Expand Up @@ -217,7 +227,7 @@ class lpsreach_algorithm
std::vector<boost::dynamic_bitset<>> group_patterns = lps::compute_summand_group_patterns(patterns, groups);
for (std::size_t j = 0; j < group_patterns.size(); j++)
{
m_summand_groups.emplace_back(lpsspec_, groups[j], group_patterns[j], group_patterns);
m_summand_groups.emplace_back(lpsspec_, groups[j], group_patterns[j], patterns);
}

for (std::size_t i = 0; i < m_summand_groups.size(); i++)
Expand Down
25 changes: 17 additions & 8 deletions tools/developer/pbesreach/pbesreach.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,8 +163,20 @@ struct summand_group: public lps::summand_group
{
using lps::project;
using utilities::as_vector;
using utilities::as_set;
using utilities::detail::set_union;
using utilities::detail::contains;

std::set<std::size_t> used;
for (std::size_t j: read)
{
used.insert(2*j);
}
for (std::size_t j: write)
{
used.insert(2*j + 1);
}

const auto& equations = pbesspec.equations();
std::size_t k = 0;
for (std::size_t i = 0; i < equations.size(); i++)
Expand All @@ -175,14 +187,11 @@ struct summand_group: public lps::summand_group
{
if (contains(summand_group_indices, k))
{
std::vector<int> copy(read.size(), 0);
for (std::size_t q = 0; q < write.size(); q++)
std::vector<int> copy;
for (std::size_t q: used)
{
bool r = read_write_pattern[2*q];
bool w = read_write_pattern[2*q+1];
bool rk = read_write_patterns[k][2*q];
bool wk = read_write_patterns[k][2*q+1];
copy.push_back(!rk && !wk && !r && w);
bool b = read_write_patterns[k][q];
copy.push_back(b ? 0 : 1);
}
const pbes_system::srf_summand& smd = equation_summands[j];
summands.emplace_back(data::and_(data::equal_to(process_parameters.front(), propvar_map.at(X_i)), smd.condition()), smd.parameters(), project(as_vector(make_state(smd.variable(), propvar_map)), write), copy);
Expand Down Expand Up @@ -303,7 +312,7 @@ class pbesreach_algorithm
std::vector<boost::dynamic_bitset<>> group_patterns = lps::compute_summand_group_patterns(patterns, groups);
for (std::size_t j = 0; j < group_patterns.size(); j++)
{
m_summand_groups.emplace_back(m_pbes, m_process_parameters, propvar_map, groups[j], group_patterns[j], group_patterns);
m_summand_groups.emplace_back(m_pbes, m_process_parameters, propvar_map, groups[j], group_patterns[j], patterns);
}

for (std::size_t i = 0; i < m_summand_groups.size(); i++)
Expand Down

0 comments on commit 86e903e

Please sign in to comment.