Alexander Bork
|
877c15ed43
|
Removed obsolete function to create transition matrices from a data structure not used anymore
|
6 years ago |
|
Alexander Bork
|
b7b213571d
|
Refactoring of underapproximation procedures to reduce code duplication
|
6 years ago |
|
Alexander Bork
|
8f81958268
|
Refactoring of reachability reward and probability methods to reduce code duplication
|
6 years ago |
|
Alexander Bork
|
4664b4244b
|
Refactoring of on-the-fly computation to reduce code duplication
|
6 years ago |
|
Alexander Bork
|
c6902e0ca7
|
Added reward MDP generation for the overapproximation
|
6 years ago |
|
Alexander Bork
|
c663edbd85
|
Added generation of an MDP for the over-approximation in the on-the-fly state exploration
|
6 years ago |
|
Alexander Bork
|
bbd3ec7287
|
Fix of wrong MDP underapproximation
|
6 years ago |
|
Alexander Bork
|
b9c0af6628
|
Added on-the-fly belief grid generation for rewards
|
6 years ago |
|
Alexander Bork
|
21e417bdac
|
Added on-the-fly belief grid generation to avoid computations for unreachable beliefs
|
6 years ago |
|
Alexander Bork
|
bc52aa86ca
|
Added procedure to repeat probability computation with higher resolution
|
6 years ago |
|
Alexander Bork
|
a65c445243
|
Avoid multiple computation of size in subsimplex computation
|
6 years ago |
|
Alexander Bork
|
7afc47f354
|
Fixed wrong size of stateLabeling if no probability 0 states were found
|
6 years ago |
|
Alexander Bork
|
11f89de9e8
|
Added preprocessing to reduce the POMDP state space before analysis
|
6 years ago |
|
Alexander Bork
|
4b8664c521
|
Added reward under-approximation
|
6 years ago |
|
Alexander Bork
|
f119e3d4c7
|
Added reward over-approximation
|
6 years ago |
|
Alexander Bork
|
4c8395c3b1
|
Speedup of probability approximation
|
6 years ago |
|
Alexander Bork
|
f6d9a6ac02
|
Changed datatype used in POMDP analysis from RationalNumber to double for better comparision of approximation speeds with PRISM
|
6 years ago |
|
Alexander Bork
|
5de96cc170
|
Modified implementation to speed up the subsimplex computation
|
6 years ago |
|
Alexander Bork
|
959a2c2400
|
Added ability to use an MDP for the underapproximation
|
6 years ago |
|
Alexander Bork
|
3bd910f42b
|
Added timing and caching of subsimplex computation results
|
6 years ago |
|
Alexander Bork
|
d814942997
|
Working version of under-approximation
|
6 years ago |
|
Alexander Bork
|
2bc79e6e07
|
Refactoring to include a list of all generated beliefs
|
6 years ago |
|
Alexander Bork
|
74cfecd011
|
Working version of over-approximation
|
6 years ago |
|
Alexander Bork
|
7f9ad39d34
|
First version for the over-approximation of POMDP reachability
|
6 years ago |
Matthias Volk
|
56a206ea5c
|
Fixed segfaults in reward parsing of DRN
|
6 years ago |
|
Matthias Volk
|
628219298e
|
Some small cleanup in verification API
|
6 years ago |
|
Matthias Volk
|
d39189c0e2
|
Scheduler extraction for MA properties which can be reduced to MDP queries
|
6 years ago |
|
Matthias Volk
|
cdaea9ea55
|
Small fix in DRNParser
|
6 years ago |
|
Matthias Volk
|
39cedc223e
|
Use ValueParsen in DFTJsonParser
|
6 years ago |
|
Matthias Volk
|
fba3223f63
|
Use typedefs of RationalFunctionAdapter
|
6 years ago |
|
Matthias Volk
|
30565e4d0c
|
Use carl hashing functions
|
6 years ago |
Tim Quatmann
|
2433671b7d
|
Changelog update
|
6 years ago |
|
Tim Quatmann
|
d4ee19c350
|
Merge branch 'lra-strategies'
|
6 years ago |
|
Tim Quatmann
|
42b7865e7e
|
DirectEncodingParser: Added support for Action-based rewards.
|
6 years ago |
|
Tim Quatmann
|
429c91ff13
|
Added support for parsing fractions in DRN files.
|
6 years ago |
|
Tim Quatmann
|
b896726c4a
|
Include choice labels in exported scheduler.
|
6 years ago |
|
Tim Quatmann
|
a47945a931
|
Cleaner output when exporting schedulers
|
6 years ago |
|
Tim Quatmann
|
8a23197a77
|
Fix for LRA scheduler generation.
|
6 years ago |
|
Tim Quatmann
|
72425ec1b2
|
CLI: Added an option to export the produced scheduler to a file.
|
6 years ago |
|
Tim Quatmann
|
009cee1c25
|
Implemented scheduler extraction for LRA properties for MDP.
|
6 years ago |
|
Tim Quatmann
|
c1b3a4f991
|
LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase.
|
6 years ago |
|
Tim Quatmann
|
48dbaa6fbd
|
Fixed a test
|
6 years ago |
|
Tim Quatmann
|
16aee7c386
|
fixed a typo
|
6 years ago |
|
Matthias Volk
|
9e63a89db7
|
Fixed operator precedence for power and modulo operator thanks to help from Joachim Klein.
|
6 years ago |
|
Matthias Volk
|
d05b132dde
|
Better error output
|
6 years ago |
|
Tim Quatmann
|
900da9e556
|
Fixed EndComponentEliminatorTest
|
6 years ago |
|
Tim Quatmann
|
2cb7b5769e
|
Jit: Fixed issues when CLN and/or GMP is installed via carl
|
6 years ago |
|
Tim Quatmann
|
b1b429e8d2
|
EndComponentEliminatorTest: Made the test more stable with respect to different orders in the result.
|
6 years ago |
|
Tim Quatmann
|
492348542f
|
SubsystemBuilder: Fix deadlocks with a selfloop (if requested)
|
6 years ago |
|
Tim Quatmann
|
0b1b0d97e2
|
utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set.
|
6 years ago |
