CHANGELOG.txt 32.2 KB
Newer Older
1
This file contains details of the changes in each new version of PRISM.
Dave Parker's avatar
Dave Parker committed
2

3
-----------------------------------------------------------------------------
4
Changes since version 4.4 (up-to-date wrt c0533b0b)
5
6
-----------------------------------------------------------------------------

7
8
9
10
11
12
13
* New features
  - add round function to language (rounds to nearest integer)
  - Java stack size can be set via command-line switch -javastack (or PRISM_JAVASTACKSIZE)
  - fractional values allowed for constants in -const switch and in GUI
  - allow rewards to be included in simulation paths exported from GUI (like for -simpath)

* Enhancements and fixes:
Dave Parker's avatar
Dave Parker committed
14
15
  - PRISM GUI settings file (.prism) moved to more standard locations
  - ITE supported in exact/parametric mode
16
17
18
  - various improvements to model checking in "exact" mode
  - faster explicit construction of models with no labels
  - command-line -exportsteadystates switch implies -steadystate
Dave Parker's avatar
Dave Parker committed
19
  - GUI shortcuts: double-clicks for addition of constants, labels
20
21
22
  - fixed Mac launch scripts for Java 10 (removed -d64 and -d32)
  - improved auto switching between model checking engines in some cases
  - many minor bugfixes
23

Dave Parker's avatar
Dave Parker committed
24
* Development changes and enhancements:
25
26
27
28
29
30
31
32
33
34
35
  - alignment of source code releases and GitHub repos (some files moved to top-level)
  - move/simplify release building Makefile scripts (see GitHub wiki)
  - utility scripts for installing PRISM on fresh OSs (in etc/scripts)
  - HTML copy of manual now included in repo
  - make clean_all cleans external libs too, e.g. lpsolve
  - switch from javah (deprecated since Java 8) to javac for JNI header generation
  - launch scripts now use exec to start Java by default (PRISM_NO_EXEC=yes to revert)

* Benchmarking/testing changes and enhancements:
  - integration of prism-tests into main repo
  - fractions/exact numbers allowed in testing RESULT specs
Dave Parker's avatar
Dave Parker committed
36
37
38
  - Travis build config for continuous integration testing
  - prism-auto guesses ngprism location
  - prism-auto options: --skip-export-runs, --skip-duplicate-runs, --timeout
39
40
  - Makefile targets/settings: test, testsecho, testsfull, TESTS_ARGS, source-jar
  - NG_MAINCLASS setting for running PRISM in Nailgun server mode (prism -ng)
41
42


Dave Parker's avatar
Dave Parker committed
43
44
45
-----------------------------------------------------------------------------
Version 4.4 (first released 23/7/2017)
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
46

Dave Parker's avatar
Dave Parker committed
47
48
* New model checking functionality:
  - expected reward to satisfy a co-safe LTL formula (MDPs, D/CTMCs, all engines)
Dave Parker's avatar
Dave Parker committed
49
50
  - interval iteration (MDPs, D/CTMCs, all engines)
  - topological value iteration (MDPs, D/CTMCs, explicit engine)
Dave Parker's avatar
Dave Parker committed
51
  - expected total reward (R[C] operator) for CTMCs and MDPs (max), all engines
Dave Parker's avatar
Dave Parker committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
  - CTL model checking in the explicit engine
  - non-probabilistic LTL model checking in the explicit engine
  - instantaneous reward computation (Rmax/min[I=x]) in the explicit engine
  - DTMC transient probability computation for the explicit engine

* Imports and exports:
  - model import from explicit files for the explicit engine (-import... switches)
  - full import of labels during explicit model import (all engines)
  - import of state rewards during explicit model import (symbolic engines)
  - export of state rewards from explicit engine
  - export of models to .dot format via the -exportmodel switch

* Miscellaneous:
  - built-in support for Nailgun client/server
  - new timeout feature (-timeout switch)
  - performance improvements in explicit engine
  - GUI also supports -javamaxmem switch to set Java memory
  - better error handling when CUDD runs out of memory
  - various bug fixes and performance improvements

* Features for developers:
  - new ModelGenerator interface for specifying models programmatically
  - extensions to test mode: complex expressions for RESULT specifications
