Try merging robots2 again, previous merge was squash

.github/workflows/make-tests.yml

@@ -11,19 +11,57 @@ jobs:
 
     strategy:
       matrix:
-        java: [9, 11, 15]
-    runs-on: ubuntu-latest
+        java: [11, 21]
+        os: [ubuntu-latest, macos-latest]
+    runs-on: ${{ matrix.os }}
 
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v4
     - name: Set up JDK
-      uses: actions/setup-java@v1
+      uses: actions/setup-java@v4
       with:
         java-version: ${{ matrix.java }}
-    - run: cd prism
+        distribution: temurin
     - name: make tests
       working-directory: ./prism
       run: |
         make
         make unittests
         make tests
+
+  build-win:
+
+    strategy:
+      matrix:
+        java: [11, 21]
+    runs-on: windows-latest
+
+    steps:
+    - run: git config --global core.autocrlf input
+    - uses: actions/checkout@v4
+    - name: Set up JDK
+      uses: actions/setup-java@v4
+      with:
+        java-version: ${{ matrix.java }}
+        distribution: temurin
+    - name: Install Cygwin Dependencies
+      uses: cygwin/cygwin-install-action@v4
+      with:
+        packages: |
+          make,
+          mingw64-x86_64-gcc-g++,
+          binutils,
+          dos2unix,
+          git,
+          wget,
+          unzip,
+          python
+    - name: make tests
+      shell: bash
+      env:
+        CYGWIN: winsymlinks:native
+      working-directory: ./prism
+      run: >-
+        make &&
+        make unittests &&
+        make tests

CHANGELOG.txt

@@ -1,5 +1,64 @@
 This file contains details of the changes in each new version of PRISM.
 
+-----------------------------------------------------------------------------
+Version 4.8.1 (first released 13/1/2024)
+-----------------------------------------------------------------------------
+
+* Migrate to CUDD version 3
+* Transition reward export (MDP-like models) for explicit engine
+* Fix broken transient probability computation
+* Updates/fixes in install/launch/testing scripts and build process
+* New tests in etc/tests available for easier build tests
+* New -javaversion switch to show Java version used
+* New --print-failures switch for prism-auto
+* Various bugfixes
+
+-----------------------------------------------------------------------------
+Version 4.8 (first released 5/7/2023)
+-----------------------------------------------------------------------------
+
+* Support for interval DTMC (IDTMC) and interval MDP (IMDP) model checking
+
+* Improved strategy (policy) generation
+  - switch -exportstrat exports to tra/dot/txt format
+  - additional export options (restrict/reduce, states, reach)
+  - strategy generation extended for bounded reachability, LTL, POMDPs
+  - GUI support for generating, exporting and simulating strategies
+
+* Other features/enhancements:
+  - PTA model checking supports global/non-local variables
+  - ModelGenerator interface now supports real-time models (e.g., PTAs)
+  - new -javaparams switch to pass command-line arguments to JVM
+  - prism-log-extract: new field 'dd_nodes' for model MTBDD size
+
+* Import/export enhancements:
+  - import of multiple (and named) reward structures
+  - reward exports include header with name/type
+  - new setting for model export precision (-exportmodelprecision)
+  - new "proplabels" option for -exportmodel and -exportlabels
+  - new -exportproplabels switch to export (just) properties file labels
+  - explicit model import without -importmodel: prism model.all
+  - results export to new formats: PRISM comment, dataframe
+  - results import from dataframe format (-importresults or GUI)
+  - observation export for POMDPs (-exportobs or GUI)
+
+* Fixes / upgrades
+  - compile fix for newer MacOS
+  - library updates: JAS (2.7.90), Log4j (2.16.0), jhoafparser (1.1.1)
+  - various bugfixes
+
+* Development and code-level changes
+  - automated testing via GitHub Actions
+  - unit testing via JUnit
+  - JavaCC upgraded from version 6.0 to 7.0
+  - major refactoring:
+    > generic model/reward classes
+    > ASTElement deepCopy()
+    > Expression evaluation
+    > explicit.StateValues
+    > Strategy and related classes
+    > Modules2MTBDD
+
 -----------------------------------------------------------------------------
 Version 4.7 (first released 19/3/2021)
 -----------------------------------------------------------------------------

README.md

@@ -7,7 +7,7 @@ This is PRISM (Probabilistic Symbolic Model Checker).
 
 For detailed installation instructions, check the online manual at:
 
-  http://www.prismmodelchecker.org/manual/InstallingPRISM/Instructions
+  https://www.prismmodelchecker.org/manual/InstallingPRISM/Instructions
 
 or see the local copy included in this distribution:
 
@@ -17,7 +17,7 @@ Very abbreviated instructions for installing/running PRISM are as follows:
 
 For Windows binary distributions:
 
- * to install, run `prism-XXX-win-installer.exe`
+ * to install, run `prism-XXX-win64-installer.exe`
  * to run, use Desktop/Start menu shortcuts or double-click `bin\xprism.bat`
 
 For other binary distributions:
