2470c31cb0
Added SteadyStateNoBoundOperator
12 years ago
08815b8c13
Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement
a "StateNoBoundOperator" now...
12 years ago
6ff25321d4
First version of CSL parser
TODO:
- Correct path formulas
- Time bounded until
- Steady state operator without bounds
12 years ago
9bc8bb2ca8
Some code style and documentation
12 years ago
5f9876e4c9
WIP on CslParser: c6060eb Minor changes (mainly improving comments)
12 years ago
c3e3ebf1f3
index on CslParser: c6060eb Minor changes (mainly improving comments)
12 years ago
c7afcecf4a
Minor changes (mainly improving comments)
12 years ago
da562bcfc9
Merge branch 'master' into PrctlParser
Conflicts:
src/modelchecker/AbstractModelChecker.h
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
12 years ago
895c2b6aad
Convenient file parser for PRCTL, and correct reward formula parsing
(together with some necessary code for that)
12 years ago
7dc36875ae
Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode.
12 years ago
d266d9effe
Fixed another bug in sparse matrix. Fixed bug in test.
12 years ago
2b4d26023a
Fixed one of the remaining bugs introduced by refactoring.
12 years ago
00b4797948
Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.
12 years ago
9ae177c9b5
Further refactoring. In particular of the matrix class.
12 years ago
bb441cdeca
Refactored some parts of sparse matrix.
12 years ago
840a9b6e07
Somewhat works now. Still has at least one bug and segfaults afterwards :-)
12 years ago
e55fca3836
Implemented module renaming.
This includes clone() routines (that accept the renaming information) for all ir::expressions classes, additional constructors for all ir classes and additional rules in PrismParser.
This is the first version that has the chance to work and actually compiles. (Insert some swearing here...)
Testing is to be done, as this will most probably not work yet.
12 years ago
43f11ccc5f
Refactoring of modelchecker folder.
12 years ago
7ce537adca
Adding testbed for prismparser
12 years ago
c1986bcc0e
Refactored two of the model checker classes.
12 years ago
6c19ddb877
Cosmetics: Trailing whitespaces, space indentation, ...
12 years ago
16c08f7d24
Merge branch 'master' into PrctlParser
Conflicts:
examples/mdp/asynchronous_leader/leader3.tra
examples/mdp/asynchronous_leader/leader4.tra
examples/mdp/asynchronous_leader/leader5.tra
examples/mdp/asynchronous_leader/leader6.tra
examples/mdp/asynchronous_leader/leader7.tra
examples/mdp/two_dice/two_dice.lab
examples/mdp/two_dice/two_dice.tra
src/formula/NoBoundOperator.h
src/formula/PathBoundOperator.h
src/formula/ProbabilisticNoBoundOperator.h
src/formula/RewardNoBoundOperator.h
src/modelchecker/AbstractModelChecker.h
src/modelchecker/DtmcPrctlModelChecker.h
src/modelchecker/EigenDtmcPrctlModelChecker.h
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
src/modelchecker/GmmxxMdpPrctlModelChecker.h
src/modelchecker/MdpPrctlModelChecker.h
src/models/GraphTransitions.h
src/parser/AutoParser.h
src/parser/DeterministicSparseTransitionParser.cpp
src/parser/NondeterministicModelParser.cpp
src/parser/NondeterministicSparseTransitionParser.cpp
src/parser/NondeterministicSparseTransitionParser.h
src/storage/BitVector.h
src/storage/SparseMatrix.h
src/storm.cpp
src/utility/GraphAnalyzer.h
src/utility/Vector.h
12 years ago
0dcebc8ff0
Start of implementing improved file parser for formulas
12 years ago
836bdb3f1c
Created new base class OptimizingOperator.
Inheriting from this class where appropriate, added constructors accepting minimumOperator argument.
12 years ago
78331dfeea
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
a5ad38a46b
Added options for optimizing max/min operator to BoundOperators.
12 years ago
e524720925
Added prototypical support for in-place matrix-vector multiplication in the style of Gauss-Seidel. This might enhance the speed of convergence for value-iteration model checkers.
12 years ago
102f38322d
Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example.
12 years ago
49ac740459
Changed a bit, how log messages are processed.
Thresholds are now as follows:
main logger INFO, consoleAppender WARN, fileAppender none (i.e. everything)
--verbose changes consoleAppender to INFO
--debug changes main logger and consoleAppender to DEBUG
12 years ago
525fc7c16f
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
c784de4d03
Added new model checker that uses topological value iteration. However, does not fully work yet.
12 years ago
bb6afcb1fd
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
1f3b172c83
Added a simple module that handles segfaults: print a message and provide a backtrace.
I grew tired of always starting gdb when it would've sufficed to know the function.
This routine will demangle C++ symbols, so you can see in which function we crashed.
12 years ago
17e0e8165a
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
bdf173c315
GraphTransition objects can now be build from the SCC decomposition of a system.
12 years ago
e4129c37d9
fixed two bugs in ExplicitModelAdapter.
12 years ago
5c25116a24
First version of ExplicitModelAdapter that supports transition rewards.
12 years ago
d9e833680a
Added convenience methods RewardModel::hasStateRewards() and RewardModel::hasTransitionRewards()
12 years ago
7dc5324a65
Program returns empty RewardModel and emits error, if invalid model is given.
12 years ago
928de19fed
Reorganized main routine. Catching errors that made it to the top level.
12 years ago
341dc50ab7
Added some better error output for basic parsers using errno
12 years ago
8dce5af515
fixed some warnings (comparison between signed/unsigned)
12 years ago
75ce91082a
Forgot to commit actual cpp file...
12 years ago
a73ae7aed4
Added new option --debug.
12 years ago
2bc32fe3de
Cleaned up handling of --verbose, proposing correct use of log levels from now on...
FATAL_LOG_LEVEL: Use, if we are going to crash.
ERROR_LOG_LEVEL: Use, if there is no reasonable way to continue.
WARN_LOG_LEVEL: Use, if we got something the average user should read.
INFO_LOG_LEVEL: Use, if this might in some cases be of interest.
DEBUG_LOG_LEVEL: Use, if this should usually not be relevant to a user.
TRACE_LOG_LEVEL: Use only during development.
There are three levels of verbosity:
- default: WARN and above
- verbose: INFO and above
- debug: DEBUG and above
12 years ago
5f64fd168b
Cleaned up structure of ExplicitModelAdapter.
- added cpp file
- returns complete models now (missing transition rewards...)
12 years ago
f52d4eb7a8
Added new option --debug.
12 years ago
fd30e8ca25
Cleaned up handling of --verbose, proposing correct use of log levels from now on...
FATAL_LOG_LEVEL: Use, if we are going to crash.
ERROR_LOG_LEVEL: Use, if there is no reasonable way to continue.
WARN_LOG_LEVEL: Use, if we got something the average user should read.
INFO_LOG_LEVEL: Use, if this might in some cases be of interest.
DEBUG_LOG_LEVEL: Use, if this should usually not be relevant to a user.
TRACE_LOG_LEVEL: Use only during development.
There are three levels of verbosity:
- default: WARN and above
- verbose: INFO and above
- debug: DEBUG and above
12 years ago
5976c9e81d
More work for ExplicitModelAdapter
* Removed templates from various functions, as we can only produce double models anyway.
* Added methods to compute state rewards and state labelings
* Added toModel() routine
12 years ago
2005eb7e73
Added getter routines, so we can retrieve the reward models
12 years ago
Lanchid
dehnert
gereon