Dave Parker's avatar
Dave Parker committed
75
  - prism-auto: new options/features (e.g., --show-warnings, --nailgun, --ngprism, --verbose-test)
Dave Parker's avatar
Dave Parker committed
76
  - DD debugging options: -dddebug and -ddtrace switches, improved ref count debugging
Dave Parker's avatar
Dave Parker committed
77
  - new option -exportiterations for visualising iterative numerical methods
Dave Parker's avatar
Dave Parker committed
78
  - code base now allows/assumes Java 8
Dave Parker's avatar
Dave Parker committed
79

80
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
81
Version 4.3.1 (first released 26/5/2016)
82
83
-----------------------------------------------------------------------------

Dave Parker's avatar
Dave Parker committed
84
85
86
* Bug fixes:
- launch scripts on OS X (especially El Capitan)
- lpsolve compile fix for recent Linux distributions
87

Dave Parker's avatar
Dave Parker committed
88
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
89
Version 4.3 (first released 14/7/2015)
Dave Parker's avatar
Dave Parker committed
90
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
91

Dave Parker's avatar
Dave Parker committed
92
* Support for external LTL-to-automata converters via the HOA format
Dave Parker's avatar
Dave Parker committed
93
  - including model checking for Generalised Rabin (GR) conditions
Dave Parker's avatar
Dave Parker committed
94
95
96

* New model checking functionality/optimisations
  - lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ])
97
  - expected total rewards (R[C]) implemented for DTMCs
Dave Parker's avatar
Dave Parker committed
98
  - backwards reachability algorithm implemented for model checking PTAs
99
  - exact (arbitrary precision) model checking via the parametric engine (experimental)
Dave Parker's avatar
Dave Parker committed
100
  - various LTL model checking optimisations
Dave Parker's avatar
Dave Parker committed
101
  - faster precomputation by pre-computing predecessors (explicit engine)
Dave Parker's avatar
Dave Parker committed
102
103
104

* Options/switches:
  - new -pathviaautomata switch to force model checking via automaton construction
Dave Parker's avatar
Dave Parker committed
105
  - new "comment" option for exporting results (exports in regression test format)
Dave Parker's avatar
Dave Parker committed
106
107
108
109
  - new -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM)
  - more convenient format for CUDD max memory setting (125k, 50m, 4g, etc.)
  - higher default values for CUDD/Java memory limits
  
Dave Parker's avatar
Dave Parker committed
110
* Additional functionality in prism-auto testing/benchmarking script
Dave Parker's avatar
Dave Parker committed
111
  - export testing, .auto files, debug mode, colouring, custom model files, ...
Dave Parker's avatar
Dave Parker committed
112
  
Dave Parker's avatar
Dave Parker committed
113
* New sbml2prism script
Dave Parker's avatar
Dave Parker committed
114

Dave Parker's avatar
Dave Parker committed
115
116
* Bug fixes

Dave Parker's avatar
Dave Parker committed
117
118
119
120
121
122
-----------------------------------------------------------------------------
Version 4.2.1 (first released 4/12/2014)
-----------------------------------------------------------------------------

* Bug fixes

Dave Parker's avatar
Dave Parker committed
123
124
125
-----------------------------------------------------------------------------
Version 4.2 (beta first released 12/5/2014)
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
126

127
* Parametric model checking
Dave Parker's avatar
Dave Parker committed
128
129
130
131
132
133

* New model checking and export functionality
  - fast adaptive uniformisation for CTMC transient analysis
  - added R[C<=k] operator for MDPs (sparse, explicit)
  - new -exportmecs and -exportsccs switches
  - additional functionality in explicit engine (export BSCCs, LTL)
Dave Parker's avatar
Dave Parker committed
134
  - improved adversary strategy generation in explicit engine
Dave Parker's avatar
Dave Parker committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
  - integer variables can be unbounded (e.g. "x:int;"), for simulation-based analysis

* New options/switches:
  - new -exportmodel and -importmodel convenience switches
  - new -sumroundoff switch (used when checking probabilities sum to 1)
  - some new '-help xxx' switches (const,simpath,exportresults,aroptions,exportmodel,importmodel)
  - allow command-line switches of form --sw (as well as -sw)
  - slight change to notation for -exportresults to match -exportmodel

