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.
8 years ago
Matthias Volk
0d9205c0e6
Fixed case in include path
8 years ago
Matthias Volk
00c210565b
Merge from dft_case_study
8 years ago
dehnert
becc43e1e1
added wokaround proposed by jklein to make the new sylvan version build on older osx
8 years ago
JK
60ab1716b1
storm: bisimulation statistics
8 years ago
JK
e536851e53
Solver: provide information about solving method + number of iterations at INFO log level
8 years ago
TimQu
170105c261
Fixed "division by zero" error that occurred when considering a CTMC with state rewards but without action rewards
8 years ago
TimQu
d5d0a5f44a
fixed a few issues related to having CLN numbers as storm::RationalNumber
8 years ago
TimQu
48d5025bd9
Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas).
8 years ago
TimQu
c5c14f3178
extended JSONExporter to properly export non-constant time/step intervals
8 years ago
TimQu
f0ae3a2dfb
Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N
8 years ago
TimQu
cde59bd436
added Expression::evaluateAsRational
8 years ago
dehnert
2f3b090a51
Merge remote-tracking branch 'origin/master' into symbolic_state_elimination
8 years ago
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
8 years ago
Tom Janson
ee510df4ec
add Path stream print for debug / Python __str__
8 years ago
TimQu
457943351d
fixed matrix building in ModelInstantiator for deterministic models. Previously, a non-trivial row grouping was introduced.
8 years ago
dehnert
b811ebcf88
dd-based policy iteration appears to be working
8 years ago
dehnert
f6e194592f
remove always building sylvan
8 years ago
dehnert
0135793c44
update to newest sylvan version
8 years ago
dehnert
153339c5be
first draft of policy iteration using DDs
8 years ago
dehnert
952776a057
hybrid engine working for rational numbers
8 years ago
dehnert
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
8 years ago
dehnert
aaa6f13cf4
separated rational numbers and rational functions and added support for rational numbers to sylvan
8 years ago
TimQu
44ab16d126
Added symbolicToSparse transformers for DTMCs and CTMCs
8 years ago
dehnert
acd486f0f2
reverted a change in ExprTk: dots are no longer recognized as letters
8 years ago
dehnert
82cc586718
fixed some issues related to assigning an initializer list to an unordered_map which causes problems on older platforms
8 years ago
dehnert
0354c9024a
moved to new sylvan version and made everything work again
8 years ago
dehnert
2e8ff870ff
completed interface of (sylvan) ADDs for storing rational functions
8 years ago
TimQu
95527421bf
added missing parenthesis
8 years ago
TimQu
ad3e99f558
Fixes in step bounded DFS implementations: A state should be reexplored whenever it is reached with a shorter path. Previously, it was not possible to explore a state multiple times.
8 years ago
dehnert
1a803f4270
created symbolic native solver to factor out numerical solution; prepared the code-path that stores rational functions in DDs (hybrid + dd engines)
8 years ago
dehnert
fd74476340
forgot to commit header file
8 years ago
dehnert
fd31e23306
allow arbitrary-layer meta variables in DdManager; make DdManager available as non-const from a DD; started on symbolic state elimination linear equation solver
8 years ago
dehnert
b7170b3c3b
fixed two issues pointed out by Joachim Klein: spirit error message (superfluous tab) and wrong treatment of strict upper bounds in bounded until and cumulative reward properties
8 years ago
Matthias Volk
0a06a2b33e
Fix in constructing pseudo state
8 years ago
Matthias Volk
fd2f83fe6d
Consider ingoing dependencies for symmetry
8 years ago
Matthias Volk
9b567608f3
Find symmetries for BEs as well
8 years ago
Matthias Volk
affa7db555
Depth heuristic did not skip
8 years ago
dehnert
ad1fdd41ea
fixed some wrong capitalizations
8 years ago
dehnert
44dc3e7d8d
fixed version output in cmake
8 years ago
dehnert
97b33cf8b1
changed version output slightly
8 years ago
Matthias Volk
8cbfccba22
Hacked approximation for probabilities
8 years ago
dehnert
98d956275a
reworked version detection via git/defaults if not available
8 years ago
dehnert
a323d21751
fixed some wrong capitalization
8 years ago
Matthias Volk
ac8cea1e53
Added transient BEs
8 years ago
dehnert
3f0afe9526
allowing underscore and dots as identifier symbols in exprtk
8 years ago
Matthias Volk
c26237c16f
Export Dft headers for stormpy
8 years ago
Matthias Volk
d813851897
Small fix
8 years ago
Matthias Volk
de568c792a
Merge branch 'master' into dft_case_study
8 years ago
dehnert
b3a02b6e8a
fix in sparse ctmc model checker: bounded until returned empty result in case there are no non-prob0-states
8 years ago