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

2322 Commits (33ddccaf6bc0c414260cbe114648d0a547c5ff7a)
 

Author SHA1 Message Date
Dave Parker 2ddaf97daf Experimental way of detecting jni.h if it is not in the same place as javac (e.g. on OS X Yosemite?).
11 years ago
Ernst Moritz Hahn 892ecc31e4 fix for dtmcs with overlapping commands
11 years ago
Ernst Moritz Hahn 363b6c0442 added forgotten deep copy
11 years ago
Ernst Moritz Hahn ac7b9d7f80 removed warning
11 years ago
Ernst Moritz Hahn 2e0463c231 corrected choice of order in which states were eliminated. The previous approach lead to states always being eliminated in ascending state number order.
11 years ago
Dave Parker 835d4a9a45 2 ref/deref bugfixes from Joachim Klein.
11 years ago
Dave Parker cc8d3883f6 Expected total rewards (R[C]) implemented for DTMCs in symbolic engine.
11 years ago
Dave Parker 789d7789bb Bug fix in export of DRAs for multi-objective model checking.
11 years ago
Dave Parker 5865c0fd89 Bug fix in exporting product during multi-objective model checking.
11 years ago
Dave Parker 9f4a6dba5f LTL explicit engine bug fix (from Joachim Klein).
11 years ago
Dave Parker 96dc514de3 Re-factoring in multi-objective model checking.
11 years ago
Dave Parker 1f27c28465 Re-factoring in multi-objective model checking.
11 years ago
Dave Parker 753d0d470a Re-factoring in multi-objective model checking.
11 years ago
Dave Parker 4f30f4f774 Re-factoring in multi-objective model checking.
11 years ago
Dave Parker b91b8f0b12 Re-factoring in multi-objective model checking.
11 years ago
Dave Parker 7798782029 Refactoring of extraction of rewards in multi-objective model checking engine.
11 years ago
Dave Parker 806b7b181d Refactoring of extraction of rewards in symbolic model checking engine.
11 years ago
Dave Parker e240865a70 Slight refactor of way that reward structures are looked by via ExpressionReward indices.
11 years ago
Dave Parker a7a6881638 Refactoring of extraction of info from P/R/S operators (in symbolic engines).
11 years ago
Dave Parker 82de131735 Small fix for previous commit.
11 years ago
Dave Parker 72c2d1602e Refactoring of extraction of info from P/R/S operators (in explicit engine).
11 years ago
Dave Parker a7ebc07de5 Copy updated Coalition class from prism-games.
11 years ago
Dave Parker 3d847fb635 Push coalition info into a separate class (including option for * = all players).
11 years ago
Dave Parker 0bb55587be Allow <<>> to be used for MDPs (explicit engine only).
11 years ago
Dave Parker 4c3c523575 Some refactoring of multi-objective model checking: push some code out into a new class prism.MultiObjModelChecker.
11 years ago
Dave Parker 6e76a24240 Better isDFA() check for DRAs.
11 years ago
Dave Parker 1f0382a0b6 LTL model checking optimisation - skip BSCC/EC detection if DRA is (syntactically) a DFA.
11 years ago
Dave Parker db8bfe65c4 Some utility methods for dealing with DRAs that are actually DBAs (or DFAs).
11 years ago
Dave Parker 4defb1a107 Compile fix for last commit.
11 years ago
Dave Parker 50e8d24c02 Add -exportpropaut option (hidden) to export DRA(s) in textual form.
11 years ago
Dave Parker e577bc851d Fix for run scripts on Mac where install directory has a space.
11 years ago
Dave Parker 290fc34bea Add option (switch -exact from command-line) to enable exact model checking via parametric model checking.
11 years ago
Dave Parker f699af97bc Move printout of result for parametric result to allow reuse in exact model checking.
11 years ago
Dave Parker acc8a65b4f Some preliminary code to add parametric model checking to GUI.
11 years ago
Dave Parker c99655eda9 Catch some divide-by-zero errors in JasFunction.
11 years ago
Dave Parker e001c3ac1d Back to "dev" version (post release).
11 years ago
Dave Parker 84f01078e6 Add a method for exact model checking via parametric methods (not connected).
11 years ago
Dave Parker 99bdf07b49 Fix in SubNondetModel: getSuccessorsIterator should return a set (i.e. no duplicates).
11 years ago
Dave Parker 43a58adaca Version/changelog - 4.2.1.
11 years ago
Dave Parker 052f0e8861 Bug fix in simplification of implication (affects explicit engine) (from Philipp Chrszon).
11 years ago
Dave Parker 7c687d5195 Bugfix in MDPSparse (from Joachim Klein).
11 years ago
Dave Parker 1314f91107 Bugfix in SubNondetModel (from Joachim Klein).
11 years ago
Dave Parker ab328b5fc7 Code tidy of comments in jdd.JDD (from Joachim Klein).
11 years ago
Dave Parker 5295b1a180 Bug fix in MDPSimple.mvMultJacSingle (from Joachim Klein).
11 years ago
Dave Parker aba185d835 Bugfix - explicit-state model checking for LTL on CTMCs (from Joachim Klein).
11 years ago
Dave Parker 73e2dfa94f More jltl2ba and jltl2dstar bug fixes from Joachim Klein.
11 years ago
Dave Parker 2690b87ff5 Bug fix in simulator: in DTMCs with local nondeterminism, random transitions can be wrongly chosen due to the distributions not being normalised.
11 years ago
Dave Parker f0db2c26f9 Improve handling of constants in parametric model checking - avoid conversion of fractional constants such as 1/3 to doubles and the resulting loss of precision.
11 years ago
Dave Parker 8cb6a437cd Add strategy operators (<<>> and [[]]) to parser, but no support model checking.
11 years ago
Dave Parker 4d80473332 Add error message if attempting to check an LTL formula on a PTA (with digital clocks).
11 years ago