Merge remote-tracking branch 'upstream/master' into HEAD

CHANGES

@@ -1,3 +1,26 @@
+===============================================================================
+Changes between toolset releases 202106.0 and 202206.0:
+===============================================================================
+
+This release brings two new tools and several improvements to existing tools.
+First of all, lpsreach is a new state space exploration tool that uses symbolic
+representations to effectively operate on state spaces consisting with billions
+of states. Next, pbessolvesymbolic is a tool to solve parameterised Boolean
+equation systems (PBESs) based on similar techniques. Both tools are
+unfortunately not yet available on Windows. Another major limitation of
+pbessolvesymbolic is that it can not yet produce counter examples.
+
+The ltscompare tool has been extended with generating distinguishing formulas
+for trace and (divergence-preserving branching) bisimulation equivalences for
+options 'bisim-gv', '(dp)branching-bisim-gv' and 'trace'. These formulas can be
+used to generate counter examples that can explain why two state spaces are
+distinct. 
+
+28 bug reports were resolved since the last release.
+List of other changes:
+  - Tool pbesconstelm has been extended with '--check-quantifiers' to
+    eliminate constant quantified parameters.
+
 ===============================================================================
 Changes between toolset releases 202006.0 and 202106.0:
 ===============================================================================

CMakeLists.txt

