777aa3a914
Intermediate commit to switch workplace.
12 years ago
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.
12 years ago
7331544377
Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place.
12 years ago
edd3a9a20e
Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter.
12 years ago
a17c99902b
The PRISM parser can now parse DTMC models that do not use synchronization.
12 years ago
f9923bac95
Fixed memory leaks involving Settings class
Settings (being a singleton) will now free it's instance itself upon program termination.
12 years ago
aba470960f
Intermediate commit to test code under linux.
12 years ago
ed43401c37
Reenable logging to prevent exception.
12 years ago
c19418b871
Intermediate commit to switch workplace.
12 years ago
d414b93bad
Added some functionality to IR. Introduced case distinction for boolean/integer assignments in updates. Started writing an IR adapter.
12 years ago
4e71cab4a7
using AutoParser in storm.cpp
12 years ago
4b7c6a8941
Splitted PrismParser class into header and implementation file. Commented both files properly. Cleaned interface of PrismParser.
12 years ago
a44da7d50a
Commit to switch workplace.
12 years ago
b381321653
Added more classes to IR. Extended PRISM-format parser.
12 years ago
557461a77d
Renamed SquareSparseMatrix to SparseMatrix
12 years ago
92efc9c345
Taming Boost::Spirit...
12 years ago
11b16f5dde
Made bound/no-bound operators more consistent to reduce similar code. Changed bound operators to have a single bound and a comparison operator instead of an interval.
12 years ago
86c7ae3f5c
Added BoundedEventually as a convenience operator.
Included check for illegal atomic propositions.
Added exception class to be raised in case a property is invalid for the respective model.
12 years ago
1561843cee
Minor bugfix in sparse matrix method to compute pointwise product.
Remove unnecessary small example files.
Add reward files for synchronous leader example.
Added test procedures to main (commented out by default) to check all of the three main models (crowds, die, synchronous leader).
12 years ago
58cf8118fe
Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas.
12 years ago
f983317b54
Renaming MRMC to STORM, see #42
Markt und Straßen stehn verlassen,
still erleuchtet jedes Haus,
Sinnend' geh ich durch die Gassen,
alles sieht so festlich aus.
An den Fenstern haben Frauen
buntes Spielzeug fromm geschmückt,
Tausend Kindlein stehn und schauen,
sind so wunderstill beglückt.
Und ich wandre aus den Mauern
Bis hinaus ins freie Feld,
Hehres Glänzen, heil'ges Schauern!
Wie so weit und still die Welt!
Sterne hoch die Kreise schlingen,
Aus des Schnees Einsamkeit
Steigt's wie wunderbares Singen-
O du gnadenreiche Zeit!
Merry Christmas commit ;)
12 years ago
b8a6a01a11
fixed settings handling: stop on unrecoverable error
12 years ago
504bcb97a6
Added die example from PRISM. Added SparseStateRewardParser. Small fix to main.
12 years ago
1b973545bb
Fixes in probabilistic operators:
- Constructors and Destructors now work correctly
- Removed check function from ProbabilisticNoBoundsOperator class (and
documented why it does not have one)
Note: I temporarily removed the -Wall parameter from gcc calls, as line
194 of GmmxxDtmcPrctlModelChecker.h throws a warning.
12 years ago
ef03284369
Changed mrmc.cpp to use the new Dtmc parser instead of the separate
ones.
12 years ago
daa5cf297a
Changed type of parameter filename to std::string const & (was const
char*)
12 years ago
64784d4e92
Renamed LabParser to AtomicPropositionLabelingParser
12 years ago
3c741fae4a
Changed filename parameter for DeterministicSparseTransitionParser to a
const reference to an std::string, instead of char pointer
12 years ago
b0b8c98f6b
Renamed TraParser to DeterministicSparseTransitionParser
12 years ago
89e38fed8f
Added temporary check() method to ProbabilisticNoBoundsOperator.
Added two check() functions to DtmcPrctlModelChecker that are to be called by the "outer world" that check a given formula and print the result the standard output.
Fixed bug in GmmxxDtmcPrctlModelChecker that prevented BiCGStab using ILU preconditioning from working
Refactored mrmc.cpp to remove larger code blocks from main().
Added option to specify logging file. If no file is set and the verbose option is not set either, logging is basically disabled by setting the logging level very high. This is a workaround for the fact that at least one log appender needs to be set in the logging framework, which would not be the case if both logging facilities (file and console) are disabled.
12 years ago
08f87d545c
Some more refactoring, renaming, adding #ifndef guards...
Fixed a warning in SquareSparseMatrix.h regarding a conversion from uint64 to uint
12 years ago
cce8391e44
Refactored everything to match naming scheme.
12 years ago
1bd0df7076
Added option support to gmm++-based model checker. Removed junk code from mrmc.cpp.
12 years ago
e802942be2
fixing memory leaks. only log4cplus left...
12 years ago
2a6228af71
Added some options to Gmmxx-Modelchecker. DO NOT PULL FOR THE TIME BEING AS THERE IS A PROBLEM WITH THE OPTIONS.
12 years ago
cc1441ce26
fixed wrong return type of operator<<() for BaseException. Templates FTW!
12 years ago
a9129c00c7
new exception
Created BaseException that can act as a stringstream. You can do the following:
throw BaseException() << "some error " << variable << " foo";
Changed InvalidSettings to use BaseException, using this new syntax in Settings.
12 years ago
c54283cef2
Merge.
12 years ago
74588c84f4
removed helpConfigfile (as we don't distinguish anymore between cli and configfile options)
added docu on how to call registerModule()
12 years ago
b28c1f64c4
fixing a few memory issues
12 years ago
ef8721a40f
removing pointless newlines
12 years ago
cd4463116e
completed work on intermediate callbacks and restructured settings class
12 years ago
82df4ba274
fixing warning: comparing signed with unsigned int
12 years ago
b50d906ae3
Added missing EigenDtmcPrctlModelChecker.h
Refactored solver to use iterative deepening for convergence :P
12 years ago
1f36724cc2
Refactored StringOutput to use std::to_string
Fixed Reference/Pointer bugs in all formulas.
Implemented EigenDtmcPrctlModelChecker
Replaced uses of int32 with 64bits
12 years ago
851e3a631d
Fixed CMakeLists.txt, made everything compile under Windows/MSVC
Added popcnt for MSVC
Fixed line ending detection in parser
12 years ago
27ba61ff74
Fixed minor bugs here and there. Improved gmm++-based model checker.
12 years ago
80b53bea18
Added more example files. Removed deletes at end of main() as these pointers are deleted by the DTMC class already. Small refactoring of GraphAnalyzer according to new guidelines. Added vector utility functions to set elements of vectors. Added conversion routine from our sparse matrix format to gmm++ format. Fixed some bugs in sparse matrix class. Added prototypical implementation of GmmxxDtmcPrctlModelChecker.
12 years ago
07ac945794
some more documentation
also call delete for objects created in parsers
as you can see, this is kind of ugly, maybe we should use a different structure there...
12 years ago
2ca83f5f31
Added functionality to rapidly extract sub-matrix from our sparse matrix format.
12 years ago
dehnert
gereon
PBerger
Lanchid