- For that implemented function that checks if a formula is a propositional logic formula to all three logics.
- Added tests for the function.
- Added documentation for the function.
Former-commit-id: 3fcb84b990
- Regrettably, the LtlFilterTest could not be done, since an Ltl modechecker would be needed for that. Which, we don't have.
|- So that is a TODO until such a modelchecker is implemented.
- This concludes the testing for the refactured formulas.
Next up: Documentation.
Former-commit-id: 2d731edcd9
- Also handled nullptr actions.
|- They are checked for in the constructor as well as in the add method and filtered out. No segfaults do to nullptr actions anymore.
Former-commit-id: 84b3b2a978
- 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
- 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
- First one concerning the MappedFileTest in which I neglected to consider that the number of characters used to signal a new line differs between Linux (\n -> 1) and Windows (\r\n -> 2) which caused the test to fail on all OS using two characters (hence not on Linux, where I ran the tests).
- Second bug concerned the case that a transition reward file contained more states than the corresponding transition file.
In that case the parser tried to acces the entry of the rowGroupIndices vector behind the last actual entry, which caused an exception to be thrown.
Now there is a check whether the highest state index found by the parser does exceed the highest state index of the model.
Former-commit-id: bc83267f3c
- Fixed comments.
- It seems to be ASSERT_EQ(expected, actual);
|-> Switched arguments of nearly all ASSERT_EQs to correctly use this macro in the parser tests.
Former-commit-id: e5059709f2
- Some renaming (among others unmatched -> mismatched).
- Added checks and tests for doubled or skipped lines as well as lines concerning the same transition.
Next up: Remerge.)
Former-commit-id: 05efcbf91c
- Done with the tests. At least for now.
|- There are tests for all parsers and helper classes now.
Next up: Some minor fixes and finally the merge.
Former-commit-id: ebb2ea50d5
- Eliminated the need for SupportedLineEndings (I hope...should work on all os, but have only tested this on linux)
- Moved fileExistsAndIsReadable to MappedFile
- Removed scanForModelHint and replaced it with its contents at the one point where is was used in the AutoParser
- Moved and renamed remaining part of Parser.cpp/.h to src/utility/cstring.cpp/.h
|- New namespace of the cstring manipulation functions is storm::utility::cstring
|- Used a using namespace storm::utility::cstring to eliminate the full namespace specification within the needing parsers. This keeps the code readable.
- Threw out some unnessesary includes.
Next up: Commenting and making things look nice.
Former-commit-id: c983d1e1a2
dehnert
sjunges
masawei