Vojtech Forejt
acd646d02c
* PrismLog now has a "printWarning" method that can be used to print warnings.
* In the end of computation PrismCL prints a message if there were some warnings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4069 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Vojtech Forejt
cd1b3dcfed
Fixed a problem where transition rewards were not being set for unnamed actions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4050 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
3bfb5929bb
Explicit bug fig (from qar/Anvesh) - can now reset rewards in MDPRewardsSimple to 0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4046 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
e9a1859339
Add binary operators to StateValues class and use in explicit model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3996 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
755295f9b4
Explicit engine handles transient with imported init distribition.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3734 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c072eb0bd3
More methods in explicit StateValues.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3733 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9707b6bf10
Added -exportstates for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3722 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
30c0c09569
Small fixes in explicit StateValues class.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3721 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
355032b5e3
Code tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3711 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9ba97fe1fc
Add MDPExplicit class to capture shared from MDPSimple/MDPSparse (also a few fixes to same thing done previously for DTMCs).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3709 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
6a046b4431
Tidy/improve passing of settings to explicit model checkers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3708 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d54e92533c
Another fix for adv gen in explicit engine: min probs should not be treated as for max probs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3691 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
e24ee33442
Bug fix in explicit MDPs: actions added as 0.0 instead of null.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3646 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
0bb97718c1
Adv gen for rewards in explicit engine (from prism-games).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3641 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
f49ce60f1b
Fixes in explicit MDP adversary generation (min case can give wrong answer).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3629 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
1076e70f9f
Bug fix in explicit-state MDP adversary generation (MDPSparse).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3627 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
995cdd3600
More printing options in StateValues (incl. state lists) + rest of filter stuff.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3594 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3351288f3a
StateValues has an associated model in explicit engine; improved printing.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3592 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c476f05eac
Partial implementation of explicit print filter.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3591 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
22d46d0cbb
More printing stuff in explicit StateValues.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3590 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3204326ebc
Improved explicit StateValues class.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3589 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
452f4f2338
More filters in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3588 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
cce915767a
More filters in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3587 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
34fc80f4b9
Partial implementation of filter for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3584 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
14025e109d
Improvements to StateValues class + it's use in explicit model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3581 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
58c6955d29
Handle bounded P/R operators in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3572 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
4cc990cdc4
Added some error detection in -aroptions settings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3549 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c5e417d292
Bugfix in MDPSparse: Copy constructors handle null (absent) action info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3517 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
bedfccb2ec
Re-arrangement of explicit model classes:
* merge ModelSimple and ModelSparse as ModelExplicit
* add ModelSimple as separate interface
* created DTMCExplicit to capture some common methods for DTMC classes
* (still need to do same for other models)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3514 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
1031845775
Bug fix in Distribution class (from Anvesh).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3464 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d73b8cbf76
Fix (simplify) STPGRewards interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3410 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
7a7932bee2
Tweaked toString for STPGAbstrSimple.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3408 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
88e8398155
Revised/expanded STPG interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3401 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
6be5202551
Slight tweak in MDP interface (to match STPG).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3399 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Vojtech Forejt
6238c3fe78
typo in variable name
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3395 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
ea9463344b
Update to (explicit) MDP interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3394 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
7282582841
Added clearRewards method to explicit rewards + better handling of set to zero.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3392 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c674352173
Re-work STPG rewards in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3391 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
be08c7ff94
Formatting (for synch with prism-qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3389 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
16a8c710ae
More re-arranging of explicit rewards (from prism-qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3388 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
a92df6c3b7
Small fixes in explicit rewards.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3385 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
385de74b06
Some tidying in explicit model construction.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3381 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
b55493f943
Method to buld rewards for arbitrary (explicit) models.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3377 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c79d0ccafb
Small fixes in explicit rewards.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3375 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
7a07921f76
Comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3373 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
80b693fee8
Added state rewards into MDP model checking in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3372 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
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