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

Commit Graph

  • fc45cdb238 Added tests for deterministic models i.e. DeterministicModelParserTest and DeterministicSparseTransitionParserTest masawei 2014-02-26 17:15:23 +0100
  • e452d58ed0 Fixed wrong parameter name for unix systems. fp893004 2014-02-26 14:38:44 +0100
  • df2e65b667 Added a test for the AutoParser. masawei 2014-02-26 13:19:07 +0100
  • 3e44d88958 Fixed a bug in the FindCUDA.cmake file on the client side PBerger 2014-02-26 04:44:48 +0100
  • d5828043de Added first signs of the CUDA Extension for Storm. PBerger 2014-02-26 04:25:34 +0100
  • af650b6666 Removed debug outputs from the TopologicalValueIterationNondeterministicLinearEquationSolver Fixed the topo tests, since the comparison values are a bit off for this solver PBerger 2014-02-25 03:50:24 +0100
  • a4ae226e57 Removed debug output from our debugging session PBerger 2014-02-24 19:59:05 +0100
  • f049a9f0af Bugfix for topological equation solver. dehnert 2014-02-24 16:24:48 +0100
  • 19ca7bedaa Added explicit casts to C-style casts PBerger 2014-02-24 04:44:49 +0100
  • 5b1513e9e5 Fixed issues with unused but named variables. PBerger 2014-02-24 04:43:36 +0100
  • 98b0bcf187 Reimplemented the TopologicalValueIterationNondeterministicLinearEquationSolver with splitting into submatrices. Added a dtmc example for tests with the StronglyConnectedComponentDecomposition. PBerger 2014-02-24 04:43:07 +0100
  • b7fae16928 Fixed a missing transition in the scc example PBerger 2014-02-12 16:36:50 +0100
  • 17d9df1ac7 Some fixes to make the branch compile with clang. dehnert 2014-02-12 15:26:49 +0100
  • 3052b19c58 Created a "real" scc example. Modified the TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to show the crash when not using TBB. PBerger 2014-02-12 02:56:42 +0100
  • 4eef3b0d57 Added an example for SCC related testing which will change soon Removed unnecessary code from the TopologicalValueIterationMdpPrctlModelChecker.h Fixed Bugs in graph.h (changes from Sparse Matrix Iterator, it didnt even compile anymore! Unused Code HAUNTS us) PBerger 2014-02-12 02:33:27 +0100
  • 07465f604a Refactored and added to the test for the AtomicPropositionLabelParser. masawei 2014-02-10 18:26:12 +0100
  • 57b6208eee Added a pseudo model which can be constructed from only a matrix to look and behave like a model for use in Decomposition classes PBerger 2014-02-10 00:42:59 +0100
  • 52f130ea5c Commenting and cleanup. masawei 2014-02-07 21:19:50 +0100
  • 6e63e1c296 Minor bugfix. dehnert 2014-02-03 15:41:02 +0100
  • 64891af785 Trying to refurbish the TopologicalValueIterationMdpPrctlModelChecker PBerger 2014-02-03 04:21:35 +0100
  • fcc17b800b Reworked SIGALRM handling to work under windows PBerger 2014-02-03 01:49:11 +0100
  • 9d1e53cff9 Added a missing include for uint_fast64_t to be recognized as a type PBerger 2014-02-03 01:48:36 +0100
  • deb9cb1e91 Duplicated the constructor of SparseMarkovAutomatonCslModelChecker to work around a bug in C++ with nested template argument deductions PBerger 2014-02-03 01:48:04 +0100
  • b9a4faea09 Removed unused named variables in MILPMinimalLabelSetGenerator.h PBerger 2014-02-03 01:47:17 +0100
  • fe7afc727f Second part of the refactoring of Parser.cpp/.h masawei 2014-01-30 10:29:57 +0100
  • 8fabc2064a Added property files for WLAN example. dehnert 2014-01-29 11:41:18 +0100
  • f0728db91d Added property files for WLAN example. dehnert 2014-01-29 11:40:08 +0100
  • 6b9fd8b331 Added timeout flag so no external tool is needed for aborting a computation. dehnert 2014-01-26 12:59:37 +0100
  • 0287fdc4a2 Added some csma examples of different sizes. dehnert 2014-01-25 19:13:29 +0100
  • 55187c3350 Moved to new sigaction API to more reliably catch signals. dehnert 2014-01-25 10:34:52 +0100
  • 486e99d6ae Added signal handler for SIGTERM. Introduced delayed update for LP solvers to reduce overhead. dehnert 2014-01-24 21:04:09 +0100
  • a52419652d Fixed a bug: formulas are now handled (more) correctly. Added some WLAN examples. dehnert 2014-01-24 21:00:37 +0100
  • 538f911283 First part of the refactoring of Parser.h/.cpp masawei 2014-01-22 18:10:23 +0100
  • 3ac03b9b5b Merge branch 'refactureParsers' of https://sselab.de/lab9/private/git/storm into refactureParsers masawei 2014-01-21 01:11:14 +0100
  • 15d13bc06d Refactored the AutoParser. masawei 2014-01-21 00:58:29 +0100
  • 46e783c981 Refactored AtomicPropositionLabelingParser. masawei 2014-01-14 01:48:04 +0100
  • c279c693e5 Refactored NondeterministicModelParser.h/.cpp masawei 2014-01-08 00:06:04 +0100
  • cc71a002f4 Refactored NondeterministicSparseTransitionParser.h/.cpp. masawei 2014-01-02 16:46:53 +0100
  • 8adee3629b Removed duplicated code in DeterministicSparseTransitionParser while still keeping it readable and the interface intact. masawei 2014-01-02 01:30:00 +0100
  • 4245b3c4e3 Changed parsers to be compilable again. masawei 2014-01-01 19:15:37 +0100
  • 8e5847ae19 Merge branch 'master' into refactureParsers masawei 2013-12-20 17:07:04 +0100
  • 1f71bb5240 Refactored the DeterministicModelParser. masawei 2013-12-20 16:35:23 +0100
  • 310a840ad5 Removed move-version of translation from SparseMatrix to gmm++, because moving is not really possible considering the different types. dehnert 2013-12-18 15:10:21 +0100
  • 8cdf128202 Fixed some performane tests to work with the relative convergence criterion as this is now the default. dehnert 2013-12-18 13:40:17 +0100
  • f946121b95 Fixed an incorrect type issue in the GmmxxAdapter. dehnert 2013-12-18 11:53:23 +0100
  • 42708a6d21 Added utility header for all parts that use std::swap. dehnert 2013-12-18 11:26:15 +0100
  • ef5eb19e9c Corrected test formulation in case StoRM was built without support for a given LP solver. dehnert 2013-12-17 11:57:32 +0100
  • 36fb44e206 Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests. dehnert 2013-12-17 11:39:50 +0100
  • 514aace4fd Added function tests for both glpk- and Gurobi-based LP solver implementations. Found and fixed some bugs while doing this. dehnert 2013-12-16 21:28:08 +0100
  • c5985be437 Minor fixes for GlpkLpSolver. dehnert 2013-12-16 17:25:51 +0100
  • 8ebd924ca6 Further work on refactoring solvers: cleaned LP solver interface a bit and adapted glpk- and Gurobi-based implementations of the interface. dehnert 2013-12-16 15:43:24 +0100
  • 588a4b60b6 Refactored linear equation solvers and nondeterministic linear equation solvers. Added functional tests for both. dehnert 2013-12-15 23:05:20 +0100
  • 3598b7195e Refactored the DeterministicSparseTransitionParser. masawei 2013-12-14 16:45:24 +0100
  • ae270cc917 Added two more example files that form a Markov automaton. dehnert 2013-12-14 00:14:13 +0100
  • 79730379e4 Started refactoring the linear equation system solvers. dehnert 2013-12-14 00:13:46 +0100
  • ee0026e0e6 Fixed minor bug in Markov automata time-bounded reachability. dehnert 2013-12-13 17:00:51 +0100
  • efb244a447 Added functional tests for scheduler classes. dehnert 2013-12-12 21:10:24 +0100
  • f79329bd9d Fixed SCC decomposition. Added functional tests for SCC decomposition. dehnert 2013-12-12 16:53:54 +0100
  • e80bb0caa5 Added functional tests for MEC decomposition. dehnert 2013-12-12 15:21:26 +0100
  • f32853b6aa Beautified remaining storage classes a bit. dehnert 2013-12-12 14:37:30 +0100
  • 35d16a1191 Replaced VectorSet bei boost::container::flat_set, which does essentially the same. Fixed a bug in sparse matrix creation. dehnert 2013-12-11 22:40:47 +0100
  • f684ce7799 Removed obsolete constructors of sparse matrix class as the new matrix builder is supposed to be used anyway. Fixed some minor issues. dehnert 2013-12-11 16:43:32 +0100
  • 5e12a65d67 Adapted performance-critical iterations in graph utility to the iterator formulation with less overhead. dehnert 2013-12-11 15:49:11 +0100
  • 41cb1a8227 Merge branch 'master' into storageRefactoring dehnert 2013-12-11 15:30:50 +0100
  • f2670883a8 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2013-12-11 15:24:47 +0100
  • 72531bcebb Added proper TBB multi-threading to all operation relevant to model checking MDPs. dehnert 2013-12-11 15:24:22 +0100
  • d723272cc1 Added some performance tests for matrix-vector multiplication. dehnert 2013-12-11 10:31:50 +0100
  • cdc369b96a Temporarily removed the detection of the repository version of TBB from CMakeLists.txt. Corrected TBB sparse matrix-vector multiplication. Added TBB parallel vector addition. dehnert 2013-12-10 21:35:37 +0100
  • 81cf0e2b22 Added SparseMatrixBuilder class that actually builds the matrices. A call to build() will then generate the matrix. This eliminates superfluous checks in the matrix that slowed down performance. dehnert 2013-12-10 17:38:47 +0100
  • cf2b84b281 Further work on iterators for sparse matrix. dehnert 2013-12-10 13:49:47 +0100
  • ab5b5be1ac First step towards pair-based column and value storage in sparse matrix. dehnert 2013-12-09 20:52:30 +0100
  • 91125c3c6d Fixed build errors on Windows David_Korzeniewski 2013-12-09 18:18:24 +0100
  • e08b61b9f7 Added functional and performance tests for sparse matrix. dehnert 2013-12-09 15:45:10 +0100
  • 97fb2f9750 All tests working with (partially) new sparse matrix implementation/interface. dehnert 2013-12-08 20:28:33 +0100
  • f8566e9dc2 A thousand things. - More tests. - Changed SparseStateRewardParser to a static class - Added comments here and there - Some reformatting. - Fixed some warnings. - Eliminated some unnecessary includes. - ... masawei 2013-12-08 00:49:56 +0100
  • 9ce47989ed The MA transition parser is now able to handle arbitrary labels. masawei 2013-12-07 15:45:33 +0100
  • a271e5ce63 Working towards making every (remaining) test work dehnert 2013-12-07 00:39:35 +0100
  • a26f63be30 Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix. dehnert 2013-12-06 18:58:35 +0100
  • ef041982b5 Further work on sparse matrix implementation. dehnert 2013-12-06 11:23:29 +0100
  • 4376708a46 Further maintenance work on sparse matrix implementation. dehnert 2013-12-05 21:11:31 +0100
  • 8a47d03cf7 Started to rework the interface of the sparse matrix class. dehnert 2013-12-05 17:35:26 +0100
  • 84bd5f3b40 Renamed ConstTemplates to constants. Removed all calls to constGetZero, constGetOne and constGetInfinity by the new names. Created performance test for bit vector iteration. dehnert 2013-12-05 14:44:20 +0100
  • d5cadc0f4b Finalized interface of bit vector. Added unit tests for all methods of the bit vector. dehnert 2013-12-05 14:09:06 +0100
  • 30322ec57d Now officially made the iterator over bit vectors an input iterator so that it can be used for constructing STL containers and other containers. dehnert 2013-12-05 00:09:38 +0100
  • a7c8c3a1a3 Added checklist file for refactoring classes. dehnert 2013-12-04 17:00:00 +0100
  • 07fbff7a07 Started refactoring bit vector class. dehnert 2013-12-04 16:57:03 +0100
  • 716f3366fc Added configuration file for astyle (a code-formatting tool) that is tailored to our formatting style. dehnert 2013-12-04 10:30:22 +0100
  • cb870c28c7 Began testing of the MarkovAutomatonSparseTransitionParser to identify inflexibilities or bugs. - Noticed to my astonishment that seemingly arbitrary use of whitespaces (as long as each transition is in its own line) is no problem for the parser. - As predicted, handling of action labels of arbitrary length especially such starting with an '!' is not supported. masawei 2013-12-03 23:49:21 +0100
  • e2cec086a3 Merge branch 'imca' dehnert 2013-12-03 22:30:08 +0100
  • c336fd7ff8 Minor fixes for implementation of GlpkLpSolver if glpk is unavailable. dehnert 2013-12-03 22:29:44 +0100
  • 344e1b6dd3 Enabled checking of some untimed properties on Markov automata. dehnert 2013-12-03 17:30:02 +0100
  • 3dab26463d Introduced precision for digitization-based techniques as a new parameter. dehnert 2013-12-02 17:48:14 +0100
  • ece4085a61 Another bugfix for matrix creation during LRA computation. dehnert 2013-12-02 17:28:18 +0100
  • fde78ad759 Bugfix for matrix creation in LRA computation. dehnert 2013-12-02 17:25:48 +0100
  • b3601782a9 Added Lp Solver class for glpk and added it as an option in CMakeLists.txt. dehnert 2013-12-02 17:06:09 +0100
  • 0a89d65f93 Started refactoring Markov automaton model checker. dehnert 2013-12-02 14:05:49 +0100
  • 18711c01a3 First working version of time-bounded reachability for Markov automata. dehnert 2013-12-01 20:08:48 +0100
  • 2ef0405104 Merge branch 'master' into imca dehnert 2013-11-30 21:38:07 +0100
  • dce43d78e7 Started implementation of time-bounded reachability of Markov automata. dehnert 2013-11-30 21:09:51 +0100
  • 175e852956 Resolved problems resulting from merge. - gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list but only an erase(iterator). This is in compliance with the c++11 draft N3337, which specifies the change from iterator to const_iterator only for "set, multiset, map [and] multimap" but not list. Therefore the constant list iterators were replaced by non constant iterators in MaximalEndComponentDecomposition and Vector set. The locations are marked with a FIXME, such that the const_iterator can be replaced back when gcc provides it. masawei 2013-11-30 20:33:59 +0100