* Additional functionality available in GUI:
  - export steady-state/transient probabilities from GUI
  - export/view labels from model/properties from GUI
  - small improvements to usability of the GUI simulator transition table
  - additional graph zoom functionality on popup menu

* Updates to build process
Dave Parker's avatar
Dave Parker committed
151
  - fixed building on new versions of Cygwin (32/64-bit Windows)
Dave Parker's avatar
Dave Parker committed
152
  - update CUDD to version 2.5.0
Dave Parker's avatar
Dave Parker committed
153

154
-----------------------------------------------------------------------------
155
Version 4.1 (first released 20/12/2012)
156
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
157

Dave Parker's avatar
Dave Parker committed
158
159
* Multi-objective model checking for MDPs

160
161
* New explicit-state (pure Java) model checking engine
  - coverage of much, but not all, of PRISM's model checking functionality
Dave Parker's avatar
Dave Parker committed
162
  - new methods for MDPs: policy iteration (-politer -modpoliter) and Gauss-Seidel (-gs)
Dave Parker's avatar
Dave Parker committed
163
  - accompanying significant changes to underlying PRISM (Java) API
164
165
166
167
168
169

* GUI improvements
  - easy plotting of graphs for simulation paths in the GUI
  - command-line GUI call (xprism)  takes both model and properties files as arguments
  - easier zoom-out (double click) for graphs in GUI

Dave Parker's avatar
Dave Parker committed
170
171
* CTL model checking (most operators)
  - and counterexample/witness generation for A[G ...] or E[F ...]
Dave Parker's avatar
Dave Parker committed
172
  
173
174
175
176
177
178
179
* Changes to deadlock handling:
  - new option for "fix deadlocks" (defaults to *true*) (and new switch -nofixdl) 
  - consistent deadlock handling everywhere, incl. GUI and experiments

* Model checking improvements
  - incremental computation of ranges of transient probabilities
    when called from command-line (e.g. -tr 0.1:0.01:0.2) 
Dave Parker's avatar
Dave Parker committed
180
181
182
  - new "printall" filter (shows zero results too, unlike "print")
  - -importinit option works for steady-state as well as transient probabilities
  - additional output in log of progress for numerical solution techniques
183

Dave Parker's avatar
Dave Parker committed
184
185
186
* Improvements to simulation path generation using -simpath switch
  - more efficient path generation (on-the-fly) where possible
  - new 'snapshot' option to only show states at certain time-points
Dave Parker's avatar
Dave Parker committed
187
  - added 'probs' option to display transition probabilities/rates
Dave Parker's avatar
Dave Parker committed
188
  - rewards are not displayed by default; use 'rewards' option to show
189
190
  
* Changes to usage of PRISM settings file
Dave Parker's avatar
Dave Parker committed
191
192
  - settings file ~/.prism only read by GUI (not command-line) by default
  - new switch -settings to read a settings file from command-line PRISM
193

Dave Parker's avatar
Dave Parker committed
194
* New file extensions for model/properties files: .prism, .props
Dave Parker's avatar
Dave Parker committed
195
* New scripts for testing and benchmarking: prism-auto/prism-test/prism-filler
196
* New -exportdigital switch for exporting PRISM code built by digital clocks PTA engine
Dave Parker's avatar
Dave Parker committed
197
* New syntax for (CTMC) transient probabilities in P operator: P=? [ F=T "target" ]
Dave Parker's avatar
Dave Parker committed
198

Dave Parker's avatar
Dave Parker committed
199
200
201
202
-----------------------------------------------------------------------------
Version 4.0.3 (released 30/1/2012)
-----------------------------------------------------------------------------

203
204
205
206
* Property names
  - properties can be named, by prefixing with "name":
  - properties can appear as sub-formulae of other properties using name references
  - command-line -prop switch allows selection of property to check by name
Dave Parker's avatar
Dave Parker committed
207
208
209
210
* New options for results export
  - export in matrix form, e.g. for surface plots
  - export in CSV (rather than tab-separated) form
  - expanded switch: -exportresults file[,opt1,opt2,...] with options: matrix,csv
