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

279 Commits (2c2533eda8ff59561441bb597e162ae4bf1c6d98)

Author SHA1 Message Date
Dave Parker e2d1f0af25 Bug fix in CNF conversion.
11 years ago
Dave Parker 795627c953 Add partial support for multi-objective queries expressed as Boolean expressions.
11 years ago
Dave Parker d44e1c7ecc Bug fix in Coalition copy constructor.
11 years ago
Dave Parker a6003f8216 Allow <<>> operator for MDPs (but not checked properly yet).
11 years ago
Dave Parker fa9b601faf Update parser to allow proper <<>> or [[]] syntax.
11 years ago
Dave Parker d07055efa6 Copy updated Coalition class from prism-games.
11 years ago
Dave Parker 234fe87e31 Fix parser tweak from previous commit.
11 years ago
Dave Parker cfa767ec0d Parser tweak to avoid ambiguities with S operator inside an R (now that LTL formulae are allowed).
11 years ago
Dave Parker 00cc653f68 Make a note that R_C is deprecated.
11 years ago
Dave Parker a76b3c73bd Remove (most) usage of R_F in temporal operators.
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 957148215e Support (symbolic/explicit) for expected reward to satisfy a co-safe LTL formula.
11 years ago
Dave Parker b037bdf604 Missing file from last commit.
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 a42e4108ee More locale setting for outputting decimals in English.
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 1d6d52f9a7 Export results in "comment" mode now also shows values of non-ranging contants.
11 years ago
Dave Parker e90e072eee Error message typos.
11 years ago
Dave Parker a298807d5d Additional toString in Values class.
11 years ago
Dave Parker 68960327c1 State.setValue returns a copy of the object (for chaining purposes).
11 years ago
Dave Parker f19cb029d7 Parse modifiers on R and S operators as well as P.
11 years ago
Dave Parker 7f1315dfc1 Do not allow any ExpressionQuant modifiers for now.
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 bb6693f43d Allow comments to have no trailing new-line (e.g. when occurring at very end of file) - cannot see a good reason not to allow this.
11 years ago
Dave Parker 38f0e001c2 Bugfix in PrismParser.isKeyword (leading to incorrect identification of bad identifiers in SBML/reactions to PRISM translation).
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 4849d6d603 Remove check for lower bounds in path formulas for DTMC, MDP. [Joachim Klein]
11 years ago
Dave Parker a9f4c14409 Don't allow lower time-bounds for weak until (e.g., for a W[l,u] b or a W>=l b) due to unintuitive semantics. [From Joachim Klein; but moved check to higher up]
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