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.

2 files changed, 369 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
+
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
+