Dave Parker
|
4806f83088
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3511 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
4369027912
|
Fix in LTL model checking to ensure that product model (when exported) has correct initial states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3510 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
e9518b6448
|
Added -exportprodtrans and -exportprodstates switches.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3508 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
4b4641678b
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3507 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
0b65c69a6b
|
Added loadPath methods to SimulatorEngine and GUISimulator; not used currently.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3470 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
2325bee04b
|
CexPathAsBDDs supports PathFullInfo interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3469 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
40ed660f6a
|
Extend PathFullInfo method to clarify what info is stored.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3468 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
2f5de7b714
|
GUISimulatorPathTableModel reads from new PathFullInfo interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3467 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
6706b44a3e
|
Added PathFullInfo interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3466 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
|
f274604e0b
|
GUI bug fix (simulator). How did this ever work?
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3459 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
f3ae5d3b23
|
Refactoring/tidying/fixing GUISimulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3458 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
6196d0cdde
|
Code doc.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3457 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
0e435b134a
|
Move CTL cex class storage into new cex package.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3453 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
a6ba42b5ad
|
Detach simulator Path objects from SimulatorEngine (do not need).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3451 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
6b21b0543d
|
Added ModelType.probabilityOrRate() method, used in simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3447 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
afa2d79305
|
Code tidy in GUI simulator: replace ==CTMC checks with isContinuousTime().
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3446 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
72551d7248
|
Refactoring: detach GUI simulator path table from SimulatorEngine and attach to PathFull.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3445 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
919fba9061
|
Fix anti-aliasing in GUI simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3444 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
a1e3b4e3e3
|
Re-factoring of GUI simulator code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3443 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
9dd562a6eb
|
Small fixes in simulator wrt experiments (one part should have been commited earlier with undefined constants improvements).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3439 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
b30c5ac74a
|
Error message if user attempts to define a constant that is already defined.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3438 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
3723afae6c
|
New isDefinedConstant methods (+ code tidy).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3437 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
4037e0701f
|
Line endings
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3425 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
|
d4ce4fa73c
|
Code doc
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3380 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 |
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 |