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

Commit Graph

  • 99bcd337f1 Made the executable not choke if no model file/property was given. Added the benchmark models to the repo (replacing the old ones). dehnert 2015-02-09 19:32:49 +0100
  • 36a65392e0 merge dehnert 2015-02-09 17:10:34 +0100
  • 3f44b1295f started polishing pstorm a bit dehnert 2015-02-09 17:07:51 +0100
  • 534c8c8a44 Set more sensible default value for elimination order. dehnert 2015-02-08 21:29:30 +0100
  • e32482b7a9 Added debug output. dehnert 2015-02-08 16:22:27 +0100
  • a602cecb26 removed simplification of final result. dehnert 2015-02-08 15:14:22 +0100
  • 43a1d0bc73 Added debug output. dehnert 2015-02-08 13:52:36 +0100
  • 197c242bb1 Some minor changes. dehnert 2015-02-08 13:40:32 +0100
  • d63086d7e3 Enabled output file, this time fo' real. dehnert 2015-02-07 02:46:48 +0100
  • 8fa67a6158 Enabled output file generation. dehnert 2015-02-07 02:40:03 +0100
  • 0f9c753778 Fixed Windows build error David_Korzeniewski 2015-02-06 16:41:45 +0100
  • 84f8a41302 More tests adapted, decreased verbosity of TopologicalValueIterationNondeterministicLinearEquationSolver David_Korzeniewski 2015-02-06 16:20:37 +0100
  • 9d95a0bc57 Merge branch 'master' into parametricSystems dehnert 2015-02-03 16:45:47 +0100
  • 4f9b5406fe Fixed simplification of unary expressions. dehnert 2015-02-03 15:13:36 +0100
  • 36e632c43c Merged master into parametricSystems. dehnert 2015-02-03 13:10:13 +0100
  • 0a59f7a7ef Fixed a bug that sometimes prevented transition rewards from being built. dehnert 2015-02-03 13:03:29 +0100
  • 40e148d9a4 Added overall performance measurements. dehnert 2015-02-03 06:25:55 +0100
  • 6585e56768 Changed program header. dehnert 2015-02-03 05:44:39 +0100
  • b288cf7abb Added overall timer to pstorm. dehnert 2015-02-03 05:39:09 +0100
  • 55e9f13cbd Merge branch 'master' into parametricSystems dehnert 2015-02-03 05:32:35 +0100
  • 8bc646ccb8 Simplification of program when substituting constants. dehnert 2015-02-03 05:31:52 +0100
  • 90958bb018 cuda library was not linked to tests, for now using static libraries as dlls don't work for non obvious reasons David_Korzeniewski 2015-02-02 18:51:02 +0100
  • 8b4309e53c Adapted first test to new interface. Test passes. David_Korzeniewski 2015-02-02 18:49:23 +0100
  • 072b7d0e1a Added performance statistics for model building. dehnert 2015-02-02 18:05:19 +0100
  • d60663d4b8 Merge branch 'master' into parametricSystems dehnert 2015-02-02 14:47:15 +0100
  • 7a55fe9208 Fixed some issues related to conditional probs. dehnert 2015-02-02 14:46:48 +0100
  • cf6b7b09fd Merged master into parametricSystems. dehnert 2015-02-02 13:19:37 +0100
  • 5343ea622a Fixed bug concerning conditional probabilities. dehnert 2015-02-02 13:16:53 +0100
  • 8fa405d492 Merge branch 'parametricSystems' of https://sselab.de/lab9/private/git/storm into parametricSystems dehnert 2015-02-02 09:55:27 +0100
  • a371d0eb04 Fixed assertion. dehnert 2015-02-02 09:28:16 +0100
  • f5a9ebe2f7 And another minor bug. dehnert 2015-02-01 23:52:40 +0100
  • 5e3eab8058 Fixed another bug dehnert 2015-02-01 23:43:59 +0100
  • adc1aa1442 Corrected an assertion. dehnert 2015-02-01 23:39:11 +0100
  • e211e269d4 Fix for the Gurobi inclusion. PBerger 2015-02-01 03:46:26 +0100
  • f7adf54be3 Added A FindGurobi file for CMake. Adapted build process to use the new file to support all version of the library (upgrading to 6.0 breaks everything). PBerger 2015-02-01 03:30:01 +0100
  • 0d8c9991c3 Merge branch 'master' into parametricSystems dehnert 2015-01-31 14:25:19 +0100
  • f49d89144e Fixed issue that could cause wrong models to be generated. dehnert 2015-01-31 14:24:55 +0100
  • a41a2d166e Merge branch 'master' into parametricSystems dehnert 2015-01-30 23:27:03 +0100
  • 19bc5eb995 Merge master into parametricSystems. dehnert 2015-01-30 23:26:45 +0100
  • 2dae5862c8 Small fix to bisimulation options. dehnert 2015-01-30 23:26:29 +0100
  • ed4f1bb7cf Added the possibility to build the bisimulation options from a formula in the sense that it automatically picks suitable settings for the formula. dehnert 2015-01-30 22:59:26 +0100
  • 8066bb6637 Small fix for test. David_Korzeniewski 2015-01-30 17:44:57 +0100
  • 4952306092 Worked on making bisimulation decomposition a bit easier to use. dehnert 2015-01-30 17:43:56 +0100
  • 3748905bcf Fixes and test refactoring for TopologicalValueIterationMdpPrctlModelChecker David_Korzeniewski 2015-01-30 17:23:33 +0100
  • 84eabdac8c Merge branch 'master' into parametricSystems dehnert 2015-01-30 11:34:59 +0100
  • 78bb94ff20 Merged master in parametricSystems. dehnert 2015-01-30 11:34:48 +0100
  • 700703140f Fixed minor issue. dehnert 2015-01-30 11:33:48 +0100
  • 9cf82bcd98 Added conversion from transition-based rewards to state-based rewards to enable proper treatment in bisimulation minimization dehnert 2015-01-30 10:59:11 +0100
  • 8f7e21c108 Small hack that prevents creating atomic propositions like 'true'. This will be solved differently in master soon. dehnert 2015-01-30 09:52:22 +0100
  • 1b568a8691 Fixed some things. dehnert 2015-01-29 21:48:28 +0100
  • cc7d44dd15 Added proper canHandle method to propositional model checker. dehnert 2015-01-29 21:19:49 +0100
  • b5f907d99d Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation. dehnert 2015-01-29 20:55:32 +0100
  • ee4c961cc9 fixes for compile errors. target "storm" builds without errors David_Korzeniewski 2015-01-29 19:44:58 +0100
  • 547e33f0f4 Merge branch 'master' into cuda_integration David_Korzeniewski 2015-01-29 19:02:55 +0100
  • 7e847e420b (Hopefully) successfully merged the changes of master into parametricSystems. dehnert 2015-01-29 18:20:48 +0100
  • d70f65ae7f Merge branch 'master' into parametricSystems dehnert 2015-01-29 18:20:21 +0100
  • 18f314d7c6 Some more bugfixes. Damn you, clang on Mac OS! dehnert 2015-01-29 18:19:09 +0100
  • 3766c6b675 Merge branch 'master' into parametricSystems dehnert 2015-01-29 18:14:13 +0100
  • 64fd308713 Another minor bugfix in the formula classes. dehnert 2015-01-29 18:13:51 +0100
  • fe7b6d1808 Merge branch 'master' into parametricSystems dehnert 2015-01-29 18:06:26 +0100
  • f5b7554590 Minor bugfix for conditional probability computation. dehnert 2015-01-29 18:06:03 +0100
  • 71e0ac470a Merge branch 'master' into parametricSystems dehnert 2015-01-29 17:47:07 +0100
  • 1fb8d72a30 Merged master in parametricSystems. dehnert 2015-01-29 17:47:06 +0100
  • 98efde80f7 Fixed some compile issues (and some other issues). dehnert 2015-01-29 17:44:43 +0100
  • 3f724e6fe2 Started merging master into parametric systems. dehnert 2015-01-29 15:58:28 +0100
  • abc222fc31 Fixed some compilation errors. dehnert 2015-01-29 15:56:39 +0100
  • ab36c5fb0d Workarounds for more Windows quirks. Compiles but tests crash. David_Korzeniewski 2015-01-29 15:04:02 +0100
  • 7da35af0bb Some compile errors on Windows fixed, some still persist. David_Korzeniewski 2015-01-29 12:35:41 +0100
  • f0a2db6485 Enabled checking formula nodes that contain an expression in the variable of the program. dehnert 2015-01-28 19:07:03 +0100
  • 92aa2607a0 The labels of the models are now only built if no property was given or the given property contains the label. dehnert 2015-01-28 19:00:18 +0100
  • ee7b591db1 Some work on cli. dehnert 2015-01-28 17:23:03 +0100
  • c85df2cd74 Conditional Probabilities working. Included two tests. dehnert 2015-01-28 12:03:09 +0100
  • 6bc6753e90 Some work on conditional probs. Not yet working. dehnert 2015-01-27 22:22:06 +0100
  • ae2b950e86 Fixed some issue in model builder. dehnert 2015-01-27 16:55:57 +0100
  • 9e8d8a2c27 Fixed wrong calculation of reachability rewards in state-elimination-based model checker. dehnert 2015-01-27 14:15:56 +0100
  • 89fc5be1ab Fixed some things and wrote tests for elimination-based DTMC modelchecker. They fail: apparently rewards are not correctly computed in some cases. dehnert 2015-01-27 08:50:32 +0100
  • 8a4706d9c9 A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated. dehnert 2015-01-26 17:54:36 +0100
  • b60c5ffdc0 Fixed a lot of tests, improved some things here and there. dehnert 2015-01-25 22:52:41 +0100
  • d0917f033c Adapted Markov automaton model checker to new formula classes. dehnert 2015-01-25 18:39:18 +0100
  • 89df9621a9 MDP model checker works again. dehnert 2015-01-25 16:48:23 +0100
  • 9026aa9ac9 Adapted first model checker to the new properties. dehnert 2015-01-24 21:05:42 +0100
  • 01d7bce205 Fixed some test. dehnert 2015-01-24 10:35:00 +0100
  • f673dccd76 Formula parser works again. Tests adapted. dehnert 2015-01-23 21:57:12 +0100
  • 1699732dce More work on logic classes. dehnert 2015-01-23 17:11:01 +0100
  • 4c9d6ccfc5 Removed actions and filters and old logic classes. dehnert 2015-01-23 13:00:51 +0100
  • 320641e597 Started working on modified property classes. dehnert 2015-01-22 21:52:14 +0100
  • 447285d6dd Fixed merge error David_Korzeniewski 2015-01-22 20:11:31 +0100
  • 2279710443 Directly use Matrix with Decomposition David_Korzeniewski 2015-01-22 19:26:44 +0100
  • 3e4495cad0 small fixes David_Korzeniewski 2015-01-22 18:58:24 +0100
  • e51c3b9f44 Conditional probabilities work for brp model from the paper by Baier et al. dehnert 2015-01-22 14:28:48 +0100
  • d991b4a26a Worked some more on conditional probabilities. dehnert 2015-01-21 19:47:29 +0100
  • 70e45d43f1 Started on computing conditional probabilities for parametric systems. dehnert 2015-01-21 17:56:40 +0100
  • 78d3a392a5 Created settings module for TopologicalValueIterationNondeterministicLinearEquationSolver and integrated that with the solver. David_Korzeniewski 2015-01-19 16:14:39 +0100
  • 01bd1fbc76 Model building works again for parametric systems. dehnert 2015-01-17 12:22:49 +0100
  • 12e6fac968 Started making generation of parametric models work again. dehnert 2015-01-16 17:00:10 +0100
  • 217ade7cc6 Merged master into parametricSystems and added/reverted certain things on the way to make the tests and everything work again. dehnert 2015-01-16 15:41:45 +0100
  • 00861a7479 Loosened the restriction to always require GMP a bit. dehnert 2015-01-16 13:31:41 +0100
  • fafeffe138 Merge branch 'master' into ExpressionModifications dehnert 2015-01-15 21:30:15 +0100
  • 2bd0e2e377 Improved performance of explicit model generation a bit. dehnert 2015-01-15 21:27:00 +0100
  • 91e177028d Started refactoring explicit model generator of PRISM models dehnert 2015-01-15 17:53:52 +0100