Dave Parker
e8e1a403b9
Bug fix in MDPRewardsSimple.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3371 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
075822347e
Reward constrcution for explicit engine pushed into separate class, and added state rewards for MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3370 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
a539e72e57
MDPSimple bug fix (from prism-qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3368 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
4d56c43157
Small fixes in explicit action construction.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3364 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c737dffa07
Remove accidental parts of last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3363 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
15de6c029c
Fix in explicit model construction: allow distinct MDP choices that differ only by action name.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3362 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9be3a42d1a
Comments.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3360 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
5ebd8b941b
Enable -exporttrans switch under explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3359 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
139b4f6dd6
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3358 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
e5b7ad597e
Expansion of transition-matrix-export functionality for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3357 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
ebf163a14e
Code doc: Added some useful references to DBM classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3348 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
42338f803c
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3333 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
61883e8197
Doc/comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3332 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
25b8626a51
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3331 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3403e8b417
Some bugfixes and adds in explicit MDP classes, mainly relating to action labels.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3330 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
edab23b581
More updates to explicit library:
* removed some old rewards code from explicit models
* (and temporarily disabled a few things in PrismSTPGAbstractRefine accordingly)
* added method addActionLabelledChoice to MDPSimple
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3325 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
687feda2ef
Vojta - copyright and acks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3324 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
b8a78c4031
Updates to explicit engine from prism-qar (Vojta):
* new rewards code for STPGs
* additional utility methods
* strip out some old reward stuff
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3323 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
68c65a560f
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3320 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
10313b7d02
Improved handling of undefined constants in properties files:
* don't need to provide values for all constants, just those required for model checking
And a few related bug fixes:
* in error handling for constants in PrismCL
* in export of labels from properties file with constants
And some small related API changes:
* don't need to call setUndefinedConstants on ModulesFile/PropertiesFile if there are no undefined constants
* more flexible UndefinedConstants classes
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3319 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
236d1db265
Tidy/document DefinedConstant and UndefinedConstants classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3309 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
120f88862d
Added PEPA zip to Eclipse config.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3308 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
49b9846c5b
Fix CTL counterexample generation for case where there are multiple initial states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3307 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
36e523c90a
Bugfix: bug added in recent changes to initial state creation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3300 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
2e065801b9
Added anti-aliasing by default to model text editors.
Note that PepaEditorKit is changed here, but never used it seems.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3299 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
26130c8d38
Correct types for initial state of ModulesFile (only a problem when there are clocks).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3298 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3ee741c788
Version num (4.0.1.dev).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3297 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
34daba81cf
Remove version num from README.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3294 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
2eaee4ef55
4.0.1 release notes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3293 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
657afdcd52
Version nums (4.0.1).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3292 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9f91ecae2f
CHANGELOG.txt.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3291 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
24caab6c97
Credit/copyright for Christian von Essen.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3290 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
5d3166a5b9
Re-arranged people in README.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3289 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
af6eef0c49
Added castValueTo method to Type classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3288 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
41f38a34fc
Added ability to have multiple RESULT test specifications for different constant values, e.g. "RESULT (x=1,y=2): 0.5".
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3285 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
f1bac71e5d
Improved doc for Values class + new toStringConcatenated method.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3284 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
f61753b14e
Slight changes to exporttransdot format (to match explicit): boxes bot circles for states (works better when there are state labels) and larger dots for mdp transitions.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3283 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
7737034db7
Removed accidental part of last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3282 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
e33c2b1301
Added action names to other MDP explicit exports (dot, PRISM lang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3281 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
ac4eac3719
Action names included in explicit MDP export to tra file (from prism-qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3280 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
5e477df476
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3266 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
5bab1a4e1c
Added -testall to -help text.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3265 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9c1436994a
Update CHANGELOG (actually, mostly done in last commit by mistake).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3264 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
88dc326670
Confirm that -importprismpp is hidden option for now.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3263 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
cb49b36fc3
Bugfix: property handling in PTA model files fails (caused by inability to call tidyUp() twice in PropertiesFile).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3262 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
0728db06cf
Explicit engine reward construction handles model constants properly.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3255 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
8bbda8f530
Added new expression evaluation methods (needed for explicit model checker). Unfortunately breaks some existing calls to evaluate(constVals, null) due to ambiguities. Need to replace them with evaluate(constVals).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3254 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d207970473
Some proposed changes to explicit.rewards classes (from prism-qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3250 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
e3549400e6
Changed storage/evalation of constants in explicit model checker to fix some bugs and allow calls to checkExpression to handle constants.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3242 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
be2d5d7b55
Added -importprismpp option to import directly from preprocessor files.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3239 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago