Dave Parker
|
4b889ef3e2
|
Removed PathExpression classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@710 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
18 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
|
18 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
|
18 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
|
18 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
|
18 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
|
18 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
|
18 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
|
19 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
|
19 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
|
19 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
|
19 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
|
19 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
|
19 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
|
19 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
|
19 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
|
19 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 |
Dave Parker
|
7afe2837b9
|
Added -simpath switch for generating random paths from command-line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@65 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
1b4036bc16
|
Major overhaul of rewards to allow multiple (named) reward structures.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@59 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
50d1d0f570
|
Bugfix in simulator trace export to file.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@58 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
13cc698041
|
Tidy (remove redundant code) in simulator wrt samples which reach max path len.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@40 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
babd8c6bc0
|
Added error on attempt to use simulator on models with system...endsystem construct.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@39 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
b54050a199
|
PRISM trunk layout rearrangement.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |
Dave Parker
|
30e24567d5
|
Setting trunk version of PRISM to 2.1.dev11.sim8.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
20 years ago |