Dave Parker's avatar
Dave Parker committed
211
* Automatic engine switching if numerical computation not supported
Dave Parker's avatar
Dave Parker committed
212
213
214
* Optimised Rabin automata for a few common LTL formulae
* Added -pf as a command-line switch alias for -pctl/-csl
* Add .props as a properties file extension (in GUI)
215
* New switches -noprob0/-noprob1 to disable individual precomputation algorithms
Dave Parker's avatar
Dave Parker committed
216
* Added prominence given to log warning messages in command-line/GUI
217
218
* GUI on Macs uses Cmd, not Ctrl
* Added PrismTest class to illustrate programmatic use of PRISM
Dave Parker's avatar
Dave Parker committed
219
* Command-line scripts can signal termination via growlnotify/notify-send 
220
* Bash completion scripts + additional syntax highlighters
Dave Parker's avatar
Dave Parker committed
221

Dave Parker's avatar
Dave Parker committed
222
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
223
Version 4.0.2 (released 9/10/2011)
Dave Parker's avatar
Dave Parker committed
224
225
226
227
228
229
230
231
232
233
234
235
-----------------------------------------------------------------------------

* Better handling of undefined constants in properties
* Added -exportprodtrans and -exportprodstates switches
* More improvements to explicit engine
* Simulator fix: ignores "max path length" for time-bounded properties
* Fixed to compile on Java 7
* Fixed anti-aliasing in GUI model editor
* Various bug fixes

-----------------------------------------------------------------------------
Version 4.0.1 (released 27/7/2011)
Dave Parker's avatar
Dave Parker committed
236
237
238
239
240
241
242
-----------------------------------------------------------------------------

* Added if-and-only-if operator (<=>) for use in models/properties
* Updated version of explicit model checking library
* Testing mode (-test and -testall switches)
* Various bug fixes

Dave Parker's avatar
Dave Parker committed
243
244
245
246
-----------------------------------------------------------------------------
Version 4.0 (released 28/6/2011)
-----------------------------------------------------------------------------

Dave Parker's avatar
Dave Parker committed
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
* Support for probabilistic timed automata (PTAs)
  - new modelling language features: clocks, invariants
  - model checking of timed/untimed probabilistic reachability properties
  - two model checking engines: abstraction-refinement, digital clocks
  - support for expected reward properties (i.e. priced PTAs)

* New approximate/statistical model checking functionality
  - additional confidence-interval (CI) based approximation methods
  - acceptance sampling: sequential probabilistic ratio test (SPRT) method

* Optimal adversary generation for MDPs
  - and for PTAs, via digital clocks engine
  
* Improvements to the property language and model checking
  - enhanced filters for property result processing
  - new, clearer reporting of results from PRISM

* Improved model export functionality
  - option to include state information in dot files (e.g. -exporttransdotstates)
  - action labels included in dot/transition matrix exports
  - clearer for file export for MDPs

* Additional functionality for transient/steady-state probabilities
  - option to specify initial distribution for transient analysis
  - option to export steady-state/transient probabilities to a file

* New components/libraries for developers:
  - completely re-written discrete-event simulation engine
  - explicit-state probabilistic model checking library
  - a quantitative abstraction-refinement engine 

* Other improvements/additions:
  - Strict upper time-bounds allowed in properties
  - Formulas used in properties are left unexpanded for legibility
  - Added check for existence of zero-reward loops in MDPs
  - New -exportprism/-exportprismconst/-nobuild switches
  - New -exporttarget switch
  - New versions of jcommon (1.0.16) and jfreechart (1.0.13)
Dave Parker's avatar
Dave Parker committed
285

Dave Parker's avatar
Dave Parker committed
286
* Changes since 4.0.beta2 (released 10/6/2011)
287
288
  - None

Dave Parker's avatar
Dave Parker committed
289
* Changes since 4.0.beta (released 16/12/2010)
290
291
  - Bug fixes: simulator, error messages, typos and examples)
  
Dave Parker's avatar
Dave Parker committed
292
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
293
Version 3.3.1 (released 22/11/2009)
Dave Parker's avatar
Dave Parker committed
294
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
295

Dave Parker's avatar
Dave Parker committed
296
297
298
299
300
301
* Bug fixes:
  - Building on new 64-bit Macs
  - Simulator bug (crashes on min/max function)
  - CTMC transient probs with MTBDD engine crash
  - State/transition reward mix-up in parser
  - Approximate verification of lower time-bounded properties for CTMCs
