dehnert
2d41de479e
added progress outputs to iterative solvers
9 years ago
dehnert
d8d3404b87
fixed termination criteria and equipped interval value iteration methods with check whether the method converged for the relevant states
9 years ago
dehnert
e7b6587170
minor fixes for new relative convergence test
9 years ago
dehnert
e719a37c6c
fixes related to relative termination criterion
9 years ago
dehnert
cb849a9ab8
started on computing upper bounds for rewards for interval value iteration
9 years ago
dehnert
df0b5fbfa5
fixed multiply-reduce operations in the presence of empty row groups
9 years ago
dehnert
8e8fc34c30
fixed some TBB-related issues and added power method for linear equation systems
9 years ago
dehnert
c5134c364f
Extraction and update of TBB-parallelized stuff
9 years ago
dehnert
5440d164b2
started on Walker-Chae algorithm
9 years ago
dehnert
3c844a487f
some more optimizations
9 years ago
dehnert
5fafe835cb
started on some optimizations for conditionals in MDPs
9 years ago
dehnert
9bda631795
symbolic MDP helper respecting solver requirements
9 years ago
dehnert
7c24607427
started on symbolic solver requirements
9 years ago
dehnert
a3cbaedcc1
intermediate commit to switch workplace
9 years ago
TimQu
76c01de25c
use utility::vector::max_if to compute the maximum exit rate in an MA
9 years ago
dehnert
4adee85fa5
added checking requirements of MinMax solvers to model checker helpers
9 years ago
TimQu
acd6c5e9be
fix for toIntegralVector
9 years ago
TimQu
2d2cc95774
fixed issue #12 raised by Joachim Klein
9 years ago
sjunges
12c79ad6ea
export choice labels
9 years ago
Sebastian Junges
fb8dd88314
fixes in parsing, support for POMDPs in DRN
9 years ago
sjunges
bbb4d16965
towards support for pomdps in storm
9 years ago
TimQu
b3507b8f96
fixed 'toIntegralVector' method
9 years ago
dehnert
d23547d99f
started optimizing some DdManager methods
9 years ago
dehnert
d0cf2ef57b
update to version 1.4.0 of sylvan
9 years ago
TimQu
9ca14a54fc
templated the LpSolvers
9 years ago
TimQu
5fdb03440d
First version of LpMinMaxLinearEquationSolver
9 years ago
Matthias Volk
7330f1659e
Set development flag for Storm version
9 years ago
Sebastian Junges
53a2723e0c
storm pars result moved from storm to storm pars
9 years ago
TimQu
988b2a9af9
added functionality to split a rational vector into an integer vector and a rational factor
9 years ago
Sebastian Junges
c46ce03e60
make storm compile with latest version of carl
9 years ago
TimQu
c7b83ffb5f
moved parameter lifting related code out of the main library/executable
9 years ago
TimQu
b1f4dfd9d1
Fixed restoring the value of std::cout.fill() after setting it to '0'
9 years ago
TimQu
2f49255db6
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
9 years ago
TimQu
ecf3c7e996
reverted renaming of LabelSetGenerators to CommandSetGenerators. Potentially, these generators work for arbitrary sets of labels, not just for sets of Prism commands.
9 years ago
TimQu
dcd9319ba4
fixed a convertNumber instantiation
9 years ago
dehnert
179cd8308e
remove old API files
9 years ago
dehnert
ea02ea0838
started overhaul of cli/api
9 years ago
TimQu
9f894667eb
Fixed DRN exporter/parser: MAs are not supported as there is no indication for Markovian choices
9 years ago
TimQu
e7a8357ee6
Fixed some tests
9 years ago
TimQu
576f92568e
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.
9 years ago
dehnert
f0f4cd7390
first version of sparse quotient extraction for dd bisimulation
9 years ago
TimQu
8dfa141a4a
Exporting .dot for explicit input.
removed duplicated code for explicit input with parametric engine
9 years ago
TimQu
77a90184e7
building choice labeling when the corresponding option is given
9 years ago
TimQu
dc079b3196
moved a function to graph.h
9 years ago
TimQu
bf97d79573
moved building the choice origin strings into the ChoiceOrigins class
9 years ago
TimQu
db31c1cb11
improved .dot export of models with choice labeling
9 years ago
TimQu
6537fd8b72
Replaced the old choice labeling with the new one and used choice origins for the minimal command set counterexample generators
9 years ago
TimQu
759e351e95
Improved explicit model building:
- There is now an option to generate a choice labeling that corresponds to the specified action names.
- The old choice labeling (where each choice was labeled with an index set representing the corresponding prism commands) is renamed to choiceOrigins and has been improved towards support of other input formats (such as Jani) and other applications such as scheduler synthesis
9 years ago
TimQu
25074b50a9
Added function to get the next unset bit in a bitvector
9 years ago
TimQu
4413afb542
used new helper functions at some points in the code
9 years ago