Tim Quatmann
|
67bcafe5e1
|
storm-pomdp: Cleaned up includes of BeliefManager and BeliefMdpExplorer.
|
6 years ago |
Alexander Bork
|
74c2f83110
|
Separated header and logic for struct in BeliefMdpExplorer
|
6 years ago |
|
Alexander Bork
|
1cce958e12
|
Separated header and logic for BeliefMdpExplorer
|
6 years ago |
|
Alexander Bork
|
8b7ab24d66
|
Moved struct functions to cpp-file
|
6 years ago |
|
Alexander Bork
|
4f61ab422e
|
Separated BeliefManager header and logic
|
6 years ago |
|
Tim Quatmann
|
4f5d54c310
|
Fixed error message.
|
6 years ago |
|
Tim Quatmann
|
ae9360af03
|
Use the new MakeStateSetObservationClosed transformer for the belief-exploration based pomdp model checker
|
6 years ago |
|
Tim Quatmann
|
8c38333dd1
|
Added transformer that can make a given set of states (e.g. goal states) observation closed.
|
6 years ago |
Sebastian Junges
|
c9ef222a7f
|
somewhat improved counting of winning region sizes
|
6 years ago |
|
Sebastian Junges
|
3a206784a3
|
better logging
|
6 years ago |
|
Sebastian Junges
|
34a226a582
|
more mature storing and loading of winning regions
|
6 years ago |
|
Sebastian Junges
|
4942e362db
|
transformation preserve canonicity, and this is now set explicitly. (Opt-out rather than opt-in might be more convenient, but also more dangerous...)
|
6 years ago |
|
Sebastian Junges
|
cdfbe8d4bb
|
from pomdp to pmc now preserves state valuations
|
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 |
|
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 |
|
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 |
|
Tim Quatmann
|
2ebb5e8383
|
Fixed detection of fixpoints.
|
6 years ago |
|
Tim Quatmann
|
703bdc4eb9
|
Changed strategy of the dynamic triangulation approach such that the number of "missed" probabilities is minimized
|
6 years ago |
|
Tim Quatmann
|
fa10087fba
|
Implemented triangulation in a more dynamic way.
|
6 years ago |
|
Tim Quatmann
|
cc5faee9c0
|
Fixed initial size threshold for over-approx.
|
6 years ago |
|
Tim Quatmann
|
ab95e7d08b
|
BeliefManager: organized stored beliefs in buckets (beliefs with the same observation belong in the same bucket)
|
6 years ago |
|
Sebastian Junges
|
e9e9b15cb1
|
store/load winning region to file
|
6 years ago |
|
Sebastian Junges
|
b2e7c5d5ed
|
various changes to allow restarting and more finegrained selection of switch-and-finish-with-policy
|
6 years ago |
|
Sebastian Junges
|
43bb70e93d
|
bugfix where the wrong successor variables where selected
|
6 years ago |
|
Sebastian Junges
|
5783719c05
|
add a validator to the winning region search
|
6 years ago |
|
Tim Quatmann
|
6f476ef079
|
belief exploration: Improved fixpoint detection for over-approx
|
6 years ago |
|
Tim Quatmann
|
ddec9ce740
|
ApproximatePomdpModelchecker: Fixed output a little.
|
6 years ago |
Matthias Volk
|
d3c8093e0f
|
Removed unnecessary semicolons
|
6 years ago |
|
Sebastian Junges
|
c0ac9814e1
|
allow for graph-analysis and sat-based analysis interleaving, and restarting sat-based solver when advantageous
|
6 years ago |
|
Sebastian Junges
|
ea73e246a7
|
A new qualitative reachability analysis for POMDPs/prob1max, based on graphs (sound but incomplete).
|
6 years ago |
|
TimQu
|
7504f6f315
|
Improved statistics output for refinements, added detection of fixpoints
|
6 years ago |
|
Tim Quatmann
|
5a76f7355d
|
Fixed an issue with refinement of under-approximation
|
6 years ago |
