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

73 Commits (5e5461da4acf808230ffc18f3014e2ef55cf8979)

Author SHA1 Message Date
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 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 8291b5984c Refactoring wrt the way that relational operators are stored for P/R/S operators (String -> RelOp).
13 years ago
Dave Parker 896048bf37 Bugfix: allow trivial LTL formulae that are just propositions (accidentally disabled a little while back by previous over-zealous type checking).
13 years ago
Dave Parker a73b36685b Add getAllLabels method to ASTElement (not used currently).
13 years ago
Dave Parker fe4cd9560c Allow unbounded integer variables in model (but forbid for symbolic model construction).
13 years ago
Dave Parker 2573445470 Typo.
13 years ago
Dave Parker 021b512512 Bugfix: error in recent additions to S operator type checking.
13 years ago
Dave Parker e1db928f9f Bugfix: missing type checking in properties: P/S/R operators were allowed to contain arbitrary types.
13 years ago
Ernst Moritz Hahn fd855d0ff4 reintegrated parametric stuff
13 years ago
Dave Parker 4d9d778515 Comment tweak
14 years ago
Dave Parker b13aa417ad Un-needed files (since fairnesss stuff not in this branch, currently).
14 years ago
Dave Parker 9b5aae301f Patch in current version of multi-objective model checking (from prism-multi branch). Still need to copy across etc/ directory containing lpsolve libraries. Also contains a few JDD fixes via Christian von Essen.
14 years ago
Dave Parker 3c44acb8e1 Added new printall filter.
14 years ago
Dave Parker a3d99e62d0 Add property reference support to PTA ans approx model checking.
14 years ago
Dave Parker b870e550e7 Fixes/renames in property reference search code.
14 years ago
Dave Parker be53bceb72 Rename a few visitor classes
14 years ago
Dave Parker fd968a89d1 Check for cyclic dependencies in property references.
14 years ago
Dave Parker ac31984b5a Fix type checking for property references (and some autoformatting - oops).
14 years ago
Dave Parker c7365ce0d9 Bugfix: look for undefined constants recursively in referenced properties.
14 years ago
Dave Parker c7d1af5f85 More fixes for bugs introduced in recent "improvements" to constant handling API:
14 years ago
Dave Parker 854cd58edd Typo in error message (old debugging info).
15 years ago
Vojtech Forejt b1e27b40c5 added a missing class for handling named properties in the gui
15 years ago
Dave Parker a066e5db8e Bugfix in handling of init/deadlock labels during constant processing - e.g. P=?[F "deadlock"&x=i] failed if i was a constant.
15 years ago
Dave Parker bf59e25a49 Fixed a bug in getAllUndefinedConstantsRecursively. Showed up when running auto in embedded example. Bug found by Janne Kauttio.
15 years ago
Dave Parker 10313b7d02 Improved handling of undefined constants in properties files:
15 years ago
Dave Parker 2654125531 * Check added to catch if the same variable is set twice in the same update
15 years ago
Dave Parker 6289094aa0 Property references can appear in properties (still a few TODOs though).
15 years ago
Dave Parker 3c8ca8495d Added iff (<=>) to PRISM model/properties language.
15 years ago
Dave Parker 8465fdeb07 Property names parsed (but not used) and -test switch added (but no property/verify blocks yet).
15 years ago
Dave Parker 4ad686212f Bug fix in ExpandLabels: missing deepCopy (only affects explicit engine currently).
15 years ago
Dave Parker ce4b0beb1e Undoing last commit.
15 years ago
Dave Parker bcab165234 Use gcc-3 etc by default when building on Cygwin.
15 years ago
Dave Parker 71ca9d28af Final (pre-4.0) fixes to filters: added "state" filter, which gives result for a filter which must satisfy exactly one state, and make this the translation for old-style {state} filter.
15 years ago
Dave Parker 35f377ab3e Improved documentation (JavaDoc mostly).
15 years ago
Dave Parker 07098cca94 Fix: inter-module var access allowed for digitsal clocks.
15 years ago
Dave Parker 5dcbaab5eb Header typo: author attrib.
16 years ago
Dave Parker 76d7039060 Code tidy: stop PrismExceptions on formula expansion (eases debugging) and remove an unused method.
16 years ago
Dave Parker da822f4a6b Code comments.
16 years ago
Dave Parker e0aa53801e Additional checks on where clock variables can appear in models.
16 years ago
Dave Parker 0ba3191214 Add restrictions on which reward properties supported by digital clocks, and remove complaint about existence of both state/transition rewards.
16 years ago
Dave Parker 248981743c Better handling of filters, including ranges returned for multiple initial states.
16 years ago
Dave Parker bc834d7d83 Better property checks for PTAs, including new computation of prob operator nesting. Better handling of labels in PTA model checker.
16 years ago
Dave Parker f0826d03e0 Bugfix in preproc due to PTA syntax checks.
16 years ago
Dave Parker 39150596a4 Semantic check for non-local variable access in PTAs.
16 years ago
Dave Parker 9ce9901d91 Further work on simulator.
16 years ago
Dave Parker 17b4d063d1 Simulator supports labels
16 years ago
Dave Parker a653cd6239 Removal of debug output.
16 years ago
Dave Parker f3e24d7997 ModulesFile bugfix (shows up when using digital clocks).
16 years ago