tempest

Author	SHA1	Message	Date
dehnert	27e06940a9	templated all explicit parsers so that they may now be modified to produce non-double models Former-commit-id: `dd7f8767f8`	9 years ago
sjunges	1086ffc1cc	Added allow early termination for min/max solvers Former-commit-id: `eaad511158`	9 years ago
dehnert	f9f5a4e206	reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas Former-commit-id: `a2849d6534`	9 years ago
dehnert	b3178e17f6	more bug fixes Former-commit-id: `0b33b30efa`	9 years ago
dehnert	dbc7d860a4	functional tests compile again, started to debug changes Former-commit-id: `efef0e6487`	9 years ago
sjunges	5e428a795a	And more includes on the right spot. Former-commit-id: `72bb348687`	9 years ago
dehnert	72cb30d6b0	started replacing ValueType template argument by model class in all instantiations Former-commit-id: `197e3876a4`	9 years ago
sjunges	3c2040f4b7	Removed many superfluous includes, added some source files -- towards faster compilation Former-commit-id: `a575a97d40`	9 years ago
dehnert	2bf7eafb4b	Further work on hybrid MDP model checker. Former-commit-id: `3192a13f55`	10 years ago
dehnert	eb5d4100a6	Renamed Nondeterminstic equation solver as this name is more than misleading. Former-commit-id: `7f08ed130c`	10 years ago
dehnert	d545fac471	Restructured solvers a bit: they now get the matrix upon construction and the model checkers use factories to retrieve solvers. Former-commit-id: `9c727f41f9`	10 years ago
dehnert	a1dae8849e	Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented. Former-commit-id: `d4e6df30b5`	10 years ago
dehnert	b5f907d99d	Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation. Former-commit-id: `517a870d2f`	10 years ago
dehnert	89df9621a9	MDP model checker works again. Former-commit-id: `2c24da6192`	10 years ago
dehnert	1699732dce	More work on logic classes. Former-commit-id: `9d94e02b74`	10 years ago
dehnert	266d660d89	Added functions responsible for printing the help. Started adapting the tests to the new option system. Former-commit-id: `0407d8223e`	10 years ago
dehnert	9ad12616e2	Renamed files in settings module a bit. Started on the pseudo-modular module-settings. Former-commit-id: `b3162aa86b`	10 years ago
dehnert	96e1f8faf9	Renamed Settings class to SettingsManager. Former-commit-id: `2b33f4c8d0`	10 years ago
masawei	d75e32b83e	Renames the folder formula to properties and the namespace property to properties. Former-commit-id: `236ed22c7d`	10 years ago
masawei	ee1ebdf91d	Removed the visitor from LTL and refactured the formulas to use shared pointer in stead of standart pointer. Next up: Continue testing. Former-commit-id: `0103895e13`	11 years ago
masawei	3271e73f01	Fixed the last test. All tests green now (well, except the ones that need gurobi, which I don't have). Former-commit-id: `7636a2a6ab`	11 years ago
masawei	9a28e5b580	Added proper formula string method to filters. - Lots of debugging - Changed the way the filter keeps information about the scheduler to use for probability/reward queries. \| This was done by keeping a special action at the first position of the action list. \| Which was not exactly consistent with the idea behind the filter actions. \| Now the filter keeps this information as an enum value in a member variable. - All but one tests are green. So we almost reestablished full functionality. \|- The last test that still fails is SparseMdpPrctlModelCheckerTest.Dice where the second to last model check returns the wrong result. Next up: Debug. Then introduce the full range of filter actions. Former-commit-id: `fd311966cc`	11 years ago
masawei	4bf0299279	Changed the Prctl/Csl formula parsers to be static classes. - Also fixed up control flow and some tests for new interfaces. \|-> It now compiles again. Next up: More functionallity in the filter. Former-commit-id: `21d43e75c4`	11 years ago
masawei	15d13bc06d	Refactored the AutoParser. - Devided the AutoParser.h into .h and .cpp - The AutoParser now is a stateless class \|- This resulted in changes to the interface between the parsers and the rest of the project. \|- The main() now directly acquires a shared_ptr to an AbstractModel from the call of the AutoParser and keeps ownership of it. \|- Additionally, the division into .h and .cpp lead to a move of includes from the header to the source. This caused several tests to need some model header to be included. \|- Tests are still showing green (except those needing Gurobi, which I do not have). Next up: Parser.h/.cpp, then comments and making things look nice.) Former-commit-id: `f59b7405e5`	11 years ago
dehnert	36fb44e206	Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests. Former-commit-id: `8c0fa08f2d`	11 years ago
dehnert	588a4b60b6	Refactored linear equation solvers and nondeterministic linear equation solvers. Added functional tests for both. Former-commit-id: `0abb11828a`	11 years ago
dehnert	0a89d65f93	Started refactoring Markov automaton model checker. Former-commit-id: `c4278de4f0`	11 years ago
dehnert	f39fb24f65	Removed pointers from Model Checker Interface (and callback methods in formulas). From now on, the results are returned in form of an object. Because of the existing move semantics for the types in question, this does not come at a performance penalty. Former-commit-id: `5befdebd92`	11 years ago
PBerger	11cc7fc6bc	Introduced a new Object called InternalOptionMemento to handle required settings for tests which auto-reset after the test is done Refactored many constants to be of type ull where required Edited all tests that used the set() function of the Settings to make use of the new InternalOptionMemento Former-commit-id: `a400a36f69`	11 years ago
PBerger	938959de56	Added a set() Method to the Settings.h for the Tests Moved all standard options into a helper class/compilation unit as to reuse it in the Tests Moved the MaxIteration set call in the tests Former-commit-id: `f436511107`	11 years ago
PBerger	e69c9f1962	Added all options from StoRM Rewrote all calls to the Settings instance with the new Syntax Implemented new ArgumentValidators.h Former-commit-id: `b4ab63f8f2`	11 years ago
dehnert	7095f8e67f	Fixed a lot of issues introduced by refactoring. Former-commit-id: `c3a5177008`	12 years ago
dehnert	c8081c4d34	Fixed wrong step-bounded backward search.	12 years ago
Lanchid	ec91dcbe2e	Merge branch master into LTLParser	12 years ago
Lanchid	f9ab6f85d0	- Restructuration of model checkers (by logic) - LTL file parser	12 years ago
dehnert	27de566228	Moved current tests to the functional test suite in an attempt to introduce performance tests.	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	cc242974dc	Renamed namespace storm::formula to storm::property	12 years ago
Lanchid	45867c33c1	Prctl works now.	12 years ago
Lanchid	f513e49084	Almost finished restruction of PRCTL formulas; adapted code (including test cases) to work correctly with the new structure	12 years ago
dehnert	43f11ccc5f	Refactoring of modelchecker folder.	12 years ago
dehnert	f1c379bbe3	Moved model checking functionality for MDPs for general superclass such that specialized model checkers only need to implement certain operations. Fixed tests.	12 years ago
dehnert	34b85b956e	Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit.	12 years ago
dehnert	abae304719	Included tests for model checkers in test suite.	12 years ago

11 Commits (cb839bedc833a37f08f2a353e7f5d9ad59535acb)