Lanchid
39ff3240d3
More convenient syntax for time bounded formulas, and respective test
cases.
12 years ago
Lanchid
35baa5ff02
Added parsing of time bounded operators
12 years ago
Lanchid
96fa125fe4
Added time bounded operators for CSL.
12 years ago
Lanchid
bfd2178ca3
Corrected define guards in some header files
12 years ago
Lanchid
7e91d5b01e
Test cases for CSL parser
12 years ago
Lanchid
509c1a2b47
Added support for SteadyStateNoBoundOperator into the CSL parser.
12 years ago
Lanchid
2470c31cb0
Added SteadyStateNoBoundOperator
12 years ago
Lanchid
08815b8c13
Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement
a "StateNoBoundOperator" now...
12 years ago
Lanchid
6ff25321d4
First version of CSL parser
TODO:
- Correct path formulas
- Time bounded until
- Steady state operator without bounds
12 years ago
Lanchid
9bc8bb2ca8
Some code style and documentation
12 years ago
Lanchid
5f9876e4c9
WIP on CslParser: c6060eb Minor changes (mainly improving comments)
12 years ago
Lanchid
c3e3ebf1f3
index on CslParser: c6060eb Minor changes (mainly improving comments)
12 years ago
Lanchid
c7afcecf4a
Minor changes (mainly improving comments)
12 years ago
Lanchid
da562bcfc9
Merge branch 'master' into PrctlParser
Conflicts:
src/modelchecker/AbstractModelChecker.h
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
12 years ago
Lanchid
895c2b6aad
Convenient file parser for PRCTL, and correct reward formula parsing
(together with some necessary code for that)
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
2b4d26023a
Fixed one of the remaining bugs introduced by refactoring.
12 years ago
dehnert
00b4797948
Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.
12 years ago
dehnert
9ae177c9b5
Further refactoring. In particular of the matrix class.
12 years ago
dehnert
bb441cdeca
Refactored some parts of sparse matrix.
12 years ago
gereon
840a9b6e07
Somewhat works now. Still has at least one bug and segfaults afterwards :-)
12 years ago
gereon
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
dehnert
43f11ccc5f
Refactoring of modelchecker folder.
12 years ago
gereon
7ce537adca
Adding testbed for prismparser
12 years ago
dehnert
c1986bcc0e
Refactored two of the model checker classes.
12 years ago
gereon
6c19ddb877
Cosmetics: Trailing whitespaces, space indentation, ...
12 years ago
Lanchid
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
Lanchid
0dcebc8ff0
Start of implementing improved file parser for formulas
12 years ago
gereon
836bdb3f1c
Created new base class OptimizingOperator.
Inheriting from this class where appropriate, added constructors accepting minimumOperator argument.
12 years ago
gereon
78331dfeea
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
gereon
a5ad38a46b
Added options for optimizing max/min operator to BoundOperators.
12 years ago
dehnert
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
dehnert
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
gereon
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
dehnert
525fc7c16f
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
dehnert
c784de4d03
Added new model checker that uses topological value iteration. However, does not fully work yet.
12 years ago
gereon
bb6afcb1fd
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
gereon
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
dehnert
17e0e8165a
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
12 years ago
dehnert
bdf173c315
GraphTransition objects can now be build from the SCC decomposition of a system.
12 years ago
gereon
e4129c37d9
fixed two bugs in ExplicitModelAdapter.
12 years ago
gereon
5c25116a24
First version of ExplicitModelAdapter that supports transition rewards.
12 years ago
gereon
d9e833680a
Added convenience methods RewardModel::hasStateRewards() and RewardModel::hasTransitionRewards()
12 years ago
gereon
7dc5324a65
Program returns empty RewardModel and emits error, if invalid model is given.
12 years ago
gereon
928de19fed
Reorganized main routine. Catching errors that made it to the top level.
12 years ago
gereon
341dc50ab7
Added some better error output for basic parsers using errno
12 years ago
gereon
8dce5af515
fixed some warnings (comparison between signed/unsigned)
12 years ago
gereon
75ce91082a
Forgot to commit actual cpp file...
12 years ago
gereon
a73ae7aed4
Added new option --debug.
12 years ago