Sebastian Junges
|
390a2ada04
|
remove test file that should not have been committed
|
5 years ago |
Tim Quatmann
|
5b103579f2
|
Fixed building state valuations for transient variables of a jani model.
|
5 years ago |
|
Sebastian Junges
|
34a226a582
|
more mature storing and loading of winning regions
|
5 years ago |
|
Sebastian Junges
|
0eec9e56da
|
better error message when a colon cannot be found in the drn file
|
5 years ago |
|
Sebastian Junges
|
65fab09931
|
comments in the model are now also allowed
|
5 years ago |
|
Sebastian Junges
|
e2b0855208
|
hashing POMDPs
|
5 years ago |
|
Sebastian Junges
|
009a60df5c
|
fix in hash computation
|
5 years ago |
Jan Erik Karuc
|
48a3b5a927
|
Optimizing original OVI & Switch for comparing minswap methods
|
5 years ago |
|
Jan Erik Karuc
|
bff888a97e
|
Renaming min upper aux method setting
|
5 years ago |
|
Jan Erik Karuc
|
6cfb2be36d
|
Preparation for minimum upper and aux benchmarking
This temporary option has not yet been implemented in OVI
|
5 years ago |
|
Tim Quatmann
|
90ade051c2
|
Added CMAKE option STORM_LOAD_QVBS to automatically download the quantitative verification benchmark set
|
5 years ago |
|
Sebastian Junges
|
a07f6068af
|
fixed some strange bug ( why did it even work? ) in counterexample generation for upper-bounded probabilities
|
5 years ago |
|
Sebastian Junges
|
2fa2ea1283
|
a first version of sparse model hashing
|
5 years ago |
|
Sebastian Junges
|
d1b34e3572
|
changelog updated with storm-pomdp change
|
5 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...)
|
5 years ago |
|
Sebastian Junges
|
8f9e81f61f
|
less means less or equal in cmake. :/
|
5 years ago |
|
Sebastian Junges
|
ec7198bf07
|
xerces-c macos fix for version 3.2.3 and newer
|
5 years ago |
|
Sebastian Junges
|
1658b98a26
|
report xerces-c version
|
5 years ago |
|
Tim Quatmann
|
574cb1918d
|
Merge remote-tracking branch 'refs/remotes/origin/master'
|
5 years ago |
|
Tim Quatmann
|
9981df3f92
|
Z3LpSolver: Removed exception that was thrown by accident.
|
5 years ago |
|
Sebastian Junges
|
4bcb541866
|
pmc simplifications are disabled by default, can be switched on via option
|
5 years ago |
|
Sebastian Junges
|
1a6f2e6fba
|
--io:nodrnplaceholders
|
5 years ago |
|
Sebastian Junges
|
1a2a4c1a8e
|
Merge branch 'master' into almostsurepomdp
|
5 years ago |
|
Tim Quatmann
|
3b68059e2b
|
Hiding the StateValuation object of a single state.
|
5 years ago |
|
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)
|
5 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
|
5 years ago |
|
Tim Quatmann
|
5733072898
|
TransientVariableInformation: Flagging a few getters const
|
5 years ago |
|
Tim Quatmann
|
ab93422fa0
|
Changed default dd library from `cudd` to `sylvan` (cf. Github issue #71)
|
5 years ago |
|
Sebastian Junges
|
cdfbe8d4bb
|
from pomdp to pmc now preserves state valuations
|
5 years ago |
|
Sebastian Junges
|
55b344c560
|
but state valuations as comments into drn
|
5 years ago |
|
Sebastian Junges
|
f23efb9eb2
|
split pomdp settings into toparametric settings for the UAI18 stuff
|
5 years ago |
|
Sebastian Junges
|
669ffc52d2
|
reworked the interface to qualitative analysis of POMDPs
|
5 years ago |
|
Sebastian Junges
|
a90a82d271
|
better performance when only looking for a winning policy
|
5 years ago |
|
Sebastian Junges
|
498067816d
|
fix stupid mistake that made subsequent searches mostly unsat by setting scheduler var to wrong value
|
5 years ago |
|
Sebastian Junges
|
53800c2145
|
major improvements by introducing real-valued ranking and various related fixes
|
5 years ago |
|
Sebastian Junges
|
34fce002cb
|
compute size of winning region
|
5 years ago |
|
Sebastian Junges
|
eca148cee0
|
graph-based analysis improved, and cleaning outputs
|
5 years ago |
|
Sebastian Junges
|
a7f05847ac
|
better info message if an engine does not support a model
|
5 years ago |
|
Sebastian Junges
|
2de8c94fd9
|
flatsets to string
|
5 years ago |
|
Sebastian Junges
|
08cb25c28c
|
to be sure: z3model by const reference
|
5 years ago |
|
Sebastian Junges
|
c2f5eb9ce0
|
do not export reward model if we find a counterexample for a probability property
|
5 years ago |
|
Sebastian Junges
|
5937a764b8
|
debug output now only appears with log level
|
5 years ago |
|
Sebastian Junges
|
22c644b42c
|
more trace messages in counterexample generation
|
5 years ago |
|
Sebastian Junges
|
ee2351ede3
|
fix logic for including xercesc on macos
|
5 years ago |
|
Sebastian Junges
|
235f335579
|
typo
|
5 years ago |
|
Sebastian Junges
|
fc49b32979
|
Merge branch 'master' into almostsurepomdp
|
5 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...).
|
5 years ago |
|
Tim Quatmann
|
ae2b63ca07
|
Eigenadapter: changed Returntype of digits10 to match the NumTraits interface
|
5 years ago |
|
Tim Quatmann
|
47ac26eb02
|
JaniScopeChanger: Fixed segfault and incorrect detection for variable accesses (GitHub issue #70)
|
5 years ago |
|
Tim Quatmann
|
52b1b8158e
|
Merge remote-tracking branch 'refs/remotes/origin/master'
|
5 years ago |
