sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
1358 Commits
2 Branches
0 Tags
187 MiB
Tree: 5a0059d110
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '5a0059d110'
${ noResults }
Commit Graph

165 Commits (5a0059d1101827a8a25f38db29f5e327568cf275)

Author SHA1 Message Date
Lanchid f9ab6f85d0 - Restructuration of model checkers (by logic)
13 years ago
gereon aafdbf7671 Fixed errors due to merging.
13 years ago
gereon 5495456991 Added new log level "trace"
13 years ago
Lanchid 5279466644 - Removed "test-prctl" option
13 years ago
Lanchid 32a32a7013 Added extended model checker factory functions.
13 years ago
Lanchid cc7b31db62 Created factory method for the creation of the Prctl model checkers
13 years ago
Lanchid 065ac8f659 Basic command line interface for SToRM
13 years ago
Lanchid 5d3b9e5cc1 Basic structure for central model checking method in storm.cpp
13 years ago
Lanchid cc242974dc Renamed namespace storm::formula to storm::property
13 years ago
gereon 12745d466e Fixing main, removing shared_ptr
13 years ago
gereon f09be5c3b4 Made BaseGrammar constructor clang-compatible, fixed ms output of CPU usage
13 years ago
Lanchid f513e49084 Almost finished restruction of PRCTL formulas; adapted code (including
13 years ago
dehnert 7dc36875ae Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode.
13 years ago
dehnert d266d9effe Fixed another bug in sparse matrix. Fixed bug in test.
13 years ago
dehnert 43f11ccc5f Refactoring of modelchecker folder.
13 years ago
gereon 7ce537adca Adding testbed for prismparser
13 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