[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
01/02: gnu: mcrl2: Update to 202206.0.
|
From: |
guix-commits |
|
Subject: |
01/02: gnu: mcrl2: Update to 202206.0. |
|
Date: |
Fri, 1 Jul 2022 09:48:12 -0400 (EDT) |
janneke pushed a commit to branch master
in repository guix.
commit 36a0ec9e784b74478f740474e7c3b8138372c3c3
Author: Jan (janneke) Nieuwenhuizen <janneke@gnu.org>
AuthorDate: Mon Jun 27 18:35:27 2022 +0200
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.
---
gnu/local.mk | 2 +
gnu/packages/maths.scm | 8 +-
gnu/packages/patches/mcrl2-fix-1687.patch | 337 +++++++++++++++++++++
.../patches/mcrl2-fix-counterexample.patch | 32 ++
4 files changed, 376 insertions(+), 3 deletions(-)
diff --git a/gnu/local.mk b/gnu/local.mk
index 353b91cfd2..3a56ad371d 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1481,6 +1481,8 @@ 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 8268b8954e..e84697c63b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -22,7 +22,7 @@
;;; Copyright © 2017, 2019, 2022 Arun Isaac <arunisaac@systemreboot.net>
;;; Copyright © 2017–2021 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2017 Dave Love <me@fx@gnu.org>
-;;; Copyright © 2018, 2019, 2020, 2021 Jan (janneke) Nieuwenhuizen
<janneke@gnu.org>
+;;; Copyright © 2018, 2019, 2020, 2021, 2022 Jan (janneke) Nieuwenhuizen
<janneke@gnu.org>
;;; Copyright © 2018 Joshua Sierles, Nextjournal <joshua@nextjournal.com>
;;; Copyright © 2018 Nadya Voronova <voronovank@gmail.com>
;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
@@ -6089,15 +6089,17 @@ reduction.")
(define-public mcrl2
(package
(name "mcrl2")
- (version "202106.0")
+ (version "202206.0")
(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
- "1xgx3cd57vc7gbjic24j1q2za6j3ybz6nk4afvvpbwsf33xnlf4v"))))
+ "0alpck09pbvwk4axqmrvcjmsabsn20yayq5b3apq284n0hcbf01q"))))
(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
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
+
diff --git a/gnu/packages/patches/mcrl2-fix-counterexample.patch
b/gnu/packages/patches/mcrl2-fix-counterexample.patch
new file mode 100644
index 0000000000..abf541f50c
--- /dev/null
+++ b/gnu/packages/patches/mcrl2-fix-counterexample.patch
@@ -0,0 +1,32 @@
+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
+