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

3369 Commits (9bc5baac099c8965ccdd443f362a1dfd49cdbe17)
 

Author SHA1 Message Date
Joachim Klein b4dd82bfa1 PrismCL: For top-level catch-all Exception handling, ignore nailgun exception
9 years ago
Joachim Klein cf16b66849 Prism.closeDown: reset cuddStarted flag
9 years ago
Joachim Klein ba6c74270f Property: handle missing constant in search for right // RESULT line
9 years ago
Joachim Klein d4d87c9ea3 ParamModelChecker: Use standard log handling
9 years ago
Joachim Klein 2ff89c09a4 prism-auto: color 'NOT TESTED' test result just like 'SKIPPED'
9 years ago
Joachim Klein bf6858ee7c param.BigRational: fix isInteger()
9 years ago
Joachim Klein 52dc54df5b ConstantList: methods for removing a constant definition
9 years ago
Joachim Klein 7cd20911e9 ast.Property: tidy comment
9 years ago
Joachim Klein b76524422a PrismCL: Error message if -param switch is given but there is no property to check
9 years ago
Joachim Klein 79e5f3b68d prism-auto: don't expand to filename for exports if 'stdout'
9 years ago
Joachim Klein 74a052a4ec LTSFromDA: small optimization in getSuccessorsIterator(s,i)
10 years ago
Dave Parker 6598fbcfa0 Tidying + refactoring in param.SymbolicEngine for alignment with simulator.Updater, on which it is based.
10 years ago
Dave Parker 3ae531c33b Minor refactoring.
10 years ago
Dave Parker e217d58339 Small comment fix
10 years ago
Dave Parker 3137e20217 Small comment fix
10 years ago
Dave Parker 7583585f99 Code tidy
10 years ago
Dave Parker 6bcdc856c4 Allow .dot extension to be passed to the -exportmodel switch for export of graphical model in Dot format (less verbose and more obvious than -exporttransdotstates).
10 years ago
Dave Parker b7093533e5 Optimisation for PTA model checking where the initial state is a target - just return 1.
10 years ago
Dave Parker 43ffa810db Catch invalid negative time bounds in PTA model checking.
10 years ago
Dave Parker 76fd3b5e80 Bug fix for time-bounded probabilistic reachability in PTAs where the initial location is already a target (reported by Joachim Klein, Linda Leuschner).
10 years ago
Joachim Klein 53036fa388 Property.checkAgainstExpectedResultString: Integer results in exact mode
10 years ago
Joachim Klein e1105ab74a Property.checkAgainstExpectedResultString: handle complex expressions
10 years ago
Joachim Klein 2c8f5427b5 Expression: add evaluateExact methods
10 years ago
Joachim Klein 70e9e56a73 BigRational: add toInt() and toBoolean() methods
10 years ago
Joachim Klein 427844cfd1 BigRational: add isInteger method
10 years ago
Joachim Klein f3d7e01c71 BigRational: add floor() and ceil()
10 years ago
Joachim Klein 48299632a1 BigRational: add from(other) static constructor
10 years ago
Joachim Klein eca03981a0 param.BigRational: fix comment typo
10 years ago
Joachim Klein 6dda865f04 Change prism.parseSingleExpressionString calls to static access
10 years ago
Joachim Klein 678d1111cb Prism: make parseSingleExpressionString a static method
10 years ago
Joachim Klein d6e222a4e1 RESULT handling for Property: Invert order for picking RESULT
10 years ago
Joachim Klein aa3ec454a8 ConstantList: add constructor from Values object
10 years ago
Joachim Klein 69211a1c35 ConstantList: move initialisation to the variable definitions
10 years ago
Joachim Klein a8a3639ee7 NondetModelChecker: use more PrismNotSupportedExceptions instead of PrismExceptions
10 years ago
Joachim Klein 1621fb31c7 mtbdd/PM_NondetInstReward.cc: comment typo
10 years ago
Joachim Klein 7f48229dc1 Prism.modelCheckExact: Properly handle boolean results
10 years ago
Joachim Klein 0632eb656a PrismCL: Catch unhandled Exceptions instead of delegating to default Java handling
10 years ago
Joachim Klein eb017f950c prism.SCCComputer: SanityJDD checks
10 years ago
Joachim Klein 36f4e3f81f prism.ECComputer: SanityJDD checks
10 years ago
Joachim Klein 296f589631 JDD.isSingleton: fix broken computation
10 years ago
Dave Parker 4626d529a5 Code tidy
10 years ago
Dave Parker 09c5b11a74 Bug fix in ConstructModel - do not call attachLabels in justReach mode.
10 years ago
Joachim Klein 0e57919d0e explicit engine: Properly signal "not supported" for MDP total reward computations
10 years ago
Dave Parker bd9f2f255d Add slightly more efficient implementation of getChoiceAction for PRISM models.
10 years ago
Dave Parker 41f4b886ce Minor code tidy
10 years ago
Dave Parker 50e13bca29 Add new getChoiceAction method to ModelGenerator interface, which is basically an alias for getTransitionAction(i, 0).
10 years ago
Dave Parker f76e72827e Correct error in documentation for ModelGenerator interface.
10 years ago
Dave Parker 9fb9d0ae26 Bug fix in StateListMTBDD.getIndexOfState.
10 years ago
Dave Parker 9eff92431e Bug fix in computation (and therefore display) of progress percentage during statistical model checking.
10 years ago
Joachim Klein e5b7f3297b Symbolic engines: Clear ODD when clearing the model (fix memory leak)
10 years ago