Tim Quatmann
|
9f1487392e
|
We now avoid the renaming of 'Eigen' to 'StormEigen' as this is (hopefully) not needed anymore.
|
5 years ago |
|
Tim Quatmann
|
dd7dc4b797
|
Towards allowing CLN numbers for RationalNumbers again.
|
5 years ago |
|
Tim Quatmann
|
e560c7f57c
|
Added some INFO output to check why there is no refinement fixpoint.
|
5 years ago |
|
Tim Quatmann
|
ee350ca384
|
Use same precision as BeliefValueType when dealing with triangulation resolutions.
|
5 years ago |
|
Tim Quatmann
|
92aa029bc5
|
Removed debug output
|
5 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
|
5 years ago |
|
Tim Quatmann
|
2f2a007896
|
Implemented 'guessing' of initial pomdp schedulers for multiple guesses
|
5 years ago |
|
Tim Quatmann
|
2500cc0cd2
|
Fixed computation of relative gap for special cases (in particular l=u=0)
|
5 years ago |
Matthias Volk
|
a95f65cc27
|
Explicit fall-through
|
5 years ago |
|
Matthias Volk
|
ac9fc7b99c
|
Fixed permutations for more than 32 bits by using correct bit-shift
|
5 years ago |
|
Matthias Volk
|
121b082139
|
Added missing break; statements
|
5 years ago |
|
Matthias Volk
|
c039b817ef
|
Removed unused variable + dependent code
|
5 years ago |
|
Matthias Volk
|
6355e07a0c
|
Fix fall-through by using assert
|
5 years ago |
|
Tim Quatmann
|
896d409602
|
Implemented simple (but incomplete) check to display whether the belief MDP is finite.
|
5 years ago |
|
Tim Quatmann
|
1766bc385e
|
POMDP Approximation: Use relative gap
|
5 years ago |
|
Tim Quatmann
|
fcbce6052c
|
Fixed getting invalid bounds if we abort during the initial approximation step.
|
5 years ago |
|
Tim Quatmann
|
2ebb5e8383
|
Fixed detection of fixpoints.
|
5 years ago |
|
Tim Quatmann
|
703bdc4eb9
|
Changed strategy of the dynamic triangulation approach such that the number of "missed" probabilities is minimized
|
5 years ago |
|
Tim Quatmann
|
71c410a3be
|
Added settings to switch between different triangulation modes.
|
5 years ago |
|
Tim Quatmann
|
fa10087fba
|
Implemented triangulation in a more dynamic way.
|
5 years ago |
|
Tim Quatmann
|
cc5faee9c0
|
Fixed initial size threshold for over-approx.
|
5 years ago |
|
Tim Quatmann
|
2ac1c73076
|
Change default initial resolution to 3
|
5 years ago |
|
Tim Quatmann
|
ab95e7d08b
|
BeliefManager: organized stored beliefs in buckets (beliefs with the same observation belong in the same bucket)
|
5 years ago |
Sebastian Junges
|
0a5717aee7
|
lowlevel storing/loading bitvectors from a string (without any error handling, that is). Helpful to store bitvecots in python
|
5 years ago |
|
Sebastian Junges
|
356eb0b3b1
|
fix debugging assistance code that is no longer valid when you compute multiple counterexamples
|
5 years ago |
Daniel Basgöze
|
93e7bac668
|
Fix bitshift overflow
|
5 years ago |
|
Tim Quatmann
|
6f476ef079
|
belief exploration: Improved fixpoint detection for over-approx
|
5 years ago |
|
Tim Quatmann
|
ddec9ce740
|
ApproximatePomdpModelchecker: Fixed output a little.
|
5 years ago |
|
Matthias Volk
|
06941e7c48
|
Setting 'dft-statistics' prints information about intermediate approximation results
|
5 years ago |
|
Matthias Volk
|
a61ea32aea
|
Fixed some GCC warnings
|
5 years ago |
|
Matthias Volk
|
d3c8093e0f
|
Removed unnecessary semicolons
|
5 years ago |
|
Tim Quatmann
|
5a221acbd0
|
Multi-objective model checking: Fixed incorrect computations for some models with end components. (Github Issue #75)
|
5 years ago |
|
Tim Quatmann
|
08c60bcb3d
|
Added OVISolverSettings to storm-pomdp
|
5 years ago |
|
TimQu
|
7504f6f315
|
Improved statistics output for refinements, added detection of fixpoints
|
5 years ago |
|
Tim Quatmann
|
5a76f7355d
|
Fixed an issue with refinement of under-approximation
|
5 years ago |
|
Tim Quatmann
|
16ad9d3a83
|
fixed storm-pomdp output a little.
|
5 years ago |
|
Tim Quatmann
|
4eed592811
|
--timeout now just sends a SIGALRM signal (which can be catched by the signal handler).
|
5 years ago |
|
Tim Quatmann
|
8b4595042e
|
Only do iteration output if the result bound improved. Handle integer overflows for the observation resolution.
|
5 years ago |
|
Tim Quatmann
|
43220759f4
|
Implemented a time limit for exploration.
|
5 years ago |
|
Tim Quatmann
|
e81b8f1622
|
BeliefManager: fixed a few assertion conditions
|
5 years ago |
|
Tim Quatmann
|
c91c98f2de
|
Pomdp: Fixing result output with exact numbers
|
5 years ago |
|
Tim Quatmann
|
1763f0c582
|
Making sure that we only store the best bounds found so far. Also added some output for the resulting values in each iteration.
|
5 years ago |
|
Tim Quatmann
|
fa624d2a20
|
Introduced new settings for controlling the refinement strategy and whether to produce only upper and/or lower bounds
|
5 years ago |
|
Tim Quatmann
|
2d94e77f2a
|
Only display the bound that was requested.
|
5 years ago |
|
Tim Quatmann
|
6dd50575f9
|
New 'belief-exploration' setting (replaces gridapproximation setting)
|
5 years ago |
|
Tim Quatmann
|
37490a8eca
|
Started to integrate new refinement options.
|
5 years ago |
|
Tim Quatmann
|
a728c01322
|
BitVector: Fixed an issue with the move assignment operator. The 'other' BitVector was left in an invalid state.
|
5 years ago |
|
Tim Quatmann
|
75d792e987
|
Implemented refinement heuristic.
|
5 years ago |
|
Tim Quatmann
|
45832d3de3
|
BeliefMdpExplorer: Implemented extraction of optimal scheduler choices and reachable states under these choices
|
5 years ago |
|
Tim Quatmann
|
61215e4b24
|
Over-Approximation: Taking current values as new lower/upper bounds for next refinement step.
|
5 years ago |
