summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--gnu/local.mk2
-rw-r--r--gnu/packages/maths.scm6
-rw-r--r--gnu/packages/patches/mcrl2-fix-1687.patch337
-rw-r--r--gnu/packages/patches/mcrl2-fix-counterexample.patch32
4 files changed, 2 insertions, 375 deletions
diff --git a/gnu/local.mk b/gnu/local.mk
index 2e9954c5a1..1ec6ba4523 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1589,8 +1589,6 @@ dist_patch_DATA = \
%D%/packages/patches/maxima-defsystem-mkdir.patch \
%D%/packages/patches/maven-generate-component-xml.patch \
%D%/packages/patches/maven-generate-javax-inject-named.patch \
- %D%/packages/patches/mcrl2-fix-1687.patch \
- %D%/packages/patches/mcrl2-fix-counterexample.patch \
%D%/packages/patches/mcrypt-CVE-2012-4409.patch \
%D%/packages/patches/mcrypt-CVE-2012-4426.patch \
%D%/packages/patches/mcrypt-CVE-2012-4527.patch \
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 420f1894f3..8b765e886b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -6555,17 +6555,15 @@ reduction.")
(define-public mcrl2
(package
(name "mcrl2")
- (version "202206.0")
+ (version "202206.1")
(source (origin
(method url-fetch)
(uri (string-append
"https://www.mcrl2.org/download/release/mcrl2-"
version ".tar.gz"))
- (patches (search-patches "mcrl2-fix-1687.patch"
- "mcrl2-fix-counterexample.patch"))
(sha256
(base32
- "0alpck09pbvwk4axqmrvcjmsabsn20yayq5b3apq284n0hcbf01q"))))
+ "1rbfyw47bi31qla1sa4fd1npryb5kbdr0vijmdc2gg1zhpqfv0ia"))))
(inputs
(list boost glu mesa qtbase-5))
(build-system cmake-build-system)
diff --git a/gnu/packages/patches/mcrl2-fix-1687.patch b/gnu/packages/patches/mcrl2-fix-1687.patch
deleted file mode 100644
index 449ecbf638..0000000000
--- a/gnu/packages/patches/mcrl2-fix-1687.patch
+++ /dev/null
@@ -1,337 +0,0 @@
-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
-
diff --git a/gnu/packages/patches/mcrl2-fix-counterexample.patch b/gnu/packages/patches/mcrl2-fix-counterexample.patch
deleted file mode 100644
index abf541f50c..0000000000
--- a/gnu/packages/patches/mcrl2-fix-counterexample.patch
+++ /dev/null
@@ -1,32 +0,0 @@
-Taken from upstream:
- https://github.com/mCRL2org/mCRL2/commit/435421429dde9dcc5956e8a978597111a3947ec1
-
-Fixes bug in ltscompare:
- https://listserver.tue.nl/pipermail/mcrl2-users/2022-June/000396.html
-
-From 435421429dde9dcc5956e8a978597111a3947ec1 Mon Sep 17 00:00:00 2001
-From: Maurice Laveaux <m.laveaux@tue.nl>
-Date: Wed, 29 Jun 2022 10:27:58 +0200
-Subject: [PATCH] Write counterexample's structured output trace on single
- line.
-
----
- libraries/lts/include/mcrl2/lts/detail/counter_example.h | 2 +-
- 1 file changed, 1 insertion(+), 1 deletion(-)
-
-diff --git a/libraries/lts/include/mcrl2/lts/detail/counter_example.h b/libraries/lts/include/mcrl2/lts/detail/counter_example.h
-index c339cfde4..ca3967768 100644
---- a/libraries/lts/include/mcrl2/lts/detail/counter_example.h
-+++ b/libraries/lts/include/mcrl2/lts/detail/counter_example.h
-@@ -139,7 +139,7 @@ class counter_example_constructor
- if (m_structured_output)
- {
- std::cout << m_name << ": ";
-- result.save("", mcrl2::lts::trace::tfPlain); // Write to stdout.
-+ result.save("", mcrl2::lts::trace::tfLine); // Write to stdout.
- }
- else
- {
---
-2.35.1
-