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

Commit Graph

  • 82ff9f3891 adding initializer for variable gereon 2013-01-12 19:29:53 +0100
  • 867d477afc removing pointless comment gereon 2013-01-12 19:29:02 +0100
  • ea84f91cf3 made a run of cpplint and fixed some of the warnings... gereon 2013-01-12 18:33:13 +0100
  • 5668b95d9b added missing include. gereon 2013-01-12 18:12:55 +0100
  • a8517c7246 fixed some documentation and changed position of const in Settings class. gereon 2013-01-12 18:10:41 +0100
  • 650a0f0a27 added documentation for AbstractModel and operator<< for ModelType gereon 2013-01-12 17:58:37 +0100
  • a695208d0e implemented check for deadlocks in parser gereon 2013-01-12 16:50:27 +0100
  • 4e71cab4a7 using AutoParser in storm.cpp gereon 2013-01-12 16:15:12 +0100
  • cdec5d44c9 adding format hint to tiny examples gereon 2013-01-12 16:13:05 +0100
  • 4dbbb1486b first working version of AutoParser gereon 2013-01-12 16:12:15 +0100
  • b4ea27d7c4 Added checks to parser: Now only local variables may be written in updates and each variable at most once. dehnert 2013-01-12 15:37:19 +0100
  • a82c8b3153 Moved implementation of PrismParser completely to source file. Fixed some minor things in IR classes. dehnert 2013-01-12 13:54:27 +0100
  • 4dc780ef77 modified AutoParser to reflect changes in the model type system. gereon 2013-01-12 13:39:06 +0100
  • b4862360ba made Ctmc and Dtmc subclasses of AbstractModel implement getType() fixed typo gereon 2013-01-12 13:38:15 +0100
  • 004633b79a fixed brackets in BaseException gereon 2013-01-12 13:37:25 +0100
  • 006c9e6b88 changed model base class gereon 2013-01-12 13:35:11 +0100
  • 4b7c6a8941 Splitted PrismParser class into header and implementation file. Commented both files properly. Cleaned interface of PrismParser. dehnert 2013-01-11 19:53:35 +0100
  • f52201466c Parsing labels works now. dehnert 2013-01-11 16:56:00 +0100
  • 6a33f84512 Another step towards PRISM model parsing: small models get recognized correctly. dehnert 2013-01-11 00:12:28 +0100
  • a44da7d50a Commit to switch workplace. dehnert 2013-01-10 18:24:52 +0100
  • 261750df9b removing two warnings from cpplint gereon 2013-01-10 13:23:26 +0100
  • 3deca3f2d3 Intermediate Commit to switch workplace. dehnert 2013-01-10 09:59:42 +0100
  • bad870f085 integrated cpplint gereon 2013-01-09 19:14:45 +0100
  • f7194a416d Cleaned IR classes a bit and made attributes private. Changed grammar rules accordingly. dehnert 2013-01-09 17:19:48 +0100
  • 1776f8ce12 first steps towards an AutoParser gereon 2013-01-09 11:13:28 +0100
  • 946128cae1 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2013-01-09 11:12:18 +0100
  • 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