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

Commit Graph

  • 6b90439424 Added functional test for the SparseMdpPrctlModelChecker. Fixed performance tests. dehnert 2013-05-22 14:57:47 +0200
  • 64a27bb871 Performance improvement for our matrix multiplication. dehnert 2013-05-22 14:56:26 +0200
  • 92fe051924 Added some newlines. dehnert 2013-05-22 14:07:54 +0200
  • 28facf9034 Fixed bug in iterator. dehnert 2013-05-22 14:07:13 +0200
  • 8daaded392 Added new example files for synchronous leader election. dehnert 2013-05-22 11:17:28 +0200
  • 6920e1ccdd Added static_casts and changed some types to signed instead of unsigned to eliminate some warnings of MSVC. dehnert 2013-05-22 11:15:44 +0200
  • d3c80dca16 Updated CMakeLists.txt - Added more sub-folders in the source-structure - Added an option for MSVC to use /bigobj with the Compiler as PrismParser.cpp bloats the object instance count - Edited CUDD Link Targets for MSVC Edited SymbolicModelAdapter.h, added an alternative implementation for log2 (NOT part of C90, not of Cxx!) Edited Program.cpp, promoted vars from int to uint to conquer warnings related to loss of precision Likewise in DeterministicSparseTransitionParser.cpp, IntegerConstantExpression.h PBerger 2013-05-20 21:48:19 +0200
  • 02cc706525 Added cudd-2.5.0 patched for Win32/Win64 incl. static lib builds for MSVC2012 PBerger 2013-05-20 21:30:47 +0200
  • 91f20b8bf2 Also added messages for windows code. gereon 2013-05-17 17:03:44 +0200
  • 131e10545b Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-05-17 17:02:19 +0200
  • 16f33d8bca Changed error messages for stat() and open() gereon 2013-05-17 17:01:09 +0200
  • 307911ca13 Fixed performance tests, they now run fine. dehnert 2013-05-16 17:41:41 +0200
  • 3c32eec8e1 Made the prob0/1 algorithms for MDPs share a common backward transition object. dehnert 2013-05-16 16:32:56 +0200
  • fbe1f41213 Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests. dehnert 2013-05-16 16:19:00 +0200
  • cde17bebb5 Merge branch 'master' into PrctlParser Lanchid 2013-05-16 17:13:18 +0200
  • 00a7c50ad4 Implemented the improvements from the PRCTL parser also in the CSL and LTL parsers. Lanchid 2013-05-16 17:09:04 +0200
  • a08db1b2cf Changed prctl parser. Lanchid 2013-05-16 16:32:31 +0200
  • ed4c6c8429 Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer. dehnert 2013-05-15 23:51:56 +0200
  • 2fcd6c95fb Performance tests now run fine (and take about 3 minutes). dehnert 2013-05-15 20:00:25 +0200
  • 8c329933ec Began correcting performance tests. dehnert 2013-05-15 18:26:07 +0200
  • 9ed1fa19e2 Added some example files. dehnert 2013-05-15 18:25:20 +0200
  • b5baae5861 Added 3 missing example files for synchronous leader election protocol. Set release optimization level for clang to O3. dehnert 2013-05-15 10:41:25 +0200
  • a956fc782a Added support for atomic propositions containing numbers. Lanchid 2013-05-15 16:25:38 +0200
  • 6a1f6fbcee Parser changed to support P and R operators annotated with min/max. Lanchid 2013-05-15 14:26:43 +0200
  • c8e8e1502b Added minimum/maximum support for probablistic no bound operators. Lanchid 2013-05-14 16:39:55 +0200
  • f9ab6f85d0 - Restructuration of model checkers (by logic) - LTL file parser Lanchid 2013-05-14 16:18:14 +0200
  • 5149a7a943 Added lab files for asynch_leader and corrected pctl file a bit. Included first (incorrect) tests for performance test suite. dehnert 2013-05-14 15:01:01 +0200
  • 6ba1cf25c8 Added new variable for base bath for project root. Changed test input files to the files from example folder. Added leader4.lab to asynchronous leader election example. dehnert 2013-05-14 13:28:19 +0200
  • 3851377064 Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future. dehnert 2013-05-13 22:53:00 +0200
  • 27de566228 Moved current tests to the functional test suite in an attempt to introduce performance tests. dehnert 2013-05-13 20:03:26 +0200
  • 5f27a932a9 Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes. dehnert 2013-05-13 18:53:34 +0200
  • 6aea8de7ba Readded cudd 2.5.0 from prismparser Harold Bruintjes 2013-05-13 10:28:03 +0200
  • 69395face2 Moved creation of SCC-dependency graph into abstract model class. Added functionality to sparse matrix class to not give the number of nonzeros upfront, but to to grow on demand. dehnert 2013-05-12 22:09:43 +0200
  • b28b827362 All methods of GraphAnalyzer: * commented, * return values instead of passing result variables by reference. dehnert 2013-05-11 19:05:04 +0200
  • a868980466 Fixed code so that tests compiles. gereon 2013-05-11 18:06:05 +0200
  • aafdbf7671 Fixed errors due to merging. gereon 2013-05-11 17:30:20 +0200
  • fad8290844 Renamed WrongFileFormatException to WrongFormatException gereon 2013-05-11 17:12:55 +0200
  • e8300825e4 Merge branch 'prismparser' gereon 2013-05-11 17:11:55 +0200
  • 5495456991 Added new log level "trace" Fixed bug in ExplicitModelAdapter gereon 2013-05-11 16:07:44 +0200
  • 8cdb6d5394 Put initial state in stateToIndexMap gereon 2013-05-11 14:43:51 +0200
  • 21e3740867 Fixed bug in computation of number of choices in case of deadlocks. gereon 2013-05-11 13:53:52 +0200
  • ab11d3c207 Further refactoring of GraphAnalyzer class. Some comments are still missing and GraphAnalyzer should be made a namespace instead of a class with static methods only. dehnert 2013-05-09 23:38:38 +0200
  • fc67cf4e3f Further refactoring of GraphAnalyzer class. dehnert 2013-05-09 23:16:35 +0200
  • cc7230abb1 Started to refactor graph analyzing to include less pointers and the like. Currently this breaks two tests. dehnert 2013-05-08 16:20:29 +0200
  • 94337f5835 Added move-constructor and move-assignment to bit vector class. dehnert 2013-05-08 16:19:26 +0200
  • 0f545630eb Adapted the pctl files according to our format. dehnert 2013-05-08 14:56:48 +0200
  • e976261e7c Merge branch 'LtlParser' Lanchid 2013-05-08 10:46:08 +0200
  • 5279466644 - Removed "test-prctl" option - Some restructuring in storm.cpp Lanchid 2013-05-07 16:38:21 +0200
  • 32a32a7013 Added extended model checker factory functions. As currently only gmm++ is usable as matrix library they are not really useful, but they can be easily extended in the future. Lanchid 2013-05-07 16:19:10 +0200
  • cc7b31db62 Created factory method for the creation of the Prctl model checkers Lanchid 2013-05-07 14:59:53 +0200
  • d4f791e80d Removed default values for prctl, csl and ltl settings and added test formulas for the "die" test as prctl file Lanchid 2013-05-07 14:38:25 +0200
  • 065ac8f659 Basic command line interface for SToRM Lanchid 2013-05-07 14:27:09 +0200
  • 6fca423152 Marked constants as unsigned to avoid comparison of signed and unsigned values Lanchid 2013-05-07 13:16:11 +0200
  • 5d3b9e5cc1 Basic structure for central model checking method in storm.cpp Lanchid 2013-05-07 11:38:17 +0200
  • 3b5602b942 Reduction of functionality of fileParser: Only does the parsing, no checking Lanchid 2013-05-07 10:24:27 +0200
  • 2e8d264594 Minor changes to state labeling class: * marked some methods as const * renamed getAtomicProposition to getLabeledStates dehnert 2013-05-06 22:24:33 +0200
  • f899914799 Adapted the labeling class such that no raw arrays are included any more, but a vector instead. dehnert 2013-05-06 22:09:01 +0200
  • cec71c9632 Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-05-04 20:33:02 +0200
  • 9dac249d88 Marked constants for expected numbers of states/transitions of the parsed models in the model checker tests as unsigned (otherwise compilers may throw annoying warnings) Lanchid 2013-05-03 16:17:05 +0200
  • 67ba49d170 Some necessary adaptions in Prctl::CumulativeReward Lanchid 2013-05-03 15:22:24 +0200
  • 758ff9fe42 Merge branch 'master' into LtlParser Lanchid 2013-05-03 15:03:03 +0200
  • cc242974dc Renamed namespace storm::formula to storm::property Lanchid 2013-05-03 11:48:19 +0200
  • 4cddd9ad78 Changing AbstractFormulaChecker and PrctlFormulaChecker to completely work with the new structure of formulas. Lanchid 2013-05-03 11:02:56 +0200
  • 860a775c18 Actually skip modules that do not have commands with current label. gereon 2013-05-02 16:55:59 +0200
  • b7a1e90579 Variables were counted in two places (VariableState and ExplicitAdapter). Now, they got mixed up... this is fixed now. gereon 2013-05-02 16:36:18 +0200
  • dfd4df2884 Removing debug output. gereon 2013-05-02 16:35:48 +0200
  • a790a7c3ec Allow != as a token. gereon 2013-05-01 02:01:27 +0200
  • 6ad0c7041e Allow DoubleExpressions to use integer constants gereon 2013-05-01 02:00:52 +0200
  • 3ff9514f7b Make clone() work for variables without initial value. gereon 2013-05-01 02:00:10 +0200
  • 966377ae32 Added a few more example files. gereon 2013-04-30 18:46:38 +0200
  • ac86932785 Fixed renaming: Command names were not considered. gereon 2013-04-30 18:43:47 +0200
  • 3b76126f6b Split PrismParser and PrismGrammar in differenc object files. Added reset method for grammars, now we can parse multiple files in one program execution. Added test for mdp parsing. gereon 2013-04-30 17:50:21 +0200
  • 4222130524 Fixed a few more bugs in clone() of various Expression classes and some in the module renaming. gereon 2013-04-30 17:16:37 +0200
  • 5840ca5bab Fixed weird error from previous commit. gereon 2013-04-30 15:20:35 +0200
  • c3cfc5404c Somewhat fixed weird issue during module renaming. gereon 2013-04-30 15:05:42 +0200
  • 63e9ad1f0a Adding test for prism parser gereon 2013-04-30 15:04:39 +0200
  • 7fe4c8c813 fixing signed/unsigned comparisons in ParseMdpTest gereon 2013-04-30 11:12:37 +0200
  • 4c0d7f6d95 adding cudd linker options for storm-tests gereon 2013-04-30 11:09:00 +0200
  • 12745d466e Fixing main, removing shared_ptr gereon 2013-04-30 10:53:08 +0200
  • 1642c5f66c Added missing functions to CUDDs cpp interface david 2013-04-30 10:50:40 +0200
  • f09be5c3b4 Made BaseGrammar constructor clang-compatible, fixed ms output of CPU usage gereon 2013-04-30 10:35:35 +0200
  • ac313cb997 Removed debug output, fixed DoubleExpressionGrammar gereon 2013-04-30 10:14:10 +0200
  • 014ecd8597 Fixed some glitches, producing meaningful error if sum of probabilities for a command is not one gereon 2013-04-28 16:01:11 +0200
  • cfb721a66e Turn off Cotire by default (because it triggers internal compilation errors not only in clang, but also in gcc 4.7). Signed-off-by: dehnert. david 2013-04-26 10:35:43 +0200
  • c1801b4ecc Changed debug output to use LOG4CPLUS gereon 2013-04-23 20:50:45 +0200
  • 766a92db3a Fixed error in *Literal::clone() gereon 2013-04-23 20:28:31 +0200
  • dffe274f64 Fixed error in MDP builder: swapped number of columns and rows. gereon 2013-04-23 19:15:09 +0200
  • a9edf2aa8c Removed some debug output. gereon 2013-04-23 18:54:50 +0200
  • 9613d099bb Removed shared_ptr for module, program and rewardmodel objects. gereon 2013-04-23 18:20:05 +0200
  • 1878962dea Fixed another nullptr, removed shared_ptr for Update and Command objects. gereon 2013-04-23 17:24:13 +0200
  • d03f8eeb9d Added checks, if we actually have a model before accessing it... gereon 2013-04-23 16:57:20 +0200
  • d0adf9d1b3 Some more test cases and, resulting from those, minor changes in LTL parser. Lanchid 2013-04-23 11:39:17 +0200
  • 01b1efc12d Some improvements/corrections to the LTL parser and some test cases for it Lanchid 2013-04-23 11:27:55 +0200
  • 834cb269a6 Minor corrections in code Lanchid 2013-04-22 17:03:29 +0200
  • fb50665564 Documentation of formula classes Lanchid 2013-04-22 16:53:52 +0200
  • ccfd1ccc6a Documentation for CSL and PRCTL classes Lanchid 2013-04-22 16:47:37 +0200
  • 0a2725d79c Documentation of abstract formulas. Lanchid 2013-04-22 16:38:55 +0200
  • 535ae933b0 Compiling implementation of LTL parser Lanchid 2013-04-22 14:37:41 +0200
  • 9e3ec6c403 Added LTL Lanchid 2013-04-22 11:00:17 +0200
  • 3c1cf4819c Fixed a few other issues. Module renaming seems to work now! gereon 2013-04-20 19:35:16 +0200