Dave Parker
|
af0fb7cba6
|
Simulator bug fix (non-compile).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1864 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
c28f11a31d
|
Further improvements to the simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1860 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
b80a050e46
|
Further simulator improvements.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1856 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
bf70579d62
|
Additions/tidying to simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1853 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
6bf2d09394
|
Updates to simulator, including random choices for CTMCs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1846 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
55e52d5e22
|
Ongoing simulator improvements.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1842 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
794fc13bf5
|
Updates to simulator: engine + GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1805 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
17 years ago |
Dave Parker
|
d199d035ed
|
Integration of prism-explicit branch into trunk, i.e. merge of trunk@1015-prism-explicit@1405 into trunk.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1406 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
17 years ago |
Dave Parker
|
c66eecb5cc
|
Bug fix in approximate model checking of time-bounded until properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1214 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
17 years ago |
Mark Kattenbelt
|
6e345734d5
|
fix bug command line path generation in presence of deadlock
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@929 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
18 years ago |
Dave Parker
|
5c7c11c23d
|
Fixes to allow building under Fedora 9 (GCC 4.3).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@808 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
18 years ago |
Dave Parker
|
539c794980
|
Typo/bug fix in logarithm calculations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@733 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
574f6e9ebb
|
Sim bug: temporal operator types.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@717 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
4b889ef3e2
|
Removed PathExpression classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@710 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
ffc6437a7e
|
Tidy of conversion to U for F/G checking/simulation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@699 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
84bc3d3d47
|
Eclipse tidy (remove unused imports).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@661 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
5d3d24bc17
|
Merged prism-parser branch (revs 577:659) into trunk.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@660 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
8a3eb3ac6f
|
Minor compilation fixes (Kostas Oikonomou) (Solaris?).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@581 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
738b806fd2
|
Added (in full) log function to PRISM language.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@569 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Mark Kattenbelt
|
b96f9ba1fa
|
Fix: no updates with probability 0 in update list simulator
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@553 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
2179deefdb
|
Updated email addresses and affiliations in copyright info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@547 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
7446459574
|
More fixes for fussy compilers: return types in simulator cc code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@484 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
544b155c56
|
Code tidying for argument types in strict compilers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@460 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
5ae5bea3dd
|
Removed temporary diagnostic outputs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@459 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
a37a947fc5
|
Properties files can use model file formulas. Model files can contain labels.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@454 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
5c1bb43a2f
|
Code tidy (function return types).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@452 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
01316021e7
|
Bugfix: Bounded G and F operators in simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@450 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
ee6dfc9c33
|
New options for -simpath: loopcheck=true/false, repeat=N (latter for deadlock generation).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@326 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
19 years ago |
Dave Parker
|
d636ab1969
|
Addition of 64-bit PRISM branch to trunk.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@262 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
5ef3824832
|
Rearrangement and tidy-up of copyright/license info in file headers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@253 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
d522e5d792
|
Updates backtracking by time. Seems to work better. (1/2)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@214 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
eaed7b4233
|
Improved Java detetction in Makefile, including case where directory has a space, e.g. "Progam Files".
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@209 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
b587c24490
|
Added time-bounded backtracking. Does not work well when backtracking should be to the first state.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@207 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
1e0cbf5533
|
Missing Linux C++ #include.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@206 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
513081bb5f
|
Added time-bound exploration option to the simulator. Needs make clean!
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@205 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
fbd754d91e
|
Fixed removed preceding so cumulative time and cumulative rewards are recalculated. Don't forget to `make clean'.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@197 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
12bf479f84
|
Bugfix (segfault) in simulator binary input.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@189 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
f57befa6b2
|
Small bugfix to simulator (for cumulative time).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@187 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
4b79591e88
|
Underlying code for cumulative time in simulator. Not used and not tested. Bound to break something.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@186 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
a2fd0dd5b7
|
Addition of F (future) and G (global) operators to property specification language.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@181 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
c08cb36e70
|
Added `cumulative reward' information to the simulator engine (the c++ part), untested and not used... yet.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@175 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Mark Kattenbelt
|
5e00f01dc0
|
Small update to both the Java and C part of the simulator to facilitate the display of (instant) state rewards of the most current state.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@174 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
69d14c44cc
|
Filed some notes about the distributed version of the simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@163 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
6845512140
|
Removal of APMC code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@129 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
83152265f5
|
Changed handling of multiple reward structures so is 1-indexed from properties, etc.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@98 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
fbebb8b759
|
Removed $(shell find ...) commands from 2 Makefiles (problems on Windows).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@88 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
20a6be968b
|
Removal of explicit lists of Java/C++ files from Makefiles (we are reliant on GNU make anyway).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@83 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
3149f54d47
|
Removal of unused code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@80 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
3c35caeafb
|
Bugfix to -simpath option.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@67 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
8a34673e81
|
Improvement to -simpath functionality (vars=... option).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@66 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |