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

2220 Commits (11ab81f540ae86626c21da683892ec7452ed7f73)
 

Author SHA1 Message Date
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
Dave Parker b9ade0d5dd Slight refactor in launch scripts to ease addition of extra libraries.
12 years ago
Dave Parker d1e2870fbc Small refactor for reward construction in other model checkers.
12 years ago
Dave Parker e24275eb8c Small refactor for reward construction in explicit model checkers.
12 years ago
Dave Parker bbbe3311d1 Add ratio reward objectives to the property parser (copied from prism-frac) but no model checking support yet.
12 years ago
Dave Parker 31690047fa Refactor extraction of reward struct from index in R.
12 years ago
Dave Parker 51191706bb Minor refactor (aligning with something in a branch).
12 years ago
Dave Parker 6e415b1403 Added Expression.isFunc() tester method.
12 years ago
Dave Parker 8907515653 Parser fix: stop some unnecessary SystemDefn nodes being created in the parse tree.
12 years ago
Dave Parker 8ce321ffb9 Code tidy (incl. remove warnings) to help with merging.
12 years ago
Dave Parker f24243ff50 Finish refactoring from last commit (missed something in STPG model checker).
12 years ago
Dave Parker 22e7009d7b Refactor explicit engine model checking of reward and steady state operators, as done recently for probabilistic stuff.
12 years ago
Dave Parker f67aee8fca Change "cat" to "edit" in error message from prism-auto/prism-test.
12 years ago
Dave Parker 1051856540 Small refactor: variable names
12 years ago
Dave Parker f0a486b0c7 Further refactoring in explicit model checkers: push more duplicated code into ProbModelChecker.
12 years ago
Dave Parker 274ef86286 Extend previous re-factoring to (unused?) STPGModelChecker.
12 years ago
Dave Parker 36997ee08c Refactor explicit model checkers a bit, including changes to way min/max info is passed around (should generalise to games more nicely).
12 years ago
Dave Parker aa11fa528b Fix in RelOp - we cannot tell whether it is numerical without the bound (= could be =? or =1 (in theory at least)).
12 years ago
Dave Parker 8cc49309b8 Change meaning of isLowerBound() in RelOp and fix calls to it accordingly (to address a problem caused elsewhere in prism-games).
12 years ago
Dave Parker c924183011 Updated to generated parser code (not sure why or when it changed).
12 years ago
Dave Parker 8611094d95 Check for cyclic dependencies in system...endsystem references.
12 years ago
Dave Parker 3ef803f384 Re-factor code to detect cycles in dependencies.
12 years ago
Dave Parker 9e2c117954 lpsolve Makefile fix (from Steffen Maercker).
12 years ago