sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Commit Graph

  • 65a310dc8b Test for allUntilProbabilities Matthias Volk 2019-05-17 10:34:53 +0200
  • c27e542bf1 Merge branch 'master' into deterministicScheds TimQu 2019-05-17 08:53:13 +0200
  • fcb5f094dc Fixed a tybo. TimQu 2019-05-17 08:52:50 +0200
  • 0eda4b4041 DeterministicSchedsLpChecker: Started to treat End Components properly. TimQu 2019-05-16 10:38:32 +0200
  • 4825cb254f Precision as argument Jip Spel 2019-05-16 16:28:07 +0200
  • 621aae1c4c DeterministicSchedsParetoExplorer: Selecting LP-based weight vector checkers in case of properties that are not supported by the standard weight vector checker. TimQu 2019-05-16 10:36:06 +0200
  • 1557f6d213 Use precision in sample checking monotonicity Jip Spel 2019-05-15 15:31:00 +0200
  • 8732a7f40d Make variabletype depend on value type Jip Spel 2019-05-15 14:34:42 +0200
  • 7f5416adb8 Clean up LatticeExtender Jip Spel 2019-05-15 14:26:10 +0200
  • c0aa6eefa3 Clean up Lattice Jip Spel 2019-05-15 12:02:21 +0200
  • fa97e0138f Clean up assumption maker Jip Spel 2019-05-15 10:08:00 +0200
  • ee08139641 Fix test Jip Spel 2019-05-15 10:06:08 +0200
  • 3ebd5f0bf6 Clean up assumption checker Jip Spel 2019-05-15 09:58:16 +0200
  • 0d1ddb6232 Make sampling in monotonicity-analysis optional Jip Spel 2019-05-14 16:25:21 +0200
  • 77a70179d3 Update MonotonicityChecker Jip Spel 2019-05-14 15:05:47 +0200
  • 1a4fe91797 Removed unused files. TimQu 2019-05-14 11:08:28 +0200
  • c361d59d65 Merge branch 'master' into dft_iso Matthias Volk 2019-05-13 16:37:10 +0200
  • 28a878f154 Adjusted lower bound correction to new BE distinction Alexander Bork 2019-05-13 15:58:16 +0200
  • 18f0c3d125 MemoryIncorporation: improved documentation. TimQu 2019-05-13 14:18:44 +0200
  • 6d67a3671b Merge branch 'master' into deterministicScheds TimQu 2019-05-13 13:55:52 +0200
  • f9b06e7eaf Updated changelog. TimQu 2019-05-13 13:55:36 +0200
  • 70b9398b90 storage/Scheduler: Fixed a constructor. TimQu 2019-05-13 13:53:24 +0200
  • 7995100441 Small fixes in DFT tests Matthias Volk 2019-05-12 19:21:32 +0200
  • 521461737a Adaption to changes in BEs Matthias Volk 2019-05-12 19:11:08 +0200
  • 23f1e73137 Merge from branch 'dft' Matthias Volk 2019-05-12 19:10:13 +0200
  • 5380d9c050 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-10 18:51:04 +0200
  • 63a9b4485b FormulaParserGrammar: Adding support for time-bounded formulas with exact time-bound, e.g., F=12 "target" Tim Quatmann 2019-05-10 15:41:32 +0200
  • f37bcea1ea Added test for bound correction Alexander Bork 2019-05-10 14:32:28 +0200
  • 73a514a9c7 Fix validation of assumptions/use it Jip Spel 2019-05-10 14:16:22 +0200
  • b4f652bbc8 Reducing the nesting when creating a expression::sum(...). Tim Quatmann 2019-05-10 14:13:03 +0200
  • a829c52a0d ExpressionParser can now parse round expressions. Tim Quatmann 2019-05-10 13:08:16 +0200
  • 66a7bd5954 implemented creation of round expression. Tim Quatmann 2019-05-10 13:07:41 +0200
  • b70f28b10e Ensured that utility function for rounding always rounds towards infinity. Tim Quatmann 2019-05-10 10:56:07 +0200
  • 0e18046934 Fixed translating ceil(x) to mathsat expressions. Tim Quatmann 2019-05-10 10:48:12 +0200
  • d201580d92 Refactored simplification of UnaryNumericalFunctionExpression. Tim Quatmann 2019-05-10 10:14:20 +0200
  • a34037bff4 Added utility function for rounding. Tim Quatmann 2019-05-10 10:04:16 +0200
  • d42dea79c3 Added comments to explain the query Alexander Bork 2019-05-10 14:03:54 +0200
  • 74d1bf3c7e Merge remote-tracking branch 'origin/dftSMT' into dftSMT Alexander Bork 2019-05-10 14:00:28 +0200
  • 948485c226 Reworked lower bound computation Alexander Bork 2019-05-10 14:00:02 +0200
  • eeccb2092a Added variables for trigger and resolution timepoints of dependencies Alexander Bork 2019-05-03 18:12:14 +0200
  • 426c293090 Travis: disable installation of carl-parser Matthias Volk 2019-05-10 10:23:05 +0200
  • 2d20365674 Travis: support for Ubuntu 19.04 Matthias Volk 2019-05-09 17:02:18 +0200
  • 75cfa17966 Fixed compile issue on Linux Matthias Volk 2019-05-09 16:32:01 +0200
  • 5729066add Merge branch 'master' into dft Matthias Volk 2019-05-09 11:20:40 +0200
  • a35735a630 Fixed computation of all until probabilities Matthias Volk 2019-05-09 11:18:19 +0200
  • 161c3ac6bf Test case for transient probabilities Matthias Volk 2019-05-09 11:14:53 +0200
  • e1af4158ae Removed unused argument Matthias Volk 2019-05-09 11:14:35 +0200
  • da6704139b Merge from master Matthias Volk 2019-05-09 10:16:03 +0200
  • 3a7f89b396 DeterministicSchedsLpChecker: Added various variants of the encoding. Tim Quatmann 2019-05-07 18:37:29 +0200
  • 7ab409fd2a BaierUpperRewardBoundsComputer: Added a function to get an upper bound for the expected number of visits of each state. Tim Quatmann 2019-05-07 18:36:22 +0200
  • df28331465 PolytopeTree: Fixed application of convex union. Tim Quatmann 2019-05-07 18:34:52 +0200
  • 349c806cae Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-07 11:29:34 +0200
  • 3a11a4b3eb Introducing a TBB adapter that #undefs TRUE and FALSE. Tim Quatmann 2019-05-07 10:37:59 +0200
  • fe658ee787 Reverting the previous fix since the jit builder wasn't happy about the carl/formula/Formula.h include. Tim Quatmann 2019-05-07 10:36:58 +0200
  • dd1d53046c utility/constants.cpp: Fixing unknown 'isnan' Tim Quatmann 2019-05-07 09:58:20 +0200
  • 035a5d52f8 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-06 18:24:40 +0200
  • 7881512a17 Removed ConstraintType<ValueType> definition out of RationalFunctionAdapter to make things more consistent. Tim Quatmann 2019-05-06 18:21:08 +0200
  • 4e078cf8fa Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-06 18:04:05 +0200
  • 70112b7315 Fixed a name clash that sometimes occurred when compiling Storm on macOS with TBB. Tim Quatmann 2019-05-06 18:03:48 +0200
  • 1bfe736fb8 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-06 11:44:06 +0200
  • 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. Tim Quatmann 2019-05-06 11:01:12 +0200
  • 4c911791e1 NativePolytope: Improved clean() operation on empty polytopes. Tim Quatmann 2019-05-06 10:58:05 +0200
  • e7454cd494 ArgumentValidators: added factory for UnsignedIntRangeValidatorIncluding Tim Quatmann 2019-05-06 10:56:53 +0200
  • 15dadf1bc3 Fixed imprecision in comparison for MA Matthias Volk 2019-05-06 11:18:32 +0200
  • 0843f5ea7b PolytopeTree: Fixed documentation. Tim Quatmann 2019-05-06 11:01:59 +0200
  • 0f13d2803c Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-06 11:01:27 +0200
  • d4e2473129 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. Tim Quatmann 2019-05-06 11:01:12 +0200
  • fab5adb275 NativePolytope: Improved clean() operation on empty polytopes. Tim Quatmann 2019-05-06 10:58:05 +0200
  • 26553b628e ArgumentValidators: added factory for UnsignedIntRangeValidatorIncluding Tim Quatmann 2019-05-06 10:56:53 +0200
  • d3052c725b DeterministicSchedsLpChecker: Make use of added Gurobi features: Specify a goal-gap and make use of solutions found during solving. Tim Quatmann 2019-05-06 10:55:36 +0200
  • 9b152e4940 Added variables vor trigger and resolution timepoints of dependencies Alexander Bork 2019-05-03 18:12:14 +0200
  • c4ba7554fd Added upper bound correction Alexander Bork 2019-05-03 17:07:52 +0200
  • f1a57494e8 DeterministicSchedsParetoExplorer: Stop splitting facets if they are already 'small' enough. Tim Quatmann 2019-05-03 15:53:52 +0200
  • 56dbbdabb4 DeterministicSchedsLpChecker: Resolved two issues in the encoding. Tim Quatmann 2019-05-03 15:52:04 +0200
  • 0baccee440 Added correction of constraint for non-Markovian states and better lower bound computation Alexander Bork 2019-05-02 16:20:53 +0200
  • bce641319f Fixed computation of maximal total expected rewards for MDPs with end components. Tim Quatmann 2019-05-02 15:29:40 +0200
  • 60ae342677 NativePolytope: Fixed affineTransformation of the universal polytope. Tim Quatmann 2019-05-02 15:29:11 +0200
  • 2fe11c5165 DeterministicSchedsParetoExplorer: Use StandardWeightVectorChecker for corner points. Tim Quatmann 2019-05-02 15:27:24 +0200
  • 9648d1a762 DeterministicSchedsObjectiveHelper: Added minimizing(). Tim Quatmann 2019-05-02 15:25:13 +0200
  • 9adf712883 DetSchedsLpChecker: Trying a slightly different encoding. Tim Quatmann 2019-05-02 15:24:23 +0200
  • 7459800002 Improve derivative check Jip Spel 2019-05-02 15:16:05 +0200
  • f6ea4d38bb Fix assumption making and checking and testing Jip Spel 2019-05-02 12:37:36 +0200
  • 509b7a8d0a Merge branch 'dft' of dft Matthias Volk 2019-05-02 11:21:33 +0200
  • 4f376caccb Fixed expand flag to avoid expanding too much Matthias Volk 2019-05-02 11:21:14 +0200
  • 9f4960161a Merge branch 'master' into dft Matthias Volk 2019-05-01 20:39:51 +0200
  • b34351ec85 Maximal exploration depth can be specified for state space generation Matthias Volk 2019-05-01 20:06:58 +0200
  • bcd4c359b7 DetScheds Objective helper: Detect when exact arithmetic is used. Tim Quatmann 2019-04-29 16:58:46 +0200
  • deaaf41af2 Fixed returning a reference to a local object. Tim Quatmann 2019-04-29 15:50:30 +0200
  • 658f4a6898 DetScheds: 'better' reference point plus clean up Tim Quatmann 2019-04-29 15:32:17 +0200
  • cd3290cb7d DetSchedsLpChecker: Helping vertex checking by shrinking the search space. Also fixed some issues w.r.t. minimizing objectives. Tim Quatmann 2019-04-29 15:05:13 +0200
  • ef7c1f6fb8 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-29 11:45:38 +0200
  • 3836fd42c0 utility/vector: Added hasZeroEntry and hasInfinityEntry Tim Quatmann 2019-04-29 11:44:51 +0200
  • 3714fc3bf2 MinMaxSolverEnvironment: Removed unused method declarations. Tim Quatmann 2019-04-29 11:44:31 +0200
  • 12c8f8928d DeterministicSchedsObjectiveHelper: Compute tighter lower/upper bounds. Tim Quatmann 2019-04-29 11:43:18 +0200
  • 9bde9c4127 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-29 09:48:06 +0200
  • ca9102616b ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected (part 2...). Tim Quatmann 2019-04-29 09:43:31 +0200
  • 91951f6714 GurobiLpSolver: Fixed an issue when popping and pushing variables with the same name. Tim Quatmann 2019-04-29 09:29:29 +0200
  • 193c961727 Removed unnecessary include. Tim Quatmann 2019-04-29 09:30:27 +0200
  • 5a017ea718 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-04-29 09:29:54 +0200
  • b86d022af1 GurobiLpSolver: Fixed an issue when popping and pushing variables with the same name. Tim Quatmann 2019-04-29 09:29:29 +0200