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

Commit Graph

  • e0276cb78f Assertion fixed. Tim Quatmann 2020-09-25 16:10:01 +0200
  • d351bd6455 WeightVectorChecker: Integrated lra objectives also in the individual phase Tim Quatmann 2020-09-25 16:06:31 +0200
  • 360c3877b7 More steps towards integrating LRA in pcaa Tim Quatmann 2020-09-25 12:30:55 +0200
  • 43db81c18f Silenced a warning. Tim Quatmann 2020-09-25 12:29:40 +0200
  • 67393a9584 Further steps towards integrating LRA in weight vector checker. Tim Quatmann 2020-09-24 17:43:59 +0200
  • b3fa8893a2 End Component Eliminator now also returns the sinkRows Tim Quatmann 2020-09-24 17:42:10 +0200
  • 29a7a7e865 WeightVectorChecker: Making initialization LRA-ready Tim Quatmann 2020-09-24 14:57:13 +0200
  • 9421a60d5a Fixes for multi-obj reward analysis. Tim Quatmann 2020-09-24 14:23:09 +0200
  • 4b13ad3220 Fix for multi-obj LRA preprocessing Tim Quatmann 2020-09-24 14:22:23 +0200
  • 56e253fac0 graph: Extended the documentation a tiny bit Tim Quatmann 2020-09-23 11:18:18 +0200
  • 33e73ed63a WeightVectorChecker: Fixed incorrectly choosing a scheduler that potentially yields infinite reward for one objective. Tim Quatmann 2020-09-23 11:18:00 +0200
  • 4bf9bd473f SparserMatrix: Added getRowGroupFilter method. Tim Quatmann 2020-09-23 11:15:24 +0200
  • 9df410e433 Merge branch 'master' into monitoring Sebastian Junges 2020-09-21 15:25:01 -0700
  • d86c763b94 support for nonstandard predicate elimination or to-dice translation Sebastian Junges 2020-09-21 10:36:29 -0700
  • b6be0f3356 convex reduction Sebastian Junges 2020-09-16 08:50:19 -0700
  • d2e36e9db3 dense belief states Sebastian Junges 2020-09-14 14:24:12 -0700
  • a358af1264 set entries that are nonzero Sebastian Junges 2020-09-14 14:23:26 -0700
  • f744176481
         Fixed lib filename for carl (Fixes #85) Matthias Volk 2020-09-14 19:17:30 +0200
  • e22f699339 parser for predicates Sebastian Junges 2020-09-12 13:12:14 -0700
  • 1f281ff45a add predicate expressions for n-ary predicates Sebastian Junges 2020-09-11 18:42:38 -0700
  • 7891492b96 Merge branch 'master' into multi-objective-lra Tim Quatmann 2020-09-11 17:05:16 +0200
  • 94311e7d30 Topological solvers: Added a warning for numerical issues triggered in cases where in non-exact mode a selfloop probability is very close to 1 but not equal to 1 Tim Quatmann 2020-09-11 17:05:04 +0200
  • 8a77e3238d Implemented isAlmostZero and isAlmostOne also for non-double value types. Tim Quatmann 2020-09-11 17:03:26 +0200
  • d2f983a0c6 Merge branch 'master' into multi-objective-lra Tim Quatmann 2020-09-09 16:34:11 +0200
  • 87456d00fc Fixes in EdgeContainer::operator= Tim Quatmann 2020-09-09 16:33:56 +0200
  • ed1a5b6ced Fixed flagging objectives for reward finiteness check incorrectly Tim Quatmann 2020-09-09 16:31:22 +0200
  • f79814bcb4 Merge remote-tracking branch 'refs/remotes/origin/master' into multi-objective-lra Tim Quatmann 2020-09-09 16:01:13 +0200
  • 33a6687721 Fixed deprecated operator= warnings Tim Quatmann 2020-09-09 16:00:46 +0200
  • 0e544a4c13 Enabled TimeOperatorFormulas for multi-objective model checking of MDPs. TimQu 2020-09-09 10:38:52 +0200
  • 3db0ff124f Started to make multiobjective reward analysis aware of LRA formulas. TimQu 2020-09-09 15:29:34 +0200
  • e898391e44 Implemented stripping away of reward accumulations in multi-objective preprocessing. TimQu 2020-09-09 15:28:42 +0200
  • f532f6461b The sparse StandardRewardModel somehow had 'dtmc' in it. TimQu 2020-09-09 15:28:09 +0200
  • 49bc9054b7 Further improvements for filtered reward model TimQu 2020-09-09 15:27:24 +0200
  • 30977ed356 Added some utility methods to reward path formulas TimQu 2020-09-09 15:26:48 +0200
  • 825454d482
         Fixed warning Matthias Volk 2020-09-09 14:52:36 +0200
  • 781fa9dbd8 StandardRewardModel: Removed a default argument because the "default" constructor is ambiguous otherwise. TimQu 2020-09-09 13:24:32 +0200
  • f328e69dc4 Added extract function to FilteredRewardModel TimQu 2020-09-09 13:23:29 +0200
  • 55999036d6
         Fixed warning Matthias Volk 2020-09-09 11:54:21 +0200
  • a5342d8b83 added functionalities in MultiObjectivePreprocessorResult to capture lra objectives TimQu 2020-09-09 10:56:13 +0200
  • 74c1972c4a Merge branch 'master' into multi-objective-lra TimQu 2020-09-09 10:39:42 +0200
  • 182f612272 Enabled TimeOperatorFormulas for multi-objective model checking of MDPs. TimQu 2020-09-09 10:38:52 +0200
  • fa0ad07f8d Added preprocessing of multi-objective lra formulas TimQu 2020-09-09 10:33:09 +0200
  • a5eb8e224b Allowing lra formulas in multi-objective formula fragment TimQu 2020-09-09 10:31:48 +0200
  • 11a893f3d2 Merge branch 'master' into rubicon Sebastian Junges 2020-09-08 17:09:55 -0700
  • 6902a3c8f8 Revert "Fixed dot output of BDDs in sylvan." TimQu 2020-09-08 18:47:42 +0200
  • 6dcfd28186 Fixed dot output of BDDs in sylvan. Tim Quatmann 2020-09-08 17:14:32 +0200
  • 41089dee26
         Throw exception in ParameterRegion if number of variables is too high Matthias Volk 2020-09-07 13:44:09 +0200
  • f91c0de9ec Storm version 1.6.2 Tim Quatmann 2020-09-04 16:23:20 +0200
  • 42ceed59c6 Removed debug output. Tim Quatmann 2020-09-04 16:16:16 +0200
  • 2c4e4b29e6 Updated documentation for new release. Tim Quatmann 2020-09-04 16:14:53 +0200
  • 50d7ee6e8d Remove debug info Jip Spel 2020-09-04 15:46:34 +0200
  • 3883c99ed0 Storm Version 1.6.1 Tim Quatmann 2020-09-04 14:53:53 +0200
  • 7f03d1e671 Remove debug info Jip Spel 2020-09-04 14:44:52 +0200
  • a04085e848 Added cmake option exclude_tests_from_all so that we can run make install without building the tests. Tim Quatmann 2020-09-04 11:50:10 +0200
  • 871a28d6f6 Fixed compiling OviSettings Tim Quatmann 2020-09-04 10:59:37 +0200
  • 50c3a28305 Fixed spacing in ovi code. Tim Quatmann 2020-09-04 10:57:43 +0200
  • cb39cc5c15 Optimistic value iteration helper: Removed unused code. Tim Quatmann 2020-09-04 10:47:48 +0200
  • c5f698f9f7 ovi: removed unused option for only taking relevant values when updating the precision Tim Quatmann 2020-09-04 10:46:13 +0200
  • 169f9201b2 ovi: Fixed heuristic for canceling a guess. Tim Quatmann 2020-09-04 10:45:16 +0200
  • a7c6b39f19 Added state valuations in unfolding. Sebastian Junges 2020-09-03 16:07:41 -0700
  • bf4a7fca3b Fixed tracker Sebastian Junges 2020-09-03 16:02:55 -0700
  • 18d9ba0f38 ovi: fixed using incorrect precision TimQu 2020-09-03 20:49:47 +0200
  • 3c682057ea Merge branch 'master' into monitoring Sebastian Junges 2020-09-03 11:37:39 -0700
  • 84c0d77772 storm-pars fixed the fix... Tim Quatmann 2020-09-03 17:03:24 +0200
  • 45803c547e storm-pars: Fixed an issue in the instantiation model checkers where maybestates were cached incorrectly. Tim Quatmann 2020-09-03 16:59:04 +0200
  • d135bc8ecb cmake: Workaround for the FATAL_ERROR that occurred whenever building shipped carl was aborted (bypassing github issue #62). Tim Quatmann 2020-09-03 14:22:15 +0200
  • 684c239f80 Using the revamped optimistic value iteration helper also for the lower bound. Tim Quatmann 2020-09-03 13:56:26 +0200
  • 1b2a78e9ac Abstract equation solver: added getOptionalRelevantValues Tim Quatmann 2020-09-03 13:55:22 +0200
  • f45b56e725 convenience operation on prism programs Sebastian Junges 2020-08-26 16:56:09 -0700
  • b494e938d0 xor Sebastian Junges 2020-09-02 22:03:12 -0700
  • cb1cf41822 Merge branch 'master' into rubicon Sebastian Junges 2020-09-02 09:24:09 -0700
  • 990d1c9759 OVI: seperated implementation from header file. Use a separate helper for computing the upper bounds. Tim Quatmann 2020-09-02 18:19:24 +0200
  • 6e2dab0e0b Silenced a warning in OVI code. Tim Quatmann 2020-09-02 11:04:40 +0200
  • 90d5da570c Renamed portfolio engine to automatic engine. Tim Quatmann 2020-09-02 11:04:09 +0200
  • 7f5f263d7b observation-trace-unfolder added Sebastian Junges 2020-09-01 22:10:06 -0700
  • 1b73f15ff9 fix == operator Sebastian Junges 2020-09-01 22:09:29 -0700
  • 9ce9ae9eeb OVI: Fixed too early termination. Tim Quatmann 2020-09-01 16:12:16 +0200
  • ee56f5b2f9 CMake Fixed version-info when the source code is not in a git repository. Tim Quatmann 2020-09-01 15:13:36 +0200
  • 9423d01631 observation valuations added Sebastian Junges 2020-08-27 15:07:45 -0700
  • fb112ab191 Added support for modulo operators when building symbolic models in exact mode. Tim Quatmann 2020-08-27 17:36:37 +0200
  • d90c14b8f5 Added progress information for LRA computations Tim Quatmann 2020-08-27 17:35:45 +0200
  • 21c07ebd42 DdPrismModelBuilder: Fixed a warning for zero-reward models that was triggered in some cases where the reward model is actually non-zero Tim Quatmann 2020-08-27 17:35:15 +0200
  • 5bcdb5f95a Fixed --sound switch for LRA properties on deterministic models. Tim Quatmann 2020-08-27 17:33:22 +0200
  • 3919c475ad Added some progress information in topological solvers. Tim Quatmann 2020-08-27 17:32:51 +0200
  • 3f2a5ffa62 Lra Tests: Added a test case for sound model checking Tim Quatmann 2020-08-27 17:32:28 +0200
  • 581b1cc392 convenience operation on prism programs Sebastian Junges 2020-08-26 16:56:09 -0700
  • fa34f44989 keep state valuations in transformers on POMDPs Sebastian Junges 2020-08-24 23:42:39 -0700
  • 3861c502b4 memory unfolder can label states with the memory state Sebastian Junges 2020-08-24 22:25:00 -0700
  • fd00d495f7 first version of the nondeterministcbelieftracker Sebastian Junges 2020-08-24 21:38:53 -0700
  • 5fa667b847 add random step functionality to simulator Sebastian Junges 2020-08-24 21:37:46 -0700
  • f3e5708dac
         Updated changelog Matthias Volk 2020-08-23 20:29:12 +0200
  • 7963419554
         Minor change in debug output Matthias Volk 2020-08-23 20:24:37 +0200
  • c0f3e2e0ce
         Skip long running HECS tests Matthias Volk 2020-08-23 20:24:05 +0200
  • a99be1bb06
         Revised relevant events Matthias Volk 2020-08-20 13:42:22 +0200
  • 4c7b069212
         Comment explaining need for std::move Matthias Volk 2020-08-14 10:32:47 +0200
  • 8d9e2a92f0 update changelog Sebastian Junges 2020-08-21 12:52:16 -0700
  • 449e4d6f0d mdp support for lower step bounds Sebastian Junges 2020-08-21 12:49:24 -0700
  • 843e6a9b6b step bounded properties for dtmcs in a new helper, and now with support for (extra) lower bounds Sebastian Junges 2020-08-20 23:15:49 -0700
  • 406ffbdc7f get submatrix now can set some columns to zero but retain them Sebastian Junges 2020-08-20 23:08:32 -0700
  • bbafd095bf no lower bound is still a zero bound :-) Sebastian Junges 2020-08-20 23:07:15 -0700