Dave Parker
|
bdd579d85d
|
New option in GUI simulator to plot path on a graph (all vars over time).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5360 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
178d3ca90e
|
SimulatorEngine only builds TransitionList on demand.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4958 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
ead22700e8
|
New SimulatorEngine/Prism method prism.isPropertyOKForSimulation().
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4741 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
1cb0822a31
|
Code tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4737 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
ce41611aa2
|
Enable viewing of witness/counterexample for E[F...] in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4726 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
a3d99e62d0
|
Add property reference support to PTA ans approx model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4507 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
90c9e53f8c
|
Tweak some warning messages (wrt new log.printWarning method) + add warning message functionality in GUI threads.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4178 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
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 |
Dave Parker
|
f578bbb893
|
Approximate model checking ignores "max path length" setting when verifying time-bounded properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3855 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
503d33a01c
|
Bug fixes for loading zero-length paths into simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3529 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
|
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
|
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
|
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
|
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
|
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
|
dec122cd20
|
Code comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3213 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
a126367821
|
Simulator engine: Documentation of Choice object, remove some unused Choice methods, add some action-querying methods in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3212 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
30be4f175e
|
Missing function in SimulatorEngine API.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3040 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
7cd3f36336
|
GUI bugfix: "Update" in GUI simulator transition table displaying wrongly for old path states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3030 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
087ea5da6a
|
General tidy up of initial state handling in simulator, including a few GUI bug fixes. GUI default is to use the default initial state. For generation of simulation paths, there is a separate menu item to start from a specified state (and no option to switch asking on/off). Additional tidying and documentation in related parts of code too.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2835 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
35f377ab3e
|
Improved documentation (JavaDoc mostly).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2436 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
ac19ffc149
|
Trap potential GUI bug (from Marco).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2394 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
5d9573628d
|
Better error message for simulator on filters.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2392 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
53a5274cb3
|
Addition of new statistical model checking stuff (patch difference between trunk and prism-statmc branch at this revision).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2391 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
c1025f4b72
|
Javadoc fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2265 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
db60e6487b
|
Javadoc fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2260 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
98126c125c
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2255 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
9f5d37ffa3
|
Bugfix: simulatino for experiments was disabled.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2254 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
fbec092ace
|
Check for overflows added to simulator, but disabled for now.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2204 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
de11a8685e
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2203 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
b6d4a15737
|
Simulator disabled for PTAs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2200 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
fcf236acd3
|
Added (self-loop) deterministic loop detection to simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2188 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 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.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2176 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
bcd6110358
|
Simulator updates: fixed display of transitions in GUI, added (some) detection of deadlocks/self-loops. (And some tidying.)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2020 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
04b7b65a42
|
Simulator tidies.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1991 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
911268e6ea
|
Simulator bug (overwrite old states when backtracking).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1989 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
4a8ea16a6c
|
Fixes, tidies in simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1963 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
84cf5db181
|
Fixes, tidies in simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1962 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
97fddcb1b9
|
Remove preceding states added to simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1960 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
ddb279d4e0
|
Removed accidental parts of last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1959 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
915edf43ba
|
Option (current enabled) to use FORMATS10 style forwards reach, plus a few zone API tweaks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1958 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
c4a8bd19c4
|
Simulator code: tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1892 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
763285cc4c
|
More simulator additions/tidying.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1891 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
a0db106a88
|
Tweaks to Sampler design + non-compilation bugfix.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1889 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
9ce9901d91
|
Further work on simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1886 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
bb2615b43b
|
Further work on simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1885 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
c3ba43e358
|
Further work on simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1883 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
17b4d063d1
|
Simulator supports labels
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1880 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |