diff options
author | Jan (janneke) Nieuwenhuizen <janneke@gnu.org> | 2022-06-27 18:35:27 +0200 |
---|---|---|
committer | Jan (janneke) Nieuwenhuizen <janneke@gnu.org> | 2022-07-01 15:45:37 +0200 |
commit | 36a0ec9e784b74478f740474e7c3b8138372c3c3 (patch) | |
tree | e7602ec1a8f8b5a5a273b7376bf447ce0ab9dfa1 /gnu/packages/patches/mcrl2-fix-1687.patch | |
parent | 81cf674a5d5e3dc020df5d43ce62e1c98f2c9711 (diff) | |
download | guix-36a0ec9e784b74478f740474e7c3b8138372c3c3.tar.gz |
gnu: mcrl2: Update to 202206.0.
* gnu/packages/patches/mcrl2-fix-1687.patch, gnu/packages/patches/mcrl2-fix-counterexample.patch: New files. * gnu/local.mk (dist_patch_DATA): Add them. * gnu/packages/maths.scm (mcrl2): Update to 202206.0 and use them.
Diffstat (limited to 'gnu/packages/patches/mcrl2-fix-1687.patch')
-rw-r--r-- | gnu/packages/patches/mcrl2-fix-1687.patch | 337 |
1 files changed, 337 insertions, 0 deletions
diff --git a/gnu/packages/patches/mcrl2-fix-1687.patch b/gnu/packages/patches/mcrl2-fix-1687.patch new file mode 100644 index 0000000000..449ecbf638 --- /dev/null +++ b/gnu/packages/patches/mcrl2-fix-1687.patch @@ -0,0 +1,337 @@ +Taken from upstream: + https://github.com/mCRL2org/mCRL2/commit/f38998be5198236bc5bf5a957b0e132d6d6d8bee + +Fixes bug in ltsconvert: + https://listserver.tue.nl/pipermail/mcrl2-users/2022-June/000395.html + +From f38998be5198236bc5bf5a957b0e132d6d6d8bee Mon Sep 17 00:00:00 2001 +From: Jan Friso Groote <J.F.Groote@tue.nl> +Date: Tue, 28 Jun 2022 12:27:47 +0200 +Subject: [PATCH] Solved bug report #1687 + +Hidden actions were not properly recognized in ltsconvert. Multiactions +that were partly hidden compared with the default action label, and had +to be compared with a tau-action. This caused multiple tau-actions to be +listed in the list of actions of an lts, and this caused other tools to +go astray. + +The code to rename actions has completely be rewritten. + +This should solve #1687. + +A test have been added. +--- + libraries/lts/include/mcrl2/lts/lts.h | 95 ++++++++++++++++++++++--- + libraries/lts/test/lts_test.cpp | 61 ++++++++-------- + tools/release/ltsconvert/ltsconvert.cpp | 3 +- + 3 files changed, 116 insertions(+), 43 deletions(-) + +diff --git a/libraries/lts/include/mcrl2/lts/lts.h b/libraries/lts/include/mcrl2/lts/lts.h +index 095031e7c..8562eb900 100644 +--- a/libraries/lts/include/mcrl2/lts/lts.h ++++ b/libraries/lts/include/mcrl2/lts/lts.h +@@ -25,6 +25,7 @@ + #include <algorithm> + #include <cassert> + #include <set> ++#include <map> + #include "mcrl2/lts/transition.h" + #include "mcrl2/lts/lts_type.h" + +@@ -482,40 +483,112 @@ class lts: public LTS_BASE + return; + } + ++ std::map<labels_size_type, labels_size_type> action_rename_map; + for (labels_size_type i=0; i< num_action_labels(); ++i) + { + ACTION_LABEL_T a=action_label(i); + a.hide_actions(tau_actions); +- if (a==ACTION_LABEL_T()) ++ if (a==ACTION_LABEL_T::tau_action()) + { +- m_hidden_label_set.insert(i); ++ if (i!=const_tau_label_index) ++ { ++ m_hidden_label_set.insert(i); ++ } + } + else if (a!=action_label(i)) + { +- set_action_label(i,a); ++ /* In this the action_label i is changed by the tau_actions but not renamed to tau. ++ We check whether a maps onto another action label index. If yes, it is added to ++ the rename map, and we explicitly rename transition labels with this label afterwards. ++ If no, we rename the action label. ++ */ ++ bool found=false; ++ for (labels_size_type j=0; !found && j< num_action_labels(); ++j) ++ { ++ if (a==action_label(j)) ++ { ++ if (i!=j) ++ { ++ action_rename_map[i]=j; ++ } ++ found=true; ++ } ++ } ++ if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a. ++ { ++ set_action_label(i,a); ++ } ++ } ++ } ++ ++ if (action_rename_map.size()>0) // Check whether there are action labels that must be renamed, and ++ { ++ for(transition& t: m_transitions) ++ { ++ auto i = action_rename_map.find(t.label()); ++ if (i!=action_rename_map.end()) ++ { ++ t=transition(t.from(),i->second,t.to()); ++ } + } + } + } + +- /** \brief Apply the recorded actions that are renamed to internal actions to the lts. +- * \details After hiding actions, it checks whether action labels are +- * equal and merges actions with the same labels in the lts. ++ /** \brief Rename the hidden actions in the lts. ++ * \details Multiactions can be partially renamed. I.e. a|b becomes a if b is hidden. ++ * In such a case the new action a is mapped onto an existing action a; if such ++ * a label a does not exist, the action a|b is renamed to a. + * \param[in] tau_actions Vector with strings indicating which actions must be + * transformed to tau's */ +- void apply_hidden_actions(void) ++ void apply_hidden_actions(const std::vector<std::string>& tau_actions) + { +- if (m_hidden_label_set.size()>0) // Check whether there is something to rename. ++ if (tau_actions.size()==0) ++ { ++ return; ++ } ++ ++ std::map<labels_size_type, labels_size_type> action_rename_map; ++ for (labels_size_type i=0; i< num_action_labels(); ++i) ++ { ++ ACTION_LABEL_T a=action_label(i); ++ a.hide_actions(tau_actions); ++#ifndef NDEBUG ++ ACTION_LABEL_T b=a; ++ b.hide_actions(tau_actions); ++ assert(a==b); // hide_actions applied twice yields the same result as applying it once. ++#endif ++ bool found=false; ++ for (labels_size_type j=0; !found && j< num_action_labels(); ++j) ++ { ++ if (a==action_label(j)) ++ { ++ if (i!=j) ++ { ++ action_rename_map[i]=j; ++ } ++ found=true; ++ } ++ } ++ if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a. ++ { ++ set_action_label(i,a); ++ } ++ } ++ ++ ++ if (action_rename_map.size()>0) // Check whether there is something to rename. + { + for(transition& t: m_transitions) + { +- if (m_hidden_label_set.count(t.label())) ++ auto i = action_rename_map.find(t.label()); ++ if (i!=action_rename_map.end()) + { +- t=transition(t.from(),tau_label_index(),t.to()); ++ t=transition(t.from(),i->second,t.to()); + } + } +- m_hidden_label_set.clear(); // Empty the hidden label set. + } + } ++ + /** \brief Checks whether this LTS has state values associated with its states. + * \retval true if the LTS has state information; + * \retval false otherwise. +diff --git a/libraries/lts/test/lts_test.cpp b/libraries/lts/test/lts_test.cpp +index 5840393d9..ad69f6275 100644 +--- a/libraries/lts/test/lts_test.cpp ++++ b/libraries/lts/test/lts_test.cpp +@@ -149,7 +149,7 @@ static void reduce_lts_in_various_ways(const std::string& test_description, + BOOST_CHECK(is_deterministic(l)); + } + +-static void reduce_simple_loop() ++BOOST_AUTO_TEST_CASE(reduce_simple_loop) + { + std::string SIMPLE_AUT = + "des (0,2,2)\n" +@@ -173,7 +173,7 @@ static void reduce_simple_loop() + reduce_lts_in_various_ways("Simple loop", SIMPLE_AUT, expected); + } + +-static void reduce_simple_loop_with_tau() ++BOOST_AUTO_TEST_CASE(reduce_simple_loop_with_tau) + { + std::string SIMPLE_AUT = + "des (0,2,2)\n" +@@ -200,7 +200,7 @@ static void reduce_simple_loop_with_tau() + /* The example below was encountered by David Jansen. The problem is that + * for branching bisimulations the tau may supersede the b, not leading to the + * necessary splitting into two equivalence classes. */ +-static void tricky_example_for_branching_bisimulation() ++BOOST_AUTO_TEST_CASE(tricky_example_for_branching_bisimulation) + { + std::string TRICKY_BB = + "des (0,3,2)\n" +@@ -226,7 +226,7 @@ static void tricky_example_for_branching_bisimulation() + } + + +-static void reduce_abp() ++BOOST_AUTO_TEST_CASE(reduce_abp) + { + std::string ABP_AUT = + "des (0,92,74)\n" +@@ -342,7 +342,7 @@ static void reduce_abp() + + // Peterson's protocol has the interesting property that the number of states modulo branching bisimulation + // differs from the number of states modulo weak bisimulation, as observed by Rob van Glabbeek. +-static void reduce_peterson() ++BOOST_AUTO_TEST_CASE(reduce_peterson) + { + std::string PETERSON_AUT = + "des (0,59,35)\n" +@@ -423,7 +423,7 @@ static void reduce_peterson() + reduce_lts_in_various_ways("Peterson protocol", PETERSON_AUT, expected); + } + +-static void test_reachability() ++BOOST_AUTO_TEST_CASE(test_reachability) + { + std::string REACH = + "des (0,4,5) \n" +@@ -449,7 +449,7 @@ static void test_reachability() + + // The example below caused failures in the GW mlogn branching bisimulation + // algorithm when cleaning the code up. +-static void failing_test_groote_wijs_algorithm() ++BOOST_AUTO_TEST_CASE(failing_test_groote_wijs_algorithm) + { + std::string GWLTS = + "des(0,29,10)\n" +@@ -511,7 +511,7 @@ static void failing_test_groote_wijs_algorithm() + // It has not been implemented fully. The problem is that it is difficult to + // prescribe the order in which refinements have to be done. + +-static void counterexample_jk_1(std::size_t k) ++void counterexample_jk_1(std::size_t k) + { + // numbering scheme of states: + // states 0..k-1 are the blue squares +@@ -571,7 +571,7 @@ static void counterexample_jk_1(std::size_t k) + + // In the meantime, the bug is corrected: this is why the first part of the + // algorithm now follows a much simpler line than previously. +-static void counterexample_postprocessing() ++BOOST_AUTO_TEST_CASE(counterexample_postprocessing) + { + std::string POSTPROCESS_AUT = + "des(0,33,13)\n" +@@ -634,7 +634,7 @@ static void counterexample_postprocessing() + test_lts("postprocessing problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count); + } + +-static void regression_delete_old_bb_slice() ++BOOST_AUTO_TEST_CASE(regression_delete_old_bb_slice) + { + std::string POSTPROCESS_AUT = + "des(0,163,100)\n" +@@ -824,7 +824,7 @@ static void regression_delete_old_bb_slice() + test_lts("regression test for GJKW bug (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count); + } + +-void is_deterministic_test1() ++BOOST_AUTO_TEST_CASE(is_deterministic_test1) + { + std::string automaton = + "des(0,2,2)\n" +@@ -837,7 +837,7 @@ void is_deterministic_test1() + BOOST_CHECK(is_deterministic(l_det)); + } + +-void is_deterministic_test2() ++BOOST_AUTO_TEST_CASE(is_deterministic_test2) + { + std::string automaton = + "des(0,2,2)\n" +@@ -850,24 +850,25 @@ void is_deterministic_test2() + BOOST_CHECK(!is_deterministic(l_det)); + } + +-void test_is_deterministic() ++BOOST_AUTO_TEST_CASE(hide_actions1) + { +- is_deterministic_test1(); +- is_deterministic_test2(); +-} ++ std::string automaton = ++ "des (0,4,3)\n" ++ "(0,\"<state>\",1)\n" ++ "(1,\"return|hello\",2)\n" ++ "(1,\"return\",2)\n" ++ "(2,\"world\",1)\n"; ++ ++ std::istringstream is(automaton); ++ lts::lts_aut_t l; ++ l.load(is); ++ std::vector<std::string>hidden_actions(1,"hello"); ++ l.apply_hidden_actions(hidden_actions); ++ reduce(l,lts::lts_eq_bisim); ++ std::size_t expected_label_count = 5; ++ std::size_t expected_state_count = 3; ++ std::size_t expected_transition_count = 3; ++ test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count); ++ + +-BOOST_AUTO_TEST_CASE(test_main) +-{ +- reduce_simple_loop(); +- reduce_simple_loop_with_tau(); +- tricky_example_for_branching_bisimulation(); +- reduce_abp(); +- reduce_peterson(); +- test_reachability(); +- test_is_deterministic(); +- failing_test_groote_wijs_algorithm(); +- counterexample_jk_1(3); +- counterexample_postprocessing(); +- regression_delete_old_bb_slice(); +- // TODO: Add groote wijs branching bisimulation and add weak bisimulation tests. For the last Peterson is a good candidate. + } +diff --git a/tools/release/ltsconvert/ltsconvert.cpp b/tools/release/ltsconvert/ltsconvert.cpp +index 231deabe2..5645d31d1 100644 +--- a/tools/release/ltsconvert/ltsconvert.cpp ++++ b/tools/release/ltsconvert/ltsconvert.cpp +@@ -123,8 +123,7 @@ class ltsconvert_tool : public input_output_tool + + LTS_TYPE l; + l.load(tool_options.infilename); +- l.record_hidden_actions(tool_options.tau_actions); +- l.apply_hidden_actions(); ++ l.apply_hidden_actions(tool_options.tau_actions); + + if (tool_options.check_reach) + { +-- +2.35.1 + |