Alexander Bork
|
02a325ba75
|
Fixed error that refinement did not stop if initial computation already yields same values for over- and under-approximation
|
5 years ago |
|
Alexander Bork
|
054c2a906e
|
Fixed wrong error when over- and under-approximation values are equal
|
5 years ago |
|
Alexander Bork
|
d28c982fbd
|
Fix for missing initial belief ID in return struct
|
5 years ago |
|
Alexander Bork
|
8e30e27eb9
|
Removal of obsolete code
|
5 years ago |
Tim Quatmann
|
581e165fb9
|
Actually use the refinement precision....
|
5 years ago |
|
Tim Quatmann
|
de483cd3c1
|
Added missing number conversion.
|
5 years ago |
|
Tim Quatmann
|
b3493b5888
|
Grid: Added cli setting to cache subsimplices.
|
5 years ago |
|
Tim Quatmann
|
3aaea1eb0a
|
Added new CLI settings for GridApproximation
|
5 years ago |
|
Tim Quatmann
|
a11ec691a9
|
Introduced options in the ApproximatePOMDPModelChecker.
|
5 years ago |
|
Tim Quatmann
|
bf7f84f796
|
Added --check-fully-observable option to easily check the underlying MDP
|
5 years ago |
|
Tim Quatmann
|
5bdcb66fcb
|
Fixes for reward formulas
|
5 years ago |
|
Tim Quatmann
|
24faf636d7
|
removed unused variables.
|
5 years ago |
|
Tim Quatmann
|
12f498356a
|
Fixed help message
|
5 years ago |
|
Tim Quatmann
|
6c32b645c4
|
Fixed compilation with mathsat.
|
5 years ago |
|
Tim Quatmann
|
58de346bd5
|
Revert "Fixed compilation with mathsat."
This reverts commit 8b57b18201.
|
5 years ago |
Sebastian Junges
|
22e20e93a9
|
permissive strategy test should also run without mathsat
|
5 years ago |
|
Alexander Bork
|
c2582058c9
|
Added first version of refinement with reuse of previous results
|
5 years ago |
|
Tim Quatmann
|
27ac99806e
|
Stopwatch: added restart() method
|
5 years ago |
|
Tim Quatmann
|
824c28f332
|
Instantiation for POMDPs in Propositional model checkers.
|
5 years ago |
|
Tim Quatmann
|
635fbc658a
|
storm-pomdp: towards a more mature cli
|
5 years ago |
|
Tim Quatmann
|
8b57b18201
|
Fixed compilation with mathsat.
|
5 years ago |
|
Tim Quatmann
|
cc66c9d758
|
Storm-conv: Added a comment explaining why this executable needs its own 'setUrgentOptions'
|
5 years ago |
|
Tim Quatmann
|
82ad509405
|
storm-cli: Splitting the 'export' part from buildPreprocessExportModelWithValueTypeAndDdLib. This allows to build the model without exporting it.
|
5 years ago |
|
Tim Quatmann
|
5c748254a6
|
Cleaning up the POMDP CLI code a bit. Now supports switching to exact arithmetic with the --exact switch.
|
5 years ago |
|
Tim Quatmann
|
0d58ea5291
|
Adding missing template instantiation.
|
5 years ago |
|
Tim Quatmann
|
5933467670
|
Silenced warnings regarding member initialization in unexpected order.
|
5 years ago |
Matthias Volk
|
57fe5106a5
|
Removed printing complete matrix
|
5 years ago |
|
Tim Quatmann
|
81356d1dc8
|
Jani JSONExporter: Increased precision for output.
|
5 years ago |
|
Tim Quatmann
|
1dccab9673
|
JaniParser: Added missing template instantiation and other fixes.
|
5 years ago |
|
Tim Quatmann
|
0433469b9e
|
Added missing template instantiation.
|
5 years ago |
|
Tim Quatmann
|
7b32aa968e
|
Fixed actually using the JaniParser with rational numbers.
|
5 years ago |
|
Tim Quatmann
|
6af6bc5472
|
Replaced remaining uses of modernjson::json with the new storm::json<..>
|
5 years ago |
|
Tim Quatmann
|
328b9c6986
|
Gave the JaniParser a template argument, so that we can use it to parse with doubles or with RationalNumbers.
|
5 years ago |
|
Tim Quatmann
|
632c9c2e1e
|
Modified the modernjson library so that it can parse numbers as rationals.
|
5 years ago |
|
Tim Quatmann
|
c70b6baf81
|
Abort unif+ also in inner iterations. Store the best known solution after each completed step.
|
5 years ago |
|
Tim Quatmann
|
80f28e196d
|
Print current iteration count when aborting a solver.
|
5 years ago |
|
Tim Quatmann
|
9fddf3858b
|
Abort topological solvers if requested.
|
5 years ago |
|
Tim Quatmann
|
463766dbe0
|
Improved numerical stability of computation of transient probabilities in CTMCs.
|
5 years ago |
|
Tim Quatmann
|
b5a64ba7e3
|
CTMC Model checker: Consider relative precision for time-bounded queries in --sound mode
|
5 years ago |
|
Tim Quatmann
|
71f22fef2f
|
Added a CLI switch to perform exact model checking over finite precision floats
|
5 years ago |
|
Matthias Volk
|
d0b54fe6b5
|
Set number of printed digits in output
|
5 years ago |
|
Matthias Volk
|
de27fa82fe
|
Changed result output iterator for DFTs
|
5 years ago |
|
Tim Quatmann
|
70e2263783
|
MarkovAutomatonCslModelCheckerTest: Prevent this test from failing in cases where z3 is installed without optimization support.
|
5 years ago |
|
Tim Quatmann
|
137f41abac
|
FormulaInformation: Fixed detection of property type.
|
5 years ago |
|
Tim Quatmann
|
1fd052aee4
|
InformationCollector: Use infinite precision to determine the state domain size.
|
5 years ago |
|
Tim Quatmann
|
2b89da2f4b
|
Updated decision tree used in portfolio engine.
|
5 years ago |
|
Tim Quatmann
|
5dcebdef93
|
Fixed invocation of storm without a model.
|
5 years ago |
|
Tim Quatmann
|
f4820628a5
|
Incorporated more features for the portfolio engine.
|
5 years ago |
|
Tim Quatmann
|
3b53e1e583
|
Implemented retrieval of jani model information with a traverser. Also determine the size of the state domain.
|
5 years ago |
|
Tim Quatmann
|
d3ece2a2e5
|
Better simplification of prism commands.
|
5 years ago |
