ArashPartow
2cdda140b8
Minor updates to ExprTk
Updated multi-sub expression operator to return final sub-expression type.
Updates to exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level.
9 years ago
TimQu
de87ff1152
fixed finding of z3 library when its location is given via -DZ3_ROOT
9 years ago
TimQu
f59e9a7f77
added flushing of cout in STORM_PRINT macro
9 years ago
TimQu
367b8f0a3e
parameter lifting with hybrid engine
9 years ago
TimQu
bb3c2bd556
Implemented policy iteration for game solver
9 years ago
Matthias Volk
0d9205c0e6
Fixed case in include path
9 years ago
Matthias Volk
00c210565b
Merge from dft_case_study
9 years ago
TimQu
e05672a87d
Merge branch 'master' into refactor_pla
9 years ago
TimQu
936293e318
Refactored GameSolver. It is now analogous to the MinMaxLinearEquationSolver.
9 years ago
TimQu
77e71b7876
capitalization error and fix for cumulative rewards
9 years ago
sjunges
c16390e7f5
Equality Comparisons for JaniVars, just to make life easier :-)
10 years ago
TimQu
3eb675f8c0
used helper methods instead of own implementations
9 years ago
TimQu
502cf4d6e0
extended model checker hint functionality to bypass the maybestates computations
9 years ago
dehnert
becc43e1e1
added wokaround proposed by jklein to make the new sylvan version build on older osx
9 years ago
JK
60ab1716b1
storm: bisimulation statistics
10 years ago
JK
e536851e53
Solver: provide information about solving method + number of iterations at INFO log level
9 years ago
TimQu
cb0d05c947
Merge branch 'master' into refactor_pla
9 years ago
TimQu
170105c261
Fixed "division by zero" error that occurred when considering a CTMC with state rewards but without action rewards
9 years ago
TimQu
9425d3506e
reworked checking whether parameter lifting is applicable
9 years ago
TimQu
cf340bed52
cleaned up some utility functions
9 years ago
TimQu
575210ae69
Merge branch 'master' into refactor_pla
9 years ago
TimQu
d5d0a5f44a
fixed a few issues related to having CLN numbers as storm::RationalNumber
9 years ago
TimQu
9ba2f90483
started to implement a validation that checks whether parameter lifting is sound
9 years ago
TimQu
36976f0607
temporarily fixed exact validation to make things compile again
9 years ago
TimQu
0464a248a4
Merge branch 'master' into refactor_pla
9 years ago
TimQu
48d5025bd9
Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas).
9 years ago
TimQu
c5c14f3178
extended JSONExporter to properly export non-constant time/step intervals
9 years ago
TimQu
f0ae3a2dfb
Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N
9 years ago
TimQu
cde59bd436
added Expression::evaluateAsRational
9 years ago
dehnert
2f3b090a51
Merge remote-tracking branch 'origin/master' into symbolic_state_elimination
9 years ago
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
9 years ago
Tom Janson
ee510df4ec
add Path stream print for debug / Python __str__
10 years ago
TimQu
3a09a378fc
Merge branch 'master' into refactor_pla
9 years ago
TimQu
457943351d
fixed matrix building in ModelInstantiator for deterministic models. Previously, a non-trivial row grouping was introduced.
9 years ago
TimQu
dd40254628
PLA for continuous models
9 years ago
dehnert
b811ebcf88
dd-based policy iteration appears to be working
9 years ago
dehnert
f6e194592f
remove always building sylvan
9 years ago
dehnert
0135793c44
update to newest sylvan version
9 years ago
dehnert
153339c5be
first draft of policy iteration using DDs
9 years ago
dehnert
952776a057
hybrid engine working for rational numbers
9 years ago
dehnert
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
9 years ago
dehnert
aaa6f13cf4
separated rational numbers and rational functions and added support for rational numbers to sylvan
9 years ago
TimQu
e877711910
Merge branch 'master' into refactor_pla
9 years ago
TimQu
44ab16d126
Added symbolicToSparse transformers for DTMCs and CTMCs
9 years ago
TimQu
64c37d4da1
minor fixes for exact validation in parameter lifting
9 years ago
TimQu
7f74f19342
exact pla
9 years ago
TimQu
3ece3317d5
template instantiation of game solver with rationals
9 years ago
dehnert
acd486f0f2
reverted a change in ExprTk: dots are no longer recognized as letters
10 years ago
TimQu
08ccef885a
pla minor cli improvements..
10 years ago
dehnert
82cc586718
fixed some issues related to assigning an initializer list to an unordered_map which causes problems on older platforms
10 years ago