154 Commits (f1cac96d4cadb278bd5882941f00440456a8237c)

Author SHA1 Message Date
gereon 12745d466e Fixing main, removing shared_ptr 12 years ago
gereon f09be5c3b4 Made BaseGrammar constructor clang-compatible, fixed ms output of CPU usage 12 years ago
Lanchid f513e49084 Almost finished restruction of PRCTL formulas; adapted code (including 12 years ago
dehnert 7dc36875ae Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode. 12 years ago
dehnert d266d9effe Fixed another bug in sparse matrix. Fixed bug in test. 12 years ago
dehnert 43f11ccc5f Refactoring of modelchecker folder. 12 years ago
gereon 7ce537adca Adding testbed for prismparser 12 years ago
gereon 6c19ddb877 Cosmetics: Trailing whitespaces, space indentation, ... 13 years ago
gereon 49ac740459 Changed a bit, how log messages are processed. 13 years ago
gereon 1f3b172c83 Added a simple module that handles segfaults: print a message and provide a backtrace. 13 years ago
gereon 928de19fed Reorganized main routine. Catching errors that made it to the top level. 13 years ago
gereon 2bc32fe3de Cleaned up handling of --verbose, proposing correct use of log levels from now on... 13 years ago
gereon fd30e8ca25 Cleaned up handling of --verbose, proposing correct use of log levels from now on... 13 years ago
dehnert 98426aa139 Added new MDP example 'consensus'. Added some test checking to storm.cpp. 13 years ago
dehnert b7d4d974ec Added a lot of test checking routines to main file. 13 years ago
dehnert e99909034c Added some more test formula for two dice example in main file. 13 years ago
Lanchid 5b57728d7e Merge branch master into PrctlParser 13 years ago
dehnert 313d48e2da Fixed the method for making rows absorbing for nondeterministic models. 13 years ago
dehnert d4cf812c5e Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example. 13 years ago
dehnert 7d7edc5a05 Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector. 13 years ago
dehnert 7ceb1ed9b2 Added logging for errors in labeling class. Corrected wrong labeling of MDP in examples. Extended test checking for first MDP example in main. 13 years ago
dehnert 8a9d766c73 Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite. 13 years ago
dehnert 7d95a45633 Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder. 13 years ago
dehnert c02271a36a Fixed typo in CTMC class. Moved GraphAnalyzer to utility. 13 years ago
gereon 47cb1aa4d9 renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...) 13 years ago
dehnert db01eb92d9 Splitted explicit model adapter into several logical functions. 13 years ago
dehnert 777aa3a914 Intermediate commit to switch workplace. 13 years ago
dehnert c4af78b859 Added singleton utility class for CUDD-based things. Added some first methods to expression classes to generate ADDs, but this should be moved to a separate class implementing the expression visitor pattern. 13 years ago
dehnert 7331544377 Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place. 13 years ago
dehnert edd3a9a20e Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter. 13 years ago
dehnert a17c99902b The PRISM parser can now parse DTMC models that do not use synchronization. 13 years ago
gereon f9923bac95 Fixed memory leaks involving Settings class 13 years ago
dehnert aba470960f Intermediate commit to test code under linux. 13 years ago
dehnert ed43401c37 Reenable logging to prevent exception. 13 years ago
dehnert c19418b871 Intermediate commit to switch workplace. 13 years ago
dehnert d414b93bad Added some functionality to IR. Introduced case distinction for boolean/integer assignments in updates. Started writing an IR adapter. 13 years ago
gereon 4e71cab4a7 using AutoParser in storm.cpp 13 years ago
dehnert 4b7c6a8941 Splitted PrismParser class into header and implementation file. Commented both files properly. Cleaned interface of PrismParser. 13 years ago
dehnert a44da7d50a Commit to switch workplace. 13 years ago
dehnert b381321653 Added more classes to IR. Extended PRISM-format parser. 13 years ago
PBerger 557461a77d Renamed SquareSparseMatrix to SparseMatrix 13 years ago
dehnert 92efc9c345 Taming Boost::Spirit... 13 years ago
dehnert 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. 13 years ago
dehnert 86c7ae3f5c Added BoundedEventually as a convenience operator. 13 years ago
dehnert 1561843cee Minor bugfix in sparse matrix method to compute pointwise product. 13 years ago
dehnert 58cf8118fe Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas. 13 years ago
PBerger f983317b54 Renaming MRMC to STORM, see #42 13 years ago
gereon b8a6a01a11 fixed settings handling: stop on unrecoverable error 13 years ago
dehnert 504bcb97a6 Added die example from PRISM. Added SparseStateRewardParser. Small fix to main. 13 years ago
Lanchid 1b973545bb Fixes in probabilistic operators: 13 years ago