s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
2806 Commits
5 Branches
0 Tags
31 MiB
Tree: e10b900018
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'e10b900018'
${ noResults }
Commit Graph

2806 Commits (e10b9000184715521a1c92561d76386ced2919de)
 

Author SHA1 Message Date
Dave Parker e10b900018 Add Makefile target "count_loc" to display a count of lines of code.
10 years ago
Dave Parker 9e18844a26 Bug fix in ModulesFileModelGenerator: need to make sure model constants are expanded in labels.
10 years ago
Dave Parker 0e01288705 Improve explicit.ConstructModel: generalise to use new ModelGenerator interface (not just ModulesFiles via the simulator) and tidy up the settings within the class.
10 years ago
Dave Parker a959beb7a7 Create ModelGenerator class for a ModulesFile object. Base code on existing stuff in SimulatorEngine, but do not remove anything from there.
10 years ago
Dave Parker 7ff1ffe2db Make ModulesFile implement new ModelInfo interface.
10 years ago
Dave Parker 89c80043df Add new ModelGenerator interface (will eventually replace ModelExplorer interface). Also add ModelInfo superclass containing just some syntactic model info and a default implementation of the class for easier use.
10 years ago
Dave Parker 9ce7e6441b Push containsUnboundedVariables methof from VarList up into ModulesFile.
10 years ago
Dave Parker f16da3762d Add missing file from last commit.
10 years ago
Dave Parker 17087eee26 Decompose semantics checks (into expressions, models, properties). This will facilitate later attempts to make model checking less tied to ModulesFile specifically, rather than other model sources.
10 years ago
Dave Parker 8775d3a993 Small fix in Expression static constructors to make return types more clearly specified. [from Steffen Marcker]
10 years ago
Dave Parker 557695e82b Small refactor in SimulatorEngine.
10 years ago
Dave Parker 4aea86b501 Comment clarifications.
10 years ago
Dave Parker 6a4e44b8ab Small refactor in SimulatorEngine.
10 years ago
Dave Parker b1cab85663 Code tidy.
10 years ago
Dave Parker 99fa6cf81b Some commenting in SimulatorEngine.
10 years ago
Dave Parker 400fcfcc45 Some refactoring in SimulatorEngine.
10 years ago
Dave Parker 11cf431209 Auto-format.
10 years ago
Dave Parker 7557171b82 Auto-format.
10 years ago
Dave Parker 15cbc73554 Tidying/commenting in GUI simulator.
10 years ago
Dave Parker e85cceb572 Small tidies/fixes in explicit engine MDP strat generation.
10 years ago
Dave Parker fb37c9a22d Slight refactoring of strategy storage in explicit engine (to match PRISM-games).
10 years ago
Dave Parker bb44582283 Set default values for some hidden options in PrismSettings.
10 years ago
Dave Parker 87b50d7da2 Small change in ExpandPropRefsAndLabels: either properties list or lable list can be omitted (and is then ignored).
10 years ago
Dave Parker b1f83bfbf5 Small fix: slightly more efficient recursion in ExpandLabels and ExpandPropRefsAndLabels.
10 years ago
Joachim Klein c11bec58ab SimpleLTL: refactor/protect simplify(), check that formula graph is actually a tree
10 years ago
Joachim Klein 59f44c56ee SimpleLTL: isTree() check to ensure that graph structure is tree, not DAG
10 years ago
Joachim Klein e3b49ea35f SimpleLTL: add toDot() output of the syntax tree / DAG
10 years ago
Joachim Klein ec84a58371 common.PlainObjectReference: For storing an object in a HashSet/HashMap, ignoring custom hashCode/equals
10 years ago
Joachim Klein 043c776914 Refactor ConvertForJltl2ba (fix regression due to custom equals/hashCode for ASTElements)
10 years ago
Dave Parker 90a79ce2d0 Some additional output during Pareto curve generation.
10 years ago
Dave Parker b46a0c31be Multi-objective Pareto curve calculation fix: more robust computation of extreme values when non-convergence is an issue.
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.
10 years ago
Dave Parker b35a8d1553 Typo in output.
10 years ago
Dave Parker 0b35370d20 Typo in multi-objective output.
10 years ago
Dave Parker 0d099446aa Refactoring and commenting in multi-objective model checking.
10 years ago
Dave Parker 5ab01f26b8 Refactoring + tidying in multi-objective value iteration.
10 years ago
Dave Parker d52576a6dd Refactoring + tidying in multi-objective value iteration.
10 years ago
Dave Parker 91c8af3aac Refactoring + tidying in multi-objective value iteration.
10 years ago
Dave Parker 1493a0c6c5 Refactoring in multi-objective value iteration: move check for step-bounded with GS.
10 years ago
Dave Parker 41ba061916 More output for multi-objective value iteration.
10 years ago
Dave Parker 3afca48506 More info printed out by multi-objective value iteration + more efficient vector access.
10 years ago
Dave Parker 75197e3d22 Handle NaN better as a constant. [from Joachim Klein]
10 years ago
Dave Parker dc146fbf63 Commenting to document recent changes to CUDD constant hashing/truncation. [from Joachim Klein]
10 years ago
Dave Parker 8597f0e71b Extend previous commit (reachability enlarging target) to STPG model checking.
10 years ago
Dave Parker bf76e587bc Small optimisation in explicit model checkers, when enlarging target for reachability. [from Steffen Marcker]
10 years ago
Dave Parker 9255d29ac8 Fix some unclosed logs when exporting. [from Steffen Marcker]
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]
10 years ago
Dave Parker 18cd16d78d Code tidy (auto-format).
10 years ago
Dave Parker f95f76ab81 Bugfix in PRISM-to-Latex translation.
10 years ago
Dave Parker c373555f9c Refactoring multi-objective code: readying for allowing lists of objectives in strategy operator.
10 years ago