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

2242 Commits (e577bc851d557911b8b52815f84948a629087f64)
 

Author SHA1 Message Date
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
Dave Parker 3ddbf6e3a0 Bug fix in parametric model checking (spotted by dbanisimov): some missing Expression.deepCopy() calls were resulting in rewards (and probably other things) being evaulated incorrectly.
11 years ago
Dave Parker a50a15c596 Comments.
11 years ago
Dave Parker 11ab81f540 README update (contributors).
11 years ago
Dave Parker 27a96022f0 README update (contributors).
11 years ago
Dave Parker caf5a0e50b Bugfix: statistical model checking of discrete-time bounded untils with strict bounds (from Joachim Klein).
11 years ago
Dave Parker 75b20e5801 Some additional error checking in explicit.StateValues (from Joachim Klein).
11 years ago
Dave Parker 690d7d93aa Some additional error checking in explicit.StateValues (from Joachim Klein).
11 years ago
Dave Parker 0a5e0b6203 Additional checks in explicit MDP model checker: don't allow policy iteration methods to be use when 'known' values are passed in (from Joachim Klein).
11 years ago
Dave Parker 63c7d1fcd0 Added a getLabels() method to the explicit.Model hierarchty (from Joachim Klein).
11 years ago
Dave Parker 575977afd3 Small jltl2dstar fix from Joachim Klein.
11 years ago
Dave Parker 48c6e73e2a Bugfix: release (R) temporal operator not displayed correctly (from Joachim Klein).
11 years ago
Dave Parker f58712cd22 Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch).
11 years ago
Dave Parker c5e4ba4f73 Another LTL-to-automaton bugfix from Joachim Klein (jltl2ba-fix-simplify-bstates--trivial-sccs.patch).
11 years ago
Dave Parker 6594babe09 Another LTL-to-automaton bugfix from Joachim Klein (fix-bdfs.patch).
11 years ago
Dave Parker 8e2bc361cd Improve simulation Sampler classes to handle deadlocks (in some cases). Deadlocks still not properly handled by the simulator.
11 years ago
Dave Parker 5e5461da4a Compile fix (to allow build on Java 6).
11 years ago
Ernst Moritz Hahn 33a7f2c9e8 fixed computation of lost probability to take into account probability mass intentionally destroyed
11 years ago
Ernst Moritz Hahn a50a254805 bugfix fau
11 years ago
Dave Parker 78d3755e4e A jltl2ba bug fix from Joachim Klein - fixes various previously reported LTL->DRA crashes.
12 years ago
Dave Parker 2acff0caed Bug fix in Dot export of DRA.
12 years ago
Dave Parker d386b73cc4 Tweak debug print out of DRA - show APs too.
12 years ago
Dave Parker 7f10ec8b60 Bug in explicit engine LTL model checking (happens when there are multiple APs in the formula and ordering is different in the DRA). Reported by Manfred Jaeger.
12 years ago
Dave Parker 124fa87de6 Amend Makefile to use -encoding UTF8 setting more widely for javac/javah/javadoc (based on reports from SIFT).
12 years ago
Dave Parker 390344d02f Undo accidental part of last commit
12 years ago
Dave Parker 06c914a476 Change visibility of some classes/methods in the param package to allow use from outside the package (and fix broken build).
12 years ago
Dave Parker 946c767fb5 Change visibility of some classes/methods in the param package to allow use from outside the package.
12 years ago
Dave Parker 89fab7269a Bug fix in getSuccessorsIterator(s) in SubNondetModel (showed up as regression test failure in prism-games-heuristics-merge), plus required missing method getSuccessorsIterator(s,i) in NondetModel.
12 years ago
Dave Parker afd1c35480 Remove getTransitionsIterator from NondetModel.
12 years ago
Dave Parker 3c6ca999b0 Test mode failure (for wrong result) shows obtained result as well as expected one.
12 years ago
Dave Parker 5cb2faff94 Slight (additional) refactor in launch scripts to ease addition of extra libraries.
12 years ago