Preparations for 3.0.beta1 release.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@44 bbc10eb1-c90d-0410-af57-cb519fbb1720

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:

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.:
     

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
-

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.

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

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 <file> ............ Import the transition matrix directly from a text file");
 		mainLog.println("-importstates <file>............ Import the list of states directly from a text file");
+		mainLog.println("-importinit <expr>.............. 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 <file> .......... Export the results of model checking to a file");
 		mainLog.println("-exporttrans <file> ............ Export the transition matrix to a file");
 		mainLog.println("-exportstaterewards <file> ..... Export the state rewards vector to a file");
-		mainLog.println("-exporttransreward <file> ...... Export the transition rewards matrix to a file");
+		mainLog.println("-exporttransrewards <file> ...... Export the transition rewards matrix to a file");
 		mainLog.println("-exportstates <file> ........... Export the list of reachable states to a file");
 		mainLog.println("-exportlabels <file> ........... Export the list of labels and satisfying states to a file");
 		mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format");