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
|
55b344c560
|
but state valuations as comments into drn
|
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
|
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).
Made the include path for the Eigen headers more unique, so we no longer use the headers at /urs/include/ instead.
|
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 |
|
Matthias Volk
|
a95f65cc27
|
Explicit fall-through
|
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 |
|
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 |
Daniel Basgöze
|
93e7bac668
|
Fix bitshift overflow
|
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
|
4eed592811
|
--timeout now just sends a SIGALRM signal (which can be catched by the signal handler).
|
5 years ago |
|
Sebastian Junges
|
4930908942
|
new version of containsVariable, with better performance and somewhat better to debug
|
5 years ago |
|
Sebastian Junges
|
91cad8164f
|
trace outputs towards debugging the JaniScopeChanger
|
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
|
88c31b36d0
|
Equation system based CTMC LRA solving: For the 'inner' linear equation system solver, also set whether the solver type has been set from default. This avoids potentially using unsound/inexact equation solvers.
|
5 years ago |
|
Daniel Basgöze
|
7076a54dfb
|
Add error checking to C style io
|
6 years ago |
|
Daniel Basgöze
|
b7c53c080b
|
Remove trailing whitespace
|
6 years ago |
|
Daniel Basgöze
|
002d9e1925
|
Add error checking to C style io
|
6 years ago |
|
Daniel Basgöze
|
1ee87a876a
|
Remove trailing whitespace
|
6 years ago |
|
Daniel Basgöze
|
64e70c406e
|
Replace size_t with uint64_t in bitoperations
|
6 years ago |
|
Daniel Basgöze
|
aa0fe082d7
|
Document bitoperations.h
|
6 years ago |
|
Daniel Basgöze
|
972abfcf6f
|
Include required headers
|
6 years ago |
|
Daniel Basgöze
|
4c5abe19f3
|
Remove unnecessary cast
|
6 years ago |
|
Matthias Volk
|
325b700c62
|
Explicitly set initialization order for SparseMatrix to avoid nasty segfaults
|
6 years ago |
|
Matthias Volk
|
c1b4c3270f
|
Fixed initialization order warnings
|
6 years ago |
|
Sebastian Junges
|
92b384c17c
|
fix in recently introduced isSinkState
|
6 years ago |
|
Sebastian Junges
|
82978f4357
|
isSinkState
|
6 years ago |
|
Sebastian Junges
|
1ef92dee9e
|
backbone for a simulator on top of explicit state models
|
6 years ago |
|
Tim Quatmann
|
feebf1a24d
|
Added scheduler export in .json
|
6 years ago |
