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

Commit Graph

  • 82df4ba274 fixing warning: comparing signed with unsigned int gereon 2012-12-09 14:05:40 +0100
  • 97122e29cd Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-09 13:57:27 +0100
  • 4935b4a10b adding infrastructure to register callbacks for settings gereon 2012-12-09 13:55:06 +0100
  • cbe162ab84 Fixed some copy-paste errors. dehnert 2012-12-08 11:31:27 +0100
  • b50d906ae3 Added missing EigenDtmcPrctlModelChecker.h Refactored solver to use iterative deepening for convergence :P PBerger 2012-12-07 19:05:02 +0100
  • d54ef9f35f Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC PBerger 2012-12-07 17:04:18 +0100
  • 1f36724cc2 Refactored StringOutput to use std::to_string Fixed Reference/Pointer bugs in all formulas. Implemented EigenDtmcPrctlModelChecker PBerger 2012-12-07 17:03:58 +0100
  • 667b60db8f Added absolute path names for command line parameters for valgrind in make targets (by CMAKE variables), so it should work with out of source builds; and a dependency to the executables (so it is built automatically if that has not been done before) Lanchid 2012-12-07 13:34:05 +0100
  • 645ebe8b9e Changed functions of GmmxxDtmcPrctlModelChecker to fit to the changed interface. Lanchid 2012-12-07 13:31:24 +0100
  • e1a4a8d8c1 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC PBerger 2012-12-07 13:10:10 +0100
  • 851e3a631d Fixed CMakeLists.txt, made everything compile under Windows/MSVC Added popcnt for MSVC Fixed line ending detection in parser PBerger 2012-12-07 13:09:43 +0100
  • 1c088c1ca6 Added a probabilistic operator class that checks whether the probability that the path formula holds is equal to one single number, instead of comparing it to a lower and upper bound. Lanchid 2012-12-07 12:19:58 +0100
  • f80a7bcab3 Deleted DtmcPrctlModelChecker.cpp (was just there to make sure the corresponding h file is compiled, but is not necessary for that any more right now) Lanchid 2012-12-07 11:42:35 +0100
  • 7bce04405e Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC/ Lanchid 2012-12-07 11:39:10 +0100
  • ede5f56e5a Set model checker in copy constructor as const. Lanchid 2012-12-07 11:30:31 +0100
  • cbf719568a Added correct return value computation in method MakeRowsAbsorbing of class SquareSparseMatrix. Lanchid 2012-12-07 11:15:12 +0100
  • 4095e87282 changing pointer to std::shared_ptr gereon 2012-12-06 21:39:00 +0100
  • 8cbb7aa7d7 fixing toEigen conversion, making test case working :-) gereon 2012-12-06 21:37:56 +0100
  • 54e52b5ab7 dtmc.h -> Dtmc.h gereon 2012-12-06 20:10:02 +0100
  • 27ba61ff74 Fixed minor bugs here and there. Improved gmm++-based model checker. dehnert 2012-12-06 20:03:12 +0100
  • 091a7740a2 Added a lot of consts to all methods provided by formula classes. dehnert 2012-12-06 18:01:13 +0100
  • 223f5a5c60 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC/ Lanchid 2012-12-06 15:56:53 +0100
  • 8a12ec03e3 Copied pointer of states labeled with an AP, as the result of the function points into the labeling object. (Ticket #24) Lanchid 2012-12-06 15:50:18 +0100
  • 60f91d52c7 Some refactoring for ticket #24 Lanchid 2012-12-06 15:44:46 +0100
  • 80b53bea18 Added more example files. Removed deletes at end of main() as these pointers are deleted by the DTMC class already. Small refactoring of GraphAnalyzer according to new guidelines. Added vector utility functions to set elements of vectors. Added conversion routine from our sparse matrix format to gmm++ format. Fixed some bugs in sparse matrix class. Added prototypical implementation of GmmxxDtmcPrctlModelChecker. dehnert 2012-12-06 15:43:08 +0100
  • c436586303 fixing error if lab file contains no trailing newline gereon 2012-12-05 22:30:58 +0100
  • 9b1e435140 Adding further small examples. dehnert 2012-12-05 19:08:40 +0100
  • 739d3e3bda Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-05 16:33:39 +0100
  • 4c6c7d5fbd Merge. dehnert 2012-12-05 16:33:29 +0100
  • 39608b4b32 Merge branch 'modelchecker' Lanchid 2012-12-05 16:11:05 +0100
  • 13a2bd3057 Moved const_templates.h from "misc" to "utility" to be able to remove the former folder. Lanchid 2012-12-05 15:49:00 +0100
  • bb9aa0dfe2 Changed check function in formula classes to use a reference of the model checker instead of a pointer. Lanchid 2012-12-05 15:30:11 +0100
  • 67b3888ba9 Implemented basic functions of the model checker Lanchid 2012-12-05 15:24:11 +0100
  • 3b8e2a488b Fix for ticket 21. Fixed the map of the AtomicPropositionsLabeling class to std::unordered_map. Lanchid 2012-12-04 21:57:43 +0100
  • 5a5705070f Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC/ Lanchid 2012-12-04 21:53:54 +0100
  • 07ac945794 some more documentation gereon 2012-12-04 21:43:53 +0100
  • 71c824b91a hunting for memory erros gereon 2012-12-04 21:20:05 +0100
  • 101c6c41ab Merge. dehnert 2012-12-04 20:56:48 +0100
  • eb91f3ea86 fixing memory errors (mostly in resize()) and some minor corrections gereon 2012-12-04 20:51:10 +0100
  • 57f7adee55 added <double> to occurences of PCTLFormula gereon 2012-12-04 20:14:14 +0100
  • bf982fee2d Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-04 19:51:23 +0100
  • ff3901dc65 Merge branch 'gmm++' dehnert 2012-12-03 15:31:36 +0100
  • b1b86b078c Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-03 15:31:05 +0100
  • ba900ab352 Adding gmm++, examples. Adding gmm to gitignore. dehnert 2012-12-03 15:27:44 +0100
  • 2ca83f5f31 Added functionality to rapidly extract sub-matrix from our sparse matrix format. dehnert 2012-12-03 15:23:21 +0100
  • 6b4945e55c Changed getter for child nodes to reference style Lanchid 2012-12-03 15:08:29 +0100
  • cdc0332fd7 Code style and fixing errors in doxygen code for model checker class Lanchid 2012-12-03 11:43:02 +0100
  • 350f1a0990 Code style for formula classes Lanchid 2012-12-03 11:40:54 +0100
  • 79761d0492 Added copy constructor to model checker Lanchid 2012-12-03 11:18:10 +0100
  • b726a07b3f Small bugfix for the dot output Lanchid 2012-12-03 10:51:03 +0100
  • 4afa0a9ad3 Oops, this file is needed for the new test case Lanchid 2012-12-03 10:43:32 +0100
  • a1854b26a5 Documentation of ModelChecker (new) and improved doc of formula classes Lanchid 2012-12-03 10:18:39 +0100
  • f5d2205352 - Removed enum to infer the correct formula (sub-)class, instead used "check" which calls the correct check function in the model checker. Lanchid 2012-12-03 08:51:56 +0100
  • 60dbf5608e adding test-bench for prctl parser. gereon 2012-12-02 22:15:20 +0100
  • dd03c85fea porting PRCTLParser to class API gereon 2012-12-02 19:13:48 +0100
  • 2068bd31df Fixed example files to have a decimal point instead of a comma. dehnert 2012-12-02 15:40:31 +0100
  • 91124aabff Adding example files. dehnert 2012-12-02 15:12:44 +0100
  • f960e20e53 porting LabParser and TraParser from c-style API to class API gereon 2012-12-02 14:05:27 +0100
  • 0e6f699625 some doxygen for settings namespace gereon 2012-12-02 13:43:47 +0100
  • 42587ea4f5 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-02 13:40:46 +0100
  • f311f043bc some documentation for parser namespace gereon 2012-12-02 13:40:32 +0100
  • 30827b543e Fixed off-by-one error in sparse matrix. Now the tests do not produce a segfault any longer. dehnert 2012-12-02 12:34:47 +0100
  • b1cc1a782d Adding graph analyzer that is able to perform reachability searches in the state space. dehnert 2012-12-02 12:17:02 +0100
  • b76f392df1 Added newlines to end of files, because clang++ complains about that. Added case distinction of struct definition in parser.h for Mac OS to work correctly with parser.cpp. dehnert 2012-12-02 12:15:16 +0100
  • 18b72bc8d7 Added necessary include of unistd.h (for close()) to parser. Removed flag MAP_DENYWRITE of mmap for Mac OS and Linux as it is non-existent and ignored, respectively. Changed call to stat64 to call to stat for MAC OS, as stat64 is deprecated and 64-bit mode is turned on by macro that is no correctly set during OS-Detection. dehnert 2012-12-02 12:13:32 +0100
  • dc7c414246 Merged bit vector and main file. dehnert 2012-12-02 12:10:55 +0100
  • febe7a2d58 adding handling for --verbose gereon 2012-12-02 10:30:48 +0100
  • c10b08bf9a adding option --verbose gereon 2012-12-02 10:30:21 +0100
  • 5a7176740a adding generic get() method for settings of arbitrary type gereon 2012-12-02 10:18:34 +0100
  • f2006d4889 fixing doxygen gereon 2012-12-02 10:14:54 +0100
  • 4147b7a7f6 removing obsolete functions gereon 2012-12-02 10:13:30 +0100
  • 19b55ef9a0 fixed handling of invalid floats in Tra parser and converted tra files still containing floats with comma gereon 2012-12-02 01:39:47 +0100
  • 296a3a1992 fixed but in BitVector.resize() gereon 2012-12-02 01:25:48 +0100
  • 3782122ac6 adding log output with LOG4CPLUS macros gereon 2012-12-02 01:11:59 +0100
  • ee4f2bd9a2 changed to new parser names gereon 2012-12-02 00:46:24 +0100
  • 5ce8355d2b removing pantheios (new logger will be added soon) and fixed a warning gereon 2012-12-02 00:45:36 +0100
  • 2998e3d812 replacing constructor delegation gereon 2012-12-02 00:44:17 +0100
  • 8d89375c6e integrated renaming within master branch into code merged from parser branch gereon 2012-12-02 00:22:36 +0100
  • b4437bed59 Merge branch 'parser' gereon 2012-12-02 00:19:24 +0100
  • 7e9ba03ec6 added boost header for uint_fastX types gereon 2012-12-01 22:06:36 +0100
  • 9156fa6d61 moving implementation of MappedFile and helper functions to .cpp gereon 2012-12-01 22:04:49 +0100
  • bb1dae23fc Lab and Tra parser pass test cases gereon 2012-12-01 21:23:54 +0100
  • 82b502970e patched tra parser, test cases work now gereon 2012-12-01 20:29:24 +0100
  • 98d18f5ddc Merge branch 'parser' of https://sselab.de/lab9/private/git/MRMC into parser gereon 2012-12-01 20:05:11 +0100
  • 93d568bd82 working on prctl parser gereon 2012-12-01 20:04:06 +0100
  • 4f7cbd450a Fixed bugs in the Windows Part of the parser, refactored includes to meet Windows Requirements. PBerger 2012-12-01 15:31:34 +0100
  • 2bf01bfea3 Added graph search algorithms for determining the set of states that have no possibility of going to a non-target state. Enhanced bit vector class. dehnert 2012-11-30 17:51:40 +0100
  • 925a9bd8c0 changing pragma to ifdef, starting implementation of PRCTLParser gereon 2012-11-28 20:32:55 +0100
  • 2eb08a603a made stuff compile with new CMakeLists started a parser built with boost::spirit. It compiles, but does not do anything useful yet... gereon 2012-11-28 19:48:41 +0100
  • 05eaab7816 Removed invocations of memcpy in favour of std::copy as compilers will take care of optimizations. dehnert 2012-11-27 22:07:28 +0100
  • 2918f855bc Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-11-27 21:57:25 +0100
  • aaa5ccada8 Added command line arguments to MRMC to log output. dehnert 2012-11-27 19:54:40 +0100
  • c634ff6d0b Removed debug output. dehnert 2012-11-27 10:08:46 +0100
  • e632fc1bb6 fixing error & warning... gereon 2012-11-26 23:21:59 +0100
  • 8857655b56 Refactored names according to guidelines. dehnert 2012-11-26 12:15:17 +0100
  • 464fe97578 Fixed initialization order in constructor. dehnert 2012-11-26 11:41:34 +0100
  • 70bf39b634 Fixed includes for graph transitions class. Added index iteration functionality to the bit vector class. dehnert 2012-11-26 11:39:11 +0100
  • d871aca351 Renamed the backward transitions class to GraphTransitions and generalized it to be able to store the forward or backward graph structure of a given system. dehnert 2012-11-26 11:38:11 +0100
  • 1ed29262ff Renamed dtmc.h to Dtmc.h and backward_transitions.h to BackwardTransitions.h. dehnert 2012-11-25 23:01:07 +0100
  • 378fe3f532 Renamed and refactored atomic propositions labeling. dehnert 2012-11-25 22:58:26 +0100