Dave Parker's avatar
Dave Parker committed
302
303
304
305
306

-----------------------------------------------------------------------------
Version 3.3 (released 29/10/2009)
-----------------------------------------------------------------------------

Dave Parker's avatar
Dave Parker committed
307
308
309
* Bug fixes:
  - Building on new Macs
  - Copy+paste bug in GUI
Dave Parker's avatar
Dave Parker committed
310

Dave Parker's avatar
Dave Parker committed
311
312
-----------------------------------------------------------------------------
Version 3.3.beta2 (released 29/7/2009)
Dave Parker's avatar
Dave Parker committed
313
314
-----------------------------------------------------------------------------

Dave Parker's avatar
Dave Parker committed
315
316
317
318
* Bug fixes:
  - LTL model checking (svn: 1112, 1132)
  - Approximate model checking (svn: 1214)
  - Building on new Macs (svn: 1103, 1105, 1349)
Dave Parker's avatar
Dave Parker committed
319

Dave Parker's avatar
Dave Parker committed
320
321
-----------------------------------------------------------------------------
Version 3.3.beta1 (released 20/5/2009) (svn: trunk rev 1066)
Dave Parker's avatar
Dave Parker committed
322
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
323
324
325

* New language parser:
  - improved efficiency, especially on large/complex models
Dave Parker's avatar
Dave Parker committed
326
  - more accurate error reporting
Dave Parker's avatar
Dave Parker committed
327
328
329
* GUI model editor improvements:
  - error highlighting
  - line numbers
Dave Parker's avatar
Dave Parker committed
330
  - undo/redo feature
Dave Parker's avatar
Dave Parker committed
331
332
333
* Expanded property specification language
  - LTL (and PCTL*) now supported
  - arbitrary expressions allowed, e.g. 1-P=?[...]
Dave Parker's avatar
Dave Parker committed
334
  - support for weak until (W) and release (R) added
Dave Parker's avatar
Dave Parker committed
335
336
337
338
339
340
341
342
  - steady-state operators (S=?[...], R=?[S]) allowed for DTMCs
  - optional semicolons to terminate properties in properties files
* Modelling language changes:
  - cleaner notation for functions, e.g. mod(i,n), not func(mod,i,n)
  - function names can be renamed in module renaming
  - language strictness: updates (x'=...) must be parenthesised
  - ranges (x=1..3,5) no longer supported
  - added conversion tool for old models (etc/scripts/prism3to4)
Dave Parker's avatar
Dave Parker committed
343
* Other minor technical changes to language:
Dave Parker's avatar
Dave Parker committed
344
345
346
347
348
349
350
351
  - implication allowed in any expression (not just properties)
  - floor/ceil are now identifiers, not keywords
  - relational operators now have precedence over equality operators
  - better but slightly different parsing of problem cases like "F<=a b"
* Improvements to memory handling, especially in sparse/hybrid engines
* Updated JFreeChart library
* Multiple -const switches allowed at command-line
* Efficiency improvements to precomputation algorithms
Dave Parker's avatar
Dave Parker committed
352
* Added symmetry reduction functionality
Dave Parker's avatar
Dave Parker committed
353
* New -exportbsccs option 
Dave Parker's avatar
Dave Parker committed
354
* Initial state info for explicit import is now via -importlabels
Dave Parker's avatar
Dave Parker committed
355
* Added prism2html/prism2latex tools (in etc/scripts)
Dave Parker's avatar
Dave Parker committed
356
357
* Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs
* Easier viewing of model checking results in GUI
Dave Parker's avatar
Dave Parker committed
358
359
* Steady-state/transient probability computation for DTMCs

Dave Parker's avatar
Dave Parker committed
360
361
362
363
364
365
366
367
-----------------------------------------------------------------------------
Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568)
-----------------------------------------------------------------------------

* Fix to allow building on Mac OS X v10.5 (Leopard)
* New option for displaying extra info during reachability (-extrareachinfo switch)
* Addition of some missing reward model checking algorithms
  - instantaneous reward properties (R=?[I=k]) for DTMCs/MDPs (MTBDD/sparse engines only)
