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

Commit Graph

  • 53f2fdf51e Changed implementation of LRA to be weighted with the probability to reach BSCCs instead of choosing min/max David_Korzeniewski 2015-04-10 16:08:59 +0200
  • 869f8c50c9 Fixed some minor CTMC-related bugs. dehnert 2015-04-10 11:49:20 +0200
  • a448cd8973 Calculating steady state using standard equation system for eigenvectors, removed all-in-one matrix transformation (nicer looking code) David_Korzeniewski 2015-04-09 21:57:00 +0200
  • be66ef2751 Finalized hybrid CTMC model checker. dehnert 2015-04-09 17:27:32 +0200
  • 52a8c324a5 make storm compile when carl is not available added settings for smt-lib solver TimQu 2015-04-09 16:12:12 +0200
  • 1df48d318a Merge branch 'master' into TimParamSysAndSMT TimQu 2015-04-08 23:47:27 +0200
  • 8868a50864 Removed superfluous code. dehnert 2015-04-08 23:11:06 +0200
  • e1761fa774 Enabled hybrid CTMC model checker in cli. Further work on hybrid CTMC model checker (not yet working). Fixed some minor issues in sparse CTMC model checker. dehnert 2015-04-08 23:08:59 +0200
  • b395b1292e started Smtlib Solver interface and some 'prototypy' method to check parameter regions TimQu 2015-04-08 22:57:42 +0200
  • 76b99a5515 Commit to switch workplace. dehnert 2015-04-08 16:55:58 +0200
  • c1917ce6d9 Finalized hybrid DTMC model checker. It now passes its tests. dehnert 2015-04-07 17:28:51 +0200
  • 04c1d51313 intermediate commit, copied transpose and get submatrix code over and started adapting it. David_Korzeniewski 2015-04-07 13:59:39 +0200
  • 72166bed37 Created new class for storing hybrid check results (symbolic as well as explicit parts) and the surrounding functionality. dehnert 2015-04-06 19:41:46 +0200
  • 3b4dca1a03 Improved Jacobi method a bit. dehnert 2015-04-03 16:12:11 +0200
  • 06bfc17ec6 Started making hybrid (dd/sparse) model checking work. dehnert 2015-04-02 17:06:29 +0200
  • 907e3512c0 Fixed a potential bug in the ODD generation and it now uses hash maps instead of regular maps. dehnert 2015-04-01 20:15:01 +0200
  • e83d191be3 ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs). dehnert 2015-04-01 19:44:48 +0200
  • c8d8f75a10 Working on ODD generation for BDDs (not yet working). dehnert 2015-04-01 16:12:19 +0200
  • d787b80fec CTMC examples now build properly using the DD-based model generator. dehnert 2015-03-31 20:01:20 +0200
  • 9d66f5128e Further work on symbolic CTMC generation. dehnert 2015-03-31 15:25:41 +0200
  • da0582405d Raise warning/error if synchronizing Markovian commands are detected. dehnert 2015-03-31 15:07:33 +0200
  • 8f4a4397e0 Started working on Markovian commands in PRISM programs. dehnert 2015-03-31 14:56:43 +0200
  • 913aa83dbc Removed ltl2dstar. dehnert 2015-03-31 09:54:17 +0200
  • 60701cebdb ADDs and BDDs are no longer mixed in the abstraction layer. dehnert 2015-03-27 22:48:04 +0100
  • 5bd6ca606f Started refactoring DD abstraction layer. dehnert 2015-03-27 14:56:38 +0100
  • eb5d4100a6 Renamed Nondeterminstic equation solver as this name is more than misleading. dehnert 2015-03-27 09:45:48 +0100
  • fda3c8a6df Made CTMC model checker work correctly again. dehnert 2015-03-24 21:55:28 +0100
  • e8dd83c4da Further work on performance of CTMC model checker. dehnert 2015-03-24 18:03:23 +0100
  • 1990567b84 Started to improve performance of sparse CTMC model checker. dehnert 2015-03-23 22:24:13 +0100
  • d545fac471 Restructured solvers a bit: they now get the matrix upon construction and the model checkers use factories to retrieve solvers. dehnert 2015-03-23 17:11:16 +0100
  • f8c867300b Optimized time-bounded reachability of CTMCs a bit. dehnert 2015-03-22 19:27:54 +0100
  • 49bed497b0 Fixed a model building problem. Included checking of reward properties on CTMCs and wrote tests for it. dehnert 2015-03-22 15:47:57 +0100
  • b096180de8 LRA on DTMCs implemented David_Korzeniewski 2015-03-20 17:15:49 +0100
  • a851fad65d More work on reward properties for CTMCs. dehnert 2015-03-20 16:55:47 +0100
  • c84751f632 Started working on reward properties for CTMCs. dehnert 2015-03-20 15:09:29 +0100
  • 799cbce775 Added function tests for CTMC creation and time-bounded reachability. dehnert 2015-03-20 12:36:32 +0100
  • ccc60ef145 Removed a lot of debug output. dehnert 2015-03-19 18:34:15 +0100
  • 7fa6b568b4 Currently debugging the computation of transient probabilities in CTMCs. dehnert 2015-03-19 17:53:26 +0100
  • 25739720e0 Finished implementation of LRA for MPDs. David_Korzeniewski 2015-03-19 15:33:41 +0100
  • c6521221bd Added tiny text example for ctmc mc. dehnert 2015-03-18 19:49:37 +0100
  • 65bf06dd50 Further steps towards CTMC model checking. dehnert 2015-03-18 19:48:04 +0100
  • 6ffd5cea88 Further work on CTMC model checking. dehnert 2015-03-18 16:09:50 +0100
  • 9d4ded66b2 Started implementing CTMC model checker. dehnert 2015-03-18 11:52:45 +0100
  • cde9786dfa Made Fox-Glynn (hopefully) work. dehnert 2015-03-17 22:11:17 +0100
  • e9d677c792 Further work on MTBDD-based mc. dehnert 2015-03-17 19:00:56 +0100
  • 3434405cf4 Started working on CTMC mc. dehnert 2015-03-17 18:13:30 +0100
  • bc1a97e38a Merge branch 'master' into LRA_for_dtmc_mdp David_Korzeniewski 2015-03-17 17:51:28 +0100
  • 7e672cddd9 Started implementation of LRA for MDPs David_Korzeniewski 2015-03-17 17:50:21 +0100
  • 96539f41a5 Fixed simplification of division: division expressions must not be simplified, because it is not (yet) clear whether integer division or floating point division is to be used. dehnert 2015-03-17 12:40:59 +0100
  • 5bbd85c379 Some bugfixes. dehnert 2015-03-17 10:39:13 +0100
  • a44a3554c8 Fixed minimal command counterexample generation. dehnert 2015-03-16 22:47:09 +0100
  • c7f262bf15 Merge branch 'mtbddIntegration' of https://sselab.de/lab9/private/git/storm into mtbddIntegration dehnert 2015-03-16 20:20:18 +0100
  • 00e7121bc4 some work towards BDD-based mc. dehnert 2015-03-16 20:20:15 +0100
  • 546e047b8d Fixed a bug that prevented correct comparison with bounds in formulas. dehnert 2015-03-16 17:40:11 +0100
  • 3fd62bc697 More work on MTBDD-based mc. dehnert 2015-03-16 17:38:57 +0100
  • 0c2080f220 Added tests for sparse Prob0/1 to functional tests dehnert 2015-02-26 18:59:30 +0100
  • 81100c7afd debugged and added more tests for prob0/1 for MDPs using BDDs dehnert 2015-02-26 18:41:33 +0100
  • c70d93f4d3 Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed. dehnert 2015-02-26 17:38:13 +0100
  • 7e14dc031b Reverted the last commit. The flag is there for performance reasons and there is no reason why it shouldn't work that way. dehnert 2015-02-26 13:35:10 +0100
  • 97936cbd8e Found a fix for a bug causing the functional tests to segfault at DeterministicModelBisimulationDecomposition.Die. masawei 2015-02-26 13:25:18 +0100
  • 923007cdc3 Merge branch 'master' into mtbddIntegration dehnert 2015-02-25 17:52:09 +0100
  • bda8d63b3b Merge master into mtbddIntegration. dehnert 2015-02-25 16:12:35 +0100
  • 7d2d1cac55 Functional Testing Suite now prints a note if not all optional dependencies were included in the build. David_Korzeniewski 2015-02-25 15:18:40 +0100
  • 95d5ebbb7d Updated build instructions with list of tested compilers and some new dependencies, but it still looks partially outdated. David_Korzeniewski 2015-02-25 15:15:56 +0100
  • 1a1906f811 Added functional tests for DD-based and sparse computation of states with prob 0 and 1. dehnert 2015-02-24 21:57:47 +0100
  • c8007876ae Symbolic models can now be built from the command line. dehnert 2015-02-24 17:01:18 +0100
  • 239caf57eb Added symbolic models and made DD-based model generator build the correct instances. dehnert 2015-02-24 15:50:11 +0100
  • 8a906038f6 Added reward model generation for DD-based model builder. dehnert 2015-02-23 18:49:07 +0100
  • 7c2f60175e Intermediate commit: fixed parsing bug and started reward generation (DD). dehnert 2015-02-23 17:41:34 +0100
  • f0b174b756 Fixed performance tests. dehnert 2015-02-20 17:58:10 +0100
  • a1dae8849e Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented. dehnert 2015-02-20 17:38:39 +0100
  • 4dc69dd6f5 Fixed performance tests, and again things concerning templates I never heard of before. David_Korzeniewski 2015-02-20 17:36:24 +0100
  • 7515ca5293 Fixed compile errors caused by parts of the c++ standard I've never heard of before... David_Korzeniewski 2015-02-20 17:01:36 +0100
  • 8ebc0e4640 Final touches on cuda nondeterministic linear equation solver & modelchecker David_Korzeniewski 2015-02-20 15:54:43 +0100
  • b623384dda Fixed merge errors and adapted to changes in master David_Korzeniewski 2015-02-20 12:49:34 +0100
  • 3936470b11 Merge branch 'master' into cuda_integration David_Korzeniewski 2015-02-20 12:25:04 +0100
  • ea2e616196 All tests for CUDA based TopologicalValueIterationMdpPrctlModelChecker passing on Windows. David_Korzeniewski 2015-02-19 18:01:03 +0100
  • 706ea56963 Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster. dehnert 2015-02-19 17:27:07 +0100
  • e79233bd7b Added check in PRISM program that prevents global varibles from written in possibly synchronizing commands. dehnert 2015-02-19 09:02:51 +0100
  • 3977cafe73 Extended DD-based model building to also build the MDP models of our benchmark suite. Added (MDP) tests for DD-based model building and explicit model building. dehnert 2015-02-18 22:11:00 +0100
  • 8c1870eb54 Intermediate commit. dehnert 2015-02-18 17:08:33 +0100
  • 0f0baf61a4 Made DD-based model construction work for all DTMC benchmarks we have. Included tests for both DD-based and excplicit model generation from PRISM models. dehnert 2015-02-17 20:06:28 +0100
  • b3d18c2367 Enabled probabilities depending on source state variables. dehnert 2015-02-16 19:55:30 +0100
  • 7d1829aefa More work on DD-based model generation. dehnert 2015-02-16 19:40:25 +0100
  • e58d38fadf More work on integrating DD-based model building. dehnert 2015-02-15 20:58:59 +0100
  • 6347e19da8 Intermediate commit: integrating MTBDD model generation/model checking to main tool. dehnert 2015-02-13 17:27:38 +0100
  • c3c83fbe4f Fixed some compilation errors. dehnert 2015-02-13 11:34:05 +0100
  • e89e089754 Removed parametric main files. dehnert 2015-02-13 10:30:50 +0100
  • f0b591be77 Further work on reintegrating parametric model checking into main executable. dehnert 2015-02-12 23:05:39 +0100
  • 53b77e673b Fixed a minor issue. dehnert 2015-02-12 19:27:33 +0100
  • 5794bbea56 Made some adaptions to make parametric model checking work in the main executable. dehnert 2015-02-12 18:52:37 +0100
  • caf8b57b60 Started integrating parametric model checking in regular tool. dehnert 2015-02-12 15:19:04 +0100
  • 0a2d079c3a Merge master in parametricSystems. dehnert 2015-02-12 13:14:46 +0100
  • 56ea5fca14 Included move-construction and move-assignment for partition. dehnert 2015-02-11 14:40:18 +0100
  • 00ddce497d corrected identifier name. David_Korzeniewski 2015-02-10 23:20:15 +0100
  • 4b44e625d0 Adapted Death-Tests in BitVectorTest.cpp to return codes upon assertion failure on Windows and deactivate them everywhere if the macro NDEBUG is defined (as that disables assertions) David_Korzeniewski 2015-02-10 23:04:18 +0100
  • e41922347d Adapted ExpressionTest.cpp to weird behavior of windows when using temporary shared_ptr in make_pair in initializer_list. David_Korzeniewski 2015-02-10 19:09:46 +0100
  • 07ddaa314c User declared move constructor and move assignment, as they are currently required to ensure pointer validity. David_Korzeniewski 2015-02-10 17:12:31 +0100
  • f5e383722f Fixed use of uninitialized value. Deleted assignment operators for classes derived from BaseExpression. dehnert 2015-02-10 14:49:29 +0100
  • 8b1a4b4e52 Quickfix s.t. we have a defined index and don't dereference end() which is bad David_Korzeniewski 2015-02-10 13:24:21 +0100