195c58e60f
Small change of plans: Abstract formulas now use a template parameter
for subformulas, so it can be determined later which kind formulas they
accept as subformulas.
12 years ago
f1383964f0
Adapted abstract formulas to new structure
12 years ago
38652f44e4
Restructuring formula classes, part I
Sorted formulas into respective folders, depending on which logic they
belong to (or if they are abstract).
The Code is NOTadapted to the new structure yet.
12 years ago
bb37bc49f2
Compiling version of PrismParser.
12 years ago
bdd93d8a6a
Merge branch 'master' into CslParser1
12 years ago
f996829836
Some minor changes in output of formulas
12 years ago
39ff3240d3
More convenient syntax for time bounded formulas, and respective test
cases.
12 years ago
35baa5ff02
Added parsing of time bounded operators
12 years ago
96fa125fe4
Added time bounded operators for CSL.
12 years ago
bfd2178ca3
Corrected define guards in some header files
12 years ago
7e91d5b01e
Test cases for CSL parser
12 years ago
509c1a2b47
Added support for SteadyStateNoBoundOperator into the CSL parser.
12 years ago
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
Lanchid
gereon
dehnert