Dave Parker
8775d3a993
Small fix in Expression static constructors to make return types more clearly specified. [from Steffen Marcker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10959 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
557695e82b
Small refactor in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10946 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
4aea86b501
Comment clarifications.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10945 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
6a4e44b8ab
Small refactor in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10939 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b1cab85663
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10936 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
99fa6cf81b
Some commenting in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10930 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
400fcfcc45
Some refactoring in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10928 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
11cf431209
Auto-format.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10921 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
7557171b82
Auto-format.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10918 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
15cbc73554
Tidying/commenting in GUI simulator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10915 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
e85cceb572
Small tidies/fixes in explicit engine MDP strat generation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10913 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
fb37c9a22d
Slight refactoring of strategy storage in explicit engine (to match PRISM-games).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10910 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
bb44582283
Set default values for some hidden options in PrismSettings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10905 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
87b50d7da2
Small change in ExpandPropRefsAndLabels: either properties list or lable list can be omitted (and is then ignored).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10901 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b1f83bfbf5
Small fix: slightly more efficient recursion in ExpandLabels and ExpandPropRefsAndLabels.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10899 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
c11bec58ab
SimpleLTL: refactor/protect simplify(), check that formula graph is actually a tree
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10898 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
59f44c56ee
SimpleLTL: isTree() check to ensure that graph structure is tree, not DAG
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10897 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
e3b49ea35f
SimpleLTL: add toDot() output of the syntax tree / DAG
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10896 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
ec84a58371
common.PlainObjectReference: For storing an object in a HashSet/HashMap, ignoring custom hashCode/equals
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10895 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
043c776914
Refactor ConvertForJltl2ba (fix regression due to custom equals/hashCode for ASTElements)
In SVN 10565, custom equals/hashCode methods were introduced for the
various ASTElements/Expressions, providing semantic equality. In the
implementation of ConvertForJltl2ba, a Hashtable was used to store
SimpleLTL formulas for the already handled Expression objects. With
the new equals/hashCode, this can lead to SimpleLTL formulas that
share subtrees, resulting in a DAG instead of a tree.
The SimpleLTL.simplify() function behaves incorrectly for DAGs, e.g.,
for "! (X (s1=7)) | (X (X s1=7))", producing wrong output formulas.
We refactor ConvertForJltl2ba to do a simple recursive transformation
from Expression-based LTL to SimpleLTL. Optionally, sharing of
identical subtrees can be enabled.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10894 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
90a79ce2d0
Some additional output during Pareto curve generation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10893 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b46a0c31be
Multi-objective Pareto curve calculation fix: more robust computation of extreme values when non-convergence is an issue.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10891 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
619b7d53c5
Re-enable disabled convergence check in multi-objective value iteration since it can give the wrong answer. Better fix follows.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10890 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b35a8d1553
Typo in output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10889 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
0b35370d20
Typo in multi-objective output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10888 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
0d099446aa
Refactoring and commenting in multi-objective model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10886 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
5ab01f26b8
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10885 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
d52576a6dd
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10884 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
91c8af3aac
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10883 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
1493a0c6c5
Refactoring in multi-objective value iteration: move check for step-bounded with GS.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10882 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
41ba061916
More output for multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10881 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
3afca48506
More info printed out by multi-objective value iteration + more efficient vector access.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10880 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
75197e3d22
Handle NaN better as a constant. [from Joachim Klein]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10877 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
dc146fbf63
Commenting to document recent changes to CUDD constant hashing/truncation. [from Joachim Klein]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10876 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
8597f0e71b
Extend previous commit (reachability enlarging target) to STPG model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10875 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
bf76e587bc
Small optimisation in explicit model checkers, when enlarging target for reachability. [from Steffen Marcker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10874 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
9255d29ac8
Fix some unclosed logs when exporting. [from Steffen Marcker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10873 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
325d8c5cd2
Fixes to handling of constants in CUDD - factor out pre-hash truncation in to a separate function and make sure truncation is also carrued oit when *re*hashing the table. [from Joachim Klein]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10872 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
18cd16d78d
Code tidy (auto-format).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10866 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
f95f76ab81
Bugfix in PRISM-to-Latex translation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10853 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
c373555f9c
Refactoring multi-objective code: readying for allowing lists of objectives in strategy operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10849 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
5a33c86e54
Comment typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10847 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
30b197918c
Comment/tidy/refactor multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10846 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
cec60108c2
Comment clarification.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10845 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
bfe2715d3b
Error message typo.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10842 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
56d5739b06
Missing header file commits for r10829.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10834 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
85b7c30d4a
Catch possible null value in GUI simulator update table display (reported by Steffen Marcker).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10833 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
a64997f903
Bugfixes in sparse engine adversary generation (cumulative reward and multi-objective): remove second stat line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10831 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
91d984cce8
Add some adversary generation for multi-objective value iteration (just exports one adv for each separated weighted objective).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10829 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
3347d55d0a
Bug fix for updateAutoParse(): from prism-games.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10826 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago