Dave Parker
|
de95d5ea89
|
Slight efficiency improvement in JDD.IsContainedIn().
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5705 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
786d2ac6a8
|
Tidy: Auto-format.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5702 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
ae798a69d9
|
Fix: explicit engine did not pick up verbose setting.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5664 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
65bb3d2d9a
|
Compiler warning.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5648 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
cd250aa6d1
|
Improved selection of matching RESULT for -test: can just have a subset of const values in the RESULT spec.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5647 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
eb8c1e9abf
|
Better error msg for unavailability of R[C<=k] for MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5638 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
84f1c97413
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5635 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3b59b8f6cd
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5633 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
da50f86281
|
Tweak comments in policy iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5632 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
eb34f465a7
|
Bounded until for DTMC/MDP in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5631 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
433c3a3414
|
Next operator for explicit model checker.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5629 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4413259325
|
Explicit model checker can handle negated path operators like G.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5624 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
582ddb0e43
|
Error message typos.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5623 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
1b5dc955e6
|
Few extra methods in StateValues.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5622 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
6e2b0b789b
|
DTMC S operator model checking for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5621 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
fd53ce813c
|
Refactor (symbolic) steady-state computation for S operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5620 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5018559d3e
|
DTMC steady-state computation for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5617 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
387fae41f4
|
Code comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5616 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
e0eca95da0
|
Refactor (symbolic) steady-state computation for S operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5615 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
d71fde3538
|
Refactor (symbolic) steady-state computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5614 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
50201cfbf7
|
Refactor single-BSCC detection in (symbolic) steady-state computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5613 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
271f6af317
|
Temporary compile fix.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5612 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4f09722850
|
Added IsContainedIn method to JDD.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5601 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
4fb0e557d9
|
More general fix replacing recent bugfix (rev 5568) for digital clocks timelocks from GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5588 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
7940a7f271
|
Undo previous commit (not ready yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5587 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
e5deabda0b
|
Connect -importinitdist functionality for explicit engine (missing from rev 5545).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5586 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
275e1b8655
|
Bugfix: c-closure on empty zone breaks when max clock constraint constant is 0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5582 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Mateusz Ujma
|
d66142cf2d
|
Fixed bug with not finding timelocks in Digital Clocks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5568 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Mateusz Ujma
|
ba03cc9671
|
Added comment
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5567 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
9565022214
|
Fix: properties files passed to GUI forgotten about in case of model parse error.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5566 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Mateusz Ujma
|
e48a274c55
|
Added loading properties from command line when using GUI
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5565 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Mateusz Ujma
|
2983cde5b2
|
Changed JLabel to JTextField to be able to copy&paste current model/properties file name.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5547 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
739f83e2ba
|
Revert to old behaviour where ss/tr probabilities exported to files do not show state indices (otherwise breaks -importinitdist).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5546 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
ab831c8a6c
|
Allow -importinitdist for steady-state (as well as transient).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5545 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
535a42be04
|
Refactor (forwards) steady-state computation in symbolic engines, partly for alignment with future corresponding code in explicit engine, partly to allow arbitrary initial distributions, as for transient.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5544 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
ad294aa981
|
Added dot product method to symbolic StateValue classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5543 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
1915395882
|
Bugfix: small optimisation was never enabled during stead-state computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5533 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
e0d68f8b74
|
Bug fix: PTA rewards on digital clocks: forgot to scale by GCD.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5523 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
0022e81b1b
|
Parser handles invalid literals (too big etc.) + tidy up of parser error reporting code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5520 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
b2f33e44a7
|
Fixed "changed" setting in graph display of simulation paths.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5482 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
7af19279f6
|
GUI bugfix: NPE.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5481 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
4f2759fadb
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5480 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
21eae01cfb
|
GUI bug fix (crash caused by model tree not displaying clocks, spotted by pk123 on forum).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5476 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
57259f67c1
|
Updated version of Path Plot dialog, including specification of max path length.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5431 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
74717ecb9a
|
Updated version of Path Plot dialog, including specification of variables.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5430 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
b80badd54c
|
Shortcut for new path plot (Ctrl/Cmd-F8).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5428 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
5131fb407f
|
Some useful code (commented out) for getting variance etc. from simulation results.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5425 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
5486e68282
|
Check for duplicate ids/names in reactions-to-PRISM translation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5423 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
0de837a4b8
|
Typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5422 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
0245cf77b4
|
Bug fix: crash on invalid integer reward struct indices.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5420 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |