ArashPartow
4c99790213
Minor updates to ExprTk
Updated unknown symbol resolver interface to handle all types (scalar, string and vector)
Added compile-time check for vector indexing when using constant values
Added return statement enable/disable via parser settings
Added exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level.
10 years ago
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.
10 years ago
Matthias Volk
0d9205c0e6
Fixed case in include path
10 years ago
Matthias Volk
00c210565b
Merge from dft_case_study
10 years ago
dehnert
becc43e1e1
added wokaround proposed by jklein to make the new sylvan version build on older osx
10 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
10 years ago
TimQu
170105c261
Fixed "division by zero" error that occurred when considering a CTMC with state rewards but without action rewards
10 years ago
TimQu
d5d0a5f44a
fixed a few issues related to having CLN numbers as storm::RationalNumber
10 years ago
TimQu
48d5025bd9
Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas).
10 years ago
TimQu
c5c14f3178
extended JSONExporter to properly export non-constant time/step intervals
10 years ago
TimQu
f0ae3a2dfb
Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N
10 years ago
TimQu
cde59bd436
added Expression::evaluateAsRational
10 years ago
dehnert
2f3b090a51
Merge remote-tracking branch 'origin/master' into symbolic_state_elimination
10 years ago
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
10 years ago
Tom Janson
ee510df4ec
add Path stream print for debug / Python __str__
10 years ago
TimQu
457943351d
fixed matrix building in ModelInstantiator for deterministic models. Previously, a non-trivial row grouping was introduced.
10 years ago
dehnert
b811ebcf88
dd-based policy iteration appears to be working
10 years ago
dehnert
f6e194592f
remove always building sylvan
10 years ago
dehnert
0135793c44
update to newest sylvan version
10 years ago
dehnert
153339c5be
first draft of policy iteration using DDs
10 years ago
dehnert
952776a057
hybrid engine working for rational numbers
10 years ago
dehnert
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
10 years ago
dehnert
aaa6f13cf4
separated rational numbers and rational functions and added support for rational numbers to sylvan
10 years ago
TimQu
44ab16d126
Added symbolicToSparse transformers for DTMCs and CTMCs
10 years ago
dehnert
acd486f0f2
reverted a change in ExprTk: dots are no longer recognized as letters
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
dehnert
0354c9024a
moved to new sylvan version and made everything work again
10 years ago
dehnert
2e8ff870ff
completed interface of (sylvan) ADDs for storing rational functions
10 years ago
TimQu
95527421bf
added missing parenthesis
10 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.
10 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)
10 years ago
dehnert
fd74476340
forgot to commit header file
10 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
10 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
10 years ago
Matthias Volk
0a06a2b33e
Fix in constructing pseudo state
10 years ago
Matthias Volk
fd2f83fe6d
Consider ingoing dependencies for symmetry
10 years ago
Matthias Volk
9b567608f3
Find symmetries for BEs as well
10 years ago
Matthias Volk
affa7db555
Depth heuristic did not skip
10 years ago
dehnert
ad1fdd41ea
fixed some wrong capitalizations
10 years ago
dehnert
44dc3e7d8d
fixed version output in cmake
10 years ago
dehnert
97b33cf8b1
changed version output slightly
10 years ago
Matthias Volk
8cbfccba22
Hacked approximation for probabilities
10 years ago
dehnert
98d956275a
reworked version detection via git/defaults if not available
10 years ago
dehnert
a323d21751
fixed some wrong capitalization
10 years ago
Matthias Volk
ac8cea1e53
Added transient BEs
10 years ago
dehnert
3f0afe9526
allowing underscore and dots as identifier symbols in exprtk
10 years ago
Matthias Volk
c26237c16f
Export Dft headers for stormpy
10 years ago
Matthias Volk
d813851897
Small fix
10 years ago
Matthias Volk
de568c792a
Merge branch 'master' into dft_case_study
10 years ago