Tim Quatmann
|
f4a3ceb60e
|
Skipping tests that fail for z3 version 4.8.8 (Issue reported at https://github.com/Z3Prover/z3/issues/4465)
|
5 years ago |
|
Tim Quatmann
|
eeeb3df4f8
|
Added some tests for BeliefExplorationPomdpModelChecker and made the testing more sensible towards very imprecise results
|
5 years ago |
|
Tim Quatmann
|
31c39d1dc7
|
storm-pomdp: Cleaned up output of belief exploration. Use --verbose to restore it.
|
5 years ago |
|
Tim Quatmann
|
08f82d44f1
|
Renamed ApproximatePOMDPModelchecker to BeliefExplorationPomdpModelChecker
|
5 years ago |
|
Tim Quatmann
|
67bcafe5e1
|
storm-pomdp: Cleaned up includes of BeliefManager and BeliefMdpExplorer.
|
5 years ago |
|
Tim Quatmann
|
073d2affa4
|
api/verification: Added a missing include
|
5 years ago |
Alexander Bork
|
74c2f83110
|
Separated header and logic for struct in BeliefMdpExplorer
|
5 years ago |
|
Alexander Bork
|
1cce958e12
|
Separated header and logic for BeliefMdpExplorer
|
5 years ago |
|
Alexander Bork
|
8b7ab24d66
|
Moved struct functions to cpp-file
|
5 years ago |
|
Alexander Bork
|
4f61ab422e
|
Separated BeliefManager header and logic
|
5 years ago |
|
Tim Quatmann
|
4f5d54c310
|
Fixed error message.
|
5 years ago |
|
Tim Quatmann
|
202c25c3db
|
Added first working test case
|
5 years ago |
|
Tim Quatmann
|
5aa3610f2e
|
Model building: Set automatically building choice labels and origins within the BuilderOptions (previously, this was done in the cli code)
|
5 years ago |
|
Tim Quatmann
|
e9ab8e65d4
|
model building: Fixed correctly setting the number of reserved bits for unbounded state variables from the cli option
|
5 years ago |
|
Tim Quatmann
|
ae9360af03
|
Use the new MakeStateSetObservationClosed transformer for the belief-exploration based pomdp model checker
|
5 years ago |
|
Tim Quatmann
|
8c38333dd1
|
Added transformer that can make a given set of states (e.g. goal states) observation closed.
|
5 years ago |
|
Tim Quatmann
|
764b6c9a3b
|
Added small pomdp example.
|
5 years ago |
|
Tim Quatmann
|
c7d167fda3
|
Delete accidentally pushed makefiles.
|
5 years ago |
|
Tim Quatmann
|
c788ec430d
|
First version of test frame work for belief exploration.
|
5 years ago |
|
Tim Quatmann
|
cd4ad03f37
|
Added output 'DEBUG BUILD' in case storm is running in debug mode.
|
5 years ago |
|
Tim Quatmann
|
55c71a8297
|
Updated .gitignore to recent changes
|
5 years ago |
|
Tim Quatmann
|
70d10bd037
|
Moved generated file `storm-version.cpp` to build folder. Moved version information to new library `storm-version-info` (addressing Github issue #78)
|
5 years ago |
Sebastian Junges
|
c9ef222a7f
|
somewhat improved counting of winning region sizes
|
5 years ago |
|
Sebastian Junges
|
3a206784a3
|
better logging
|
5 years ago |
|
Tim Quatmann
|
ad39b23c1c
|
StateValuations: Added class to conveniently iterate over the variable-value assignments of a given state
|
5 years ago |
|
Sebastian Junges
|
a7b6e00e88
|
builderoptions no longer implicitly takes settings from buildersettings
|
5 years ago |
|
Sebastian Junges
|
d71e70da42
|
build-all-labels for building all labels without building everything, and renamed build-overlapping-guards-label and build-out-of-bounds-state
|
5 years ago |
|
Sebastian Junges
|
c4c680438f
|
fix exporting POMDPs with rewards & observations
|
6 years ago |
|
Sebastian Junges
|
9d35eab33e
|
fix warning regarding hash
|
6 years ago |
|
Sebastian Junges
|
390a2ada04
|
remove test file that should not have been committed
|
6 years ago |
|
Tim Quatmann
|
5b103579f2
|
Fixed building state valuations for transient variables of a jani model.
|
6 years ago |
|
Sebastian Junges
|
34a226a582
|
more mature storing and loading of winning regions
|
6 years ago |
|
Sebastian Junges
|
0eec9e56da
|
better error message when a colon cannot be found in the drn file
|
6 years ago |
|
Sebastian Junges
|
65fab09931
|
comments in the model are now also allowed
|
6 years ago |
|
Sebastian Junges
|
e2b0855208
|
hashing POMDPs
|
6 years ago |
|
Sebastian Junges
|
009a60df5c
|
fix in hash computation
|
6 years ago |
Jan Erik Karuc
|
48a3b5a927
|
Optimizing original OVI & Switch for comparing minswap methods
|
6 years ago |
|
Jan Erik Karuc
|
bff888a97e
|
Renaming min upper aux method setting
|
6 years ago |
|
Jan Erik Karuc
|
6cfb2be36d
|
Preparation for minimum upper and aux benchmarking
This temporary option has not yet been implemented in OVI
|
6 years ago |
|
Tim Quatmann
|
90ade051c2
|
Added CMAKE option STORM_LOAD_QVBS to automatically download the quantitative verification benchmark set
|
6 years ago |
|
Sebastian Junges
|
a07f6068af
|
fixed some strange bug ( why did it even work? ) in counterexample generation for upper-bounded probabilities
|
6 years ago |
|
Sebastian Junges
|
2fa2ea1283
|
a first version of sparse model hashing
|
6 years ago |
|
Sebastian Junges
|
d1b34e3572
|
changelog updated with storm-pomdp change
|
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
|
8f9e81f61f
|
less means less or equal in cmake. :/
|
6 years ago |
|
Sebastian Junges
|
ec7198bf07
|
xerces-c macos fix for version 3.2.3 and newer
|
6 years ago |
|
Sebastian Junges
|
1658b98a26
|
report xerces-c version
|
6 years ago |
|
Tim Quatmann
|
574cb1918d
|
Merge remote-tracking branch 'refs/remotes/origin/master'
|
6 years ago |
|
Tim Quatmann
|
9981df3f92
|
Z3LpSolver: Removed exception that was thrown by accident.
|
6 years ago |
|
Sebastian Junges
|
4bcb541866
|
pmc simplifications are disabled by default, can be switched on via option
|
6 years ago |