@@ -28,7 +28,7 @@ For other binary distributions:
 For source code distributions:
 
  * enter the PRISM directory and type `cd prism` then `make`
- * to check the install, type `make test`
+ * to check the install, type `make test` or `etc/tests/run.sh`
  * to run, execute `bin/xprism` or `bin/prism`
 
 If you have problems check the manual, especially the section "Common Problems And Questions".
@@ -38,57 +38,62 @@ If you have problems check the manual, especially the section "Common Problems A
 
 The best source of information about using PRISM is the online manual:
 
-  http://www.prismmodelchecker.org/manual/
+  https://www.prismmodelchecker.org/manual/
 
 You can also view the local copy included in this distribution:
 
   * `manual/index.html`
 
 For other PRISM-related information, see the website:
 
-  http://www.prismmodelchecker.org/
+  https://www.prismmodelchecker.org/doc
 
+Information for developers is kept here:
+
+  https://github.com/prismmodelchecker/prism/wiki
 
 ## Licensing
 
 PRISM is distributed under the GNU General Public License (GPL), version 2.
 A copy of this license can be found in the file `COPYING.txt`.
 For more information, see:
 
-  http://www.gnu.org/licenses/
-
-PRISM uses the CUDD (Colorado University Decision Diagram) library of Fabio Somenzi,
-which is freely available. For more information about this library, see:
-
-  http://vlsi.colorado.edu/~fabio/CUDD/
+  https://www.gnu.org/licenses/
 
 PRISM also uses various other libraries (mainly to be found in the lib directory).
-For details of those, and for links to source where we distribute only binaries, see:
+For details of those, including licenses and links to downloads and source code, see:
 
-http://www.prismmodelchecker.org/other-downloads.php
+https://www.prismmodelchecker.org/other-downloads.php
 
 
 ## Acknowledgements
 
 PRISM was created and is still actively maintained by:
 
- * Dave Parker (University of Birmingham)
+ * Dave Parker (University of Oxford)
  * Gethin Norman (University of Glasgow)
  * Marta Kwiatkowska (University of Oxford) 
 
-Development of the tool is currently led from Birmingham by Dave Parker. Other current key developers are:
+Development of the tool is currently led from Oxford by Dave Parker.
+
+The following have made a wide range of contributions to
+PRISM covering many different aspects of the tool
+(in approximately reverse chronological order):
 
+ * Steffen Märcker (Technische Universität Dresden)
  * Joachim Klein (formerly Technische Universität Dresden)
+ * Vojtech Forejt (formerly University of Oxford)
 
-We gratefully acknowledge contributions to the PRISM code-base from various sources,
-including (in approximately reverse chronological order):
+We also gratefully acknowledge contributions to the PRISM code-base from
+(in approximately reverse chronological order):
 
+ * Max Kurze: Language parser code improvements
+ * Ludwig Pauly: Reward import/export
+ * Alberto Puggelli: First version of interval DTMC/MDP code
  * Xueyi Zou: Partially observable Markov decision processes (POMDPs)
- * Steffen Märcker: Fixes and improvements, especially in explicit engine
  * Chris Novakovic: Build infrastructure and explicit engine improvements
  * Ernst Moritz Hahn: Parametric model checking, fast adaptive uniformisation + various other features
  * Frits Dannenberg: Fast adaptive uniformisation
- * Vojtech Forejt: Various model checking code, including multi-objective + GUI enhancements
  * Hongyang Qu: Multi-objective model checking
  * Mateusz Ujma: Bug fixes and GUI improvements
  * Christian von Essen: Symbolic/explicit-state model checking
@@ -107,22 +112,21 @@ including (in approximately reverse chronological order):
 
 For more details see:
 
-  http://www.prismmodelchecker.org/people.php
+  https://www.prismmodelchecker.org/people.php
 
 
 ## Contact
 
 If you have problems or questions regarding PRISM, please use the help forum provided. See:
 
-  http://www.prismmodelchecker.org/support.php
+  https://www.prismmodelchecker.org/support.php
 
 Other comments and feedback about any aspect of PRISM are also very welcome. Please contact:
 
   Dave Parker  
-  ([email protected])  
-  School of Computer Science  
-  University of Birmingham  
-  Edgbaston  
-  Birmingham  
-  B15 2TT  
-  ENGLAND
+  ([email protected])  
+  Department of Computer Science  
+  University of Oxford  
+  Oxford  
+  OX1 3QG
+  UK

cudd/.gitignore

@@ -0,0 +1,30 @@
+# general patterns to ignore
+# Emacs backup files
+*~
+# OS X system files
+.DS_Store
+
+# build artefacts by pattern:
+*.o
+*.a
+*.class
+*.dylib
+*.jnilib
+*.so
+*.dll
+*.lo
+*.la
+*.dirstamp
+.deps
+.libs
+
+# build artefacts:
+config.h
+config.log
+config.status
+Makefile
+libtool
+stamp-h1
+doc/cudd.tex
+dddmp/exp/*.sh
+include