Dave Parker's avatar
Dave Parker committed
368
  - cumulative reward properties (R=?[C<=k]) for DTMCs
Dave Parker's avatar
Dave Parker committed
369
370
371
372
373
374
375
376
377
378
379
380
  - sparse engine version of reach reward properties (R=?[F...]) for MDPs
* New option for displaying extra (MT)BDD info (-extraddinfo switch)
* Font increase/decrease feature in GUI
* Labels (for use in properties file) can be defined in the model file
* Properties files can use formulas from model file
* Partially correct property files can be loaded into the GUI
* New icon set and graphics
* New graph plotting engine using JFreeChart
* Prototype SBML-to-PRISM translator
* New option for -simpath feature: can enable/disable loop checking
* New option for -simpath feature: generation of multiple paths to find deadlock
* New "rows" option for matrix exports (-exportrows switch)
Dave Parker's avatar
Dave Parker committed
381
382
383
384
385
386
* Support for 64-bit architectures
* Addition of F and G operators to property language (eventually/globally)
* Redesign of the simulator GUI, plus new features:
  - ability to display cumulated time/rewards
  - new "Configure view" dialog
  - easier selection of next step (double click) 
Dave Parker's avatar
Dave Parker committed
387
* Resizeable experiment results table 
Dave Parker's avatar
Dave Parker committed
388
* Function "log" for use in expressions
389

390
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
391
Version 3.1.1 (5/4/2007) (svn: derived from 3.1 tag)
392
393
394
395
396
397
398
-----------------------------------------------------------------------------

* Minor bug fixes:
  - bug in "New Graph" dialog which fails on Java 6
  - threading bug which can cause graph plotting to freeze
  - fix to possible failure of Windows launch scripts

Dave Parker's avatar
Dave Parker committed
399
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
400
Version 3.1 (15/11/2006) (svn: derived from 3.1.beta1 tag)
401
402
403
404
405
-----------------------------------------------------------------------------

* No changes

-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
406
Version 3.1.beta1 (3/11/2006) (svn: trunk rev 116)
Dave Parker's avatar
Dave Parker committed
407
408
409
410
411
412
413
414
415
416
417
418
-----------------------------------------------------------------------------

* New installer for Windows binary
* Models can now have multiple (named) reward structures
* New -simpath switch for command-line generation of random paths with simulator
* Minor PRISM language improvements:
  - type keyword does not need to be first thing in model file
  - doubles in exponential form (1.4e-9) and unary minus (-1) allowed
* PRISM settings file now used by command-line version too
* Small GUI improvements
* New option to disable steady-state detection for CTMC transient analysis
* Bug fixes
Dave Parker's avatar
Dave Parker committed
419

420
-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
421
Version 3.0 (6/7/2006) (svn: trunk rev 55)
Dave Parker's avatar
Dave Parker committed
422
423
424
425
426
-----------------------------------------------------------------------------

* Bug fixes

-----------------------------------------------------------------------------
Dave Parker's avatar
Dave Parker committed
427
Version 3.0.beta1 (29/3/2006) (svn: trunk rev 45)
428
429
430
431
432
433
434
435
436
437
438
439
-----------------------------------------------------------------------------

* Changes to export functionality
  - transition matrix graph can be exported to a Dot file (-exporttransdot)
  - can export state/transition rewards
  - can export labels and their satisfying states
  - can export to stdout/log instead of a file
  - can export in MRMC format
  - improved support for Matlab format export
  - exported matrices now ordered by default (by row)
  - new/rearranged command-line switches
* Added new options to Model|View menu in GUI
440
441
442
443
444
445
446
447
448
449
450
451
452
* 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  
453

454
-----------------------------------------------------------------------------
455
Version 2.1.dev11.sim8 (3/3/2006)
456
457
458
459
460
461
462
-----------------------------------------------------------------------------

* Bug fix: computation of powers in simulator
* Bug fix: calculation of transition rewards from multiple actions
* Bug fixes: loop detection and deadlocks in simulator

-----------------------------------------------------------------------------
463
Version 2.1.dev11.sim7 (5/1/2006)
464
465
466
467
468
-----------------------------------------------------------------------------

* Bug fixes, tidying

