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

Commit Graph

  • b381321653 Added more classes to IR. Extended PRISM-format parser. dehnert 2013-01-08 22:34:51 +0100
  • 557461a77d Renamed SquareSparseMatrix to SparseMatrix PBerger 2013-01-08 22:21:06 +0100
  • 36e2f5f15b Refactored SparseMatrix, made references const. Refactored Adapter to GMM to make use of new internal format PBerger 2013-01-08 22:15:36 +0100
  • b89db58fbb Made changes to all files that use the Sparse Matrix, as the diagonal entries are now included in the main storage. This refs #34 PBerger 2013-01-08 22:03:46 +0100
  • 99c5f4799e checking file format hint gereon 2013-01-07 12:34:16 +0100
  • a6dcb236e2 implementing check for filename extension gereon 2013-01-07 12:25:53 +0100
  • a4b7b27829 Added parsing support for expressions. Now working on parsing probabilistic programs. dehnert 2013-01-04 23:38:45 +0100
  • a7ab5bb309 More fun with Spirit. dehnert 2013-01-03 23:46:45 +0100
  • 92efc9c345 Taming Boost::Spirit... dehnert 2013-01-03 15:48:09 +0100
  • 6e2acc5159 add checked_strtod and use it in all parsers gereon 2012-12-29 22:43:32 +0100
  • 11b16f5dde Made bound/no-bound operators more consistent to reduce similar code. Changed bound operators to have a single bound and a comparison operator instead of an interval. dehnert 2012-12-27 17:47:25 +0100
  • 86c7ae3f5c Added BoundedEventually as a convenience operator. Included check for illegal atomic propositions. Added exception class to be raised in case a property is invalid for the respective model. dehnert 2012-12-27 14:15:00 +0100
  • 1561843cee Minor bugfix in sparse matrix method to compute pointwise product. Remove unnecessary small example files. Add reward files for synchronous leader example. Added test procedures to main (commented out by default) to check all of the three main models (crowds, die, synchronous leader). dehnert 2012-12-27 13:37:09 +0100
  • 58cf8118fe Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas. dehnert 2012-12-26 19:30:07 +0100
  • f983317b54 Renaming MRMC to STORM, see #42 PBerger 2012-12-25 02:37:56 +0100
  • a9b6e92306 Added adapters folder and GmmxxAdapter that is a friend class of the matrix class and can convert the sparse matrix to the gmm++ format. Removed this conversion from the matrix class. dehnert 2012-12-24 14:20:39 +0100
  • 364d8e4861 added Matrix::getRowSum() gereon 2012-12-24 13:46:43 +0100
  • 9775f7ae7e Added CTMC model, doing c&p from dtmc. gereon 2012-12-24 13:37:35 +0100
  • 4cc86cc7e3 fixing bracket... gereon 2012-12-24 13:27:36 +0100
  • 0f8c598529 making inheritance of Parsers public (for AutoParser) gereon 2012-12-24 12:07:22 +0100
  • ab30a95f74 first version of AutoTransitionParser. gereon 2012-12-24 11:59:21 +0100
  • 614fe3df9f removing unused variable gereon 2012-12-24 11:53:05 +0100
  • 34a4b91f49 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-24 11:18:33 +0100
  • eeaee58a56 first version of NonDeterministicSparseTransitionParser gereon 2012-12-23 14:59:06 +0100
  • b8a6a01a11 fixed settings handling: stop on unrecoverable error gereon 2012-12-23 14:54:12 +0100
  • 504bcb97a6 Added die example from PRISM. Added SparseStateRewardParser. Small fix to main. dehnert 2012-12-23 14:53:12 +0100
  • b26a731383 Added reward parsing: * Transition-based rewards are parsed using the existing (Deterministic)SparseTransitionsParser. * State-based rewards are parsed using a new SparseStateRewardParser that parses lines consisting of a state and an associated reward. * The Dtmc class now stores the two reward models. * The DtmcParser class now parses up to one transition-based and one state-based reward file. They may, however, be omitted in which case the respective reward model is set to null. dehnert 2012-12-23 14:45:01 +0100
  • de85bfa80e Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-23 10:43:43 +0100
  • e4c1241b2b Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-23 00:14:59 +0100
  • 37f6337fa5 using new iterator for checking matrix gereon 2012-12-23 00:13:33 +0100
  • cdc24b1456 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-22 22:40:28 +0100
  • 48098b596d Removed the parameter from const templates, as types can be stated explicitly (see documentation) Lanchid 2012-12-22 20:52:08 +0100
  • a04bdd9b97 Fixed a few bugs. dehnert 2012-12-22 19:41:01 +0100
  • 4d4219991c renaming sanity check, fix brackets gereon 2012-12-22 18:24:02 +0100
  • 4b373b2146 fixing a warning and changing calls to std::string.compare() to == gereon 2012-12-22 15:09:43 +0100
  • fa68492b55 removing distinction between different platform using " \t\n\r" on all platforms now for lab parser gereon 2012-12-22 15:04:01 +0100
  • c8ec52f111 Merge branch 'refactoring' Lanchid 2012-12-21 13:15:08 +0100
  • 1b973545bb Fixes in probabilistic operators: Lanchid 2012-12-21 13:06:59 +0100
  • ef03284369 Changed mrmc.cpp to use the new Dtmc parser instead of the separate ones. Lanchid 2012-12-19 20:37:29 +0100
  • afb0373358 Added DtmcParser class that parses a whole DTMC, making use of the labeling and transitions parser. Lanchid 2012-12-19 20:28:54 +0100
  • 383f34e745 Function renaming Lanchid 2012-12-19 20:25:50 +0100
  • daa5cf297a Changed type of parameter filename to std::string const & (was const char*) Lanchid 2012-12-19 18:46:25 +0100
  • 64784d4e92 Renamed LabParser to AtomicPropositionLabelingParser Lanchid 2012-12-19 18:42:46 +0100
  • 3c741fae4a Changed filename parameter for DeterministicSparseTransitionParser to a const reference to an std::string, instead of char pointer Lanchid 2012-12-19 18:35:10 +0100
  • 2da19207de Removed check for valid probablilities, as we want to use the DeterministicSparseTransitionParser for CTMCs (which have edges that are not labeled with probabilities, but with weights) later on Lanchid 2012-12-19 18:25:32 +0100
  • b0b8c98f6b Renamed TraParser to DeterministicSparseTransitionParser Lanchid 2012-12-19 18:21:47 +0100
  • 89e38fed8f Added temporary check() method to ProbabilisticNoBoundsOperator. Added two check() functions to DtmcPrctlModelChecker that are to be called by the "outer world" that check a given formula and print the result the standard output. Fixed bug in GmmxxDtmcPrctlModelChecker that prevented BiCGStab using ILU preconditioning from working Refactored mrmc.cpp to remove larger code blocks from main(). Added option to specify logging file. If no file is set and the verbose option is not set either, logging is basically disabled by setting the logging level very high. This is a workaround for the fact that at least one log appender needs to be set in the logging framework, which would not be the case if both logging facilities (file and console) are disabled. dehnert 2012-12-19 18:19:26 +0100
  • 5cc8e8bb2d modified sanity check to use internal data structures... gereon 2012-12-17 16:12:25 +0100
  • 83e660ac3d check is sums of each row is one (or zero for "imaginary" states) gereon 2012-12-17 15:49:56 +0100
  • 470fa4c4b7 added sys/mman.h for linux target gereon 2012-12-17 15:37:03 +0100
  • 0369207e9d Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2012-12-17 15:32:53 +0100
  • a5d922c6a8 removed pointless return that produces an error (return value...) gereon 2012-12-17 15:28:03 +0100
  • 2f05d035fe Refactored all exceptions to use the macro generator to remove all redundant base code. PBerger 2012-12-17 04:05:15 +0100
  • fe95c2225b Added missing contructors to all exceptions. PBerger 2012-12-17 04:01:21 +0100
  • 01ea2c8427 Moved os specific includes into OsDetection.h PBerger 2012-12-17 03:25:59 +0100
  • 9e5b69b211 Further naming scheme enforcement. PBerger 2012-12-17 03:20:01 +0100
  • 96c7dd9a79 Added the (default) external build path /build to git ignore. PBerger 2012-12-17 03:08:30 +0100
  • 08f87d545c Some more refactoring, renaming, adding #ifndef guards... Fixed a warning in SquareSparseMatrix.h regarding a conversion from uint64 to uint PBerger 2012-12-17 02:56:15 +0100
  • 59408b2ab4 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC PBerger 2012-12-16 23:21:13 +0100
  • 64bf554cad some more reformatting gereon 2012-12-16 20:48:16 +0100
  • 6a720709a5 refactored opening braces in settings classes gereon 2012-12-16 20:43:18 +0100
  • 94f46568d5 adding default value for trigger options gereon 2012-12-16 20:14:52 +0100
  • cce8391e44 Refactored everything to match naming scheme. PBerger 2012-12-16 18:17:40 +0100
  • c7781f8137 Added option matrixlib to the generic options of the settings class to define a default value for the used backend. Related to ticket #29. dehnert 2012-12-14 15:15:21 +0100
  • 18832101a4 Removed this-> in initializer list as clang++ does not like that. dehnert 2012-12-14 15:13:35 +0100
  • 1bd0df7076 Added option support to gmm++-based model checker. Removed junk code from mrmc.cpp. dehnert 2012-12-14 15:13:14 +0100
  • 50d9ce22de Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC PBerger 2012-12-14 01:33:26 +0100
  • 0c3cfeef20 Updated project files of included resources. PBerger 2012-12-14 01:33:07 +0100
  • 95b000436b Added a JacobiDecomposition container and conversion function. Added const where possible. PBerger 2012-12-14 01:32:21 +0100
  • 25ee8f906a added a few words about the current state of the PRCTLParser gereon 2012-12-13 23:47:45 +0100
  • b9d1eb28f1 Removed superfluous operator. dehnert 2012-12-13 23:38:14 +0100
  • d965595fbe Evaluated given options in gmm++-based model checker. dehnert 2012-12-13 23:29:25 +0100
  • e802942be2 fixing memory leaks. only log4cplus left... gereon 2012-12-13 23:09:04 +0100
  • 331d3c7a11 fixing invalid read gereon 2012-12-13 22:34:36 +0100
  • d34c39293e Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-13 22:25:49 +0100
  • 2a6228af71 Added some options to Gmmxx-Modelchecker. DO NOT PULL FOR THE TIME BEING AS THERE IS A PROBLEM WITH THE OPTIONS. dehnert 2012-12-13 22:25:23 +0100
  • cc1441ce26 fixed wrong return type of operator<<() for BaseException. Templates FTW! gereon 2012-12-13 22:21:13 +0100
  • f9cabfd483 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-13 22:05:15 +0100
  • a9129c00c7 new exception gereon 2012-12-13 22:03:22 +0100
  • 467988f97d Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC dehnert 2012-12-13 17:58:51 +0100
  • c54283cef2 Merge. dehnert 2012-12-13 17:58:49 +0100
  • 74588c84f4 removed helpConfigfile (as we don't distinguish anymore between cli and configfile options) added docu on how to call registerModule() gereon 2012-12-13 16:50:03 +0100
  • f6c88b3801 fixing some more documentation, adding dummy implementation gereon 2012-12-13 16:34:29 +0100
  • 3610172125 updating documentation gereon 2012-12-13 16:18:36 +0100
  • c93b325e19 some cleanups gereon 2012-12-13 16:06:49 +0100
  • 09b35a2fa1 replace callbacks by register methods gereon 2012-12-13 15:45:51 +0100
  • be6223e4a7 Forgot the file for the probabilistic operator in the previous commit. Also, improved toString methods for other probabilistic operators Lanchid 2012-12-12 16:12:43 +0100
  • bc698ffd20 Implemented probabilistic operator without specified bounds, including check method in the model checker. Lanchid 2012-12-12 15:55:14 +0100
  • 89d93d87d4 adding put methods for callbacks gereon 2012-12-10 12:30:27 +0100
  • b28c1f64c4 fixing a few memory issues gereon 2012-12-09 23:21:31 +0100
  • ef8721a40f removing pointless newlines gereon 2012-12-09 23:08:09 +0100
  • 39cd84a469 adding documentation that is visible to doxygen, adding logging gereon 2012-12-09 23:07:33 +0100
  • cd4463116e completed work on intermediate callbacks and restructured settings class gereon 2012-12-09 22:32:27 +0100
  • 2ff00441cb adding intermediate callbacks for settings gereon 2012-12-09 19:23:14 +0100
  • 08ad2fe2f3 Fixed non-convergence of Eigen solver (for crowds examples) by correctly invoking solveWithGuess instead of solve. dehnert 2012-12-09 17:54:08 +0000
  • 19a1a38c47 made Callbacks::getInstance private gereon 2012-12-09 15:06:12 +0100
  • 64f5430427 documented CallbackType gereon 2012-12-09 15:02:02 +0100
  • a2f27293f7 adding code samples for Register class gereon 2012-12-09 14:57:34 +0100
  • 4361647ef4 made settings callbacks work and changed names to match our conventions. gereon 2012-12-09 14:41:46 +0100
  • 8aca56ea5b fixing warning: unused variable pr gereon 2012-12-09 14:06:00 +0100