Dave Parker
|
fff1065289
|
Javadoc fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2263 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
37f9cf9325
|
Javadoc fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2262 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
|
dbfd975c66
|
Some formatting issues in Win launch scripts.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2256 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
|
fa8a5b7b06
|
Bug fix: time-bounded PTA properties (from Nico).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2253 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
22b8658fbd
|
Flagged possible bug (explicit MC).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2252 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
e700693b0e
|
Clocks not allowed in reward structures (digital clocks).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2250 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
0ba3191214
|
Add restrictions on which reward properties supported by digital clocks, and remove complaint about existence of both state/transition rewards.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2248 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
eac2ee9c17
|
Bug fix: Strict constraint check for digital clocks got disabled.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2247 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
acaa6e2e11
|
Added "try digital clocks" to some PTA error messages.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2245 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
a2fdbb007c
|
Partial support for plotting interval results in GUI: just plot lower value.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2242 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
5bea84a402
|
Fix: Interval results show in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2241 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
248981743c
|
Better handling of filters, including ranges returned for multiple initial states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2240 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
489758c2ba
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2239 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
b6fcd8ab8a
|
Code tidy (forwards reach).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2238 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
f790b47bf1
|
Better detection of timelocks (in forwards reach) + some additions/fixes to DBMs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2236 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
afc67f2204
|
Undo last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2225 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
29b7905290
|
Removed unnecessary svn:ignore (these are handles in global svn config).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2224 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
66206e8905
|
Catch mem-out on PTA module explore.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2221 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
bb929f64f3
|
Bug fix: Model check freeze in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2220 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
eafa913f05
|
Bug fix in just-added unbounded methods for Zone.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2217 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
93d028bde5
|
Added unbounded check to Zone classes (+ API tweak).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2216 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
bd3e821069
|
Added getMin and getMax to Zone classes + tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2215 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
8b7990d6ab
|
Better checks for convexity in (A-R) PTA model checking (again).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2214 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
b9b4cb821f
|
Bug fix in detection of strict clock contraints in props for digital clocks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2211 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
f827f6d38c
|
Fixed -exportprism switch for digital clocks case.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2207 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
f2855a95f4
|
Better checks for convexity in (A-R) PTA model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2206 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
2e8a2d4b2e
|
Bug fix in integer power type checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2205 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
|
3f734e76db
|
Added func in odd to convert index to BDD.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2202 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
31707a7729
|
Two bugs in LTL model checking for MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2201 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
|
5666a51b0c
|
Possible bug fix: Termination of simulation check in GUI not detected (thread issue?).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2199 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
a97d6d9841
|
Digitsl clocks enabled for model checking in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2198 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
c4b176232c
|
Error message when trying to do bounded properties with digital clocks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2197 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
c19b257e70
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2196 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
146b5f35be
|
Moved digital clocks translation so it can be done per property (in PrismCL).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2195 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
3da3b1e298
|
Bugfix: no double display of error message in GUI result dialog.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2194 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
dcfc7c59de
|
Added option to do experiments for PTAs in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2193 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
4b3cf8c6b4
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2192 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
e9545cac7c
|
Added option to verify PTAs in GUI (no experiments yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2191 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
da9ca7124c
|
Small tidy in simpath generation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2190 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
29c462722c
|
Simulator bugfix: exported path was one short.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2189 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
|
55899baab5
|
Simulator bug: picking wrong random choice in CTMCs with multi-update commands (e.g. DTMCs seen as CTMCs).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2187 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
7607a567da
|
Add isDeterministic() method to TransitionList.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2186 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
03cf76f5d6
|
Fix: floor/ceil of NaN/inf is an error.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2185 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |