diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index dff9949f..42120ef9 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -3,7 +3,7 @@ including development and beta versions. For a less detailed overview of the main changes in each public release, see the file VERSIONS.txt. ----------------------------------------------------------------------------- -Version 2.1.dev11.sim9 +Version 3.0.beta1 (29/3/2006) ----------------------------------------------------------------------------- * Changes to export functionality @@ -16,9 +16,22 @@ Version 2.1.dev11.sim9 - exported matrices now ordered by default (by row) - new/rearranged command-line switches * Added new options to Model|View menu in GUI +* Additional checks when parsing models: + - synchronous commands modifying globals + (now disallowed, previously just advised against) + - modification of local variables by another module + (previously detected later at build-time) +* Improvements/changes to explicit import functionality: + - -importstates understands Boolean variables now + - -importinit option added + - Default module variable (x) indexed from 0, not 1 +* Non-convergence of iterative methods is an error, not a warning +* Changed layout of simulator transition table (4 -> 3 columns) +* Bugfixes +* Makefile improvements ----------------------------------------------------------------------------- -Version 2.1.dev11.sim8 (3/3/06) +Version 2.1.dev11.sim8 (3/3/2006) ----------------------------------------------------------------------------- * Bug fix: computation of powers in simulator @@ -26,20 +39,20 @@ Version 2.1.dev11.sim8 (3/3/06) * Bug fixes: loop detection and deadlocks in simulator ----------------------------------------------------------------------------- -Version 2.1.dev11.sim7 (5/1/06) +Version 2.1.dev11.sim7 (5/1/2006) ----------------------------------------------------------------------------- * Bug fixes, tidying ----------------------------------------------------------------------------- -Version 2.1.dev11.sim6 (16/12/05) +Version 2.1.dev11.sim6 (16/12/2005) ----------------------------------------------------------------------------- * Merged with simulator branch * Improved options management including saving of user settings ----------------------------------------------------------------------------- -Version 2.1.dev11 (5/12/05) +Version 2.1.dev11 (5/12/2005) ----------------------------------------------------------------------------- Changes: @@ -48,7 +61,7 @@ Changes: * Bugfix: out-of-range initial values banned ----------------------------------------------------------------------------- -Version 2.1.dev10 (21/10/05) +Version 2.1.dev10 (21/10/2005) ----------------------------------------------------------------------------- Changes: @@ -60,7 +73,7 @@ Changes: * Ability to disable checks of probabilities/rates ----------------------------------------------------------------------------- -Version 2.1.dev9 (27/05/05) +Version 2.1.dev9 (27/05/2005) ----------------------------------------------------------------------------- Changes: diff --git a/prism/README.txt b/prism/README.txt index 6bb5758a..fd253d27 100644 --- a/prism/README.txt +++ b/prism/README.txt @@ -2,7 +2,7 @@ README ====== -This is PRISM (Probabilistic Symbolic Model Checker), version 2.1. +This is PRISM (Probabilistic Symbolic Model Checker), version 3.0.beta1 This document contains information about installing and running PRISM. @@ -87,7 +87,7 @@ Java installed, but your path may not be set up correctly. 1. Enter the PRISM directory, e.g.: - cd prism-2.1-src + cd prism-3.0.beta1-src 2. Hopefully, you can build PRISM simply by typing: @@ -151,11 +151,11 @@ For Linux/Solaris/OS X: 1. Unpack the PRISM distribution into a suitable location, e.g.: - tar xfz prism-2.1-linux.tar.gz + tar xfz prism-3.0.beta1-linux.tar.gz 2. Enter the prism directory and run the installation script - cd prism-2.1-linux + cd prism-3.0.beta1-linux ./install.sh Please note that if your move or rename the PRISM directory after @@ -208,7 +208,7 @@ For Windows: 1. Run the command prompt and go into the PRISM bin directory, e.g.: - cd "c:\Program Files\prism-2.1-win\bin" + cd "c:\Program Files\prism-3.0.beta1-win\bin" 2. Execute the prism.bat batch file, passing a PRISM example file as an argument, e.g.: diff --git a/prism/VERSIONS.txt b/prism/VERSIONS.txt index 13914f4f..0c016fc2 100644 --- a/prism/VERSIONS.txt +++ b/prism/VERSIONS.txt @@ -1,8 +1,46 @@ +This file summarises the principal changes between each main public release of PRISM. +For more detailed information about the various changes, see the file CHANGELOG.txt. + ----------------------------------------------------------------------------- -Version 2.1 (released 8/9/2004) +Version 3.0 (beta 1 released 29/3/2006) ----------------------------------------------------------------------------- -Changes: +* Discrete-event simulation engine added, providing: + - generation of approximate quantitative results via sampling + - debugging tool: manual model exploration and automatic trace generation + +* Support for costs and rewards: + - state-based and transition-based (impulse) costs/reward specification added to PRISM language + - verification (and simulation) of properties based on expected value of costs/rewards + (e.g. cumulated reward to reach state/time-bound, transient or steady-state reward value) + +* Overhaul of import/export functionality, including: + - export of transition matrix graph (Dot file) + - export of state/transition rewards + - export of property file labels and their satisfying states + - improved support for other export formats: Matlab, MRMC + - possibility to export to stdout/log instead of a file + - import of explicit model descriptions (from transition matrix and, optionally, state list) + +* GUI improvements, e.g.: + - additional graph plotting functionality + - XML-based import/export of graphs + - export of graphs to Matlab + +* Improved options management including saving of user settings +* Support for Mac OS X +* Easier compilation process +* Direct computation of transient probabilities +* Support for multiple initial states +* Improvements/additions to PRISM modelling/property languages +* Additional error checking on PRISM models +* Underlying data structure and efficiency improvements +* Bug fixes + + +----------------------------------------------------------------------------- +Version 2.1 (released 8/9/2004) +----------------------------------------------------------------------------- * Now possible to build/run PRISM on Windows * Compilation/installation procedures slightly simplified @@ -13,8 +51,6 @@ Changes: Version 2.0 (released 17/3/2004) ----------------------------------------------------------------------------- -Changes: - * Completely new graphical user interface, including: - Text editor for PRISM language - Automated results collection/graph plotting @@ -56,8 +92,6 @@ Changes: Version 1.3.1 (released 20/2/2003) ----------------------------------------------------------------------------- -Changes: - * Bug fixes in model construction code @@ -65,8 +99,6 @@ Changes: Version 1.3 (released 10/2/2003) ----------------------------------------------------------------------------- -Changes: - * Steady-state probability computation improved to include strongly connected component (SCC) computation * Extended support for CSL time-bounded until operator to include arbitrary intervals * More flexible parallel composition options in the PRISM language (for DTMCs and CTMCs) @@ -89,4 +121,3 @@ Version 1.2 (released 17/9/2001) ----------------------------------------------------------------------------- First public release - diff --git a/prism/etc/prism.pats b/prism/etc/prism.pats index 093f3745..1e357cce 100644 --- a/prism/etc/prism.pats +++ b/prism/etc/prism.pats @@ -1,9 +1,9 @@ -! This file is used to provide syntax highlighting for PRISM 2.1 +! This file is used to provide syntax highlighting for PRISM ! in the NEdit editor (www.nedit.org). ! ! To use it, close any NEdit programs and restart with: ! -! nedit -import prism-2.1.dev.pats +! nedit -import prism.pats ! ! Now, select "Save Defaults" from the "Preferences" menu ! to save these changes to your personal settings. diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b462fa41..ec1871b9 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -42,7 +42,7 @@ import simulator.*; public class Prism { // prism version - private static final String version = "2.1.dev11.sim9"; + private static final String version = "3.0.beta1"; //------------------------------------------------------------------------------ // Constants diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 5dfcc143..d5977b5f 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1439,6 +1439,7 @@ public class PrismCL mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language"); mainLog.println("-importtrans ............ Import the transition matrix directly from a text file"); mainLog.println("-importstates ............ Import the list of states directly from a text file"); + mainLog.println("-importinit .............. Specify the initial state for explicitly imported models"); mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC"); mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC"); mainLog.println("-mdp ........................... Force imported/built model to be an MDP"); @@ -1446,7 +1447,7 @@ public class PrismCL mainLog.println("-exportresults .......... Export the results of model checking to a file"); mainLog.println("-exporttrans ............ Export the transition matrix to a file"); mainLog.println("-exportstaterewards ..... Export the state rewards vector to a file"); - mainLog.println("-exporttransreward ...... Export the transition rewards matrix to a file"); + mainLog.println("-exporttransrewards ...... Export the transition rewards matrix to a file"); mainLog.println("-exportstates ........... Export the list of reachable states to a file"); mainLog.println("-exportlabels ........... Export the list of labels and satisfying states to a file"); mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format");