@@ -48,6 +48,7 @@ option(MCRL2_ENABLE_HEADER_TESTS    "Enable generation of headertest targets." O
 option(MCRL2_ENABLE_TESTS           "Enable generation of library, tool and random test targets." OFF)
 option(MCRL2_ENABLE_DOCUMENTATION   "Enable generation of documentation." OFF)
 option(MCRL2_ENABLE_BENCHMARKS      "Enable benchmarks. Build the 'benchmarks' target to generate the necessary files and tools. Run the benchmarks using ctest." OFF)
+option(MCRL2_ENABLE_SYLVAN          "Enable the Sylvan library required by the following symbolic tools: lpsreach, pbessolvesymbolic and ltsconvertsymbolic" ${UNIX})
 option(MCRL2_EXTRA_TOOL_TESTS       "Enable testing of tools on more mCRL2 specifications." OFF)
 option(MCRL2_TEST_JITTYC            "Also test the compiling rewriters in the library tests. This can be time consuming." OFF)
 set(MCRL2_QT_APPS "" CACHE INTERNAL "Internally keep track of Qt apps for the packaging procedure")
@@ -87,7 +88,7 @@ if(MCRL2_ENABLE_CODE_COVERAGE)
 endif()
 
 add_subdirectory(3rd-party/dparser)
-if (UNIX)
+if (MCRL2_ENABLE_SYLVAN)
   add_subdirectory(3rd-party/sylvan/src)
 endif()
 

COPYING

@@ -1,5 +1,5 @@
 mCRL2 toolset
-Copyright (C) 2005-2019 Eindhoven University of Technology.
+Copyright (C) 2005-2022 Eindhoven University of Technology.
 
 All files except for those found under the 3rd-party directory are distributed
 under the Boost Software License, Version 1.0 (see accompanying file

README

@@ -16,6 +16,6 @@ does not answer, send a mail to <[email protected]>.
 
 -----
 
-Copyright (C) 2005-2019 Eindhoven University of Technology
+Copyright (C) 2005-2022 Eindhoven University of Technology
 
 See the file COPYING for license information.

README.md

@@ -29,8 +29,10 @@ mCRL2 has the following minimum dependencies:
  - Boost (Linux: 1.65.1, MacOS/Windows: 1.67.0)
 
 Furthermore, sphinx and xsltproc are required to build the documentation.
-Makefiles can be generated using cmake. To build the toolset in Release mode
-using 4 threads, run the following commands (preferably in an empty directory):
+Makefiles can be generated using cmake. The compiling rewriter and the symbolic
+tools (lpsreach and pbessolvesymbolic) are only available for MacOS and Linux.
+qTo build the toolset in Release mode using 4 threads, run the following
+commands (preferably in an empty directory):
 
 ```
 git clone https://github.com/mCRL2org/mCRL2 src
@@ -40,7 +42,7 @@ make -j4
 ```
 
 When compilation is finished, the binaries can be found in `stage/bin/`.
-Convenient front-ends for cmake are ccmake (macOS/Linux) and cmake-gui. Under
+Convenient front-ends for cmake are ccmake (MacOS/Linux) and cmake-gui. Under
 Windows and macOS, it is usually necessary to set the variables
 `Boost_INCLUDE_DIR` and `Qt5_DIR` manually. More build instructions can be found
 in the
@@ -58,7 +60,7 @@ If you have questions about using the mCRL2 toolset which the documentation does
 not answer, send a mail to <[email protected]> or open an issue.
 
 ## License
-Copyright (C) 2005-2019 Eindhoven University of Technology  
+Copyright (C) 2005-2022 Eindhoven University of Technology  
 mCRL2 is licensed under the [Boost
 license](https://www.boost.org/LICENSE_1_0.txt). See the file COPYING for
 detailed license information.

benchmarks/CMakeLists.txt

@@ -98,7 +98,7 @@ foreach(benchmark ${STATESPACE_BENCHMARKS} ${GAME_BENCHMARKS})
 endforeach()
 
 # Only add the symbolic benchmarks when the tools are part of the build, i.e., developer tools enabled and Sylvan can be compiled.
-if (MCRL2_ENABLE_DEVELOPER AND TARGET sylvan)
+if (MCRL2_ENABLE_EXPERIMENTAL AND MCRL2_ENABLE_SYLVAN)
 
   add_dependencies(benchmarks lpsreach pbessolvesymbolic)
 

build/cmake/ConfigureCompiler.cmake

@@ -40,6 +40,10 @@ if(NOT ${MCRL2_ENABLE_DEBUG_SOUNDNESS_CHECKS})
   add_definitions(-DMCRL2_NO_SOUNDNESS_CHECKS)
 endif()
 
+if(MCRL2_ENABLE_SYLVAN)
+  add_definitions(-DMCRL2_ENABLE_SYLVAN)
+endif()
+
 # Enable C++17 for all targets.
 set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_STANDARD_REQUIRED true)

build/cmake/ConfigureGNU.cmake

@@ -129,6 +129,12 @@ if(APPLE)
   endif()
   set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-stack_size,${MCRL2_OSX_STACK_SIZE}")
   set(CMAKE_EXE_LINKER_FLAGS_DEBUG "")
+  if (NOT DEFINED CMAKE_APPLE_SILICON_PROCESSOR) 
+    set(CMAKE_APPLE_SILICON_PROCESSOR "x86_64" CACHE STRING "Select whether the generated code is x86_64 or arm64" FORCE) 
+  endif()
+  set_property(CACHE CMAKE_APPLE_SILICON_PROCESSOR PROPERTY STRINGS "x86_64" "arm64")
+  set(CMAKE_OSX_ARCHITECTURES ${CMAKE_APPLE_SILICON_PROCESSOR} CACHE INTERNAL "" FORCE)
+  #set(CMAKE_OSX_ARCHITECTURES "x86_64", CACHE STRING "Set compiler to generate x86_64 code" FORCE)
 else()
   set(CMAKE_EXE_LINKER_FLAGS "-Wl,--as-needed")
   set(CMAKE_EXE_LINKER_FLAGS_DEBUG "-Wl,--warn-unresolved-symbols,--warn-once")

build/cmake/MCRL2Version.cmake

@@ -24,7 +24,7 @@
 #     not be generated from a clean Git clone.
 #
 # Package maintainers may set the variable below to issue a new release.
-set(MCRL2_MAJOR_VERSION "202106.0")
+set(MCRL2_MAJOR_VERSION "202206.0")
 string(SUBSTRING ${MCRL2_MAJOR_VERSION} 0 4 MCRL2_COPYRIGHT_YEAR)
 
 option(MCRL2_PACKAGE_RELEASE "Include release version information. This discards Git commit information and only uses the MCRL2_MAJOR_VERSION CMake variable." FALSE)

build/docker/fedora-34/Dockerfile → build/docker/fedora-36/Dockerfile

@@ -1,4 +1,4 @@
-FROM fedora:34
+FROM fedora:36
 
 # 1. Install packages needed for compiling and testing the tools
 RUN dnf install -y \
@@ -30,7 +30,7 @@ RUN dnf install -y \
 RUN pip install --user dparser
 
 # 2. Clone the git repository in the home directory
-RUN cd ~/ && git clone -b release-202106 git://github.com/mcrl2org/mcrl2.git mcrl2
+RUN cd ~/ && git clone -b release-202206 https://github.com/mcrl2org/mcrl2.git mcrl2
 
 # 3. Configure out of source build
 RUN mkdir ~/mcrl2-build && cd ~/mcrl2-build && cmake \
@@ -58,5 +58,5 @@ RUN cd ~/mcrl2-build \
     && make -j8 \
     && ctest . -j8
 
-# 7. Build the documentation
-RUN cd ~/mcrl2-build && make doc
+# 7. Build the documentation (this does not work with sphinx v4.4.0)
+#RUN cd ~/mcrl2-build && make doc

build/docker/make_release/Dockerfile

@@ -1,9 +1,9 @@
-FROM ubuntu:focal
+FROM ubuntu:jammy
 LABEL version="1.0"
 LABEL description="prepares the ppa release using the make_release scripts"
 
-ARG MCRL2_RELEASE_BRANCH="release-202106"
-ARG MCRL2_VERSION="202106.0"
+ARG MCRL2_RELEASE_BRANCH="release-202206"
+ARG MCRL2_VERSION="202206.0"
 
 # 1. Install packages needed for compilation.
 ARG DEBIAN_FRONTEND=noninteractive
@@ -13,16 +13,14 @@ RUN apt-get update && apt-get install -y \
  git \
  libboost-dev \
  libgl1-mesa-dev \
- qt5-default \
-# Needed to create the debian package.
+ qtbase5-dev \
  ubuntu-dev-tools \
  debhelper \
-# Needed for testing
- python-psutil \
- python-yaml
+ python3-psutil \
+ python3-yaml
 
 # 2. Clone the latest version of the repository in case that the make_release script must be updated.
-RUN mkdir ~/ppa && cd ~/ppa && git clone git://github.com/mcrl2org/mcrl2.git mcrl2
+RUN mkdir ~/ppa && cd ~/ppa && git clone https://github.com/mcrl2org/mcrl2.git mcrl2
 
 # 3. Build the mCRL2 release.
 RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_release && MCRL2_VERSION=$MCRL2_VERSION build_mcrl2_release"]
@@ -35,5 +33,5 @@ RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_
 # 5. Test the debian packages.
 #RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_release && MCRL2_VERSION=$MCRL2_VERSION test_ppa_package bionic "]
 #RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_release && MCRL2_VERSION=$MCRL2_VERSION test_ppa_package focal "]
-#RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_release && MCRL2_VERSION=$MCRL2_VERSION test_ppa_package groovy "]
+#RUN ["/bin/bash", "-c", "cd ~/packaging && source mcrl2/build/make_release/make_release && MCRL2_VERSION=$MCRL2_VERSION test_ppa_package jammy "]
 

build/docker/ubuntu-focal/Dockerfile → build/docker/ubuntu-jammy/Dockerfile

@@ -1,59 +1,59 @@
-FROM ubuntu:focal
-
-# 1. Install packages needed for compiling and testing the tools
-ARG DEBIAN_FRONTEND=noninteractive
-RUN apt-get update && apt-get install -y \
- build-essential \
- cmake \
- git \
- libboost-dev \
- libgl1-mesa-dev \
- qt5-default \
-# Packages needed for packaging
-# Packages needed for testing
- python3-psutil \
- python3-yaml \
-# Packages needed for generating the documentation
- doxygen \
- python3-pip \
- sphinx-common \
- swig \
- texlive \
- texlive-latex-extra \
- texlive-science \
- xsltproc
-
-# This package is not available in the ubuntu repository
-RUN pip install --user dparser
-
-# 2. Clone the git repository in the home directory
-RUN cd ~/ && git clone -b release-202106 git://github.com/mcrl2org/mcrl2.git mcrl2
-
-# 3. Configure out of source build
-RUN mkdir ~/mcrl2-build && cd ~/mcrl2-build && cmake . \
- -DCMAKE_BUILD_TYPE=RELEASE \
- -DBUILD_SHARED_LIBS=ON \
- -DMCRL2_ENABLE_DOCUMENTATION=ON \
- -DMCRL2_ENABLE_DEVELOPER=OFF \
- -DMCRL2_ENABLE_DEPRECATED=OFF \
- -DMCRL2_ENABLE_EXPERIMENTAL=OFF \
- -DMCRL2_ENABLE_GUI_TOOLS=ON \
- -DMCRL2_PACKAGE_RELEASE=ON \
- -DCMAKE_INSTALL_PREFIX=`pwd`/install \
- ~/mcrl2
-
-# 4. Build the toolset
-RUN cd ~/mcrl2-build && make -j8 
-
-# 5. Package the build
-RUN cd ~/mcrl2-build && cpack -G DEB
-
-# 6. Test the toolset; tests require the experimental tools.
-RUN cd ~/mcrl2-build \
-    && cmake -DMCRL2_ENABLE_EXPERIMENTAL=ON \
-             -DMCRL2_ENABLE_TESTS=ON . \
-    && make -j8 \
-    && ctest . -j8
-
-# 7. Build the documentation
+FROM ubuntu:jammy
+
+# 1. Install packages needed for compiling and testing the tools
+ARG DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install -y \
+ build-essential \
+ cmake \
+ git \
+ libboost-dev \
+ libgl1-mesa-dev \
+ qtbase5-dev \
+# Packages needed for packaging
+# Packages needed for testing
+ python3-psutil \
+ python3-yaml \
+# Packages needed for generating the documentation
+ doxygen \
+ python3-pip \
+ sphinx-common \
+ swig \
+ texlive \
+ texlive-latex-extra \
+ texlive-science \
+ xsltproc
+
+# This package is not available in the ubuntu repository
+RUN pip install --user dparser
+
+# 2. Clone the git repository in the home directory
+RUN cd ~/ && git clone -b release-202206 https://github.com/mcrl2org/mcrl2.git mcrl2
+
+# 3. Configure out of source build
+RUN mkdir ~/mcrl2-build && cd ~/mcrl2-build && cmake . \
+ -DCMAKE_BUILD_TYPE=RELEASE \
+ -DBUILD_SHARED_LIBS=ON \
+ -DMCRL2_ENABLE_DOCUMENTATION=ON \
+ -DMCRL2_ENABLE_DEVELOPER=OFF \
+ -DMCRL2_ENABLE_DEPRECATED=OFF \
+ -DMCRL2_ENABLE_EXPERIMENTAL=OFF \
+ -DMCRL2_ENABLE_GUI_TOOLS=ON \
+ -DMCRL2_PACKAGE_RELEASE=ON \
+ -DCMAKE_INSTALL_PREFIX=`pwd`/install \
+ ~/mcrl2
+
+# 4. Build the toolset
+RUN cd ~/mcrl2-build && make -j8 
+
+# 5. Package the build
+RUN cd ~/mcrl2-build && cpack -G DEB
+
+# 6. Test the toolset; tests require the experimental tools.
+RUN cd ~/mcrl2-build \
+    && cmake -DMCRL2_ENABLE_EXPERIMENTAL=ON \
+             -DMCRL2_ENABLE_TESTS=ON . \
+    && make -j8 \
+    && ctest . -j8
+
+# 7. Build the documentation
 RUN cd ~/mcrl2-build && make doc 

build/make_release/debian/compat

@@ -1 +1 @@
-5
+7

build/make_release/debian/control

@@ -7,8 +7,8 @@ Build-Depends: debhelper (>= 5),
  cmake,
  libboost-dev,
  libgl1-mesa-dev,
- python-psutil,
- python-yaml,
+ python3-psutil,
+ python3-yaml,
  qtbase5-dev,
  libqt5opengl5-dev,
  git

build/make_release/make_release

@@ -30,8 +30,8 @@
 # do_ppa_upload. If these steps fail, it makes no sense to do an upload. After
 # every failed upload attempt the version number needs to be updated.
 
-MCRL2_RELEASE_BRANCH="release-202106"
-MCRL2_VERSION="202106.0"
+MCRL2_RELEASE_BRANCH="release-202206"
+MCRL2_VERSION="202206.0"
 UBUNTU_VERSION="1ubuntu1ppa1"
 DEBEMAIL="[email protected]"
 DEBFULLNAME="Maurice Laveaux"

doc/sphinx/user_manual/download.rst

@@ -36,11 +36,6 @@ latest release of the toolset.
 Stable releases for Arch Linux are available via the `Arch User Repository <https://aur.archlinux.org/packages/mcrl2/>`_.
 This package is currently maintained by Jorai Rijsdijk.
 
-.. note::
-
-   The Windows release has received a minor fix on the 12th of July, 2021,
-   which resolves not being able to open mcrl2ide from mcrl2-gui.
-
 Download a nightly build of mCRL2
 =================================
 

doc/sphinx/user_manual/historic_releases.rst

@@ -7,6 +7,43 @@ Previous releases of mCRL2
 
 This page shows a list of historic releases of mCRL2.
 
+Release 202106.0
+----------------
+
+.. |bin_w64_202106.0| replace:: Windows Installer (64-bit)
+.. _bin_w64_202106.0: http://www.mcrl2.org/download/release/mcrl2-202106.0_x86_64.exe
+
+.. |zip_w64_202106.0| replace:: Windows ZIP (64-bit)
+.. _zip_w64_202106.0: http://www.mcrl2.org/download/release/mcrl2-202106.0_x86_64.zip
+
+.. |bin_osx_202106.0| replace:: macOS DMG (64-bit)
+.. _bin_osx_202106.0: http://www.mcrl2.org/download/release/mcrl2-202106.0_x86_64.dmg
+
+.. |bin_ppa_202106.0| replace:: PPA release
+.. _bin_ppa_202106.0: https://launchpad.net/~mcrl2/+archive/release-ppa
+
+.. |bin_fedora64_202106.0| replace:: Fedora RPM (64-bit)
+.. _bin_fedora64_202106.0: http://www.mcrl2.org/download/release/mcrl2-202106.0_x86_64.rpm
+
+.. |src_tgz_202106.0| replace:: GZipped Tarball
+.. _src_tgz_202106.0: http://www.mcrl2.org/download/release/mcrl2-202106.0.tar.gz
+
+   +------------------------+--------------------------+
+   |Operating system        | Release (202106.0)       |
+   +========================+==========================+
+   |Windows                 | |bin_w64_202106.0|_      |
+   |                        +--------------------------+
+   |                        | |zip_w64_202106.0|_      |
+   +------------------------+--------------------------+
+   |macOS                   | |bin_osx_202106.0|_      |
+   +------------------------+--------------------------+
+   |Ubuntu                  | |bin_ppa_202106.0|_      |
+   +------------------------+--------------------------+
+   |Fedora                  | |bin_fedora64_202106.0|_ |
+   +------------------------+--------------------------+
+   |Source                  | |src_tgz_202106.0|_      |
+   +------------------------+--------------------------+
+
 Release 202006.0
 ----------------