-----------------------------------------------------------------------------
469
Version 2.1.dev11.sim6 (16/12/2005)
470
471
472
473
474
475
-----------------------------------------------------------------------------

* Merged with simulator branch
* Improved options management including saving of user settings

-----------------------------------------------------------------------------
476
Version 2.1.dev11 (5/12/2005)
477
478
479
480
481
482
483
484
-----------------------------------------------------------------------------

Changes:

* Bugfixes in GUI syntax highlighting, esp. for large model files
* Bugfix: out-of-range initial values banned

-----------------------------------------------------------------------------
485
Version 2.1.dev10 (21/10/2005)
486
487
488
489
490
491
492
493
494
495
496
-----------------------------------------------------------------------------

Changes:

* GUI syntax highlighting restructure and efficiency improvement
* Bugfix/tidy in GUI experiments, esp. with Booleans
* Bugfix/improvements in modulo operations
* Improvements to checks of probabilities/rates, e.g. for NaN
* Ability to disable checks of probabilities/rates

-----------------------------------------------------------------------------
497
Version 2.1.dev9 (27/05/2005)
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
-----------------------------------------------------------------------------

Changes:

* Tidied up simulator code/stubs
* Graphical model editor disabled

-----------------------------------------------------------------------------
Version 2.1.dev8 (11/05/2005)
-----------------------------------------------------------------------------

Changes:

* Can now be built on OS X
* Makefile improvements including better OS detection
* Bug fix improving efficiency of BSCC computation
* Improved reporting of multiple missing constants

-----------------------------------------------------------------------------
Version 2.1.dev7 (22/2/2005)
-----------------------------------------------------------------------------

Changes:

* Graphical model editor (temporarily?) enabled
* Addition of simulator code and stubs
* Tweaked main Makefile: stops after first error

-----------------------------------------------------------------------------
Version 2.1.dev6 (18/2/2005)
-----------------------------------------------------------------------------

Changes:

* Bug fix - alphabet for default synchronisation is now derived syntactically
* Updates to some APMC code

-----------------------------------------------------------------------------
Version 2.1.dev5 (11/2/2005)
-----------------------------------------------------------------------------

Partially completed changes:

* PRISM Preprocessor
* Improved hybrid GS
* Improved syntax highlighting

Changes:

* Max memory for Java VM modifiable via PRISM_JAVAMAXMEM environment variable
* Reorganisation of Linux/Solaris launch scripts
* New notation for functions in PRISM language: func(f,x,y)
* New built-in functions in PRISM language (new notation only) - power(pow), modulo(mod)
* Upgrade to newest version of CUDD (2.4.0)
* GUI supports multi-line comments for properties
* Command-line override of model type allowed (-dtmc,-ctmc,-mdp switches)
* Tidy up of output generated by filters in P/S operators
* Added built-in label "deadlock", true in states where deadlocks fixed by PRISM
* Conditional evaluation operator now allows bracketless nesting, e.g. a?b:c?d:e
* Bug fixes

-----------------------------------------------------------------------------
Version 2.1.dev4 (21/1/2005)
-----------------------------------------------------------------------------

Changes:

* New syntax for transition rewards (within rewards construct)
* Bugfix in Prob1A precomputation algorithm
* Bugfix: disappearing "{min}"/"{max}" from P/R operators
* Numerous improvements to graph plotting tool
  - Export of graphs to Matlab
  - Import/export of graphs from/to XML
  - Enhanced scale behaviour/options
  - Improved editing of series properties/data
  - Various bug fixes
* More thorough checks of commands during model construction
  - each command must define transitions for all states satisfying guard

-----------------------------------------------------------------------------
Version 2.1.dev3 (17/11/2004)
-----------------------------------------------------------------------------

Partially completed changes:

* Graphical model editor significantly improved (but disabled for now)

Changes:

* Support for import of (explicit) transition matrix and state space
  (command-line only, via -importtrans/-importstates switches (and -dtmc,-ctmc,-mdp))
* Improvements to graph plotting functionality
* Log in GUI now operates with a limited size buffer to avoid out-of-memory problems


-----------------------------------------------------------------------------
Version 2.1.dev2 (20/10/2004)
-----------------------------------------------------------------------------

Partially completed changes:

