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

153 Commits (99e5420e4cc474a4d926372ef43d73c8b52ea5bf)

Author SHA1 Message Date
Dave Parker d07055efa6 Copy updated Coalition class from prism-games.
11 years ago
Dave Parker 00cc653f68 Make a note that R_C is deprecated.
11 years ago
Dave Parker 17a946783d Disallow properties of the form R[F<=k].
11 years ago
Dave Parker 69c8b2ce1f Bug fix: better detection of R[F] when seeing if it is cosafe.
11 years ago
Dave Parker 812930e490 Comment typo
11 years ago
Dave Parker b1c31f56e1 Utility methods for detecting syntactically cosafe LTL.
11 years ago
Dave Parker 9f6777bed5 Regression tests: detect and warn about spaces in Error RESULT specifications.
11 years ago
Dave Parker e73a7b2fb5 Undo regression test change: Error RESULT specifications cannot contains spaces (causes problems on specs with comments).
11 years ago
Dave Parker 30bec11226 Regression tests: Case-insensitive checks when comparing Error RESULT specifications.
11 years ago
Dave Parker cdbc634b26 Regression testing: allow spaces in "Error" RESULT specifications.
11 years ago
Dave Parker c7d8a01190 Fix JavaDoc bugs.
11 years ago
Dave Parker 2dc4ef9a4a Fix JavaDoc bugs.
11 years ago
Dave Parker f1ce23b1b4 Simplify/iimprove checking of rational results: can convert doubles.
11 years ago
Dave Parker 6b4125b1bd Tidy up and improve checking of rational results
11 years ago
Dave Parker 862d605ac5 Some basic checking of rational results
11 years ago
Dave Parker 8475ae29be ExpressionQuant: mode -> modifier.
11 years ago
Dave Parker adba5a090c ExpressionQuant: mode -> modifier.
11 years ago
Dave Parker 1945ef1d40 More refactoring of ExpressionQuant and add "mode" field, currently ignored.
11 years ago
Dave Parker 5c8439c0e6 Convert ExpressionQuant from interface to abstract class and push some shared code in ExpressionProb/Reward/SS into it.
11 years ago
Dave Parker 88928e8b89 New PrismNotSupportedException, to be throw when a model/prop/engine combination is not supported. Displays as UNSUPPORTED, not FAIL, in test mode. [from Joachim Klein]
11 years ago
Dave Parker e02281dc86 Add Expression.isPathFormula(). [Joachim Klein]
11 years ago
Dave Parker d9ec3199b9 Refactoring: Expression.convertSimplePathFormulaToCanonicalForm(), converts to (negated) a U b or X a. Use in model checkers. [Joachim Klein]
11 years ago
Dave Parker 1f27c28465 Re-factoring in multi-objective model checking.
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 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 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.
12 years ago
Dave Parker 8cb6a437cd Add strategy operators (<<>> and [[]]) to parser, but no support model checking.
12 years ago
Dave Parker a50a15c596 Comments.
12 years ago
Dave Parker 48c6e73e2a Bugfix: release (R) temporal operator not displayed correctly (from Joachim Klein).
12 years ago
Dave Parker 5e5461da4a Compile fix (to allow build on Java 6).
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 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 6e415b1403 Added Expression.isFunc() tester method.
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 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 45daee70e4 Update author info in some recently change classes.
12 years ago
Dave Parker 7fb4426803 Models can have multiple system...endsystem constructs, they can be named, and they can be referenced from each other.
12 years ago
Dave Parker 309cfc0294 Code tidy (JavaDoc).
12 years ago
Dave Parker 07bed0bbe6 Bug fix - multiple constants in RESULT spec for testing was not working.
12 years ago
Dave Parker 7a4b42efde Add an (as yet unimplemented) option to Prism to store the vector of results during model checking.
12 years ago
Dave Parker f85400152d Re-factoring - push the creation of default filters during model checking into a utility method in ExpressionFilter.
12 years ago
Dave Parker 8291b5984c Refactoring wrt the way that relational operators are stored for P/R/S operators (String -> RelOp).
12 years ago
Dave Parker d81ef64ff2 Code refactoring (checking for LTL with time bounds).
12 years ago