sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
8377 Commits
2 Branches
0 Tags
187 MiB
Tree: 009a60df5c
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '009a60df5c'
${ noResults }
Commit Graph

7159 Commits (009a60df5c97a78f63b9b12fa8828c6bdb98b79d)

Author SHA1 Message Date
Sebastian Junges 009a60df5c fix in hash computation
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 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
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
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 235f335579 typo
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 aae44a3b4b Fixed error message that appeared when using jit.
5 years ago
Matthias Volk c09c31be6a Enable pragmas in eigen.h only for GCC 9
5 years ago
Matthias Volk 7b6101c220 Updated list of ignored warnings for Eigen
5 years ago
Tim Quatmann ee0e90462f Fixed incorrect result of canHandleStatic for multi-objective formulas for MDP in hybrid engine and MA in sparse engine.
5 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).
5 years ago
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
Sebastian Junges 005e23d5d5 two fixes after encoding from non-empty winning regions
5 years ago
Sebastian Junges 972332810b cosmetic changes, better output, some assertions
5 years ago
Sebastian Junges 556a884e74 use target state to initialise winning region, better timers and slight improvements in partial scheduler extension
5 years ago
Sebastian Junges f00a208e9c validate whether a winning region is maximal
5 years ago
Sebastian Junges d3c593fe74 set validation level from command line
5 years ago
Sebastian Junges a1f50253d9 compact output of winning region
5 years ago
Tim Quatmann 2500cc0cd2 Fixed computation of relative gap for special cases (in particular l=u=0)
5 years ago