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

Commit Graph

  • ce0283d80d Cmake: checked whether the stack-check issue still persists with current AppleClang v12.0.0 Tim Quatmann 2020-11-20 09:35:57 +0100
  • 8619a4d833 CMake: Implemented a workaround for building CUDD on MacOS Big Sur. Tim Quatmann 2020-11-19 17:31:29 +0100
  • 1982dc0dba SparsePcaaParetoQuery: Added a (hopefully explaining) comment Tim Quatmann 2020-11-19 17:29:28 +0100
  • 6a71c19d8a added sparse smg model Stefan Pranger 2020-10-25 12:57:25 +0100
  • bb05b9c03c aggregate player indices into model Stefan Pranger 2020-08-19 12:04:51 +0200
  • cea09f932b generator now assigns player indices to states Stefan Pranger 2020-08-19 12:02:39 +0200
  • 163dfa8654 ModelComponents now feature a player mapping Stefan Pranger 2020-08-19 11:59:25 +0200
  • 6b715792aa added player related helpers Stefan Pranger 2020-08-19 11:54:46 +0200
  • 160a2c32a2 added SMGs to existing ModelTypes Stefan Pranger 2020-08-17 14:51:19 +0200
  • dce9496300 Model validity check now handles SMGs Stefan Pranger 2020-08-17 14:42:52 +0200
  • 9bf2a572a7 check if state is controlled by multiple players Stefan Pranger 2020-08-13 22:08:03 +0200
  • e9a6077acb adapted player ostream output Stefan Pranger 2020-08-13 21:00:13 +0200
  • 1cf2e544ac add assertion for module indices in second Stefan Pranger 2020-08-13 18:49:53 +0200
  • de301323d6 check module and action names when parsing players Stefan Pranger 2020-08-13 11:39:40 +0200
  • 43353d5243 store name index map for player member Stefan Pranger 2020-08-13 11:38:26 +0200
  • 271ed284a6 fix player ostream output Stefan Pranger 2020-08-13 09:12:50 +0200
  • 11f7464372 players now get stored in PRISM programs Stefan Pranger 2020-08-13 09:12:35 +0200
  • 48276e47a9 further work on player parsing Stefan Pranger 2020-08-12 14:22:11 +0200
  • 3f3b154ce0 first progress on player parsing Stefan Pranger 2020-08-12 10:37:43 +0200
  • 55f4efd40a added SMG ModelType Stefan Pranger 2020-08-11 16:33:38 +0200
  • bf54ca8a52 init Player class for SMG parsing Stefan Pranger 2020-08-11 16:33:05 +0200
  • d35e9a6a40 removed plenty of empty line whitespaces Stefan Pranger 2020-08-11 16:32:32 +0200
  • c12c0352f7
         Support for parsing jani model from string Matthias Volk 2020-11-10 16:52:28 +0100
  • 209090eb93
         storm-dft: Ignore compound nodes in json parser Matthias Volk 2020-11-03 10:40:31 +0100
  • d0c153da8d Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs) Tim Quatmann 2020-10-23 17:41:05 +0200
  • 9775964f43 Pcaa: Fixed unnecessary insertion of diagonal entries in deterministic transitions. Tim Quatmann 2020-10-23 15:30:48 +0200
  • 3a4af89b66 graph: Cycle check ignores Zero entries. Tim Quatmann 2020-10-23 15:25:51 +0200
  • d53cffab08 avoid resize that caused unstable behavior Sebastian Junges 2020-10-22 22:26:32 -0700
  • f7d75b1677 Merge remote-tracking branch 'refs/remotes/origin/master' Tim Quatmann 2020-10-22 17:50:36 +0200
  • 2cadf3a252 Added support for generating optimal schedulers for globally formulae Tim Quatmann 2020-10-22 17:39:23 +0200
  • f5ce4860ac Updated changelog. Tim Quatmann 2020-10-22 17:38:17 +0200
  • 4ffe13063c Fixed the offline_package.md documentation to incorporate more recent changes in Storm. Tim Quatmann 2020-10-22 15:56:48 +0200
  • dc8612b751 Fixed not always using the acyclic solver within LRA and multi-objective time-bounded reachability computations. Tim Quatmann 2020-10-22 15:55:56 +0200
  • 8b05837e77
         Fixed assertion for RationalFunction Matthias Volk 2020-10-21 10:09:45 +0200
  • dced2bb9b6 Merge branch 'master' into rubicon Sebastian Junges 2020-10-20 14:55:12 -0700
  • 32c88825e2 cleanup Sebastian Junges 2020-10-20 14:07:24 -0700
  • 50a82c1127 Merge branch 'master' into monitoring Sebastian Junges 2020-10-20 11:49:05 -0700
  • 664484883a allow termination in inner loop of OVI Sebastian Junges 2020-10-20 11:48:23 -0700
  • c247b4ab55 fixed type in offline_package documentation Tim Quatmann 2020-10-19 15:33:17 +0200
  • 90e1eeba28 Merge branch 'multi-objective-lra' TimQu 2020-10-16 13:13:32 +0200
  • 9d29f369e2 fixed incorrect hanlding of lra objecties in bounded phase Tim Quatmann 2020-10-16 13:12:40 +0200
  • 9a8f40bb33 Multi-obj preprocessor: Fixed an issue when preprocessing LRA operator formulas Tim Quatmann 2020-10-14 14:45:27 +0200
  • 6dcbf75fe3
         Update progress measurments only if --progress flag is set Matthias Volk 2020-10-08 11:47:08 +0200
  • 27cb582243 MDP Instantiation model checker: Fixed setting model checking hint information. TimQu 2020-10-06 21:39:22 +0200
  • 5213be9b69 More statistics output. Tim Quatmann 2020-10-02 17:15:25 +0200
  • 20665eb862 multi-objective: Aborting time-bounded reachability computation when termination signal is received. Tim Quatmann 2020-10-02 12:48:35 +0200
  • c1c0fcf8f3 Display a bit more statistics for multi-objective model checking. Tim Quatmann 2020-10-02 12:37:26 +0200
  • ce14b45578 Pcaa: Implemented termination signal. Tim Quatmann 2020-10-02 12:09:42 +0200
  • b6259e7ea3 SparseMaPcaaTest: Temporarily disabled a test as it did contain non-optimal points due to numerical issues. TimQu 2020-10-01 20:03:58 +0200
  • ce962bf1df SparseMaPcaaChecker: Fixed cycle detection. TimQu 2020-10-01 20:03:15 +0200
  • 5a6952899b MaPcaaWeightVectorChecker now uses the acyclic solver if possible. Tim Quatmann 2020-10-01 15:51:31 +0200
  • 5e9241fcd1 Allowing reward accumulations in multi-objective model checking queries. Tim Quatmann 2020-10-01 15:51:07 +0200
  • da6333cead Fix in scheduler export for acyclic Min Max solver Tim Quatmann 2020-10-01 15:50:38 +0200
  • e513a3fb62 progress in monitoring with timeouts etc Sebastian Junges 2020-10-01 00:24:52 -0700
  • 4760a12815 reset signal handler Sebastian Junges 2020-10-01 00:23:47 -0700
  • f9ee3d10e4 simulating with rationals Sebastian Junges 2020-10-01 00:23:22 -0700
  • b7ad55b34b random prob generator for rationals Sebastian Junges 2020-09-30 20:31:54 -0700
  • b45497a8c4 Added --propsasmulti switch to interpret input formulas as multi-objective formula TimQu 2020-09-30 22:00:10 +0200
  • 2aab7f99db Merge branch 'master' into multi-objective-lra Tim Quatmann 2020-09-30 15:02:34 +0200
  • 260c14a3f6 ExpressionParser: Allow sequences of unary operators, like '!!x=0' (fixes #89) Tim Quatmann 2020-09-30 13:54:18 +0200
  • 16ecb0fc8d OVI: display current number of iterations with --progress --verbose. Tim Quatmann 2020-09-30 13:53:15 +0200
  • bd3c42561b Added multi-objective lra test case for MA Tim Quatmann 2020-09-29 14:02:59 +0200
  • 97d4dba540 Added test case for Multi-objective LRA combined with step-bounded property. Tim Quatmann 2020-09-29 14:02:37 +0200
  • c990d27c50 Added MA test case + fixes Tim Quatmann 2020-09-29 13:22:48 +0200
  • 5bfb3b132e New MDP LRA Test case + fix Tim Quatmann 2020-09-29 11:42:17 +0200
  • 7023736e3d Added resource-gathering testfile Tim Quatmann 2020-09-29 09:17:07 +0200
  • ee06a1f1a6 Also added test case for lra operator formula. Tim Quatmann 2020-09-28 19:29:47 +0200
  • 6154bd39f9 Fixes for new test case. Tim Quatmann 2020-09-28 19:22:59 +0200
  • 3789fbb3e9 Test case for multi-objective lra Tim Quatmann 2020-09-28 19:22:48 +0200
  • 07f7ce7963 Merge branch 'master' into multi-objective-lra TimQu 2020-09-28 11:12:50 +0200
  • f100ff6275 LraViHelper: Fixed unordered insertion into SparseMatrixBuilder. TimQu 2020-09-28 11:12:38 +0200
  • 36f27e4391 Added a simple example model for multi-objective lra. TimQu 2020-09-25 23:25:44 +0200
  • 139c86f6a0 Fixes for multi-obj LRA TimQu 2020-09-25 23:24:42 +0200
  • 400b69663a Fixed multi-obj. tests TimQu 2020-09-25 21:26:32 +0200
  • 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