Tim Quatmann
fe658ee787
Reverting the previous fix since the jit builder wasn't happy about the carl/formula/Formula.h include.
6 years ago
Tim Quatmann
dd1d53046c
utility/constants.cpp: Fixing unknown 'isnan'
6 years ago
Tim Quatmann
7881512a17
Removed ConstraintType<ValueType> definition out of RationalFunctionAdapter to make things more consistent.
6 years ago
Tim Quatmann
70112b7315
Fixed a name clash that sometimes occurred when compiling Storm on macOS with TBB.
6 years ago
Tim Quatmann
cc02383591
GurobiLpSolver: Improved interface by
* adding settings MIPFocus (to switch between solving strategies) and ConcurrentMIP (to spawn multiple MIP solvers)
* allowing to set the desired and get the achieved gap between lower- and upper bound when solving MIP models
* retrieving other solutions found during optimization.
6 years ago
Tim Quatmann
4c911791e1
NativePolytope: Improved clean() operation on empty polytopes.
6 years ago
Tim Quatmann
e7454cd494
ArgumentValidators: added factory for UnsignedIntRangeValidatorIncluding
6 years ago
Matthias Volk
15dadf1bc3
Fixed imprecision in comparison for MA
6 years ago
Alexander Bork
9b152e4940
Added variables vor trigger and resolution timepoints of dependencies
6 years ago
Alexander Bork
c4ba7554fd
Added upper bound correction
6 years ago
Alexander Bork
0baccee440
Added correction of constraint for non-Markovian states
and better lower bound computation
6 years ago
Tim Quatmann
bce641319f
Fixed computation of maximal total expected rewards for MDPs with end components.
6 years ago
Tim Quatmann
60ae342677
NativePolytope: Fixed affineTransformation of the universal polytope.
6 years ago
Matthias Volk
509b7a8d0a
Merge branch 'dft' of dft
6 years ago
Matthias Volk
4f376caccb
Fixed expand flag to avoid expanding too much
6 years ago
Matthias Volk
9f4960161a
Merge branch 'master' into dft
6 years ago
Matthias Volk
b34351ec85
Maximal exploration depth can be specified for state space generation
6 years ago
Tim Quatmann
3836fd42c0
utility/vector: Added hasZeroEntry and hasInfinityEntry
6 years ago
Tim Quatmann
3714fc3bf2
MinMaxSolverEnvironment: Removed unused method declarations.
6 years ago
Tim Quatmann
ca9102616b
ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected (part 2...).
6 years ago
Tim Quatmann
91951f6714
GurobiLpSolver: Fixed an issue when popping and pushing variables with the same name.
6 years ago
Tim Quatmann
adaba03648
ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected.
6 years ago
Tim Quatmann
160c6a67f4
Added missing method in case z3 lp solver is not available.
6 years ago
Tim Quatmann
4322d00034
FilteredRewardModel: added create method that works without a checkout.
6 years ago
TimQu
c72b97dfca
Cleared unused variable warning.
6 years ago
TimQu
76cabb8287
geometry: Fixed a merge issue.
6 years ago
Tim Quatmann
cf25f2f941
SparseMatrix: Create a pretty string of the matrix dimensions.
6 years ago
Tim Quatmann
138e0f2cee
solver: Implemented incremental support for LP solvers (Z3 and Gurobi)
6 years ago
Tim Quatmann
1eee9a89bd
storage/geometry/polytopes: New Methods: setminus and clean
6 years ago
Tim Quatmann
3a21ce8009
utility/vector: buildVectorForRange now gets the type of the vector as a template parameter.
6 years ago
Alexander Bork
f16b488590
Added conservative lower bound correction
6 years ago
Alexander Bork
a669c69fc9
Added tests for SMT encoding
6 years ago
Alexander Bork
aff9d21811
Easier fix for bound computation using SMT encoding
6 years ago
Alexander Bork
b89f8f8de4
Refactoring of SMT tests
6 years ago
Alexander Bork
5d5487140f
Fixed bound calculation for SMT encoding
6 years ago
Matthias Volk
f2840f3a66
Explore relevant events further even if the DFT has already failed
6 years ago
Matthias Volk
944c5ac0fe
Only set operational BEs as failable
6 years ago
Matthias Volk
f1c91d9280
Test case for SEQ bug
6 years ago
Matthias Volk
32dc2dbcc0
Fixed bug where children of SEQ gates were not properly enabled
6 years ago
Matthias Volk
0f1b05f28c
Added support for '_dc' label suffix
6 years ago
Matthias Volk
c272e65d30
Changed suffix label for failed elements to '_failed'
6 years ago
Matthias Volk
92d05ec368
Fixed handling of relevant events from properties
6 years ago
Matthias Volk
534d2cf51b
Fixed concatenation of multiple properties
6 years ago
Matthias Volk
0a1ed0270a
Output relevant events for better debugging
6 years ago
Matthias Volk
9398832ce8
Add formula in parse exception for easier debugging
6 years ago
Matthias Volk
b77009897f
Ensure unique names in JSON Parser
6 years ago
Matthias Volk
22c6dfc212
Merge from master
6 years ago
Matthias Volk
2b8cf84c97
Adapted tests to changes
6 years ago
Matthias Volk
f2c902eedb
Set labels, dont care propagation and unique failed state according to relevant events
6 years ago
Matthias Volk
51959d4334
Set labels in property as relevant events as well
6 years ago