diff --git a/.gitignore b/.gitignore index 52d8b1c637..a4af938140 100644 --- a/.gitignore +++ b/.gitignore @@ -14,6 +14,7 @@ build/ .cache # Ignore IDE files +.idea .vscode # Ignore the python virtual environment diff --git a/libraries/atermpp/include/mcrl2/atermpp/aterm_list.h b/libraries/atermpp/include/mcrl2/atermpp/aterm_list.h index 110ad44223..6bcbf4923a 100644 --- a/libraries/atermpp/include/mcrl2/atermpp/aterm_list.h +++ b/libraries/atermpp/include/mcrl2/atermpp/aterm_list.h @@ -423,7 +423,7 @@ void make_term_list(term_list& target, Iter first, Iter last, const ATermC /// \param target The variable to which the list is assigned. /// \param first The start of a range of elements. /// \param last The end of a range of elements. -/// \param convert_to_aterm A class with a () operation, whic is applied to each element +/// \param convert_to_aterm A class with a () operation, which is applied to each element /// before it is put into the list. /// \param aterm_filter A class with an operator () that is used to determine whether elements can be inserted in the list. template diff --git a/libraries/lps/include/mcrl2/lps/linearise.h b/libraries/lps/include/mcrl2/lps/linearise.h index 0f2d3eae4f..0ee87990e9 100644 --- a/libraries/lps/include/mcrl2/lps/linearise.h +++ b/libraries/lps/include/mcrl2/lps/linearise.h @@ -69,7 +69,7 @@ struct t_lin_options /// \exception mcrl2::runtime_error Linearisation failed mcrl2::lps::stochastic_specification linearise( const mcrl2::process::process_specification& type_checked_spec, - mcrl2::lps::t_lin_options lin_options = t_lin_options()); + const mcrl2::lps::t_lin_options& lin_options = t_lin_options()); /// \brief Linearises a process specification from a textual specification /// \param[in] text A string containing a process specification @@ -78,7 +78,7 @@ mcrl2::lps::stochastic_specification linearise( /// \exception mcrl2::runtime_error Linearisation failed inline mcrl2::lps::stochastic_specification linearise( const std::string& text, - mcrl2::lps::t_lin_options lin_options = t_lin_options()) + const mcrl2::lps::t_lin_options& lin_options = t_lin_options()) { mcrl2::process::process_specification spec = mcrl2::process::parse_process_specification(text); diff --git a/libraries/lps/include/mcrl2/lps/linearise_allow_block.h b/libraries/lps/include/mcrl2/lps/linearise_allow_block.h new file mode 100644 index 0000000000..7c14583ed7 --- /dev/null +++ b/libraries/lps/include/mcrl2/lps/linearise_allow_block.h @@ -0,0 +1,258 @@ +// Author(s): Jan Friso Groote, Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file mcrl2/lps/linearise_allow_block.h +/// \brief Apply the allow and block operators to summands. + +#ifndef MCRL2_LPS_LINEARISE_ALLLOW_BLOCK_H +#define MCRL2_LPS_LINEARISE_ALLLOW_BLOCK_H + +#include "mcrl2/atermpp/aterm_list.h" +#include "mcrl2/lps/deadlock_summand.h" +#include "mcrl2/lps/stochastic_action_summand.h" +#include "mcrl2/lps/linearise_utility.h" +#include "mcrl2/process/process_expression.h" + + +namespace mcrl2 +{ + +namespace lps +{ + +/**************** allow/block *************************************/ + +/// Determine if allow_action allows multi_action. +/// +/// \param allow_action A sorted action_name_multiset a1|...|an +/// \param multi_action A multiaction b1(d1)|...|bm(dm) +/// \param termination_action The action that encodes successful termination (used only in debug mode) +/// \returns n == m and ai == bi for 1 <= i <= n +inline +bool allow_(const process::action_name_multiset& allow_action, + const process::action_list& multi_action, + const process::action& termination_action) +{ + /* The special cases where multiaction==tau and multiaction=={ Terminated } must have been + dealt with separately. */ + assert(!multi_action.empty()); + assert(multi_action != process::action_list({ termination_action })); + assert(std::is_sorted(allow_action.names().begin(), allow_action.names().end(), action_name_compare())); + assert(std::is_sorted(multi_action.begin(), multi_action.end(), action_compare())); + + const core::identifier_string_list& names = allow_action.names(); + if (names.size() != multi_action.size()) + { + return false; + } + + core::identifier_string_list::const_iterator names_it = names.begin(); + process::action_list::const_iterator multiaction_it = multi_action.begin(); + + while (names_it != names.end()) + { + if (*names_it != multiaction_it->label().name()) + { + return false; + } + ++names_it; + ++multiaction_it; + } + + assert(names_it == names.end()); + assert(multiaction_it == multi_action.end()); + + return true; +} + +/// \brief Determine if multi_action is allowed by an allow expression in allow_list +/// +/// Calculates if the names of the action in multi_action match with an expression in allow_list. +/// If multi_action is the termination action, or multi_action is the empty multiaction, the result is also true. +inline +bool allow_(const process::action_name_multiset_list& allow_list, + const process::action_list& multi_action, + const process::action& termination_action) +{ + // The empty multiaction and the termination action can never be blocked by allows. + if (multi_action.empty() || multi_action == process::action_list({ termination_action })) + { + return true; + } + + for (const process::action_name_multiset& allow_action: allow_list) + { + if (allow_(allow_action, multi_action, termination_action)) + { + return true; + } + } + return false; +} + +/// \brief Calculate if any of the actions in multiaction is blocked by encap_list. +/// +/// \param encap_list is a list of action_name_multisets of size 1. Its single element contains all the blocked actions. +/// \param multi_action contains a multiaction a1(d1)|...|an(dn) +/// \returns \exists i: ai \in encap_list +inline +bool encap(const process::action_name_multiset_list& encaplist, const process::action_list& multiaction) +{ + assert(encaplist.size() == 1); + assert(std::is_sorted(multiaction.begin(), multiaction.end(), action_compare())); + + const core::identifier_string_list& blocked_actions = encaplist.front().names(); + assert(std::is_sorted(blocked_actions.begin(), blocked_actions.end(), action_name_compare())); + + core::identifier_string_list::const_iterator blocked_actions_it = blocked_actions.begin(); + process::action_list::const_iterator multiaction_it = multiaction.begin(); + + while (blocked_actions_it != blocked_actions.end() && multiaction_it != multiaction.end()) + { + if (*blocked_actions_it == multiaction_it->label().name()) + { + return true; + } + + if (action_name_compare()(*blocked_actions_it, multiaction_it->label().name())) + { + ++blocked_actions_it; + } + else + { + // The following assertion should hold because blocked_actions_it is not less than or equal to the name + // of multiaction_it + assert(action_name_compare()(multiaction_it->label().name(), *blocked_actions_it)); + ++multiaction_it; + } + } + + return false; +} + +/// Calculate the application of the allow or block operator over the action +/// summands. +/// +/// \param allowlist1 the allowset. If is_allow is false, the list has length 1, +/// and its only element contains the blocked actions. +/// \param is_allow determines if we calculate the allow or the block operator +/// \param action_summands the summands over which to compute the operator +/// \param deadlock_summands the deadlock summands tha may be extended. +/// \param termination_action the termination action generated by the linearizer. This action is always allowed. +/// \param ignore_time if true, and nodeltaelimination is false, a true->delta summand is added that subsumes all other deadlock summands +/// \param nodeltaaelimination do not eliminate deadlock summands. +void allowblockcomposition( + const process::action_name_multiset_list& allowlist1, // This is a list of list of identifierstring. + const bool is_allow, + stochastic_action_summand_vector& action_summands, + deadlock_summand_vector& deadlock_summands, + const process::action& termination_action, + bool ignore_time, + bool nodeltaelimination) + { + /* This function calculates the allow or the block operator, + depending on whether is_allow is true */ + + stochastic_action_summand_vector sourcesumlist; + action_summands.swap(sourcesumlist); + + deadlock_summand_vector resultdeltasumlist; + deadlock_summand_vector resultsimpledeltasumlist; + deadlock_summands.swap(resultdeltasumlist); + + process::action_name_multiset_list allowlist((is_allow)?sort_multi_action_labels(allowlist1):allowlist1); + + std::size_t sourcesumlist_length=sourcesumlist.size(); + if (sourcesumlist_length>2 || is_allow) // This condition prevents this message to be printed + // when performing data elimination. In this case the + // term delta is linearised, to determine which data + // is essential for all processes. In these cases a + // message about the block operator is very confusing. + { + mCRL2log(mcrl2::log::verbose) << "- calculating the " << (is_allow?"allow":"block") << + " operator on " << sourcesumlist.size() << " action summands and " << resultdeltasumlist.size() << " delta summands"; + } + + /* First add the resulting sums in two separate lists + one for actions, and one for delta's. The delta's + are added at the end to the actions, where for + each delta summand it is determined whether it ought + to be added, or is superseded by an action or another + delta summand */ + for (const stochastic_action_summand& smmnd: sourcesumlist) + { + const data::variable_list& sumvars=smmnd.summation_variables(); + const process::action_list& multiaction=smmnd.multi_action().actions(); + const data::data_expression& actiontime=smmnd.multi_action().time(); + const data::data_expression& condition=smmnd.condition(); + + // Explicitly allow the termination action in any allow. + if ((is_allow && allow_(allowlist,multiaction,termination_action)) || + (!is_allow && !encap(allowlist,multiaction))) + { + action_summands.push_back(smmnd); + } + else + { + if (smmnd.has_time()) + { + resultdeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock(actiontime))); + } + else + { + // summand has no time. + if (condition==data::sort_bool::true_()) + { + resultsimpledeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock())); + } + else + { + resultdeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock())); + } + } + } + } + + if (nodeltaelimination) + { + deadlock_summands.swap(resultsimpledeltasumlist); + copy(resultdeltasumlist.begin(),resultdeltasumlist.end(),back_inserter(deadlock_summands)); + } + else + { + if (!ignore_time) /* if a delta summand is added, conditional, timed + delta's are subsumed and do not need to be added */ + { + for (const deadlock_summand& summand: resultsimpledeltasumlist) + { + insert_timed_delta_summand(action_summands,deadlock_summands,summand,ignore_time); + } + for (const deadlock_summand& summand: resultdeltasumlist) + { + insert_timed_delta_summand(action_summands,deadlock_summands,summand,ignore_time); + } + } + else + { + // Add a true -> delta + insert_timed_delta_summand(action_summands,deadlock_summands,deadlock_summand(data::variable_list(),data::sort_bool::true_(),deadlock()), ignore_time); + } + } + if (mCRL2logEnabled(mcrl2::log::verbose) && (sourcesumlist_length>2 || is_allow)) + { + mCRL2log(mcrl2::log::verbose) << ", resulting in " << action_summands.size() << " action summands and " << deadlock_summands.size() << " delta summands\n"; + } + } + +} // namespace lps + +} // namespace mcrl2 + + + +#endif // MCRL2_LPS_LINEARISE_ALLLOW_BLOCK_H diff --git a/libraries/lps/include/mcrl2/lps/linearise_communication.h b/libraries/lps/include/mcrl2/lps/linearise_communication.h new file mode 100644 index 0000000000..17cae9d9e9 --- /dev/null +++ b/libraries/lps/include/mcrl2/lps/linearise_communication.h @@ -0,0 +1,864 @@ +// Author(s): Jan Friso Groote, Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file mcrl2/lps/linearise_communication.h +/// \brief Apply the rename operator to action summands. + +#ifndef MCRL2_LPS_LINEARISE_COMMUNICATION_H +#define MCRL2_LPS_LINEARISE_COMMUNICATION_H + +#include +#include "mcrl2/atermpp/aterm_list.h" +#include "mcrl2/core/detail/print_utility.h" +#include "mcrl2/lps/linearise_allow_block.h" +#include "mcrl2/lps/linearise_utility.h" +#include "mcrl2/lps/stochastic_action_summand.h" +#include "mcrl2/lps/sumelm.h" +#include "mcrl2/process/process_expression.h" + +// Define the following to add logging of statistics for the calculation of communication. +//#define MCRL2_COUNT_COMMUNICATION_OPERATIONS + +namespace mcrl2 +{ + +namespace lps +{ + +namespace detail +{ + +/// Get a sorted list of action names that appear in any of the elements of allowlist +/// The result does not contain duplicates. +/// We use this to remove possible communication results that are not relevant because they +/// are guaranteed to be removed from the result after the fact. +inline +std::vector get_actions(const process::action_name_multiset_list& allowlist) +{ + std::vector result; + for (const process::action_name_multiset& l : allowlist) + { + const core::identifier_string_list& names = l.names(); + result.insert(result.end(), names.begin(), names.end()); + } + std::sort(result.begin(), result.end(), action_name_compare()); + const auto it = std::unique(result.begin(), result.end()); + result.erase(it, result.end()); + + return result; +} + +/// a tuple_list contains pairs of actions (multi-action) and the condition under which this action +/// can occur. +struct tuple_list +{ + std::vector < process::action_list > actions; + std::vector < data::data_expression > conditions; + + std::size_t size() const + { + assert(actions.size() == conditions.size()); + return actions.size(); + } + + tuple_list() = default; + + tuple_list(const std::vector < process::action_list>& actions_, const std::vector< data::data_expression >& conditions_) + : actions(actions_), conditions(conditions_) + {} + + tuple_list(std::vector < process::action_list>&& actions_, std::vector< data::data_expression >&& conditions_) + : actions(std::move(actions_)), conditions(std::move(conditions_)) + {} +}; + +/// Extends the list S to S ++ [(a \oplus alpha, c \land c') | (alpha, c') \in T] +/// +/// Note that by using move semantics for L, we force the caller to transfer ownership of L to this function, +/// and make it explicit that L should not be used by the caller afterwards. +/// If firstaction == action(), it is not added to the multiactions in L', but the conditions will be strengthened. +/// \pre condition != sort_bool::false_() +inline +void addActionCondition(const process::action& a, const data::data_expression& c, tuple_list&& L, tuple_list& S) +{ + assert(c!=data::sort_bool::false_()); // It makes no sense to add an action with condition false, as it cannot happen anyhow. + + if (a == process::action()) + { + S.actions.insert(S.actions.end(), std::make_move_iterator(L.actions.begin()), std::make_move_iterator(L.actions.end())); + } + else + { + for (process::action_list& m: L.actions) + { + m = insert(a, m); + S.actions.emplace_back(std::move(m)); + } + } + + if (c == data::sort_bool::true_()) + { + S.conditions.insert(S.conditions.end(), std::make_move_iterator(L.conditions.begin()), std::make_move_iterator(L.conditions.end())); + } + else + { + // Strengthen the conditions in L with condition and append to S. + for (const data::data_expression& x: L.conditions) + { + S.conditions.emplace_back(data::lazy::and_(x, c)); + } + } +} + +/// Data structure to store the communication function more efficiently. +class comm_entry +{ + protected: + /// Left-hand sides of communication expressions + const std::vector m_lhs; + + /// Right-hand sides of communication expressions + const std::vector m_rhs; + + /// Temporary data using in determining whether communication is allowed. + /// See usages of the data structure below. + std::vector m_lhs_iters; // offset into lhs + std::vector m_match_failed; + + void reset_temporary_data() + { + for (std::size_t i = 0; i < size(); ++i) + { + m_lhs_iters[i] = m_lhs[i].begin(); + m_match_failed[i] = false; + } + } + + /// Check if m is contained in a lhs in the communication entry. (in fact, it must be a prefix). + /// Returns true if this is the case, false otherwise. + /// Postcondition: for every i such that m is not contained in lhs[i], match_failed[i] is true. + /// NB: resets temporary data before performing computations. + bool match_multiaction(const process::action_list& multi_action) { + assert(std::is_sorted(multi_action.begin(), multi_action.end(), action_compare())); + + reset_temporary_data(); + + // m must match a lhs; check every action + for (const process::action& action: multi_action) + { + // check every lhs for actionname + bool comm_ok = false; + for (std::size_t i=0; i < size(); ++i) + { + if (m_match_failed[i]) // lhs i does not match + { + continue; + } + if (m_lhs_iters[i] == m_lhs[i].end()) // lhs cannot match actionname + { + m_match_failed[i]=true; + continue; + } + if (action.label().name() != *m_lhs_iters[i]) + { + // no match + m_match_failed[i] = true; + } + else + { + // possible match; on to next action + ++m_lhs_iters[i]; + comm_ok = true; + } + } + + if (!comm_ok) // no (possibly) matching lhs + { + return false; + } + } + + // There must be an lhs that contains m. + return true; + } + + // Initialization of lhs, defined as static function so it can be used in the constructor. + // Allows lhs to be defined as const. + static std::vector < core::identifier_string_list > init_lhs(const process::communication_expression_list& communications) + { + std::vector result; + for (const process::communication_expression& l: communications) + { + const core::identifier_string_list& names = l.action_name().names(); + assert(std::is_sorted(names.begin(), names.end(), action_name_compare())); + result.emplace_back(names.begin(), names.end()); + } + return result; + } + + // Initialization of rhs, defined as static function so it can be used in the constructor. + // Allows rhs to be defined as const. + static std::vector init_rhs(const process::communication_expression_list& communications) + { + std::vector result; + for (const process::communication_expression& l: communications) + { + result.push_back(l.name()); + } + return result; + } + + public: + // comm_entries are not copyable. + comm_entry(const comm_entry& )=delete; + comm_entry& operator=(const comm_entry& )=delete; + + comm_entry(const process::communication_expression_list& communications) + : m_lhs(init_lhs(communications)), + m_rhs(init_rhs(communications)), + m_lhs_iters(communications.size()), + m_match_failed(communications.size()) + {} + + ~comm_entry() = default; + + std::size_t size() const + { + assert(m_lhs.size() == m_rhs.size()); + assert(m_rhs.size() == m_lhs_iters.size()); + assert(m_lhs_iters.size() == m_match_failed.size()); + return m_lhs.size(); + } + + /// Determine if there exists a communication expression a1|...|an -> b in comm_table + /// such that m' = a1|...|an , where m' is the multiset of actionnames for multiaction m. + /// That is, the actions in m consting of actions and data occur in C, such tat a communication + /// can take place. + /// + /// if \exists_{(b,c) \in C} b = \mu(m), return c, otherwise return action_label() + process::action_label can_communicate(const process::action_list& m) + { + assert(std::is_sorted(m.begin(), m.end(), action_compare())); + + process::action_label result; // if no match found, return process::action_label() + + if(match_multiaction(m)) + { + // There is a lhs that has m as prefix. Find it, and determine if the lhs matches m completely. + for (std::size_t i = 0; i < size(); ++i) + { + // lhs i matches only if comm_table[i] is empty + if ((!m_match_failed[i]) && m_lhs_iters[i] == m_lhs[i].end()) + { + if (m_rhs[i] == process::tau()) + { + throw mcrl2::runtime_error("Cannot linearise a process with a communication operator, containing a communication that results in tau or that has an empty right hand side"); + } + result = process::action_label(m_rhs[i], m.begin()->label().sorts()); + break; + } + } + } + + return result; + } + + /// Calculate \exists_{o,c} (\mu(m) \oplus o, c) \in C, with o \subseteq n + /// + /// The function calculates whether the actions in m (consisting of actions and data) occur in a left hand side + /// of a communication a1|...|ak -> b in C (that is, the names of m are a subbag of a1|...|ak), and the actions + /// a1|...|ak that are not in m are in n. I.e., there is a subbag o of n such that m+o can communicate. + bool might_communicate(const process::action_list& m, const process::action_list& n) + { + assert(std::is_sorted(m.begin(), m.end(), action_compare())); + assert(std::is_sorted(n.begin(), n.end(), action_compare())); + + /* this function indicates whether the actions in m + consisting of actions and data occur in C, such that + a communication might take place (i.e. m is a subbag + of the lhs of a communication in C). + if n is not empty, then all actions of a matching communication + that are not in m should be in n (i.e. there must be a + subbag o of n such that m+o can communicate. */ + bool result = false; + + if(match_multiaction(m)) + { + // the rest of actions of lhs that are not in m should be in n + // rest[i] contains the part of n in which lhs i has to find matching actions + // if rest[i] cannot match the next remaining action in the left hand side, stored in m_lhs_iters[i], i.e., rest[i] becomes empty + // before matching all actions in the lhs, we set it to std::nullopt. + // N.B. when rest[i] becomes empty after matching all actions in the lhs, + // rest[i].empty() is a meaningful result: we have a successful match. + std::vector> + rest(size(), n.begin()); // pairs of iterator into n; the second element of the pair indicates the end of the range in n. + + // check every lhs + for (std::size_t i = 0; i < size(); ++i) + { + if (m_match_failed[i]) // lhs i did not contain m + { + continue; + } + + // as long as there are still unmatched actions in lhs i... + while (m_lhs_iters[i] != m_lhs[i].end()) + { + assert(rest[i] != std::nullopt); + // .. find them in rest[i] + if (*rest[i] == n.end()) // no luck + { + rest[i] = std::nullopt; + break; + } + // get first action in lhs i + const core::identifier_string& comm_name = *m_lhs_iters[i]; + core::identifier_string rest_name = (*rest[i])->label().name(); + // find it in rest[i] + while (comm_name != rest_name) + { + ++(*rest[i]); + if (*rest[i] == n.end()) // no more + { + rest[i] = std::nullopt; + break; + } + rest_name = (*rest[i])->label().name(); + } + if (comm_name != rest_name) // action was not found + { + break; + } + + // action found; try next + ++(*rest[i]); + ++m_lhs_iters[i]; + } + + if (rest[i] != std::nullopt) // lhs was found in rest[i] + { + result = true; + break; + } + } + } + + return result; + } +}; + +template +class apply_communication_algorithm +{ +public: + apply_communication_algorithm(const process::action& termination_action, + DataRewriter& data_rewriter, + const process::communication_expression_list& communications, + const process::action_name_multiset_list& allowlist, + bool is_allow, + bool is_block) + : m_terminationAction(termination_action), + m_data_rewriter(data_rewriter), + m_communications(sort_communications(communications)), + m_allowlist(sort_multi_action_labels(allowlist)), + m_blocked_actions(is_block?get_actions(allowlist):std::vector()), + m_allowed_actions(init_allowed_actions(is_allow, allowlist, termination_action)), + m_comm_table(m_communications), + m_is_allow(is_allow), + m_is_block(is_block) + {} + + ~apply_communication_algorithm() = default; + +/// Calculate the communication operator applied to a multiaction. +/// +/// As the actions in the multiaction can be parameterized with open data expressions, for every subset of communication +/// expressions that match the multiaction, the result contains a multiaction (in which the particular subset of +/// communication expressions has been applied), and a corresponding condition that requires that the parameters are +/// equal for the actions in the left-hand-sides of the matching communication expressions. +/// Multiactions whose condition is false may be removed. +/// +/// This is the function $\overline{\gamma}$ in M. v. Weerdenburg. Calculation of Communication with Open Terms in +/// GenSpect Process Algebra. +/// +/// \param m The multiaction to which the communication operator is applied +/// \param C The communication expressions to be applied +/// \param RewriteTerm The rewriter that should be used to simplify the conditions. +tuple_list apply(const process::action_list& m) +{ + assert(std::is_sorted(m.begin(), m.end(), action_compare())); + const process::action_list r; + return makeMultiActionConditionList_aux(m, r); +} + +/// Apply the communication composition to a list of action summands. +void apply( + stochastic_action_summand_vector& action_summands, + deadlock_summand_vector& deadlock_summands, + bool nosumelm, + bool nodeltaelimination, + bool ignore_time) +{ + assert(!(m_is_allow && m_is_block)); + + /* We follow the implementation of Muck van Weerdenburg, described in + a note: Calculation of communication with open terms. */ + + mCRL2log(mcrl2::log::verbose) << + (m_is_allow ? "- calculating the communication operator modulo the allow operator on " : + m_is_block ? "- calculating the communication operator modulo the block operator on " : + "- calculating the communication operator on ") << action_summands.size() << " action summands"; + +#ifdef MCRL2_COUNT_COMMUNICATION_OPERATIONS + mCRL2log(mcrl2::log::info) << "Calculating communication operator using a set of " << m_communications.size() << " communication expressions." << std::endl; + mCRL2log(mcrl2::log::info) << "Communication expressions: " << std::endl << core::detail::print_set(m_communications) << std::endl; + mCRL2log(mcrl2::log::info) << "Allow list: " << std::endl << core::detail::print_set(m_allowlist) << std::endl; +#endif + + deadlock_summand_vector resulting_deadlock_summands; + deadlock_summands.swap(resulting_deadlock_summands); + + const bool inline_allow = m_is_allow || m_is_block; + if (inline_allow) + { + // Inline allow is only supported for ignore_time, + // for in other cases generation of delta summands cannot be inlined in any simple way. + assert(!nodeltaelimination && ignore_time); + deadlock_summands.push_back(deadlock_summand(data::variable_list(), data::sort_bool::true_(),deadlock())); + } + + stochastic_action_summand_vector resulting_action_summands; + + for (const stochastic_action_summand& smmnd: action_summands) + { + const data::variable_list& sumvars = smmnd.summation_variables(); + const process::action_list& multiaction = smmnd.multi_action().actions(); + const data::data_expression& time = smmnd.multi_action().time(); + const data::data_expression& condition = smmnd.condition(); + const data::assignment_list& nextstate = smmnd.assignments(); + const stochastic_distribution& dist = smmnd.distribution(); + + if (!inline_allow) + { + /* Recall a delta summand for every non delta summand. + * The reason for this is that with communication, the + * conditions for summands can become much more complex. + * Many of the actions in these summands are replaced by + * delta's later on. Due to the more complex conditions it + * will be hard to remove them. By adding a default delta + * with a simple condition, makes this job much easier + * later on, and will in general reduce the number of delta + * summands in the whole system */ + + // Create new list of summand variables containing only those that occur in the condition or the timestamp. + data::variable_list newsumvars; + atermpp::make_term_list(newsumvars, sumvars.begin(), sumvars.end(), [](const data::variable& v) { return v; }, + [&condition, &time](const data::variable& v) { return occursinterm(condition, v) || occursinterm(time, v); }); + + resulting_deadlock_summands.emplace_back(newsumvars, condition, deadlock(time)); + } + + /* the multiactionconditionlist is a list containing + tuples, with a multiaction and the condition, + expressing whether the multiaction can happen. All + conditions exclude each other. Furthermore, the list + is not empty. If no communications can take place, + the original multiaction is delivered, with condition + true. */ + + // We calculate the communication operator on the multiaction in this single summand. As the actions in the + // multiaction can be parameterized with open data expressions, for every subset of applicable communication expressions + // this list in principle contains one summand (unless the condition can be rewritten to false, in which case it + // is omitted). + +#ifdef MCRL2_COUNT_COMMUNICATION_OPERATIONS + mCRL2log(mcrl2::log::info) << "Calculating communication on multiaction with " << multiaction.size() << " actions." << std::endl; + mCRL2log(mcrl2::log::info) << " Multiaction: " << process::pp(multiaction) << std::endl; +#endif + + const tuple_list multiactionconditionlist = apply(multiaction); + +#ifdef MCRL2_COUNT_COMMUNICATION_OPERATIONS + mCRL2log(mcrl2::log::info) << "Calculating communication on multiaction with " << multiaction.size() << " actions results in " << multiactionconditionlist.size() << " potential summands" << std::endl; + std::size_t disallowed_summands = 0; + std::size_t blocked_summands = 0; + std::size_t false_condition_summands = 0; + std::size_t added_summands = 0; +#endif + + for (std::size_t i=0 ; i m_blocked_actions; // used only if m_is_block is set +const std::vector m_allowed_actions; // used only if m_is_allow is set +comm_entry m_comm_table; +const bool m_is_allow; // If is_allow or is_block is set, perform inline allow/block filtering. They are mutually exclusive +const bool m_is_block; + +/// Static initialization function to ensure m_allowed_actions can be const. +static const std::vector +init_allowed_actions(bool is_allow, const process::action_name_multiset_list& allow_list, const process::action& termination_action) +{ +std::vector result; +if (is_allow) +{ + result = get_actions(allow_list); + // Ensure that the termination action is always allowed, even when it is not an explicit part of + // the list of allowed actions. + // We maintains sort order of the vector + std::vector::iterator it = std::upper_bound(result.begin(), result.end(), termination_action.label().name(), action_name_compare()); + result.insert(it, termination_action.label().name()); +} + +return result; +} + +/// Calculate data expression for pairwise equality of the elements of l1 and l2. +/// +/// If the lengths of l1 and l2 differ, or for some index i, the sort l1[i] and l2[i] is different, the pairwise +/// match is false, otherwise an expression equivalent to \bigwegde_i (l1[i] == l2[i]) is returned. +data::data_expression pairwise_equal_to(const data::data_expression_list& l1, const data::data_expression_list& l2) const +{ +data::data_expression result = data::sort_bool::true_(); + +if (l1.size()!=l2.size()) +{ + result = data::sort_bool::false_(); +} + +auto i1 = l1.begin(); +auto i2 = l2.begin(); + +while (i1 != l1.end() && i2 != l2.end() && result != data::sort_bool::false_()) +{ + if (i1->sort() != i2->sort()) + { + result = data::sort_bool::false_(); + } + else + { + result = data::lazy::and_(result, m_data_rewriter(equal_to(*i1++, *i2++))); + } +} + +return result; +} + + +/// Determine if the action is allowable, that is, it is part of an allow expression +/// and it is not part of a block expression +bool maybe_allowed(const process::action_label& a) const +{ + assert(std::is_sorted(m_allowed_actions.begin(), m_allowed_actions.end(), action_name_compare())); + assert(std::is_sorted(m_blocked_actions.begin(), m_blocked_actions.end(), action_name_compare())); + assert(!m_is_block || m_allowed_actions.empty()); + assert(!m_is_allow || m_blocked_actions.empty()); + + return !(m_is_allow || m_is_block) + || (m_is_allow && std::binary_search(m_allowed_actions.begin(), m_allowed_actions.end(), a.name(), action_name_compare())) + || (m_is_block && !std::binary_search(m_blocked_actions.begin(), m_blocked_actions.end(), a.name(), action_name_compare())); +} + + +/// Calculate the communication operator applied to a multiaction. +/// +/// This is the function $\overline(\gamma, C, r)$ as described in M. v. Weerdenburg. Calculation of Communication +/// with Open Terms in GenSpect Process Algebra. +/// +/// \param m_first Start of a range of multiactions to which the communication operator should be applied +/// \param m_last End of a range of multiactions to which the communication operator should be applied +/// \param C The communication expressions that must be applied to the multiaction +/// \param r +/// \param RewriteTerm Data rewriter for simplifying expressions. +inline +tuple_list makeMultiActionConditionList_aux( + const process::action_list& m, + const process::action_list& r) +{ + assert(std::is_sorted(m.begin(), m.end(), action_compare())); + assert(std::is_sorted(r.begin(), r.end(), action_compare())); + + tuple_list S; // result + + // if m = [], then S := { (r, \psi(r, C)) } + if (m.empty()) + { + if (r.empty()) + { + S.conditions.emplace_back(data::sort_bool::true_()); + } + else + { + S.conditions.emplace_back(psi(r)); + } + + // TODO: Why don't we insert r here, as van Weerdenburg writes? + S.actions.emplace_back(); + } + else + { + // m = [a(d)] \oplus n + const process::action& a = m.front(); + const process::action_list& m_tail = m.tail(); + + // S = \phi(a(d), d, [], n, C, r) + S = phi({a}, a.arguments(), process::action_list(), m_tail, r); + + // addActionCondition adds a to every multiaction in T; so if a is not part of any allowed action, + // we can skip this part. + if (maybe_allowed(a.label())) + { + // T = \overline{\gamma}(n, C, [a(d)] \oplus r) + tuple_list T = makeMultiActionConditionList_aux(m_tail, insert(a, r)); + + // S := S \cup \{ (a,true) \oplus t \mid t \in T \} + // TODO: van Weerdenburg in his note only calculates S := S \cup T. Understand why that is not correct. + addActionCondition(a,data::sort_bool::true_(),std::move(T),S); + } + } + return S; +} + +/// Calculate $\phi(m, d, w, n, C, r)$ as described in M. v. Weerdenburg. Calculation of Communication +/// with Open Terms in GenSpect Process Algebra. +/// +/// phi is a function that yields a list of pairs indicating how the actions in m|w|n can communicate. +/// The pairs contain the resulting multi action and a condition on data indicating when communication can take place. +/// In the communication all actions of m, none of w and a subset of n can take part in the communication. +/// d is the data parameter of the communication and comm_table contains a list of multiaction action pairs +/// indicating possible communications. +inline +tuple_list phi(const process::action_list& m, + const data::data_expression_list& d, + const process::action_list& w, + const process::action_list& n, + const process::action_list& r) +{ + assert(std::is_sorted(m.begin(), m.end(), action_compare())); + assert(std::is_sorted(w.begin(), w.end(), action_compare())); + assert(std::is_sorted(n.begin(), n.end(), action_compare())); + assert(std::is_sorted(r.begin(), r.end(), action_compare())); + + tuple_list S; + + // \exists_{o,c} (\mu(m) \oplus o, c) \in C, with o \subseteq n + if (m_comm_table.might_communicate(m, n)) + { + if (n.empty()) // b \land n = [] + { + // There is communication expression whose lhs matches m, result is c. + const process::action_label c = m_comm_table.can_communicate(m); /* returns process::action_label() if no communication + is possible */ + + if (c!=process::action_label() && maybe_allowed(c)) + { + // \exists_{(b,c) \in C} b = \mu(m) + // the result of the communication is part of an allow, not in the block set. + // Calculate communication for multiaction w. + // T := \overline{\gamma}(w, C) + tuple_list T = makeMultiActionConditionList_aux(w, r); + + // S := \{ (c(d) \oplus r, e) \mid (r,e) \in T \} + addActionCondition(process::action(c,d), data::sort_bool::true_(), std::move(T), S); + } + } + else + { + // n = [a(f)] \oplus o + const process::action& a = n.front(); + const process::action_list& n_tail = n.tail(); + + const data::data_expression condition=pairwise_equal_to(d,a.arguments()); + if (condition==data::sort_bool::false_()) + { + // a(f) cannot take part in communication as the arguments do not match. Move to w and continue with next action + S = phi(m,d,insert(a, w), n_tail, r); + } + else + { + tuple_list T=phi(insert(a, m),d,w, n_tail,r); + + S = phi(m,d,insert(a, w), n_tail,r); + addActionCondition(process::action(), condition, std::move(T), S); + } + } + } + + return S; +} + +bool xi(const process::action_list& alpha, + const process::action_list& beta) +{ + bool result = false; + + if (beta.empty()) + { + result = m_comm_table.can_communicate(alpha)!=process::action_label(); + } + else + { + const process::action_list alpha_ = insert(beta.front(), alpha); + + if (m_comm_table.can_communicate(alpha_)!=process::action_label()) + { + result = true; + } + else + { + const process::action_list& beta_tail = beta.tail(); + if (m_comm_table.might_communicate(alpha_, beta_tail)) + { + result = xi(alpha, beta_tail); + } + + result = result || xi(alpha, beta_tail); + } + } + return result; +} + +data::data_expression psi(process::action_list alpha) +{ + assert(std::is_sorted(alpha.begin(), alpha.end(), action_compare())); + data::data_expression cond = data::sort_bool::false_(); + + process::action_list actl; // used in inner loop. + while (!alpha.empty()) + { + process::action_list beta = alpha.tail(); + + while (!beta.empty()) + { + actl = process::action_list(); + actl = insert(alpha.front(), actl); + actl = insert(beta.front(), actl); + const process::action_list& beta_tail = beta.tail(); + if (m_comm_table.might_communicate(actl, beta_tail) && xi(actl, beta_tail)) + { + // sort and remove duplicates?? + cond = data::lazy::or_(cond,pairwise_equal_to(alpha.front().arguments(), beta.front().arguments())); + } + beta = beta_tail; + } + + alpha = alpha.tail(); + } + cond = data::lazy::not_(cond); + return cond; +} + +}; +} + +inline +void communicationcomposition( + const process::communication_expression_list& communications, + const process::action_name_multiset_list& allowlist, // This is a list of list of identifierstring. + const bool is_allow, // If is_allow or is_block is set, perform inline allow/block filtering. + const bool is_block, + stochastic_action_summand_vector& action_summands, + deadlock_summand_vector& deadlock_summands, + const process::action& terminationAction, + const bool nosumelm, + const bool nodeltaelimination, + const bool ignore_time, + const std::function& RewriteTerm) + +{ + return detail::apply_communication_algorithm(terminationAction, RewriteTerm, communications, allowlist, is_allow, is_block).apply( + action_summands, deadlock_summands, nosumelm, nodeltaelimination, ignore_time); +} + + +} // namespace lps + +} // namespace mcrl2 + + + +#endif // MCRL2_LPS_LINEARISE_COMMUNICATION_H diff --git a/libraries/lps/include/mcrl2/lps/linearise_rename.h b/libraries/lps/include/mcrl2/lps/linearise_rename.h new file mode 100644 index 0000000000..0381c695ec --- /dev/null +++ b/libraries/lps/include/mcrl2/lps/linearise_rename.h @@ -0,0 +1,94 @@ +// Author(s): Jan Friso Groote, Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file mcrl2/lps/linearise_rename.h +/// \brief Apply the rename operator to action summands. + +#ifndef MCRL2_LPS_LINEARISE_RENAME_H +#define MCRL2_LPS_LINEARISE_RENAME_H + +#include "mcrl2/atermpp/aterm_list.h" +#include "mcrl2/lps/stochastic_action_summand.h" +#include "mcrl2/lps/linearise_utility.h" +#include "mcrl2/process/process_expression.h" + + +namespace mcrl2 +{ + +namespace lps +{ + + /// Apply renamings to a single action + inline + process::action rename(const process::rename_expression_list& renamings, const process::action& action) + { + const process::action_label& action_label = action.label(); + const core::identifier_string& action_name = action_label.name(); + for (const process::rename_expression& renaming: renamings) + { + if (action_name == renaming.source()) + { + return process::action(process::action_label(renaming.target(), action_label.sorts()), action.arguments()); + } + } + return action; + } + + inline + process::action_list rename(const process::rename_expression_list& renamings, + const process::action_list& actions) + { + process::action_list result; + + for (const process::action& a: actions) + { + result.push_front(rename(renamings, a)); + } + + result = sort_actions(result); + return result; + } + + inline + multi_action rename(const process::rename_expression_list& renamings, + const multi_action& multi_action) + { + return lps::multi_action(rename(renamings, multi_action.actions()), multi_action.time()); + } + + inline + stochastic_action_summand rename(const process::rename_expression_list& renamings, + const stochastic_action_summand& summand) + { + return stochastic_action_summand(summand.summation_variables(), + summand.condition(), + rename(renamings, summand.multi_action()), + summand.assignments(), + summand.distribution()); + } + + + inline + void rename( + const process::rename_expression_list& renamings, + lps::stochastic_action_summand_vector& action_summands) + { + for (auto& action_summand: action_summands) + { + action_summand = rename(renamings, action_summand); + } + } + +} // namespace lps + +} // namespace mcrl2 + + + +#endif // MCRL2_LPS_LINEARISE_RENAME_H diff --git a/libraries/lps/include/mcrl2/lps/linearise_utility.h b/libraries/lps/include/mcrl2/lps/linearise_utility.h new file mode 100644 index 0000000000..8a752195b8 --- /dev/null +++ b/libraries/lps/include/mcrl2/lps/linearise_utility.h @@ -0,0 +1,295 @@ +// Author(s): Jan Friso Groote, Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file mcrl2/lps/linearise_utility.h +/// \brief Utilities used in linearisation. Mainly for actions and multiactions. + +#ifndef MCRL2_LPS_LINEARISE_UTILITY_H +#define MCRL2_LPS_LINEARISE_UTILITY_H + +#include "mcrl2/data/data_expression.h" +#include "mcrl2/process/process_expression.h" +#include "mcrl2/lps/deadlock_summand.h" +#include "mcrl2/lps/stochastic_action_summand.h" + + +namespace mcrl2 +{ + +namespace lps +{ + +struct action_name_compare +{ + bool operator()(const core::identifier_string& s1, const core::identifier_string& s2) const + { + return std::string(s1) < std::string(s2); + } +}; + +/// Determine if a1 < a2; the key requirement is that orderings of action labels and the actions in multiactions are +/// consistent. +struct action_label_compare +{ + + bool operator()(const process::action_label& a1, const process::action_label& a2) const + { + /* first compare the strings in the actions */ + const core::identifier_string& a1_name = a1.name(); + const core::identifier_string& a2_name = a2.name(); + + return action_name_compare()(a1_name, a2_name) || + (a1_name == a2_name && a1.sorts() < a2.sorts()); + } +}; + + +/// Determine if a1 < a2; the key requirement is that orderings of action labels and the actions in multiactions are +/// consistent. +/// +/// \returns true iff the label of a1 is less than the label of a2. +/// The arguments are ignored in this comparison. +/// The sort order is used for efficient application of process operators such as allow and comm +/// which are defined in terms of action names. +struct action_compare +{ + bool operator()(const process::action& a1, const process::action& a2) const + { + const process::action_label& a1_label = a1.label(); + const process::action_label& a2_label = a2.label(); + + return action_label_compare()(a1_label, a2_label); + } +}; + +/// Insert action into an action_list, keeping the action list sorted w.r.t. action_compare. +/// Complexity: O(n) for an action_list of length n. +inline +process::action_list insert( + const process::action& act, + process::action_list l) +{ + if (l.empty()) + { + return process::action_list({ act }); + } + const process::action& head = l.front(); + + if (action_compare()(act, head)) + { + l.push_front(act); + return l; + } + + process::action_list result = insert(act, l.tail()); + result.push_front(head); + return result; +} + +/// insert an action name into the list, while preserving the sorting of action names. +inline +core::identifier_string_list insert( + const core::identifier_string& s, + core::identifier_string_list l) +{ + if (l.empty()) + { + return core::identifier_string_list({ s }); + } + const core::identifier_string& head = l.front(); + + if (action_name_compare()(s, head)) + { + l.push_front(s); + return l; + } + + core::identifier_string_list result = insert(s, l.tail()); + result.push_front(head); + return result; +} + +inline +process::action_name_multiset sort_action_names(const process::action_name_multiset& action_labels, + const std::function& cmp + = [](const core::identifier_string& t1, const core::identifier_string& t2){ return action_name_compare()(t1, t2);}) +{ + return process::action_name_multiset(atermpp::sort_list(action_labels.names(), cmp)); +} + +inline +process::action_name_multiset_list sort_multi_action_labels(const process::action_name_multiset_list& l) +{ + return process::action_name_multiset_list(l.begin(),l.end(),[](const process::action_name_multiset& al){ return sort_action_names(al); }); +} + +inline +process::action_list sort_actions(const process::action_list& actions, + const std::function& cmp + = [](const process::action& t1, const process::action& t2){ return action_compare()(t1, t2);}) +{ + return process::action_list(atermpp::sort_list(actions, cmp)); +} + + +/// Sort the left-hand sides of the communication expressions in communications +/// +/// Sorting is done using sort_action_labels, so by default, the left-hand sides of the communications are sorted by names of the actions. +inline +process::communication_expression_list sort_communications(const process::communication_expression_list& communications) +{ + process::communication_expression_list result; + + for (const process::communication_expression& comm: communications) + { + result.push_front(process::communication_expression(sort_action_names(comm.action_name()),comm.name())); + } + + return result; +} + +inline +bool implies_condition(const data::data_expression& c1, const data::data_expression& c2) +{ + if (c2==data::sort_bool::true_()) + { + return true; + } + + if (c1==data::sort_bool::false_()) + { + return true; + } + + if (c1==data::sort_bool::true_()) + { + return false; + } + + if (c2==data::sort_bool::false_()) + { + return false; + } + + if (c1==c2) + { + return true; + } + + /* Dealing with the conjunctions (&&) first and then the disjunctions (||) + yields a 10-fold speed increase compared to the case where first the + || occur, and then the &&. This result was measured on the alternating + bit protocol, with --regular. */ + + if (data::sort_bool::is_and_application(c2)) + { + return implies_condition(c1,data::binary_left(atermpp::down_cast(c2))) && + implies_condition(c1,data::binary_right(atermpp::down_cast(c2))); + } + + if (data::sort_bool::is_or_application(c1)) + { + return implies_condition(data::binary_left(atermpp::down_cast(c1)),c2) && + implies_condition(data::binary_right(atermpp::down_cast(c1)),c2); + } + + if (data::sort_bool::is_and_application(c1)) + { + return implies_condition(data::binary_left(atermpp::down_cast(c1)),c2) || + implies_condition(data::binary_right(atermpp::down_cast(c1)),c2); + } + + if (data::sort_bool::is_or_application(c2)) + { + return implies_condition(c1,data::binary_left(atermpp::down_cast(c2))) || + implies_condition(c1,data::binary_right(atermpp::down_cast(c2))); + } + + return false; +} + +/// Determine if action summand as subsumes delta summand ds. +/// +/// The action summand subsumes the deadlock summand if its condition is implied by that of the deadlock summand, +/// and either the action summand is not timed, or the timestamp of the deadlock summand and the action summand coincide. +inline +bool subsumes(const stochastic_action_summand& as, const deadlock_summand& ds) +{ + return (!as.multi_action().has_time() || ds.deadlock().time() == as.multi_action().time()) + && implies_condition(ds.condition(), as.condition()); +} + +/// Determine if delta summand ds1 subsumes delta summand ds2. +inline +bool subsumes(const deadlock_summand& ds1, const deadlock_summand& ds2) +{ + return (!ds1.deadlock().has_time() || ds2.deadlock().time() == ds1.deadlock().time()) + && implies_condition(ds2.condition(), ds1.condition()); +} + + +inline +void insert_timed_delta_summand( + const stochastic_action_summand_vector& action_summands, + deadlock_summand_vector& deadlock_summands, + const deadlock_summand& s, + const bool ignore_time) +{ + if (ignore_time) + { + deadlock_summands.push_back(s); + return; + } + + assert(!ignore_time); + + // First check whether the delta summand is subsumed by an action summand. + if (std::any_of(action_summands.begin(), action_summands.end(), + [&s](const stochastic_action_summand& as) { return subsumes(as, s); })) + { + return; + } + + deadlock_summand_vector result; + + for (deadlock_summand_vector::iterator i=deadlock_summands.begin(); i!=deadlock_summands.end(); ++i) + { + if (subsumes(*i, s)) + { + /* put the summand that was effective in removing + this delta summand to the front, such that it + is encountered early later on, removing a next + delta summand */ + + copy(i,deadlock_summands.end(),back_inserter(result)); + deadlock_summands.swap(result); + return; + } + if (!subsumes(s, *i)) + { + result.push_back(*i); + } + } + + result.push_back(s); + deadlock_summands.swap(result); +} + +inline +bool occursinterm(const data::data_expression& t, const data::variable& var) +{ + return data::search_free_variable(t, var); +} + +} // namespace lps + +} // namespace mcrl2 + + + +#endif // MCRL2_LPS_LINEARISE_RENAME_H diff --git a/libraries/lps/source/linearise.cpp b/libraries/lps/source/linearise.cpp index 051efb0793..6786e1aa91 100644 --- a/libraries/lps/source/linearise.cpp +++ b/libraries/lps/source/linearise.cpp @@ -32,11 +32,16 @@ #include "mcrl2/data/real_utilities.h" // linear process libraries. -#include "mcrl2/lps/detail/ultimate_delay.h" -#include "mcrl2/lps/linearise.h" -#include "mcrl2/lps/sumelm.h" #include "mcrl2/lps/constelm.h" +#include "mcrl2/lps/linearise.h" +#include "mcrl2/lps/linearise_allow_block.h" +#include "mcrl2/lps/linearise_utility.h" +#include "mcrl2/lps/linearise_rename.h" +#include "mcrl2/lps/linearise_communication.h" #include "mcrl2/lps/replace_capture_avoiding_with_an_identifier_generator.h" +#include "mcrl2/lps/sumelm.h" + +#include "mcrl2/lps/detail/ultimate_delay.h" // Process libraries. #include "mcrl2/process/alphabet_reduce.h" @@ -106,7 +111,7 @@ class objectdatatype constructor=false; processstatus=unknown; object=none; - canterminate=0; + canterminate=false; containstime=false; } @@ -238,14 +243,14 @@ class specification_basic_type terminatedProcId, variable_list(), seq(terminationAction,delta()), - pCRL,0,false); + pCRL,false,false); delta_process=newprocess(variable_list(),delta(),pCRL,false,false); tau_process=newprocess(variable_list(),tau(),pCRL,true,false); } ~specification_basic_type() { - for (; stack_operations_list!=nullptr;) + while (stack_operations_list!=nullptr) { stackoperations* temp=stack_operations_list->next; delete stack_operations_list; @@ -255,18 +260,8 @@ class specification_basic_type } private: - /* data_expression real_zero() - { - static data_expression zero=sort_real::creal(sort_int::cint(sort_nat::c0()),sort_pos::c1()); - return zero; - } - - data_expression real_one() - { - static data_expression one=sort_real::creal(sort_int::cint(sort_nat::cnat(sort_pos::c1())),sort_pos::c1()); - return one; - } */ + static data_expression real_times_optimized(const data_expression& r1, const data_expression& r2) { if (r1==sort_real::real_zero() || r2==sort_real::real_zero()) @@ -284,7 +279,8 @@ class specification_basic_type return sort_real::times(r1,r2); } - process_expression delta_at_zero(void) + static + process_expression delta_at_zero() { return at(delta(), sort_real::real_(0)); } @@ -344,6 +340,7 @@ class specification_basic_type fresh_identifier_generator.add_identifier(str); } + static process_expression action_list_to_process(const action_list& ma) { if (ma.size()==0) @@ -357,6 +354,9 @@ class specification_basic_type return process::sync(ma.front(),action_list_to_process(ma.tail())); } + /// Convert the process expression to an action list. + /// Note: The resulting actions are not sorted. + static action_list to_action_list(const process_expression& p) { if (is_tau(p)) @@ -377,7 +377,15 @@ class specification_basic_type return action_list(); } - process::action_label_list getnames(const process_expression& multiAction) + /// Convert the process expression to a sorted action list. + static + action_list to_sorted_action_list(const process_expression& p) + { + return sort_actions(to_action_list(p)); + } + + static + action_label_list getnames(const process_expression& multiAction) { if (is_action(multiAction)) { @@ -433,6 +441,7 @@ class specification_basic_type return getparameters_rec(multiAction,occurs_set); } + static data_expression_list getarguments(const action_list& multiAction) { data_expression_list result; @@ -443,6 +452,7 @@ class specification_basic_type return reverse(result); } + static action_list makemultiaction(const process::action_label_list& actionIds, const data_expression_list& args) { action_list result; @@ -540,6 +550,7 @@ class specification_basic_type /************ upperpowerof2 *********************************************/ + static std::size_t upperpowerof2(std::size_t i) /* function yields n for the smallest value n such that 2^n>=i. This constitutes the number of bits necessary @@ -749,7 +760,7 @@ class specification_basic_type e.identifier(), e.formal_parameters(), e.expression(), - unknown,0,false); + unknown,false,false); } } @@ -759,7 +770,7 @@ class specification_basic_type const processstatustype s, const bool canterminate, const bool containstime, - process_identifier& p) + process_identifier& p) const { for(const std::pair& d: objectdata) { @@ -787,67 +798,22 @@ class specification_basic_type because it cannot occur as a string in the input */ process_identifier initprocess(std::string("init"), variable_list()); - insert_process_declaration(initprocess,variable_list(),init,unknown,0,false); + insert_process_declaration(initprocess,variable_list(),init,unknown,false,false); return initprocess; } private: /********** various functions on action and multi actions ***************/ - bool actioncompare(const action_label& a1, const action_label& a2) - { - /* first compare the strings in the actions */ - if (std::string(a1.name())& vars_set, @@ -1326,11 +1286,12 @@ class specification_basic_type filter_vars_by_termlist(a.begin(),a.end(),vars_set,vars_result_set); } - bool occursintermlist(const variable& var, const data_expression_list& r) const + static + bool occursintermlist(const variable& var, const data_expression_list& r) { for (const data_expression& d: r) { - if (occursinterm(var,d)) + if (occursinterm(d, var)) { return true; } @@ -1343,7 +1304,7 @@ class specification_basic_type std::set assigned_variables; for (const assignment& l: r) { - if (occursinterm(var,l.rhs())) + if (occursinterm(l.rhs(), var)) { return true; } @@ -1419,7 +1380,7 @@ class specification_basic_type } if (is_if_then(p)) { - return occursinterm(var,if_then(p).condition())|| + return occursinterm(if_then(p).condition(), var) || occursinpCRLterm(var,if_then(p).then_case(),strict); } @@ -1441,13 +1402,13 @@ class specification_basic_type if (strict) { return occursintermlist(var,variable_list_to_data_expression_list(sto.variables())) || - occursinterm(var,sto.distribution()) || + occursinterm(sto.distribution(), var) || occursinpCRLterm(var,sto.operand(),strict); } else { return (!occursintermlist(var,variable_list_to_data_expression_list(sto.variables()))) && - (occursinterm(var,sto.distribution()) || + (occursinterm(sto.distribution(), var) || occursinpCRLterm(var,sto.operand(),strict)); } } @@ -1466,7 +1427,7 @@ class specification_basic_type } if (is_at(p)) { - return occursinterm(var,at(p).time_stamp()) || + return occursinterm(at(p).time_stamp(), var) || occursinpCRLterm(var,at(p).operand(),strict); } if (is_delta(p)) @@ -1738,6 +1699,7 @@ class specification_basic_type } /* Remove assignments that do not appear in the parameter list. */ + static assignment_list filter_assignments(const assignment_list& assignments, const variable_list& parameters) { assignment_vector result; @@ -1877,6 +1839,7 @@ class specification_basic_type } // Sort the assignments, such that they have the same order as the parameters + static assignment_list sort_assignments(const assignment_list& ass, const variable_list& parameters) { std::mapassignment_map; @@ -2399,6 +2362,7 @@ class specification_basic_type } + static assignment_list parameters_to_assignment_list(const variable_list& parameters, const std::set& variables_bound_in_sum) { assignment_vector result; @@ -3123,6 +3087,7 @@ class specification_basic_type return process_expression(); } + static int match_sequence( const std::vector < process_instance_assignment >& s1, const std::vector < process_instance_assignment >& s2, @@ -3868,7 +3833,7 @@ class specification_basic_type { std::vector todo; todo.push_back(procsIdDecl); - for (; !todo.empty() ;) + while (!todo.empty()) { const process_identifier pi=todo.back(); todo.pop_back(); @@ -3967,6 +3932,7 @@ class specification_basic_type that no id1 that occurs at the right of the map can occur at the left. */ + static process_identifier get_last(const process_identifier& id, const std::map< process_identifier, process_identifier >& identifier_identifier_map) { process_identifier target_id=id; @@ -3988,6 +3954,7 @@ class specification_basic_type } + static void set_proc_identifier_map( std::map< process_identifier, process_identifier >& identifier_identifier_map, const process_identifier& id1_, @@ -4011,6 +3978,7 @@ class specification_basic_type } } + static void complete_proc_identifier_map(std::map< process_identifier, process_identifier >& identifier_identifier_map) { std::map< process_identifier, process_identifier > new_identifier_identifier_map; @@ -4236,6 +4204,7 @@ class specification_basic_type /**************** Collectparameterlist ******************************/ + static bool alreadypresent(variable& var,const variable_list& vl) { /* Note: variables can be different, although they have the @@ -4262,6 +4231,7 @@ class specification_basic_type return alreadypresent(var,vl.tail()); } + static variable_list joinparameters(const variable_list& par1, const variable_list& par2) { @@ -4385,7 +4355,7 @@ class specification_basic_type stacklisttype(const stacklisttype& )=delete; stacklisttype& operator=(const stacklisttype& )=delete; - + static stackoperations* find_suitable_stack_operations( const variable_list& parameters, stackoperations* stack_operations_list) @@ -4491,7 +4461,7 @@ class specification_basic_type } data_expression getvar(const variable& var, - const stacklisttype& stack) + const stacklisttype& stack) const { /* first search whether the variable is a free process variable */ if (global_variables.count(var)>0) @@ -4780,37 +4750,25 @@ class specification_basic_type return result; } - - action_list adapt_multiaction_to_stack_rec( - const action_list& multiAction, - const stacklisttype& stack, - const variable_list& vars) + /// Adapt multiactions to stack by traversing the list. + /// Note: the result is sorted w.r.t action_compare(). + action_list + adapt_multiaction_to_stack(const action_list& multiAction, const stacklisttype& stack, const variable_list& vars) { - if (multiAction.empty()) - { - return multiAction; - } + action_vector result; - const action act=action(multiAction.front()); + for (action_list::const_iterator it = multiAction.begin(); it != multiAction.end(); ++it) { + const action& act = *it; + const data_expression_vector vec( + adapt_termlist_to_stack(act.arguments().begin(), act.arguments().end(), stack, vars, variable_list())); + result.push_back(action(act.label(), data_expression_list(vec.begin(), vec.end()))); + } - action_list result=adapt_multiaction_to_stack_rec(multiAction.tail(),stack,vars); + // As the arguments change, sort order w.r.t. action_label is preserved, but order w.r.t. arguments is changed. + // resort the list. + std::sort(result.begin(), result.end(), action_compare()); - const data_expression_vector vec(adapt_termlist_to_stack( - act.arguments().begin(), - act.arguments().end(), - stack, - vars, - variable_list())); - result.push_front(action(act.label(),data_expression_list(vec.begin(),vec.end()))); - return result; - } - - action_list adapt_multiaction_to_stack( - const action_list& multiAction, - const stacklisttype& stack, - const variable_list& vars) - { - return adapt_multiaction_to_stack_rec(multiAction,stack,vars); + return action_list(result.begin(), result.end()); } data_expression representative_generator_internal(const sort_expression& s, const bool allow_dont_care_var=true) @@ -5082,6 +5040,7 @@ class specification_basic_type return assignment_list({ assignment(stack.stackvar,sf) }); } + static bool occursin(const variable& name, const variable_list& pars) { @@ -5276,7 +5235,9 @@ class specification_basic_type const bool has_time, const bool is_deadlock_summand) { - assert(distribution!=stochastic_distribution()); + assert(distribution != stochastic_distribution()); + assert(std::is_sorted(multiAction.begin(), multiAction.end(), action_compare())); + const data_expression rewritten_condition=RewriteTerm(condition); if (rewritten_condition==sort_bool::false_()) { @@ -5289,14 +5250,14 @@ class specification_basic_type deadlock_summands, deadlock_summand(sumvars, rewritten_condition, - has_time?deadlock(actTime):deadlock())); + has_time?deadlock(actTime):deadlock()),options.ignore_time); } else { action_summands.push_back(stochastic_action_summand( sumvars, rewritten_condition, - has_time?multi_action(multiAction,actTime):multi_action(multiAction), + has_time ? multi_action(multiAction, actTime) : multi_action(multiAction), procargs, stochastic_distribution(distribution.variables(), RewriteTerm(distribution.distribution())))); @@ -5330,7 +5291,7 @@ class specification_basic_type list sumvars */ variable_list sumvars; - for (; is_sum(summandterm) ;) + while (is_sum(summandterm)) { sumvars=sum(summandterm).variables() + sumvars; summandterm=sum(summandterm).operand(); @@ -5358,7 +5319,7 @@ class specification_basic_type stochastic_distribution cumulative_distribution(variable_list(),sort_real::real_one()); /* The conditions are collected for use. The stochastic operators before the action are ignored */ - for (; (is_if_then(summandterm)||is_stochastic_operator(summandterm)) ;) + while ((is_if_then(summandterm)||is_stochastic_operator(summandterm))) { if (is_if_then(summandterm)) { @@ -5416,7 +5377,7 @@ class specification_basic_type else { assert(is_tau(t1)||is_action(t1)||is_sync(t1)); - multiAction=to_action_list(t1); + multiAction=to_sorted_action_list(t1); } stochastic_distribution distribution(variable_list(),sort_real::real_one()); @@ -5474,11 +5435,12 @@ class specification_basic_type } else if (is_action(summandterm)) { + assert(multiAction.empty()); // so the result must be sorted. multiAction.push_front(action(summandterm)); } else if (is_sync(summandterm)) { - multiAction=to_action_list(summandterm); + multiAction=to_sorted_action_list(summandterm); } else { @@ -5671,7 +5633,7 @@ class specification_basic_type return w; } - data::function_symbol find_case_function(std::size_t index, const sort_expression& sort) + data::function_symbol find_case_function(std::size_t index, const sort_expression& sort) const { for (const data::function_symbol& f: enumeratedtypes[index].functions) { @@ -5921,6 +5883,7 @@ class specification_basic_type return false; } + static data_expression_list extend(const data_expression& c, const data_expression_list& cl) { return data_expression_list(cl.begin(), @@ -6124,6 +6087,7 @@ class specification_basic_type return construct_binary_case_tree_rec(n-1,sums,terms,termsort,e); } + static bool summandsCanBeClustered( const stochastic_action_summand& summand1, const stochastic_action_summand& summand2) @@ -6159,6 +6123,7 @@ class specification_basic_type return i2 == multiactionlist2.end(); } + static data_expression getRHSassignment(const variable& var, const assignment_list& as) { for (const assignment& a: as) @@ -7047,6 +7012,7 @@ class specification_basic_type some_summand_has_time?deadlock(resulttime):deadlock()); } + static sort_expression_list getActionSorts(const action_list& actionlist) { sort_expression_list resultsorts; @@ -7185,8 +7151,8 @@ class specification_basic_type from the underlying GNF */ { // We use action_summands and deadlock_summands as an output. - assert(action_summands.size()==0); - assert(deadlock_summands.size()==0); + assert(action_summands.empty()); + assert(deadlock_summands.empty()); bool singlecontrolstate=false; std::set< process_identifier > reachable_process_identifiers; @@ -7275,6 +7241,7 @@ class specification_basic_type /**************** hiding *****************************************/ + static action_list hide_(const identifier_string_list& hidelist, const action_list& multiaction) { action_list resultactionlist; @@ -7291,6 +7258,7 @@ class specification_basic_type return reverse(resultactionlist); } + static void hidecomposition(const identifier_string_list& hidelist, stochastic_action_summand_vector& action_summands) { for (stochastic_action_summand_vector::iterator i=action_summands.begin(); i!=action_summands.end() ; ++i) @@ -7304,362 +7272,16 @@ class specification_basic_type } } - /**************** allow/block *************************************/ - - bool implies_condition(const data_expression& c1, const data_expression& c2) - { - if (c2==sort_bool::true_()) - { - return true; - } - - if (c1==sort_bool::false_()) - { - return true; - } - - if (c1==sort_bool::true_()) - { - return false; - } - - if (c2==sort_bool::false_()) - { - return false; - } - - if (c1==c2) - { - return true; - } - - /* Dealing with the conjunctions (&&) first and then the disjunctions (||) - yields a 10-fold speed increase compared to the case where first the - || occur, and then the &&. This result was measured on the alternating - bit protocol, with --regular. */ - - if (sort_bool::is_and_application(c2)) - { - return implies_condition(c1,data::binary_left(down_cast(c2))) && - implies_condition(c1,data::binary_right(down_cast(c2))); - } - - if (sort_bool::is_or_application(c1)) - { - return implies_condition(data::binary_left(down_cast(c1)),c2) && - implies_condition(data::binary_right(down_cast(c1)),c2); - } - - if (sort_bool::is_and_application(c1)) - { - return implies_condition(data::binary_left(down_cast(c1)),c2) || - implies_condition(data::binary_right(down_cast(c1)),c2); - } - - if (sort_bool::is_or_application(c2)) - { - return implies_condition(c1,data::binary_left(down_cast(c2))) || - implies_condition(c1,data::binary_right(down_cast(c2))); - } - - return false; - } - - void insert_timed_delta_summand( - const stochastic_action_summand_vector& action_summands, - deadlock_summand_vector& deadlock_summands, - const deadlock_summand& s) - { - deadlock_summand_vector result; - - // const variable_list sumvars=s.summation_variables(); - const data_expression& cond=s.condition(); - const data_expression& actiontime=s.deadlock().time(); - - // First check whether the delta summand is subsumed by an action summands. - if (!options.ignore_time) - { - for (const stochastic_action_summand& as: action_summands) - { - const data_expression& cond1=as.condition(); - if (((actiontime==as.multi_action().time()) || (!as.multi_action().has_time())) && - (implies_condition(cond,cond1))) - { - /* De delta summand is subsumed by action summand as. So, it does not - have to be added. */ - - return; - } - } - } - - for (deadlock_summand_vector::iterator i=deadlock_summands.begin(); i!=deadlock_summands.end(); ++i) - { - const deadlock_summand& smmnd=*i; - const data_expression& cond1=i->condition(); - if ((!options.ignore_time) && - ((actiontime==i->deadlock().time()) || (!i->deadlock().has_time())) && - (implies_condition(cond,cond1))) - { - /* put the summand that was effective in removing - this delta summand to the front, such that it - is encountered early later on, removing a next - delta summand */ - - copy(i,deadlock_summands.end(),back_inserter(result)); - deadlock_summands.swap(result); - return; - } - if (((options.ignore_time)|| - (((actiontime==smmnd.deadlock().time())|| (!s.deadlock().has_time())) && - (implies_condition(cond1,cond))))) - { - /* do not add summand to result, as it is superseded by s */ - } - else - { - result.push_back(smmnd); - } - } - - result.push_back(s); - deadlock_summands.swap(result); - } - - static action_name_multiset_list sort_multi_action_labels(const action_name_multiset_list& l) - { - return action_name_multiset_list(l.begin(),l.end(),[](const action_name_multiset& al){ return sort_action_labels(al); }); - } - - /// \brief determine whether the multiaction has the same labels as the allow action, - // in which case true is delivered. If multiaction is the action Terminate, - // then true is also returned. - - bool allowsingleaction(const action_name_multiset& allowaction, - const action_list& multiaction) - { - /* The special cases where multiaction==tau and multiaction=={ Terminated } must have been - dealt with separately. */ - assert(multiaction.size()!=0 && multiaction != action_list({ terminationAction })); - - const identifier_string_list& names=allowaction.names(); - identifier_string_list::const_iterator i=names.begin(); - - for (action_list::const_iterator walker=multiaction.begin(); - walker!=multiaction.end(); ++walker,++i) - { - if (i==names.end()) - { - return false; - } - if (*i!=walker->label().name()) - { - return false; - } - } - return i==names.end(); - } - - bool allow_(const action_name_multiset_list& allowlist, - const action_list& multiaction) - { - /* The empty multiaction, i.e. tau, is never blocked by allow */ - if (multiaction.empty()) - { - return true; - } - - /* The multiaction is equal to the special Terminate action. This action cannot be blocked. */ - if (multiaction == action_list({ terminationAction })) - { - return true; - } - - for (action_name_multiset_list::const_iterator i=allowlist.begin(); - i!=allowlist.end(); ++i) - { - if (allowsingleaction(*i,multiaction)) - { - return true; - } - } - return false; - } - - bool encap(const action_name_multiset_list& encaplist, const action_list& multiaction) - { - for (const action& a: multiaction) - { - assert(encaplist.size()==1); - for (const identifier_string& s1: encaplist.front().names()) - { - const identifier_string s2=a.label().name(); - if (s1==s2) - { - return true; - } - } - } - return false; - } - - void allowblockcomposition( - const action_name_multiset_list& allowlist1, // This is a list of list of identifierstring. - const bool is_allow, - stochastic_action_summand_vector& action_summands, - deadlock_summand_vector& deadlock_summands) - { - /* This function calculates the allow or the block operator, - depending on whether is_allow is true */ - - stochastic_action_summand_vector sourcesumlist; - action_summands.swap(sourcesumlist); - - deadlock_summand_vector resultdeltasumlist; - deadlock_summand_vector resultsimpledeltasumlist; - deadlock_summands.swap(resultdeltasumlist); - - action_name_multiset_list allowlist((is_allow)?sort_multi_action_labels(allowlist1):allowlist1); - - std::size_t sourcesumlist_length=sourcesumlist.size(); - if (sourcesumlist_length>2 || is_allow) // This condition prevents this message to be printed - // when performing data elimination. In this case the - // term delta is linearised, to determine which data - // is essential for all processes. In these cases a - // message about the block operator is very confusing. - { - mCRL2log(mcrl2::log::verbose) << "- calculating the " << (is_allow?"allow":"block") << - " operator on " << sourcesumlist.size() << " action summands and " << resultdeltasumlist.size() << " delta summands"; - } - - /* First add the resulting sums in two separate lists - one for actions, and one for delta's. The delta's - are added at the end to the actions, where for - each delta summand it is determined whether it ought - to be added, or is superseded by an action or another - delta summand */ - for (const stochastic_action_summand& smmnd: sourcesumlist) - { - const variable_list& sumvars=smmnd.summation_variables(); - const action_list multiaction=smmnd.multi_action().actions(); - const data_expression& actiontime=smmnd.multi_action().time(); - const data_expression& condition=smmnd.condition(); - - // Explicitly allow the termination action in any allow. - if ((is_allow && allow_(allowlist,multiaction)) || - (!is_allow && !encap(allowlist,multiaction))) - { - action_summands.push_back(smmnd); - } - else - { - if (smmnd.has_time()) - { - resultdeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock(actiontime))); - } - else - { - // summand has no time. - if (condition==sort_bool::true_()) - { - resultsimpledeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock())); - } - else - { - resultdeltasumlist.push_back(deadlock_summand(sumvars, condition, deadlock())); - } - } - } - } - - if (options.nodeltaelimination) - { - deadlock_summands.swap(resultsimpledeltasumlist); - copy(resultdeltasumlist.begin(),resultdeltasumlist.end(),back_inserter(deadlock_summands)); - } - else - { - if (!options.ignore_time) /* if a delta summand is added, conditional, timed - delta's are subsumed and do not need to be added */ - { - for (const deadlock_summand& summand: resultsimpledeltasumlist) - { - insert_timed_delta_summand(action_summands,deadlock_summands,summand); - } - for (const deadlock_summand& summand: resultdeltasumlist) - { - insert_timed_delta_summand(action_summands,deadlock_summands,summand); - } - } - else - { - // Add a true -> delta - insert_timed_delta_summand(action_summands,deadlock_summands,deadlock_summand(variable_list(),sort_bool::true_(),deadlock())); - } - } - if (mCRL2logEnabled(mcrl2::log::verbose) && (sourcesumlist_length>2 || is_allow)) - { - mCRL2log(mcrl2::log::verbose) << ", resulting in " << action_summands.size() << " action summands and " << deadlock_summands.size() << " delta summands\n"; - } - } - - /**************** renaming ******************************************/ - - action rename_action(const rename_expression_list& renamings, const action& act) - { - const action_label& actionId=act.label(); - const identifier_string& s=actionId.name(); - for (const rename_expression& renaming: renamings) - { - if (s==renaming.source()) - { - return action(action_label(renaming.target(),actionId.sorts()), - act.arguments()); - } - } - return act; - } - - action_list rename_actions(const rename_expression_list& renamings, - const action_list& multiaction) - { - action_list resultactionlist; - - for (const action& a: multiaction) - { - resultactionlist=linInsertActionInMultiActionList( - rename_action(renamings,a), - resultactionlist); - } - return resultactionlist; - } - - void renamecomposition( - const rename_expression_list& renamings, - stochastic_action_summand_vector& action_summands) - { - for (stochastic_action_summand_vector::iterator i=action_summands.begin(); i!=action_summands.end(); ++i) - { - const action_list actions=rename_actions(renamings,i->multi_action().actions()); - - *i= stochastic_action_summand(i->summation_variables(), - i->condition(), - i->multi_action().has_time()?multi_action(actions,i->multi_action().time()):multi_action(actions), - i->assignments(), - i->distribution()); - - } - } - /**************** equalargs ****************************************/ + static bool occursinvarandremove(const variable& var, variable_list& vl) { bool result=false; if (vl.empty()) { - return 0; + return false; } vl.pop_front(); const variable var1=vl.front(); @@ -7743,591 +7365,13 @@ class specification_basic_type /**************** communication operator composition ****************/ - static action_name_multiset sort_action_labels(const action_name_multiset& actionlabels) - { - return action_name_multiset(atermpp::sort_list( - actionlabels.names(), - [](const identifier_string& a1, const identifier_string& a2) - { return std::string(a1) - sort_expression_list get_sorts(const List& l) + static sort_expression_list get_sorts(const List& l) { return sort_expression_list(l.begin(), l.end(), [](const typename List::value_type& d) -> sort_expression {return d.sort();}); } - // Check that the sorts of both termlists match. - data_expression pairwiseMatch(const data_expression_list& l1, const data_expression_list& l2) - { - if (l1.size()!=l2.size()) - { - return sort_bool::false_(); - } - data_expression_list::const_iterator i2=l2.begin(); - data_expression result=sort_bool::true_(); - for(const data_expression& t1: l1) - { - if (t1.sort()!=i2->sort()) - { - return sort_bool::false_(); - } - result=lazy::and_(result,RewriteTerm(equal_to(t1,*i2))); - ++i2; - } - return result; - } - - // a tuple_list contains pairs of actions (multi-action) and the condition under which this action - // can occur. - struct tuple_list - { - std::vector < action_list > actions; - std::vector < data_expression > conditions; - }; - - tuple_list addActionCondition( - const action& firstaction, - const data_expression& condition, - const tuple_list& L, - tuple_list S) - { - /* if firstaction==action(), it should not be added */ - assert(condition!=sort_bool::false_()); // It makes no sense to add an action with condition false, - // as it cannot happen anyhow. - for (std::size_t i=0; i lhs; - std::vector rhs; - std::vector tmp; - std::vector< bool > match_failed; - - comm_entry(const communication_expression_list& communications) - { - for (const communication_expression& l: communications) - { - lhs.push_back(l.action_name().names()); - rhs.push_back(l.name()); - tmp.push_back(identifier_string_list()); - match_failed.push_back(false); - } - } - - ~comm_entry() - {} - - std::size_t size() const - { - assert(lhs.size()==rhs.size() && rhs.size()==tmp.size() && tmp.size()==match_failed.size()); - return lhs.size(); - } - }; - - process::action_label can_communicate(const action_list& m, comm_entry& comm_table) - { - /* this function indicates whether the actions in m - consisting of actions and data occur in C, such that - a communication can take place. If not action_label() is delivered, - otherwise the resulting action is the result. */ - // first copy the left-hand sides of communications for use - for (std::size_t i=0; i rest(comm_table.size(),n); - std::vector < bool > rest_is_null(comm_table.size(),false); - - // check every lhs - for (std::size_t i=0; i(sort_bool::true_()):psi(r,comm_table)); - t.actions.push_back(action_list()); - return t; - } - - const action& firstaction=multiaction.front(); - const action_list& remainingmultiaction=multiaction.tail(); /* This is m in [1] */ - - const tuple_list S=phi(action_list({ firstaction }), - firstaction.arguments(), - action_list(), - remainingmultiaction, - r,r_is_null,comm_table); - action_list tempr=r; - tempr.push_front(firstaction); - const tuple_list T=makeMultiActionConditionList_aux( - remainingmultiaction,comm_table, - (r_is_null) ? action_list({ firstaction }) : tempr, false); - return addActionCondition(firstaction,sort_bool::true_(),T,S); - } - - tuple_list makeMultiActionConditionList( - const action_list& multiaction, - const communication_expression_list& communications) - { - comm_entry comm_table(communications); - return makeMultiActionConditionList_aux(multiaction,comm_table,action_list(),true); - } - - void communicationcomposition( - const communication_expression_list& communications, - const action_name_multiset_list& allowlist1, // This is a list of list of identifierstring. - const bool is_allow, // If is_allow or is_block is set, perform inline allow/block filtering. - const bool is_block, - stochastic_action_summand_vector& action_summands, - deadlock_summand_vector& deadlock_summands) - - { - /* We follow the implementation of Muck van Weerdenburg, described in - a note: Calculation of communication with open terms. */ - - mCRL2log(mcrl2::log::verbose) << - (is_allow ? "- calculating the communication operator modulo the allow operator on " : - is_block ? "- calculating the communication operator modulo the block operator on " : - "- calculating the communication operator on ") << action_summands.size() << " action summands"; - - /* first we sort the multiactions in communications */ - communication_expression_list resultingCommunications; - - for (const communication_expression& comm: communications) - { - const action_name_multiset& source=comm.action_name(); - const identifier_string& target=comm.name(); - resultingCommunications.push_front(communication_expression(sort_action_labels(source),target)); - } - communication_expression_list communications1=resultingCommunications; - - stochastic_action_summand_vector resultsumlist; - deadlock_summand_vector resultingDeltaSummands; - deadlock_summands.swap(resultingDeltaSummands); - - bool inline_allow = is_allow || is_block; - if (inline_allow) - { - // Inline allow is only supported for ignore_time, - // for in other cases generation of delta summands cannot be inlined in any simple way. - assert(!options.nodeltaelimination && options.ignore_time); - deadlock_summands.push_back(deadlock_summand(variable_list(),sort_bool::true_(),deadlock())); - } - action_name_multiset_list allowlist((is_allow)?sort_multi_action_labels(allowlist1):allowlist1); - - for (const stochastic_action_summand& smmnd: action_summands) - { - const variable_list& sumvars=smmnd.summation_variables(); - const action_list multiaction=smmnd.multi_action().actions(); - const data_expression& condition=smmnd.condition(); - const assignment_list& nextstate=smmnd.assignments(); - const stochastic_distribution& dist=smmnd.distribution(); - - if (!inline_allow) - { - /* Recall a delta summand for every non delta summand. - * The reason for this is that with communication, the - * conditions for summands can become much more complex. - * Many of the actions in these summands are replaced by - * delta's later on. Due to the more complex conditions it - * will be hard to remove them. By adding a default delta - * with a simple condition, makes this job much easier - * later on, and will in general reduce the number of delta - * summands in the whole system */ - - /* But first remove free variables from sumvars */ - - variable_vector newsumvars_; - for (const variable& sumvar: sumvars) - { - if (occursinterm(sumvar,condition) || - (smmnd.has_time() && occursinterm(sumvar,smmnd.multi_action().time()))) - { - newsumvars_.push_back(sumvar); - } - } - variable_list newsumvars=variable_list(newsumvars_.begin(), newsumvars_.end()); - - resultingDeltaSummands.push_back(deadlock_summand(newsumvars, - condition, - smmnd.multi_action().has_time()?deadlock(smmnd.multi_action().time()):deadlock())); - } - - /* the multiactionconditionlist is a list containing - tuples, with a multiaction and the condition, - expressing whether the multiaction can happen. All - conditions exclude each other. Furthermore, the list - is not empty. If no communications can take place, - the original multiaction is delivered, with condition - true. */ - - const tuple_list multiactionconditionlist= - makeMultiActionConditionList( - multiaction, - communications1); - - assert(multiactionconditionlist.actions.size()== - multiactionconditionlist.conditions.size()); - for (std::size_t i=0 ; i(actiontime); - if (occursintermlist(t, variable_list_to_data_expression_list(sumvars)) && !occursinterm(t, condition)) + if (occursintermlist(t, variable_list_to_data_expression_list(sumvars)) && !occursinterm(condition, t)) { return true; } @@ -8408,7 +7452,7 @@ class specification_basic_type } for (const variable& v: freevars) { - if (occursinterm(v,result)) + if (occursinterm(result, v)) { variables.push_front(v); } @@ -8416,7 +7460,7 @@ class specification_basic_type for (const variable& v: global_variables) { - if (occursinterm(v,result)) + if (occursinterm(result, v)) { variables.push_front(v); } @@ -8424,7 +7468,7 @@ class specification_basic_type for (const variable& v: sumvars) { - if (occursinterm(v,result)) + if (occursinterm(result, v)) { used_sumvars.push_front(v); } @@ -8719,17 +7763,18 @@ class specification_basic_type maintain_variables_in_rhs< mutable_map_substitution<> > sigma; alphaconvert(sumvars,sigma,summand1.summation_variables(),data_expression_list()); - variable_list sumvars1=summand1.summation_variables() + sumvars; - action_list multiaction1=summand1.multi_action().actions(); - data_expression actiontime1=summand1.multi_action().time(); - data_expression condition1=summand1.condition(); - const assignment_list& nextstate1=summand1.assignments(); + variable_list sumvars1 = summand1.summation_variables() + sumvars; + const action_list& multiaction1 = summand1.multi_action().actions(); + assert(std::is_sorted(multiaction1.begin(), multiaction1.end(), action_compare())); + data_expression actiontime1 = summand1.multi_action().time(); + data_expression condition1 = summand1.condition(); + const assignment_list& nextstate1 = summand1.assignments(); const stochastic_distribution& distribution1=summand1.distribution(); - bool has_time=summand1.has_time(); + bool has_time = summand1.has_time(); if (multiaction1 != action_list({ terminationAction })) { - if (is_allow && !allow_(allowlist,multiaction1)) + if (is_allow && !allow_(allowlist,multiaction1,terminationAction)) { continue; } @@ -8833,7 +7878,8 @@ class specification_basic_type { insert_timed_delta_summand(action_summands, deadlock_summands, - deadlock_summand(sumvars1,condition1, has_time?deadlock(actiontime1):deadlock())); + deadlock_summand(sumvars1,condition1, has_time?deadlock(actiontime1):deadlock()), + options.ignore_time); } } } @@ -8896,7 +7942,7 @@ class specification_basic_type multiaction3=linMergeMultiActionList(multiaction1,multiaction2); } - if (is_allow && !allow_(allowlist,multiaction3)) + if (is_allow && !allow_(allowlist,multiaction3,terminationAction)) { continue; } @@ -8943,6 +7989,7 @@ class specification_basic_type condition3=RewriteTerm(condition3); if (condition3!=sort_bool::false_()) { + assert(std::is_sorted(multiaction3.begin(), multiaction3.end(), action_compare())); action_summands.push_back(stochastic_action_summand( allsums, condition3, @@ -9006,7 +8053,8 @@ class specification_basic_type deadlock_summands, deadlock_summand(allsums, condition3, - has_time3?deadlock(action_time3):deadlock())); + has_time3?deadlock(action_time3):deadlock()), + options.ignore_time); } } @@ -9064,7 +8112,8 @@ class specification_basic_type deadlock_summands, deadlock_summand(allsums, condition3, - has_time3?deadlock(action_time3):deadlock())); + has_time3?deadlock(action_time3):deadlock()), + options.ignore_time); } } @@ -9107,11 +8156,9 @@ class specification_basic_type assert(action_summands.size()==0); assert(deadlock_summands.size()==0); - variable_list allpars; - allpars=par1 + par3; + variable_list allpars = par1 + par3; - bool inline_allow = is_allow || is_block; - if (inline_allow) + if (is_allow || is_block) { // Inline allow is only supported for ignore_time, // for in other cases generation of delta summands cannot be inlined in any simple way. @@ -9363,12 +8410,12 @@ class specification_basic_type { generateLPEmCRLterm(action_summands,deadlock_summands,comm(par).operand(), regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); - communicationcomposition(comm(par).comm_set(),allow(t).allow_set(),true,false,action_summands,deadlock_summands); + communicationcomposition(comm(par).comm_set(),allow(t).allow_set(),true,false,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[this](const data::data_expression& e) { return RewriteTerm(e); }); return; } generateLPEmCRLterm(action_summands,deadlock_summands,par,regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); - allowblockcomposition(allow(t).allow_set(),true,action_summands,deadlock_summands); + allowblockcomposition(allow(t).allow_set(),true,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination); return; } @@ -9401,13 +8448,13 @@ class specification_basic_type regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); // Encode the actions of the block list in one multi action. communicationcomposition(comm(par).comm_set(),action_name_multiset_list( { action_name_multiset(block(t).block_set())} ), - false,true,action_summands,deadlock_summands); + false,true,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[this](const data::data_expression& e) { return RewriteTerm(e); }); return; } generateLPEmCRLterm(action_summands,deadlock_summands,par,regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); // Encode the actions of the block list in one multi action. - allowblockcomposition(action_name_multiset_list({action_name_multiset(block(t).block_set())}),false,action_summands,deadlock_summands); + allowblockcomposition(action_name_multiset_list({action_name_multiset(block(t).block_set())}),false,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination); return; } @@ -9415,7 +8462,7 @@ class specification_basic_type { generateLPEmCRLterm(action_summands,deadlock_summands,process::rename(t).operand(), regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); - renamecomposition(process::rename(t).rename_set(),action_summands); + lps::rename(process::rename(t).rename_set(),action_summands); return; } @@ -9423,7 +8470,7 @@ class specification_basic_type { generateLPEmCRLterm(action_summands,deadlock_summands,comm(t).operand(), regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition); - communicationcomposition(comm(t).comm_set(),action_name_multiset_list(),false,false,action_summands,deadlock_summands); + communicationcomposition(comm(t).comm_set(),action_name_multiset_list(),false,false,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[this](const data::data_expression& e) { return RewriteTerm(e); }); return; } @@ -9492,11 +8539,12 @@ class specification_basic_type { ultimate_delay_condition=getUltimateDelayCondition(action_summands,deadlock_summands,pars); - // The ultimate_delay_condition can be complex. Try to simplify it with a fourier_motzkin reduction. - data_expression simplified_ultimate_delay_condition; - variable_list reduced_sumvars; try { + // The ultimate_delay_condition can be complex. Try to simplify it with a fourier_motzkin reduction. + data_expression simplified_ultimate_delay_condition; + variable_list reduced_sumvars; + fourier_motzkin(ultimate_delay_condition.constraint(), ultimate_delay_condition.variables(), simplified_ultimate_delay_condition, @@ -9871,13 +8919,13 @@ class specification_basic_type it prints the process variables that contain time. Furtermore, it returns whether there are processes that contain an if-then that will be translated to an if-then-else with an delta@0 in the else branch, introducing time */ - bool stable=0; + bool stable=false; bool contains_if_then=false; while (!stable) { std::set < process_identifier > visited; - stable=1; + stable=true; containstime_rec(procId,&stable,visited,contains_if_then); } return contains_if_then; @@ -9913,7 +8961,7 @@ class specification_basic_type for(const variable& v: relevant_stochastic_variables) { new_assignments=push_back(new_assignments,assignment(*i,local_sigma1(v))); - i++; + ++i; } data_expression new_distribution = data::replace_variables_capture_avoiding(sto.distribution(),local_sigma1); @@ -11246,7 +10294,7 @@ class specification_basic_type initial_state, initial_stochastic_distribution, dummy_ultimate_delay_condition); - allowblockcomposition(action_name_multiset_list({action_name_multiset()}),false,action_summands,deadlock_summands); // This removes superfluous delta summands. + allowblockcomposition(action_name_multiset_list({action_name_multiset()}),false,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination); // This removes superfluous delta summands. if (options.final_cluster) { cluster_actions(action_summands,deadlock_summands,parameters); @@ -11261,7 +10309,7 @@ class specification_basic_type mcrl2::lps::stochastic_specification mcrl2::lps::linearise( const mcrl2::process::process_specification& type_checked_spec, - mcrl2::lps::t_lin_options lin_options) + const mcrl2::lps::t_lin_options& lin_options) { mCRL2log(mcrl2::log::verbose) << "linearising the process specification using the '" << lin_options.lin_method << "' method.\n"; mcrl2::process::process_specification input_process=type_checked_spec; diff --git a/libraries/lps/test/linearise_allow_block_test.cpp b/libraries/lps/test/linearise_allow_block_test.cpp new file mode 100644 index 0000000000..e9dce5d4c5 --- /dev/null +++ b/libraries/lps/test/linearise_allow_block_test.cpp @@ -0,0 +1,157 @@ +// Author(s): Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file linearise_allow_block_test.cpp +/// \brief Test for applying allow and block operator + +#define BOOST_TEST_MODULE linearise_allow_block_test +#include +#include + +#include "../include/mcrl2/lps/linearise_allow_block.h" + +using namespace mcrl2; +using namespace mcrl2::process; +using namespace mcrl2::lps; + +struct LogDebug +{ + LogDebug() + { + log::logger::set_reporting_level(log::debug); + } +}; +BOOST_GLOBAL_FIXTURE(LogDebug); + + +inline +process::action make_action(const std::string& name, const data::data_expression_list& arguments = data::data_expression_list()) +{ + data::sort_expression_list sorts; + for(const auto& expression : arguments) + { + sorts.push_front(expression.sort()); + } + sorts = atermpp::reverse(sorts); + + const action_label label(core::identifier_string(name), sorts); + return process::action(label, arguments); +} + +inline +action_name_multiset allow_ab() +{ + core::identifier_string_list result; + result.push_front(core::identifier_string("b")); + result.push_front(core::identifier_string("a")); + return action_name_multiset(result); +} + +inline +action_name_multiset allow_abb() +{ + core::identifier_string_list result; + result.push_front(core::identifier_string("b")); + result.push_front(core::identifier_string("b")); + result.push_front(core::identifier_string("a")); + return action_name_multiset(result); +} + +inline +action_name_multiset allow_cd() +{ + core::identifier_string_list result; + result.push_front(core::identifier_string("d")); + result.push_front(core::identifier_string("c")); + return action_name_multiset(result); +} + +inline +action_name_multiset_list allow_ab_abb_cd() +{ + action_name_multiset_list result; + result.push_front(allow_cd()); + result.push_front(allow_abb()); + result.push_front(allow_ab()); + return result; +} + +BOOST_AUTO_TEST_CASE(test_single_allow) +{ + auto a = make_action("a"); + auto b = make_action("b"); + auto c = make_action("c"); + auto termination_action = make_action("Terminate"); + + action_list a_; + a_.push_front(a); + + BOOST_ASSERT(!allow_(allow_ab(), a_, termination_action)); + BOOST_ASSERT(!allow_(allow_abb(), a_, termination_action)); + BOOST_ASSERT(!allow_(allow_cd(), a_, termination_action)); + + action_list ab; + ab.push_front(b); + ab.push_front(a); + + BOOST_ASSERT(allow_(allow_ab(), ab, termination_action)); + BOOST_ASSERT(!allow_(allow_abb(), ab, termination_action)); + BOOST_ASSERT(!allow_(allow_cd(), ab, termination_action)); + + action_list abb; + abb.push_front(b); + abb.push_front(b); + abb.push_front(a); + + BOOST_ASSERT(!allow_(allow_ab(), abb, termination_action)); + BOOST_ASSERT(allow_(allow_abb(), abb, termination_action)); + BOOST_ASSERT(!allow_(allow_cd(), abb, termination_action)); + + action_list bb; + bb.push_front(b); + bb.push_front(b); + + BOOST_ASSERT(!allow_(allow_ab(), bb, termination_action)); + BOOST_ASSERT(!allow_(allow_abb(), bb, termination_action)); + BOOST_ASSERT(!allow_(allow_cd(), bb, termination_action)); +} + +BOOST_AUTO_TEST_CASE(test_allow) +{ + auto a = make_action("a"); + auto b = make_action("b"); + auto c = make_action("c"); + auto termination_action = make_action("Terminate"); + + BOOST_ASSERT(allow_(allow_ab_abb_cd(), action_list(), termination_action)); + action_list terminate; + terminate.push_front(termination_action); + BOOST_ASSERT(allow_(allow_ab_abb_cd(), terminate, termination_action)); + + action_list a_; + a_.push_front(a); + BOOST_ASSERT(!allow_(allow_ab_abb_cd(), a_, termination_action)); + + action_list ab; + ab.push_front(b); + ab.push_front(a); + BOOST_ASSERT(allow_(allow_ab_abb_cd(), ab, termination_action)); + + action_list abb; + abb.push_front(b); + abb.push_front(b); + abb.push_front(a); + BOOST_ASSERT(allow_(allow_ab_abb_cd(), abb, termination_action)); + + action_list bb; + bb.push_front(b); + bb.push_front(b); + BOOST_ASSERT(!allow_(allow_ab_abb_cd(), bb, termination_action)); +} + +// TODO: extend with tests for block. \ No newline at end of file diff --git a/libraries/lps/test/linearise_communication_test.cpp b/libraries/lps/test/linearise_communication_test.cpp new file mode 100644 index 0000000000..3a0a4c90d7 --- /dev/null +++ b/libraries/lps/test/linearise_communication_test.cpp @@ -0,0 +1,248 @@ +// Author(s): Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file linearise_communication_test.cpp +/// \brief Test for applying communication operator + +#define BOOST_TEST_MODULE linearise_communication_test +#include +#include + +#include "../../process/include/mcrl2/process/detail/alphabet_parse.h" +#include "../include/mcrl2/lps/linearise_communication.h" +#include "../include/mcrl2/lps/parse.h" + +using namespace mcrl2; +using namespace mcrl2::process; +using namespace mcrl2::lps; + +struct LogDebug +{ + LogDebug() + { + log::logger::set_reporting_level(log::debug); + } +}; +BOOST_GLOBAL_FIXTURE(LogDebug); + +/// Return all tuples in l from which the action is in allowed. +inline +lps::detail::tuple_list filter_allow(const lps::detail::tuple_list& l, const action_name_multiset_list& allowed) +{ + lps::detail::tuple_list result; + for (std::size_t i = 0; i < l.size(); ++i) + { + if (allow_(allowed, l.actions[i], action(action_label("Terminate", data::sort_expression_list()), data::data_expression_list()))) + { + result.conditions.push_back(l.conditions[i]); + result.actions.push_back(l.actions[i]); + } + } + return result; +} + +inline +void run_test_case(const std::string& multiaction_str, const data::data_specification& data_spec, + const process::action_label_list& act_decls, const action_name_multiset_list& allow_set, + const communication_expression_list& comm_exprs, std::size_t expected_number_of_multiactions, + std::size_t expected_number_of_multiactions_filtered) +{ + data::rewriter R(data_spec); + const process::action terminate(process::action_label("Terminate", data::sort_expression_list()), data::data_expression_list()); + lps::detail::apply_communication_algorithm alg(terminate, R, comm_exprs, allow_set, true, false); + + const multi_action multiaction(parse_multi_action(multiaction_str, act_decls, data_spec)); + const action_list actions = sort_actions(multiaction.actions()); + + lps::detail::tuple_list result = alg.apply(actions); + BOOST_CHECK_EQUAL(result.size(), expected_number_of_multiactions); + + result = filter_allow(result, allow_set); + BOOST_CHECK_EQUAL(result.size(), expected_number_of_multiactions_filtered); +} + +// The following data specification and multiactions are for a large testcase that is extracted from a real-life case +// study (translating Cordis models to mCRL2). Calculating communication expressions, especially on the large sets +// used to take close to 10 minutes. +inline +data::data_specification data_spec_large() +{ + const std::string spec( + "sort D;\n" + "map d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d26, d27, d28, d29, d30, d31, d32, d33, " + " d34, d35, d36, d37, d38, d39, d40, d41, d42, d43, d44, d45, d46, d47: D;\n" + " d16, d17, d18, d19, d20, d21, d22, d23, d24, d25: Bool;\n" + ); + + return data::parse_data_specification(spec); +} + +inline +action_label_list action_declarations_large() +{ + const std::string decl_d( + "a1, a4, a5, a9, a11, a13, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a56, a57, a64, a83," + "a1_r, a4_r, a5_r, a9_r, a11_r, a13_r, a32_r, a33_r, a34_r, a35_r, a36_r, a37_r, a38_r, a39_r, a40_r, a41_r, a56_r, a57_r, a64_r, a83_r," + "a1_s, a4_s, a5_s, a9_s, a11_s, a13_s, a32_s, a33_s, a34_s, a35_s, a36_s, a37_s, a38_s, a39_s, a40_s, a41_s, a56_s, a57_s, a64_s, a83_s: D;"); + const std::string decl_bool( + "a22, a23, a24, a25, a26, a27, a28, a29, a30, a31," + "a22_r, a23_r, a24_r, a25_r, a26_r, a27_r, a28_r, a29_r, a30_r, a31_r," + "a22_s, a23_s, a24_s, a25_s, a26_s, a27_s, a28_s, a29_s, a30_s, a31_s: Bool;" + ); + const std::string decl( + "a2, a3, a6, a7, a8, a10, a12, a14, a15, a16, a17, a18, a19, a20, a21, a42, a43, a44, a45, a46, a47, a48, a49," + "a50, a51, a52, a53, a54, a55, a58, a59, a60, a61, a62, a63, a65, a66, a67, a68, a69, a70, a71, a72," + "a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, " + "a2_r, a3_r, a6_r, a7_r, a8_r, a10_r, a12_r, a14_r, a15_r, a16_r, a17_r, a18_r, a19_r, a20_r, a21_r, a42_r, a43_r, a44_r, a45_r, a46_r, a47_r, a48_r, a49_r," + "a50_r, a51_r, a52_r, a53_r, a54_r, a55_r, a58_r, a59_r, a60_r, a61_r, a62_r, a63_r, a65_r, a66_r, a67_r, a68_r, a69_r, a70_r, a71_r, a72_r," + "a73_r, a74_r, a75_r, a76_r, a77_r, a78_r, a79_r, a80_r, a81_r, a82_r, " + "a2_s, a3_s, a6_s, a7_s, a8_s, a10_s, a12_s, a14_s, a15_s, a16_s, a17_s, a18_s, a19_s, a20_s, a21_s, a42_s, a43_s, a44_s, a45_s, a46_s, a47_s, a48_s, a49_s," + "a50_s, a51_s, a52_s, a53_s, a54_s, a55_s, a58_s, a59_s, a60_s, a61_s, a62_s, a63_s, a65_s, a66_s, a67_s, a68_s, a69_s, a70_s, a71_s, a72_s," + "a73_s, a74_s, a75_s, a76_s, a77_s, a78_s, a79_s, a80_s, a81_s, a82_s," + "b0, b1, b2, b3, b4, b5;" + ); + const action_label_list act_d(parse_action_declaration(decl_d, data_spec_large())); + const action_label_list act_bool(parse_action_declaration(decl_bool, data_spec_large())); + const action_label_list act(parse_action_declaration(decl, data_spec_large())); + + return act_d + act_bool + act; +} + +inline +action_name_multiset_list allow_set_large() +{ + const std::string allow_string( + "{ b1, b2, b3, a1 | a4 | a5 | a9 | a10 | a11 | a13 | a56 | a57 | a64, a1 | a4 | a5 | a9 | a11 | a13 | a56 | a57 | a64," + " a1 | a4 | a5 | a9 | a11 | a13 | a64, a1 | a8 | a64, a1 | a8 | a64 | a63, a1 | a11 | a64, a1 | a12 | a64, a1 | a20 | a64," + " a1 | a64, a1 | a64 | a63, a1 | a64 | a63 | a65, a2, a3, a4 | a5 | a9 | a20 | a64, a4 | a5 | a9 | a40 | a54 | a64 | a72," + " a4 | a5 | a13 | a20 | a64, a4 | a5 | a13 | a39 | a52 | a64 | a71, a4 | a9 | a20 | a64, a4 | a9 | a54 | a64 | a70," + " a4 | a20 | a64, a4 | a20 | a64 | a73, a4 | a39 | a52 | a64, a4 | a39 | a52 | a64 | a71, a4 | a52 | a64, a4 | a52 | a64 | a68," + " a5 | a13 | a20 | a64, a5 | a13 | a52 | a64 | a69, a5 | a20 | a64, a5 | a20 | a64 | a74, a5 | a40 | a54 | a64," + " a5 | a40 | a54 | a64 | a72, a5 | a54 | a64, a5 | a54 | a64 | a68, a6, a7, a8 | a20 | a52 | a64 | a63 | a76," + " a8 | a20 | a54 | a64 | a63 | a76, a8 | a20 | a64 | a63, a8 | a20 | a64 | a63 | a76, a9 | a20 | a64, a9 | a52 | a64," + " a13 | a20 | a64, a13 | a54 | a64, a14, a15, a16, a17, a18, a19, a20, a20 | a52 | a54 | a64 | a63 | a65," + " a20 | a52 | a64 | a63 | a65, a20 | a54 | a64 | a63 | a65, a20 | a64, a20 | a64 | a63 | a65, a20 | a64 | a66 | a67," + " a20 | a64 | a74, a21, a22 | a23 | a24 | a25 | a26 | a27 | a28 | a29 | a30 | a31 | a32 | a33 | a34 | a35 | a36 | a37 | a38 | a39 | a40 | a41," + " a22 | a32, a23 | a33, a27 | a37, a28 | a38, a29 | a39, a30 | a40, a31 | a41, a39 | a52 | a64, a40 | a54 | a64," + " a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52 | a64, a52 | a64 | a68, a52 | a64 | a71, a53, a54 | a64," + " a54 | a64 | a68, a54 | a64 | a72, a55, a58, a59, a60, a61, a62, a64, a64 | a63, a64 | a63 | a65, a64 | a66 | a67," + " a75, a77, a78, a79, a80, a81, a82, a83, b4, b5 }" + ); + return sort_multi_action_labels(process::detail::parse_allow_set(allow_string)); +} + +inline +communication_expression_list comm_set_large() +{ + const std::string comm_string("{ a1_r | a1_s -> a1, a2_r | a2_s -> a2, a3_r | a3_s -> a3, a4_r | a4_s -> a4, a5_r | a5_s -> a5," + "a6_r | a6_s -> a6, a7_r | a7_s -> a7, a8_r | a8_s -> a8, a9_r | a9_s -> a9, a10_r | a10_s -> a10, a11_r | a11_s -> a11," + "a12_r | a12_s -> a12, a13_r | a13_s -> a13, a14_r | a14_s -> a14, a15_r | a15_s -> a15, a16_r | a16_s -> a16, a17_r | a17_s -> a17," + "a18_r | a18_s -> a18, a19_r | a19_s -> a19, a20_r | a20_s -> a20, a21_r | a21_s -> a21, a22_r | a22_s -> a22, a23_r | a23_s -> a23," + "a24_r | a24_s -> a24, a25_r | a25_s -> a25, a26_r | a26_s -> a26, a27_r | a27_s -> a27, a28_r | a28_s -> a28, a29_r | a29_s -> a29," + "a30_r | a30_s -> a30, a31_r | a31_s -> a31, a32_r | a32_s -> a32, a33_r | a33_s -> a33, a34_r | a34_s -> a34, a35_r | a35_s -> a35," + "a36_r | a36_s -> a36, a37_r | a37_s -> a37, a38_r | a38_s -> a38, a39_r | a39_s -> a39, a40_r | a40_s -> a40, a41_r | a41_s -> a41," + "a42_r | a42_s -> a42, a43_r | a43_s -> a43, a44_r | a44_s -> a44, a45_r | a45_s -> a45, a46_r | a46_s -> a46, a47_r | a47_s -> a47," + "a48_r | a48_s -> a48, a49_r | a49_s -> a49, a50_r | a50_s -> a50, a51_r | a51_s -> a51, a52_r | a52_s -> a52, a53_r | a53_s -> a53," + "a54_r | a54_s -> a54, a55_r | a55_s -> a55, a56_r | a56_s -> a56, a57_r | a57_s -> a57, a58_r | a58_s -> a58, a59_r | a59_s -> a59," + "a60_r | a60_s -> a60, a61_r | a61_s -> a61, a62_r | a62_s -> a62, a63_r | a63_s -> a63, a64_r | a64_s -> a64, a65_r | a65_s -> a65," + "a66_r | a66_s -> a66, a67_r | a67_s -> a67, a68_r | a68_s -> a68, a69_r | a69_s -> a69, a70_r | a70_s -> a70, a71_r | a71_s -> a71," + "a72_r | a72_s -> a72, a73_r | a73_s -> a73, a74_r | a74_s -> a74, a75_r | a75_s -> a75, a76_r | a76_s -> a76, a77_r | a77_s -> a77," + "a78_r | a78_s -> a78, a79_r | a79_s -> a79, a80_r | a80_s -> a80, a81_r | a81_s -> a81, a82_r | a82_s -> a82, a83_r | a83_s -> a83 }"); + + return sort_communications(process::detail::parse_comm_set(comm_string)); +} + +// Show that the number of multiactions in the result can be dramatically reduced +BOOST_AUTO_TEST_CASE(test_multact_19_pruning) +{ + run_test_case( + "a1_r(d1)|a1_s(d2)|a4_r(d3)|a4_s(d4)|a5_r(d5)|a5_s(d6)|a9_r(d7)|a9_s(d8)|a11_r(d9)|a11_s(d10)|a13_r(d9)|a13_s(d11)|" + "a56_r(d12)|a56_s(d13)|a57_r(d9)|a57_s(d14)|a64_r(d15)|a64_s(d47)|a82_r", + data_spec_large(), + action_declarations_large(), + allow_set_large(), + comm_set_large(), + 0, + 0 + ); +} + +BOOST_AUTO_TEST_CASE(test_multact_19a) +{ + run_test_case( + "a1_r(d1)|a1_s(d2)|a4_r(d3)|a4_s(d4)|a5_r(d5)|a5_s(d6)|a9_r(d7)|a9_s(d8)|a11_r(d9)|a11_s(d10)|a13_r(d9)|a13_s(d11)|" + "a56_r(d12)|a56_s(d13)|a57_r(d9)|a57_s(d14)|a64_r(d15)|a64_s(d47)|a82_r", + data_spec_large(), + action_declarations_large(), + sort_multi_action_labels(process::detail::parse_allow_set("{ a1|a4|a5|a9|a11|a13|a56|a57|a64|a82_r }")), + comm_set_large(), + 1, + 1 + ); +} + + +BOOST_AUTO_TEST_CASE(test_multact_19b) +{ + run_test_case( + "a1_r(d1)|a1_s(d2)|a4_r(d3)|a4_s(d4)|a5_r(d5)|a5_s(d6)|a9_r(d7)|a9_s(d8)|a11_r(d9)|a11_s(d10)|a13_r(d9)|a13_s(d11)|" + "a56_r(d12)|a56_s(d13)|a57_r(d9)|a57_s(d14)|a64_r(d15)|a64_s(d47)|a82_r", + data_spec_large(), + action_declarations_large(), + sort_multi_action_labels(process::detail::parse_allow_set("{ a1|a4|a5|a9|a11|a13|a56|a57|a64|a82_r, a1|a4_r|a4_s|a5|a9|a11|a13|a56|a57|a64|a82_r }")), + comm_set_large(), + 2, + 2 + ); +} + +BOOST_AUTO_TEST_CASE(test_multact_19c) +{ + run_test_case( + "a1_r(d1)|a1_s(d2)|a4_r(d3)|a4_s(d4)|a5_r(d5)|a5_s(d6)|a9_r(d7)|a9_s(d8)|a11_r(d9)|a11_s(d10)|a13_r(d9)|a13_s(d11)|" + "a56_r(d12)|a56_s(d13)|a57_r(d9)|a57_s(d14)|a64_r(d15)|a64_s(d47)|a82_r", + data_spec_large(), + action_declarations_large(), + sort_multi_action_labels(process::detail::parse_allow_set("{ a1|a4|a5|a9|a11|a13|a56|a57|a64|a82 }")), + comm_set_large(), + 0, + 0 + ); +} + +BOOST_AUTO_TEST_CASE(test_multact_41a) +{ + run_test_case( + "a22_r(d16)|a22_s(true)|a23_r(d17)|a23_s(true)|a24_r(d18)|a24_s(true)|a25_r(d19)|a25_s(true)|a26_r(d20)|" + "a26_s(true)|a27_r(d21)|a27_s(true)|a28_r(d22)|a28_s(true)|a29_r(d23)|a29_s(true)|a30_r(d24)|a30_s(true)|a31_r(d25)|" + "a31_s(true)|a32_r(d26)|a32_s(d27)|a33_r(d28)|a33_s(d29)|a34_r(d30)|a34_s(d31)|a35_r(d32)|a35_s(d33)|a36_r(d34)|" + "a36_s(d35)|a37_r(d36)|a37_s(d37)|a38_r(d38)|a38_s(d39)|a39_r(d40)|a39_s(d41)|a40_r(d42)|a40_s(d43)|a41_r(d44)|a41_s(d45)|b4", + data_spec_large(), + action_declarations_large(), + allow_set_large(), + comm_set_large(), + 1, + 0 + ); +} + +BOOST_AUTO_TEST_CASE(test_multact_41b) +{ + run_test_case( + "a22_r(d16)|a22_s(true)|a23_r(d17)|a23_s(true)|a24_r(d18)|a24_s(true)|a25_r(d19)|a25_s(true)|a26_r(d20)|" + "a26_s(true)|a27_r(d21)|a27_s(true)|a28_r(d22)|a28_s(true)|a29_r(d23)|a29_s(true)|a30_r(d24)|a30_s(true)|a31_r(d25)|" + "a31_s(true)|a32_r(d26)|a32_s(d27)|a33_r(d28)|a33_s(d29)|a34_r(d30)|a34_s(d31)|a35_r(d32)|a35_s(d33)|a36_r(d34)|" + "a36_s(d35)|a37_r(d36)|a37_s(d37)|a38_r(d38)|a38_s(d39)|a39_r(d40)|a39_s(d41)|a40_r(d42)|a40_s(d43)|a41_r(d44)|a41_s(d45)|a83_s(d46)", + data_spec_large(), + action_declarations_large(), + allow_set_large(), + comm_set_large(), + 0, + 0 + ); +} diff --git a/libraries/lps/test/linearise_rename_test.cpp b/libraries/lps/test/linearise_rename_test.cpp new file mode 100644 index 0000000000..08440a4b63 --- /dev/null +++ b/libraries/lps/test/linearise_rename_test.cpp @@ -0,0 +1,183 @@ +// Author(s): Jeroen Keiren +// Copyright: see the accompanying file COPYING or copy at +// https://github.com/mCRL2org/mCRL2/blob/master/COPYING +// +// Distributed under the Boost Software License, Version 1.0. +// (See accompanying file LICENSE_1_0.txt or copy at +// http://www.boost.org/LICENSE_1_0.txt) +// +/// \file linearise_rename_test.cpp +/// \brief Test for applying rename operator + +#define BOOST_TEST_MODULE linearise_rename_test +#include +#include + +#include "../../process/include/mcrl2/process/rename_expression.h" +#include "../include/mcrl2/lps/linearise_rename.h" + +using namespace mcrl2; +using namespace mcrl2::process; +using namespace mcrl2::lps; + +struct LogDebug +{ + LogDebug() + { + log::logger::set_reporting_level(log::debug); + } +}; +BOOST_GLOBAL_FIXTURE(LogDebug); + +inline +process::action make_action(const std::string& name, const data::data_expression_list& arguments = data::data_expression_list()) +{ + data::sort_expression_list sorts; + for(const auto& expression : arguments) + { + sorts.push_front(expression.sort()); + } + sorts = atermpp::reverse(sorts); + + const action_label label(core::identifier_string(name), sorts); + return process::action(label, arguments); +} + +inline +rename_expression_list rename_rule_ab() +{ + rename_expression_list result; + result.push_front(rename_expression("a", "b")); + return result; +} + +inline +rename_expression_list rename_rule_cd() +{ + rename_expression_list result; + result.push_front(rename_expression("c", "d")); + return result; +} + +inline +rename_expression_list rename_rules_ab_cd() +{ + rename_expression_list result; + result.push_front(rename_expression("c", "d")); + result.push_front(rename_expression("a", "b")); + return result; +} + +BOOST_AUTO_TEST_CASE(test_rename_action) +{ + auto a = make_action("a"); + auto b = make_action("b"); + auto c = make_action("c"); + auto d = make_action("d"); + auto e = make_action("e"); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), a), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), c), c); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), e), e); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), a), a); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), c), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), e), e); + + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), a), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), c), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), e), e); +} + +BOOST_AUTO_TEST_CASE(test_rename_action_with_sort) +{ + auto a = make_action("a", {data::sort_bool::true_()}); + auto b = make_action("b", {data::sort_bool::true_()}); + auto c = make_action("c", {data::variable("x", data::basic_sort("D"))}); + auto d = make_action("d", {data::variable("x", data::basic_sort("D"))}); + auto e = make_action("e"); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), a), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), c), c); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), e), e); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), a), a); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), c), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), e), e); + + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), a), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), b), b); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), c), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), d), d); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), e), e); +} + +BOOST_AUTO_TEST_CASE(test_rename_action_list) +{ + auto a = make_action("a"); + auto b = make_action("b"); + auto c = make_action("c"); + auto d = make_action("d"); + auto e = make_action("e"); + + action_list ab; + ab.push_front(b); + ab.push_front(a); + + action_list bb; + bb.push_front(b); + bb.push_front(b); + + action_list bc; + bc.push_front(c); + bc.push_front(b); + + action_list bd; + bd.push_front(d); + bd.push_front(b); + + action_list cd; + cd.push_front(d); + cd.push_front(c); + + action_list dd; + dd.push_front(d); + dd.push_front(d); + + action_list de; + de.push_front(e); + de.push_front(d); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), ab), bb); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), bb), bb); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), bc), bc); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), bd), bd); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), cd), cd); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_ab(), de), de); + + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), ab), ab); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), bb), bb); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), bc), bd); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), bd), bd); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), cd), dd); + BOOST_CHECK_EQUAL(lps::rename(rename_rule_cd(), de), de); + + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), ab), bb); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), bb), bb); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), bc), bd); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), bd), bd); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), cd), dd); + BOOST_CHECK_EQUAL(lps::rename(rename_rules_ab_cd(), de), de); +} + +// TODO: extend with tests for renaming multiactions, summands and lps. \ No newline at end of file diff --git a/tests/regression/tickets/1114/1.aut b/tests/regression/tickets/1114/1.aut new file mode 100644 index 0000000000..6a93101b8d --- /dev/null +++ b/tests/regression/tickets/1114/1.aut @@ -0,0 +1,85 @@ +des (0,84,31) +(0,"tau",1) +(0,"tau",2) +(0,"tau",3) +(0,"b",4) +(0,"b",5) +(0,"b",6) +(0,"b",7) +(1,"b",8) +(1,"tau",3) +(1,"b",9) +(1,"b",5) +(1,"b",7) +(2,"tau",3) +(2,"b",10) +(2,"b",11) +(2,"b",6) +(2,"b",7) +(3,"b",9) +(3,"b",11) +(3,"b",7) +(4,"tau",5) +(4,"tau",6) +(4,"tau",7) +(5,"b",12) +(5,"tau",7) +(5,"b",13) +(6,"tau",7) +(6,"b",14) +(6,"b",15) +(7,"b",13) +(7,"b",15) +(8,"tau",9) +(8,"b",12) +(8,"b",13) +(9,"b",16) +(9,"b",13) +(10,"tau",11) +(10,"tau",17) +(10,"tau",18) +(10,"b",14) +(10,"b",15) +(10,"b",19) +(11,"b",16) +(11,"tau",18) +(11,"b",20) +(11,"b",15) +(11,"b",21) +(12,"tau",13) +(13,"b",22) +(14,"tau",15) +(14,"tau",19) +(14,"tau",21) +(15,"b",22) +(15,"tau",21) +(15,"b",23) +(16,"tau",20) +(16,"b",22) +(16,"b",23) +(17,"tau",18) +(17,"b",24) +(17,"b",25) +(17,"b",19) +(17,"b",21) +(18,"b",20) +(18,"b",25) +(18,"b",21) +(19,"tau",21) +(19,"b",26) +(19,"b",27) +(20,"b",28) +(20,"b",23) +(21,"b",23) +(21,"b",27) +(22,"tau",23) +(23,"b",29) +(24,"tau",25) +(24,"b",26) +(24,"b",27) +(25,"b",28) +(25,"b",27) +(26,"tau",27) +(27,"b",29) +(28,"b",29) +(29,"Terminate",30) diff --git a/tests/regression/tickets/1114/2.aut b/tests/regression/tickets/1114/2.aut new file mode 100644 index 0000000000..1e8e4e6a3c --- /dev/null +++ b/tests/regression/tickets/1114/2.aut @@ -0,0 +1,3 @@ +des (0,2,2) +(0,"b",1) +(0,"b",1) diff --git a/tests/utility/run_process.py b/tests/utility/run_process.py index 75bef09dd3..02bf061f54 100644 --- a/tests/utility/run_process.py +++ b/tests/utility/run_process.py @@ -115,7 +115,7 @@ def __init__( self._max_memory_used = 0 # Start a thread to limit the process memory and time usage. - def enforce_limits(proc): + def enforce_limits(proc): try: process = psutil.Process(proc.pid) while proc.returncode is None: @@ -142,7 +142,7 @@ def enforce_limits(proc): with concurrent.futures.ThreadPoolExecutor(max_workers=1) as executor: future = executor.submit(enforce_limits, proc) - + try: stdout, stderr = proc.communicate() self.stdout = stdout.decode("utf-8") @@ -157,11 +157,11 @@ def enforce_limits(proc): if proc.returncode != 0: print(self.stderr) raise ToolRuntimeError( - f"Tool {tool} ended with return code {proc.returncode}" + f"Tool {tool} {arguments} ended with return code {proc.returncode}" ) if platform.system() == "Windows" and proc.returncode == -1073740777: raise ToolRuntimeError( - f"Tool {tool} failed with the return code STATUS_INVALID_CRUNTIME_PARAMETER (0xC0000417)" + f"Tool {tool} {arguments} failed with the return code STATUS_INVALID_CRUNTIME_PARAMETER (0xC0000417)" ) if platform.system() == "Windows" and proc.returncode == -1073741571: raise StackOverflowError(tool)