dehnert
|
8c329933ec
|
Began correcting performance tests.
|
12 years ago |
|
dehnert
|
9ed1fa19e2
|
Added some example files.
|
12 years ago |
|
dehnert
|
b5baae5861
|
Added 3 missing example files for synchronous leader election protocol. Set release optimization level for clang to O3.
|
12 years ago |
Lanchid
|
a956fc782a
|
Added support for atomic propositions containing numbers.
|
12 years ago |
|
Lanchid
|
6a1f6fbcee
|
Parser changed to support P and R operators annotated with min/max.
|
12 years ago |
|
Lanchid
|
c8e8e1502b
|
Added minimum/maximum support for probablistic no bound operators.
|
12 years ago |
|
Lanchid
|
f9ab6f85d0
|
- Restructuration of model checkers (by logic)
- LTL file parser
|
12 years ago |
|
dehnert
|
5149a7a943
|
Added lab files for asynch_leader and corrected pctl file a bit. Included first (incorrect) tests for performance test suite.
|
12 years ago |
|
dehnert
|
6ba1cf25c8
|
Added new variable for base bath for project root. Changed test input files to the files from example folder. Added leader4.lab to asynchronous leader election example.
|
12 years ago |
|
dehnert
|
3851377064
|
Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future.
|
12 years ago |
|
dehnert
|
27de566228
|
Moved current tests to the functional test suite in an attempt to introduce performance tests.
|
12 years ago |
|
dehnert
|
5f27a932a9
|
Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes.
|
12 years ago |
Harold Bruintjes
|
6aea8de7ba
|
Readded cudd 2.5.0 from prismparser
|
12 years ago |
|
dehnert
|
69395face2
|
Moved creation of SCC-dependency graph into abstract model class. Added functionality to sparse matrix class to not give the number of nonzeros upfront, but to to grow on demand.
|
12 years ago |
|
dehnert
|
b28b827362
|
All methods of GraphAnalyzer:
* commented,
* return values instead of passing result variables by reference.
|
12 years ago |
gereon
|
a868980466
|
Fixed code so that tests compiles.
|
12 years ago |
|
gereon
|
aafdbf7671
|
Fixed errors due to merging.
|
12 years ago |
|
gereon
|
fad8290844
|
Renamed WrongFileFormatException to WrongFormatException
|
12 years ago |
|
gereon
|
e8300825e4
|
Merge branch 'prismparser'
Conflicts:
CMakeLists.txt
examples/dtmc/crowds/crowds15_5.pm
examples/dtmc/crowds/crowds20_5.pm
examples/dtmc/crowds/crowds5_5.pm
examples/dtmc/die/die.pm
examples/dtmc/synchronous_leader/leader3_5.pm
src/parser/PrctlParser.cpp
src/parser/PrctlParser.h
src/storm.cpp
src/utility/Settings.cpp
test/parser/ParseMdpTest.cpp
|
12 years ago |
|
gereon
|
5495456991
|
Added new log level "trace"
Fixed bug in ExplicitModelAdapter
|
12 years ago |
|
gereon
|
8cdb6d5394
|
Put initial state in stateToIndexMap
|
12 years ago |
|
gereon
|
21e3740867
|
Fixed bug in computation of number of choices in case of deadlocks.
|
12 years ago |
|
dehnert
|
ab11d3c207
|
Further refactoring of GraphAnalyzer class. Some comments are still missing and GraphAnalyzer should be made a namespace instead of a class with static methods only.
|
12 years ago |
|
dehnert
|
fc67cf4e3f
|
Further refactoring of GraphAnalyzer class.
|
12 years ago |
|
dehnert
|
cc7230abb1
|
Started to refactor graph analyzing to include less pointers and the like. Currently this breaks two tests.
|
12 years ago |
|
dehnert
|
94337f5835
|
Added move-constructor and move-assignment to bit vector class.
|
12 years ago |
|
dehnert
|
0f545630eb
|
Adapted the pctl files according to our format.
|
12 years ago |
|
Lanchid
|
e976261e7c
|
Merge branch 'LtlParser'
Conflicts:
src/storm.cpp
|
12 years ago |
|
Lanchid
|
5279466644
|
- Removed "test-prctl" option
- Some restructuring in storm.cpp
|
12 years ago |
|
Lanchid
|
32a32a7013
|
Added extended model checker factory functions.
As currently only gmm++ is usable as matrix library they are not really
useful, but they can be easily extended in the future.
|
12 years ago |
|
Lanchid
|
cc7b31db62
|
Created factory method for the creation of the Prctl model checkers
|
12 years ago |
|
Lanchid
|
d4f791e80d
|
Removed default values for prctl, csl and ltl settings and added
test formulas for the "die" test as prctl file
|
12 years ago |
|
Lanchid
|
065ac8f659
|
Basic command line interface for SToRM
|
12 years ago |
|
Lanchid
|
6fca423152
|
Marked constants as unsigned to avoid comparison of signed and unsigned
values
|
12 years ago |
|
Lanchid
|
5d3b9e5cc1
|
Basic structure for central model checking method in storm.cpp
|
12 years ago |
|
Lanchid
|
3b5602b942
|
Reduction of functionality of fileParser: Only does the parsing, no
checking
|
12 years ago |
|
dehnert
|
2e8d264594
|
Minor changes to state labeling class:
* marked some methods as const
* renamed getAtomicProposition to getLabeledStates
|
12 years ago |
|
dehnert
|
f899914799
|
Adapted the labeling class such that no raw arrays are included any more, but a vector instead.
|
12 years ago |
|
gereon
|
cec71c9632
|
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Conflicts:
src/modelchecker/AbstractModelChecker.h
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
|
12 years ago |
|
Lanchid
|
9dac249d88
|
Marked constants for expected numbers of states/transitions of the
parsed models in the model checker tests as unsigned (otherwise
compilers may throw annoying warnings)
|
12 years ago |
|
Lanchid
|
67ba49d170
|
Some necessary adaptions in Prctl::CumulativeReward
|
12 years ago |
|
Lanchid
|
758ff9fe42
|
Merge branch 'master' into LtlParser
|
12 years ago |
|
Lanchid
|
cc242974dc
|
Renamed namespace storm::formula to storm::property
|
12 years ago |
|
Lanchid
|
4cddd9ad78
|
Changing AbstractFormulaChecker and PrctlFormulaChecker to completely
work with the new structure of formulas.
|
12 years ago |
|
gereon
|
860a775c18
|
Actually skip modules that do not have commands with current label.
|
12 years ago |
|
gereon
|
b7a1e90579
|
Variables were counted in two places (VariableState and ExplicitAdapter).
Now, they got mixed up... this is fixed now.
|
12 years ago |
|
gereon
|
dfd4df2884
|
Removing debug output.
|
12 years ago |
|
gereon
|
a790a7c3ec
|
Allow != as a token.
|
12 years ago |
|
gereon
|
6ad0c7041e
|
Allow DoubleExpressions to use integer constants
|
12 years ago |
|
gereon
|
3ff9514f7b
|
Make clone() work for variables without initial value.
|
12 years ago |
