Tim Quatmann
|
adfdf8c572
|
Refactored state valuations. They now store values for transient jani variables and do not store values for constants (solving Github issue #73)
|
6 years ago |
|
Tim Quatmann
|
3a86cc4391
|
CompressedState: Added a method to create a human readable string out of the state. Added a method to "uncompress" by extracting all values into corresponding value vectors
|
6 years ago |
|
Tim Quatmann
|
5733072898
|
TransientVariableInformation: Flagging a few getters const
|
6 years ago |
|
Tim Quatmann
|
ab93422fa0
|
Changed default dd library from `cudd` to `sylvan` (cf. Github issue #71)
|
6 years ago |
Sebastian Junges
|
cdfbe8d4bb
|
from pomdp to pmc now preserves state valuations
|
6 years ago |
|
Sebastian Junges
|
55b344c560
|
but state valuations as comments into drn
|
6 years ago |
|
Sebastian Junges
|
f23efb9eb2
|
split pomdp settings into toparametric settings for the UAI18 stuff
|
6 years ago |
|
Sebastian Junges
|
669ffc52d2
|
reworked the interface to qualitative analysis of POMDPs
|
6 years ago |
|
Sebastian Junges
|
a90a82d271
|
better performance when only looking for a winning policy
|
6 years ago |
|
Sebastian Junges
|
498067816d
|
fix stupid mistake that made subsequent searches mostly unsat by setting scheduler var to wrong value
|
6 years ago |
|
Sebastian Junges
|
53800c2145
|
major improvements by introducing real-valued ranking and various related fixes
|
6 years ago |
|
Sebastian Junges
|
34fce002cb
|
compute size of winning region
|
6 years ago |
|
Sebastian Junges
|
eca148cee0
|
graph-based analysis improved, and cleaning outputs
|
6 years ago |
|
Sebastian Junges
|
a7f05847ac
|
better info message if an engine does not support a model
|
6 years ago |
|
Sebastian Junges
|
2de8c94fd9
|
flatsets to string
|
6 years ago |
|
Sebastian Junges
|
08cb25c28c
|
to be sure: z3model by const reference
|
6 years ago |
|
Sebastian Junges
|
c2f5eb9ce0
|
do not export reward model if we find a counterexample for a probability property
|
6 years ago |
|
Sebastian Junges
|
5937a764b8
|
debug output now only appears with log level
|
6 years ago |
|
Sebastian Junges
|
22c644b42c
|
more trace messages in counterexample generation
|
6 years ago |
|
Sebastian Junges
|
235f335579
|
typo
|
6 years ago |
|
Tim Quatmann
|
890dca30cf
|
Nativepolytope: When intersecting, check easy cases where one of the polytopes are universal first. This also prevents that an internal Eigen assertion is raised in cases where an empty and a non-empty matrix are concatenated (somehow only relevant for gcc 9.3 in debug mode...).
|
6 years ago |
|
Tim Quatmann
|
ae2b63ca07
|
Eigenadapter: changed Returntype of digits10 to match the NumTraits interface
|
6 years ago |
|
Tim Quatmann
|
47ac26eb02
|
JaniScopeChanger: Fixed segfault and incorrect detection for variable accesses (GitHub issue #70)
|
6 years ago |
|
Tim Quatmann
|
aae44a3b4b
|
Fixed error message that appeared when using jit.
|
6 years ago |
Matthias Volk
|
c09c31be6a
|
Enable pragmas in eigen.h only for GCC 9
|
6 years ago |
|
Matthias Volk
|
7b6101c220
|
Updated list of ignored warnings for Eigen
|
6 years ago |
|
Tim Quatmann
|
ee0e90462f
|
Fixed incorrect result of canHandleStatic for multi-objective formulas for MDP in hybrid engine and MA in sparse engine.
|
6 years ago |
|
Tim Quatmann
|
74f7cd17ea
|
Changed the target directory for the downloaded Eigen headers so that they are now located within the build folder (hopefully avoiding conflicts with multiple build-folders).
Made the include path for the Eigen headers more unique, so we no longer use the headers at /urs/include/ instead.
|
6 years ago |
|
Tim Quatmann
|
9f1487392e
|
We now avoid the renaming of 'Eigen' to 'StormEigen' as this is (hopefully) not needed anymore.
|
6 years ago |
|
Tim Quatmann
|
dd7dc4b797
|
Towards allowing CLN numbers for RationalNumbers again.
|
6 years ago |
|
Tim Quatmann
|
e560c7f57c
|
Added some INFO output to check why there is no refinement fixpoint.
|
6 years ago |
|
Tim Quatmann
|
ee350ca384
|
Use same precision as BeliefValueType when dealing with triangulation resolutions.
|
6 years ago |
|
Tim Quatmann
|
92aa029bc5
|
Removed debug output
|
6 years ago |
|
Tim Quatmann
|
55c4408c6a
|
Storing the observation resolutions as a float so that we can increase the resolution more accurately with a non-integer factor
|
6 years ago |
|
Tim Quatmann
|
2f2a007896
|
Implemented 'guessing' of initial pomdp schedulers for multiple guesses
|
6 years ago |
|
Sebastian Junges
|
005e23d5d5
|
two fixes after encoding from non-empty winning regions
|
6 years ago |
|
Sebastian Junges
|
972332810b
|
cosmetic changes, better output, some assertions
|
6 years ago |
|
Sebastian Junges
|
556a884e74
|
use target state to initialise winning region, better timers and slight improvements in partial scheduler extension
|
6 years ago |
|
Sebastian Junges
|
f00a208e9c
|
validate whether a winning region is maximal
|
6 years ago |
|
Sebastian Junges
|
d3c593fe74
|
set validation level from command line
|
6 years ago |
|
Sebastian Junges
|
a1f50253d9
|
compact output of winning region
|
6 years ago |
|
Tim Quatmann
|
2500cc0cd2
|
Fixed computation of relative gap for special cases (in particular l=u=0)
|
6 years ago |
|
Matthias Volk
|
a95f65cc27
|
Explicit fall-through
|
6 years ago |
|
Matthias Volk
|
ac9fc7b99c
|
Fixed permutations for more than 32 bits by using correct bit-shift
|
6 years ago |
|
Matthias Volk
|
121b082139
|
Added missing break; statements
|
6 years ago |
|
Matthias Volk
|
c039b817ef
|
Removed unused variable + dependent code
|
6 years ago |
|
Matthias Volk
|
6355e07a0c
|
Fix fall-through by using assert
|
6 years ago |
|
Tim Quatmann
|
896d409602
|
Implemented simple (but incomplete) check to display whether the belief MDP is finite.
|
6 years ago |
|
Tim Quatmann
|
1766bc385e
|
POMDP Approximation: Use relative gap
|
6 years ago |
|
Tim Quatmann
|
fcbce6052c
|
Fixed getting invalid bounds if we abort during the initial approximation step.
|
6 years ago |
