Dave Parker
|
77bfea558f
|
Fix Makefile so that it does not mis-show ARCH as 86_64 when building on 32-bit Win.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8238 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
9c0273f878
|
Assume Java 7 not 6 when building binaries now.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8236 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
81d8cad3aa
|
Better error message when trying to use "multi" function on models other than MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8232 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
850ed89353
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8224 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
e124caac03
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8215 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
c546ba5c03
|
Fix version for 4.2.beta1
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8213 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
8f7913074d
|
Fix version for 4.2
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8212 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
9d7faf1da8
|
Comment clarification.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8211 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
945432ed63
|
Fixed bugs in output of vectors when showing states but no indices.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8210 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
17dc2a91b2
|
NaN values in rewards cause an error (explicit engine only so far).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8188 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
dfce095d45
|
Make sure that some PrismFileLogs are close()ed after use - spotted as a bug by Bruno.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8168 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
21748bcaa4
|
Tidy up of export-to-Dot functionality, plus new "dot" option for exporting strategy (explicit engine only, currently).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8110 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
7b8b7832a4
|
Code tidy + new methods in PrismFileLog.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8074 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
4d4d288488
|
Output tweak: extra new line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8073 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
08abf1bffe
|
Bug fix: pre-strategy generation check done before model construction.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8072 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
e773d28c15
|
Add buildMCRewardsFromPrismExplicit method (untested).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8071 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Frits Dannenberg
|
16d294eca9
|
changed output se
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8026 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Ernst Moritz Hahn
|
e1bfb8637f
|
fix for fau
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8025 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Vojtech Forejt
|
9ca61c1f74
|
changing permissions, to fix cygwin 64bit compilation
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8005 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Frits Dannenberg
|
720cde341d
|
small bug fix for extremely large right truncation points from Fox-Glynn in the FAU method
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7857 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Ernst Moritz Hahn
|
1397f39709
|
improved description of FAU in commandline and GUI
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7827 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Ernst Moritz Hahn
|
b5c09de4c4
|
fixed stopping criterion for fast adaptive uniformisation when being in array mode
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7817 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
2ef13b46e5
|
Small fix in prism2latex.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7816 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
4e5f05a203
|
Remove debug output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7809 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
87d58db935
|
Bug fix in prism-auto: if directory = . then log file names are not created correctly.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7808 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
13cce4f8da
|
Bug fix: new long setting for simulator max path not read properly (shows up in GUI).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7803 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
06e4c5fee1
|
Move normalisation of DTMC probabilities from SimulatorEngine into Updater class.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7801 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
99d4873c47
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7800 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
d128da069b
|
Bug fix: simulator was normalising DTMC bu dividing by number of choices (which was inconsistent with symbolic construction when using -noprobchecks).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7797 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
928a44101d
|
Make simulator.Updater objects extract settings more cleanly. And respect doProbChecks option.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7795 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
02c26dbf53
|
Update simulator to allow path lengths over 2^31.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7785 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
4a29528714
|
Bug fix: missing state rewards in mvMultRewMinMaxSingleChoices methods (showed up on mdps/reach/mdp_simple.nm regression test).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7773 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
2306ee39ac
|
Bugfix: latest fix to policy iteration broke a previous regression test (rewpoliter.nm) - solved by doing inner solution using lowe level method which takes infinity-states as an argument (in any case, precomputation should not be needed for inner solution).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7772 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
8291b5984c
|
Refactoring wrt the way that relational operators are stored for P/R/S operators (String -> RelOp).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7766 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
56c484d390
|
Code re-factoring in NondetModelChecker.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7735 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
d81ef64ff2
|
Code refactoring (checking for LTL with time bounds).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7731 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
5171fc804e
|
Code re-factoring in NondetModelChecker.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7730 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
896048bf37
|
Bugfix: allow trivial LTL formulae that are just propositions (accidentally disabled a little while back by previous over-zealous type checking).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7723 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
ce694441b8
|
GUI crash fixed - caused by model tree not handling unbounded variables properly.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7721 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
0a8ace99eb
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7720 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
16015890dd
|
Look up of constant value in test RESULT specification should allow imprecision for double values.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7715 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
6073712dc9
|
Bugfix in policy iteration (bug found by Aaron Bohy): needs to be passed in strategy from Prob1.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7707 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
440b539364
|
Bugfix in optimal strategy check for reward properties (showing up as bug in policy iteration).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7669 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
4d3d52edaf
|
Policy iteration for reachability reward problems (explicit engine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7667 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
565f2882d8
|
Tweak to Prism object: simpler constructor.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7641 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
8ebc511308
|
Code tweaks: make Updater independent of PRISM/sim + make SimEngine into PrismComponent.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7639 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
453342d5ba
|
Code tidy (remove warnings).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7636 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
17a222a59f
|
Typo.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7635 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
7fd5c495bd
|
Add labels to explicit models more cleanly and tidy code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7633 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |
Dave Parker
|
60b6307181
|
Add experimental bisimulation option (explicit engine, hidden option).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7630 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
12 years ago |