* Support for costs/rewards
  - DTMC: R[F] H/S/M
  - MDP: R[F] M ok, H partial
  - CTMC: R[F] H/S/M, R[I=t] H/S/M, R[S] H/S/M, C[<=t] H/S/M

Changes:

* Added facility to compute transient probabilities


-----------------------------------------------------------------------------
Version 2.1.dev1 (7/10/2004)
-----------------------------------------------------------------------------

Partially completed changes:

* Support for costs/rewards
* Checks during model construction that rates are non-negative and probabilities sum to one

Changes:

* Multiple initial states init...endinit
* Support for displaying min/max of a range of probabilities using {} notation
* New "compact" storage schemes (distinct values only) added to sparse/hybrid engines
* Sparse storage schemes now use (more compact) counts instead of start indices for rows/cols
* True Gauss-Seidel algorithm for hybrid engine
* New switches (-pgs, -psor, -bpgs, -bpsor) to access hybrid "psuedo" methods
* Language modification: updates can be "true", i.e. no variables change
* Added conditional evaluation operator (cond ? then : else) to PRISM language


-----------------------------------------------------------------------------
Version 2.1 (released 8/9/2004)
-----------------------------------------------------------------------------

Changes:

* Now possible to build/run PRISM on Windows
* Compilation/installation procedures slightly simplified
* Splash screen on load


-----------------------------------------------------------------------------
Version 2.0 (released 17/3/2004)
-----------------------------------------------------------------------------

Changes:

* Completely new graphical user interface, including:
  - Text editor for PRISM language
  - Automated results collection/graph plotting
  
* Enhancements to PRISM language:
  - Types (ints, doubles and booleans) and type checking added
  - Probabilities/rates can now be expressions
  - Variable ranges/initial values can now be expressions
  - Constant/formula definitions can be expressions (including in terms of each other)
  - Process algebra style definitions allowed for MDPs too (via "system" construct)
  
* Enhancements to property specifications:
  - Probability/time bounds in PCTL/CSL properties can now be expressions
  - Use of constants now permitted: both those from the model and newly declared ones
  - Added "init" keyword to PCTL/CSL (atomic proposition true only in initial state)
  - Can define and reuse "labels" (atomic propositions) (like formulas in model files)
  - Can write properties of the form "P=?[...]" which return the actual probability
  
 * Additional features:
  - Automatic handling of multiple model checking computations,
    e.g. check "P~p[true U<=k error]" for k=1..100
  - Added -exportstates switch, exports reachable states to text file
  - Added -nobscc switch for optional bypass of BSCC computation
  - Added explicit versions of export options (including first export option for MDPs)
  - Export options can now be used in conjunction with each other and with model checking
  - Added -version switch to display version
  
* Efficiency improvements
  - Improved heuristics for hybrid engine (sb/sbmax/gsl switches -> sbmax/sbl/gsmax/gsl)
  - More efficient construction process for unstructured models
  - General restructuring/improvements to model construction process implementation
  
* Miscellaneous
  - Various bug fixes
  - Fairness (for MDP model checking) now OFF by default (used to be ON)


-----------------------------------------------------------------------------
Version 1.3.1 (released 20/2/2003)
-----------------------------------------------------------------------------

Changes:

* Bug fixes in model construction code


-----------------------------------------------------------------------------
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)
* Added option to import PEPA process algebra descriptions as models
* Improved range of numerical methods: (Backwards) Gauss-Seidel and (Backwards) SOR (plus variants for hybrid engine)
* Added -pctl/-csl switches to allow command line specification of properties
* Improved handling of deadlock states: can add self-loops to these states automatically (e.g. -fixdl switch)
* Steady-state probabilities are no longer automatically computed for CTMCs: use the -ss switch
* Addition of {} operator to PCTL/CSL formulas to support printing of probabilities
* Resolved problem with PRISM language syntax: updates must now be parenthesised
* Default value for maximum number of iterations reduced from 500,000 to (more sensible) 10,000
* Added switches to control CUDD behaviour (-cuddmaxmem, -cuddepsilon)
* Additional example files
* Numerous bug fixes
* Now released under the GPL license


-----------------------------------------------------------------------------
Version 1.2 (released 17/9/2001)
-----------------------------------------------------------------------------

First public release