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

Commit Graph

  • 6fde42850d fix for gcc 4.9 sjunges 2014-09-10 14:57:22 +0200
  • 9da54842b7 remove stray symbol sjunges 2014-09-10 11:52:22 +0200
  • fff4e61fc3 Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space. dehnert 2014-09-06 00:55:03 +0200
  • f767cfe844 Started to modify the matrix builder to be a bit smarter about preallocation. dehnert 2014-09-05 15:56:54 +0200
  • 05b8b942fb merge sjunges 2014-09-05 15:17:09 +0200
  • ac420f13d0 Fixed some warnings in various places. dehnert 2014-09-05 14:04:04 +0200
  • 72af8c7246 Added missing (but implicitly declared) template instance. PBerger 2014-09-04 23:48:10 +0200
  • ab58103555 Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values). dehnert 2014-09-04 21:20:42 +0200
  • 0d9ccde6af merge with master sjunges 2014-09-04 13:47:50 +0200
  • 01cefbb2c0 Modified the multiplication of a sparse matrix with a dense vector to only use the parallel version if available and the number of nonzero entries exceeds a certain threshold. dehnert 2014-09-01 11:04:02 +0200
  • 21eb9cb898 Merge branch 'master' into philippTopologicalRevival PBerger 2014-08-30 13:23:34 +0200
  • c8e05f7137 Added explicit template instance. PBerger 2014-08-30 13:09:14 +0200
  • d40573640f Dropped our current Tarjan-implementation in favour of the path-based algorithm by Gabow (and others) as this seems to perform a lot better (at when comparing our implementations). dehnert 2014-08-30 11:20:29 +0200
  • 0c305825f3 Merge branch 'master' into philippTopologicalRevival PBerger 2014-08-30 03:41:45 +0200
  • 59ca5fcdba Merge branch 'master' into philippTopologicalRevival PBerger 2014-08-30 03:38:20 +0200
  • 493f93a94b Added __restrict__ keyword to CUDA kernel. This should enhance compiler optimization. Refactored TopologicalValueIterationNondeterministicLinearEquationSolver to support "down-casting" to float. Added better timing output. PBerger 2014-08-30 03:32:55 +0200
  • 4f25312a6b Adapted SMT-based counterexample generator such that it works with the new property classes. dehnert 2014-08-29 18:36:43 +0200
  • 7f7ddc06e1 Removed two erronous keywords. masawei 2014-08-29 17:27:43 +0200
  • 5a0059d110 Commented out the SMTMinimalCommandSetGeneraator, again. masawei 2014-08-29 15:55:58 +0200
  • 4f5b0b5949 Merge branch 'refactorFormulas' masawei 2014-08-29 15:36:48 +0200
  • 52cfe9f02d Fixed some compile errors. masawei 2014-08-29 15:15:15 +0200
  • b84ef7bebc Merge branch 'master' into refactorFormulas masawei 2014-08-29 14:05:44 +0200
  • d75e32b83e Renames the folder formula to properties and the namespace property to properties. masawei 2014-08-29 13:16:56 +0200
  • 6b2b1e4d7b Finished the documentation of the formulas. masawei 2014-08-29 05:08:59 +0200
  • 71320239f1 Some debug output. PBerger 2014-08-21 14:27:00 +0200
  • ea427fcde1 Fixed include directories for CUDA Plugin in CMakeLists.txt Refactored all code related to the SPMV kernels to work with float. Wrote a test that determines whether the compiler uses 64bit boundary alignments on std::pairs of uint64 and float. Introduced functions that allow for conversions between different ValueTypes (e.g. from float to double and backwards). PBerger 2014-08-20 23:46:14 +0200
  • cbf1301e47 Small bugfix. dehnert 2014-08-18 12:23:01 +0200
  • 7f15f358c1 Removed the FormulaCheckers. masawei 2014-08-14 13:17:11 +0200
  • 532b0cf3ad Added function to test if a formula is a probability bounded reachability formula, i.e. conforms to the pattern P[<,<=,>,>=]p ([phi U, E] psi) where phi, psi are propositional formulas (consisting only of And, Or, Not and AP). masawei 2014-08-14 12:45:58 +0200
  • 27df78c2b0 Finished testing Ltl. masawei 2014-08-13 00:40:24 +0200
  • 57882db84e Fixed warnings about unused variables in PathBasedSubsystemGenerator and SMTMinimalCommandSetGenerator. Also some stuff with type conversions. PBerger 2014-08-13 00:28:50 +0200
  • 40a8fdd6e4 Merge branch 'refactorFormulas' of https://sselab.de/lab9/private/git/storm into refactorFormulas masawei 2014-08-13 00:06:41 +0200
  • 0a2a759932 Ltl testng. masawei 2014-08-13 00:06:10 +0200
  • a49991484c Fixed missing definitions for the current working directory. PBerger 2014-08-12 23:47:05 +0200
  • 3bc31e927d Added per-formula timing output. This is basically a picky merge from my CUDA branch. PBerger 2014-08-12 23:19:31 +0200
  • 94b2d45e05 Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp. PBerger 2014-08-12 23:14:02 +0200
  • 422a317407 Made the OptimalSCC algorithm MUCH faster. Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp. PBerger 2014-08-12 23:12:12 +0200
  • 4614eccccb Addendum to last commit: Forgot the files for the csl filter test. masawei 2014-08-12 02:27:30 +0200
  • 2687809591 Finished testing of Csl. masawei 2014-08-12 02:07:03 +0200
  • 33386f4c5f Changed the actions in the filters to be shared_ptr instead of raw pointers. This prevents memory leaks when a filter is destructed. masawei 2014-08-11 00:02:13 +0200
  • b7357c2cf9 Testing, noticed that vectors of pointers are not good. Changing that. masawei 2014-08-10 22:23:15 +0200
  • a39e9a821f Fixed a type error in TBB implementation. PBerger 2014-08-10 19:54:49 +0200
  • 7e77fbb6bb Some testing stuff. PBerger 2014-08-10 18:13:28 +0200
  • 4a1358fb79 Merge branch 'master' of https://sselab.de/lab9/private/git/storm into philippTopologicalRevival PBerger 2014-08-10 17:56:01 +0200
  • 73ddba5b29 Merged master, applied fixes. Added feedback from the cuda plugin and return of iteration count. PBerger 2014-08-10 17:48:14 +0200
  • 67cd9e58ba Merge branch 'master' of https://sselab.de/lab9/private/git/storm into philippTopologicalRevival PBerger 2014-08-10 15:51:50 +0200
  • 4ba45efd1c Merge branch 'parametricSystems' of https://sselab.de/lab9/private/git/storm into parametricSystems sjunges 2014-08-08 16:50:53 +0200
  • ff572c7f6f Sped up PRISM parser by letting it skip the actual command definitions in the first run (because only gathering constants, variables and formulas is important in this particular run). dehnert 2014-08-08 10:12:38 +0200
  • f485974187 Fixed (asynch) leader election to comply with our grammar. Added LOG_DEBUG macro. dehnert 2014-08-07 17:22:08 +0200
  • 1c4d7b9ef9 Some more testing. masawei 2014-08-07 15:34:03 +0200
  • 577e48f8bf Bugfix for the dimensions of some data of parsed Markov automata. dehnert 2014-08-03 22:50:51 +0200
  • 93a08538e3 Reverted debug change in test. dehnert 2014-08-02 19:18:51 +0200
  • 7c5603de3e Improved performance of the expression parser a bit more. dehnert 2014-08-02 19:17:56 +0200
  • 952747a9bc Modified some rules in the expression parser such that less redundant parsing is done. dehnert 2014-08-02 11:44:08 +0200
  • aecd0e3cb8 Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available. dehnert 2014-07-25 13:14:49 +0200
  • 5bb76eb12e Bugfix for storm::utility::vector::reduceVector to correctly compute which choices were taken to achieve extremal values. dehnert 2014-07-22 18:41:00 +0200
  • e2c2177dca Adapted MaxSAT-based minimal command set generator to some recent changes to make it work again. dehnert 2014-07-22 17:53:36 +0200
  • 2c59dd6f32 Finished unit tests for the actions. masawei 2014-07-21 16:36:34 +0200
  • ee1ebdf91d Removed the visitor from LTL and refactured the formulas to use shared pointer in stead of standart pointer. masawei 2014-07-18 13:02:37 +0200
  • 40c698af90 Some fixes to make new SMT framework compile with clang under Mac OS (includes fixes to some initializiation ordering warnings). Bugfix for PRISM parser to correctly handle formulas. dehnert 2014-07-07 18:14:44 +0200
  • 3887cb57aa Fix for temporaries and non const references David_Korzeniewski 2014-07-02 17:13:21 +0200
  • ee89065b07 Fixed type error on gcc and clang (int_fast64_t is not the same type as on msvc) David_Korzeniewski 2014-07-02 16:50:21 +0200
  • 430aa086be Merge branch 'master' into SmtSolvers David_Korzeniewski 2014-07-02 15:39:50 +0200
  • 52d3d91060 Implemented Unsat Core/Assumtions & simple test David_Korzeniewski 2014-07-02 13:09:16 +0200
  • d2f4c85711 Made changes to comply with new SparseMatrix Interface (YUCK). Fixed tests, all that stuff. PBerger 2014-07-01 01:35:06 +0200
  • eca20ce085 Merge branch 'master' into philippTopologicalRevival PBerger 2014-07-01 00:04:15 +0200
  • 9fe246a98b Renamed the folders containing the formulas to lowercase to adhere to the naming conventions and Started with testing. masawei 2014-06-28 23:25:33 +0200
  • 671797738a Now the parameter that is set for dynamic reordering actually gets passed to CUDD. dehnert 2014-06-27 17:28:20 +0200
  • a815a6f425 Implemented allSat with z3 and test David_Korzeniewski 2014-06-25 15:59:53 +0200
  • 93c03fff3f Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation David_Korzeniewski 2014-06-25 10:44:35 +0200
  • 758fac5389 Merge branch 'master' into SmtSolvers David_Korzeniewski 2014-06-25 09:04:06 +0200
  • df5bafc38b Finished the implementation of the Cls and Ltl filters. masawei 2014-06-24 00:55:04 +0200
  • a5e28fcf04 Added some filter actions. masawei 2014-06-22 22:26:47 +0200
  • caf96c04e0 Extended DD interface by methods to generate explicit row-grouped matrices from DDs. dehnert 2014-06-19 18:53:43 +0200
  • 8587f68eb1 Fixed toMatrix conversion using ODDs. The next step is to generate non-deterministic matrices, i.e., matrices with row groups. dehnert 2014-06-17 23:33:55 +0200
  • 084bb14acd Bugfix for expression parser. dehnert 2014-06-16 09:23:43 +0200
  • 236e7fa290 Another step towards generating explicit data structures from DDs using ODDs. dehnert 2014-06-15 22:45:49 +0200
  • f12ff82baf Added getNodeCount for ODD and fixed a bug concerning boolean meta variables. dehnert 2014-06-15 19:27:39 +0200
  • 5d53c6efa5 Added ODD-concept to easily convert between DD-based and explicit formats. dehnert 2014-06-15 17:56:46 +0200
  • dd73387ed1 Add missing case. dehnert 2014-06-06 19:30:40 +0200
  • 72cc5f2188 Added 'power' as a binary operator in expression classes and expression grammar. dehnert 2014-06-06 17:04:17 +0200
  • 478f5ee38c Started separating expression parsing from PRISM model parsing. dehnert 2014-06-06 15:14:14 +0200
  • 28eed65a0d Fixed a reference to a non-existant option. dehnert 2014-06-06 11:41:56 +0200
  • 5503e91bb3 Added detailed time measurement using std::chrono, leading to more useful information for comparison against Prism, etc. PBerger 2014-06-05 00:31:36 +0200
  • 7ab2a84c0f Small beauty fixes to the Cudd Interface PBerger 2014-06-05 00:30:28 +0200
  • 03399375f8 Fixed an unintended 32bit shift being expanded to 64 bit PBerger 2014-06-05 00:29:36 +0200
  • b5cb0cde1d Fixed a typo in the StormOptions.cpp PBerger 2014-06-05 00:28:28 +0200
  • b7ad4398e2 Fixed an error in the interface of the LpSolvers. PBerger 2014-06-05 00:28:05 +0200
  • 9a7c24372e Added crude version of 'dump to explicit format' for Dtmcs. dehnert 2014-06-04 17:25:42 +0200
  • 63f55b38f0 Removed debug output that was - of course - never there. (You saw nothing!) dehnert 2014-06-01 14:14:25 +0200
  • 7b2def2b11 Added function to retrieve the minterms of a DD as an expression and added corresponding test. dehnert 2014-06-01 11:22:55 +0200
  • e79fa50999 Changed naming of DD variables belonging to one meta variable slightly: only integer-valued meta variables now get a '.i' suffix to denote their i-th bit. dehnert 2014-05-31 21:29:18 +0200
  • 60b2145461 Added function to DD interface that creates a nested if-then-else expression that represents the very same function as the DD. Added a test for this functionality. Added some methods offereded by Cudd to simplify DDs. dehnert 2014-05-31 21:20:56 +0200
  • 3271e73f01 Fixed the last test. All tests green now (well, except the ones that need gurobi, which I don't have). masawei 2014-05-30 23:49:14 +0200
  • 9a28e5b580 Added proper formula string method to filters. masawei 2014-05-30 23:06:22 +0200
  • 1513241985 Added functions for more efficiently retrieving the DD for 'greater than constant', 'greater or equal than constant' and 'notZero'. dehnert 2014-05-30 19:53:35 +0200
  • b1f22c1747 Added shortcut DD interface to compute \'greaterZero\' on a DD. dehnert 2014-05-30 17:34:09 +0200
  • 9e506f40bc Some fixes for MSVC. :P dehnert 2014-05-26 13:29:40 +0200
  • 50eb16f9f9 Merge branch 'master' into SmtSolvers David_Korzeniewski 2014-05-22 18:56:31 +0200
  • a0319cb6e7 Model Generation and Tests for translating from z3 to storm David_Korzeniewski 2014-05-22 18:45:34 +0200