s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
1568 Commits
5 Branches
0 Tags
31 MiB
Tree: fa2b70f1e6
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'fa2b70f1e6'
${ noResults }
Commit Graph

1568 Commits (fa2b70f1e6f07d52d1738f04f22484e1343f8648)
 

Author SHA1 Message Date
Dave Parker fa2b70f1e6 Better error message for lack of filters in PTA m/c.
14 years ago
Dave Parker 19ef6934e8 More cases handled when cacheing filter info in (symbolic/explicit) model checkers.
14 years ago
Dave Parker 4a8285eec7 Utility method in ODDUtils for converting state index to BDD (already existed at C++ level).
14 years ago
Dave Parker 43d52add46 Model checkers (symbolic/explicit) cache some filter info for optimisations/checks during model checking.
14 years ago
Dave Parker 3982420c3d Utility method in ODDUtils for finding index of first state in a BDD.
14 years ago
Dave Parker 2e6582c108 Utility method in ODDUtils for finding index of first state in a BDD.
14 years ago
Dave Parker e681ec2ae7 Remove old un-needed code in explicit model checking function.
14 years ago
Dave Parker 1ff7316aa0 Remove un-needed check for LTL formula inside time-bounded until.
14 years ago
Dave Parker b88899c998 Add support for computing ranges of transient probabilities (e.g. -tr 0.1:0.01:0.2) to command-line. Transient probability computation is done incrementally, using each computed distribution.
14 years ago
Dave Parker 9786d49b3c Fix: missing parts of last commit.
14 years ago
Dave Parker c1e24408ae New (hidden) options for different symbolic reachability methods (-frontier, -bfs). Also: new way to read options from C++ code: PrismNative stores reference to Prism object which is then queried.
14 years ago
Dave Parker 3199c3daa2 Tidy up reachability code: strip out old diagnostic output, uncomment frontier method for easier testing.
14 years ago
Dave Parker be4417dbe9 Comment
14 years ago
Dave Parker 397fc1b4aa Tidy of explicit engine settings import, to identify some missing features.
14 years ago
Dave Parker 750f3fd0ba Separate setting explicit engine for MDP solution method (stoch games still uses old solnMethod field).
14 years ago
Dave Parker 1e0dff70d2 Separate setting explicit engine for linear equation system solution method.
14 years ago
Dave Parker a51157e11a Update syntax highlighters for .prism/.props file extensions (untested).
14 years ago
Dave Parker 8f00acc289 Finish up missing parts of explicit.StateModelChecker - no longer relies on evaluate()ing all states for missing operators.
14 years ago
Dave Parker 507e721b97 Bug fix in just-added code for explicit model checker.
14 years ago
Dave Parker 955e3c9aaa Functions handled properly by explicit model checker.
14 years ago
Dave Parker 4a20773172 Better error message for unexpected non-exception.
14 years ago
Dave Parker 2a609cb942 Better error message for unexpected non-exception.
14 years ago
Dave Parker 1955392c65 Test mode can expect exceptions, e.g. using:
14 years ago
Dave Parker e3846c7d21 Push some function evaluation code into separate methods, for easier re-use elsewhere.
14 years ago
Dave Parker 6f7a25d070 Code tidy
14 years ago
Dave Parker 4bd2319af1 Unary operators handled properly in explicit engine.
14 years ago
Dave Parker 1f315247a3 Test commit
14 years ago
Dave Parker 0b83c9a079 Test commit
14 years ago
Dave Parker e4114f8144 Add .prism as model file extension to GUI.
14 years ago
Dave Parker 7eebb21135 Bugfix: model rebuild avoidance in Prism works ok when there are no undefined constants.
14 years ago
Dave Parker 1b87d356a8 Move explicitBuildTest code into PRISM, but currently unfinished/unused.
14 years ago
Dave Parker 63f338e2b5 Remove some TODO comments.
14 years ago
Dave Parker 58c1803f32 Push some log output into Prism (+ autoformat).
14 years ago
Dave Parker 3ee7bb5651 Bugfix in recent changes to GUIExperiment.
14 years ago
Dave Parker 01c3826d8d Less exceptions thrown from ResultCollection error setting methods, with knock-on effect (cleaner code) in various calling sites.
14 years ago
Dave Parker 735c9f0e5c First attempt at making PrismCL deal with model build failures using new API.
14 years ago
Dave Parker 98cd895717 Add deadlock handling (e.g. for nofixdl) for explicit engine.
14 years ago
Dave Parker 80f8605a1e Deadlock info preserved in explicit model copies.
14 years ago
Dave Parker 47d5de8371 Bugfix: ModelExplicit should preserve deadlocks on copy.
14 years ago
Dave Parker d853309bb1 Code tidy
14 years ago
Dave Parker feb5161cda Remove modifiedSinceBuild flag from GUI.
14 years ago
Dave Parker e27cf12c14 GUI fix: update model info display for explicit engine.
14 years ago
Dave Parker 20150621ce Code tidy
14 years ago
Dave Parker 38e0844687 Tidy
14 years ago
Dave Parker 1ebd851512 Added exportprod{states,trans} functionality to D/CTMC model checker too.
14 years ago
Dave Parker a3c6b759f0 Small tidies.
14 years ago
Dave Parker 4d4278fefe Change exportprodstates option to use Model not (old) Prism API.
14 years ago
Dave Parker 2f0c968ff5 Push "export states" functionality into models (symbolic/explicit), use from Prism.
14 years ago
Dave Parker 9d13945300 New toString method + comments in State.
14 years ago
Dave Parker f6582ef185 Fix some other refs to old Prism API.
14 years ago