dehnert
236e7fa290
Another step towards generating explicit data structures from DDs using ODDs.
Former-commit-id: 5b7e3e8680
11 years ago
dehnert
f12ff82baf
Added getNodeCount for ODD and fixed a bug concerning boolean meta variables.
Former-commit-id: 79eb69226b
11 years ago
dehnert
5d53c6efa5
Added ODD-concept to easily convert between DD-based and explicit formats.
Former-commit-id: f2a2a002b7
11 years ago
dehnert
72cc5f2188
Added 'power' as a binary operator in expression classes and expression grammar.
Former-commit-id: c58321709e
11 years ago
PBerger
03399375f8
Fixed an unintended 32bit shift being expanded to 64 bit
Former-commit-id: b2adc2a5ba
11 years ago
dehnert
7b2def2b11
Added function to retrieve the minterms of a DD as an expression and added corresponding test.
Former-commit-id: afaf1f02a3
11 years ago
dehnert
60b2145461
Added function to DD interface that creates a nested if-then-else expression that represents the very same function as the DD. Added a test for this functionality. Added some methods offereded by Cudd to simplify DDs.
Former-commit-id: 4fc816f64b
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
David_Korzeniewski
a0319cb6e7
Model Generation and Tests for translating from z3 to storm
translating from z3 to storm has still some errors
Former-commit-id: 2a46b6c615
11 years ago
David_Korzeniewski
79984db3ee
Added test for checkWithAssumptions
Former-commit-id: 4f64100ec5
11 years ago
David_Korzeniewski
9a7b4f69ef
More tests and some small bugfixes for Z3SmtSolver
Former-commit-id: 71def90649
11 years ago
David_Korzeniewski
45bc8ea665
Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3
Added first simple tests for Z3SmtSolver and Z3ExpressionAdapter
Former-commit-id: 77ade5ffa6
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
dehnert
45486600f7
Made parts of the interface of the DdManager protected (because they shouldn't be accessible from the outside world).
Former-commit-id: bf52a653b8
11 years ago
dehnert
29d8111991
Adapted Gurobi and glpk LP solvers to expression-based interface. Adapted tests and made them work again.
Former-commit-id: 62379ddafd
11 years ago
dehnert
389fddc996
Added some more methods to valuations. Changed visitor invocation slightly. Moves ExpressionReturnType in separate file. Finished linearity checking visitor. Started on visitor that extracts coefficients of linear expressions.
Former-commit-id: 6e3d0ec910
11 years ago
dehnert
57a8381f91
If requested, the DD iterator can now skip meta variables which are 'don't cares' for the function value.
Former-commit-id: 061cb5f0fa
11 years ago
dehnert
db232fe39b
Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way.
Former-commit-id: f6514eb0cd
11 years ago
dehnert
92ee6187fa
Added more query methods to expressions. SparseMatrix now keeps track of non zero entries and models show correct number of transitions by referring to nonzero entries rather than all entries in the matrix.
Former-commit-id: 48180be2fe
11 years ago
dehnert
219af9b43b
Removed constants from expressions. Even though PRISM has the concept of constants and variables, it currently makes no sense to distinguish them in our expression classes.
Former-commit-id: 787e921e2c
11 years ago
dehnert
c6976dd8b5
Added some query methods for new expression classes.
Former-commit-id: 0633c7740e
11 years ago
dehnert
c76e0e8d4d
Added class for initial construct of PRISM programs (to capture position information). Added more validity checks for programs and tests for them (not all though).
Former-commit-id: cf4e985684
11 years ago
dehnert
82836f1ad1
Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite.
Former-commit-id: fc44db75a7
11 years ago
dehnert
8d3ed7d2fa
Added min/max functions on DDs. Added tests for them and ite operation.
Former-commit-id: 8e6df90a38
11 years ago
dehnert
39ec9401ef
Fixed the PrismParser so the exact format of PRISMs boolean expressions can now be parsed.
Former-commit-id: bb08ec1646
11 years ago
dehnert
6078e07476
First version of DD iterator; small test included.
Former-commit-id: 2ec2323886
11 years ago
PBerger
1d8ae9fc89
Fixed an issue with templated variadic template arguments (see http://stackoverflow.com/questions/23119273/use-a-templated-variadic-template-parameter-as-specialized-parameter for discussion)
Former-commit-id: e7d2d054b6
11 years ago
dehnert
311247ff0c
Added support for Xor in expression classes and added parsing functionality for Xor, Implies and Iff.
Former-commit-id: 16e023cf26
11 years ago
dehnert
61d4bb956c
Added functionality to compare two ADDs up to a given precision. Added logical operator overloads to DD interface. Added tests for all new features.
Former-commit-id: 738ad49d62
11 years ago
dehnert
5a4730ae22
When exporting DDs to the dot format, edges leading to the zero node are now suppressed. Also, nodes in the dot file are now labeled with variable names (+ the number of the bit).
Former-commit-id: 410d61d333
11 years ago
PBerger
94b25c02ca
Fixed bugs in some files.
Made LTL a little better to compile under WIN32.
Former-commit-id: 71377f0672
11 years ago
dehnert
dc8921037e
Added missing test inputs.
Former-commit-id: 537971f365
11 years ago
dehnert
164c8225fd
Fixed some minor issues.
Former-commit-id: 80f0ae4c9c
11 years ago
dehnert
199b6576a9
Added ternary operator. Parsing standard PRISM models into the PRISM classes now works. Included tests for parsing stuff. ToDo: add remaining semantic checks for parsing/PRISM classes and fix explicit model adapter.
Former-commit-id: cb37c98f1f
11 years ago
dehnert
f6587b424d
Further work on PrismParser and the related PRISM classes...
Former-commit-id: be4ae055dd
11 years ago
dehnert
7610bc8e76
Started reducing the complexity in the PRISM grammar.
Former-commit-id: c17dc6d27b
11 years ago
dehnert
eb2b2fed30
Hotfix for DD abstraction layer: copy and paste mistake in operator !\= is now fixed.
Former-commit-id: b815b7d7e8
11 years ago
dehnert
41b31df0ab
Added small tests for implies/iff in expressions.
Former-commit-id: 3d90be7596
11 years ago
dehnert
6e1241211b
Started moving IR and adjusting it to the new expression classes.
Former-commit-id: 24a182701f
11 years ago
dehnert
8af52c8866
Finished new expression classes and corresponding functional tests.
Former-commit-id: 9268eab3a9
11 years ago
dehnert
c8a8beca2a
Started working on new easy-to-use expression classes.
Former-commit-id: 9ee1be5822
11 years ago
dehnert
88d9f36ef4
Added min/max abstract over DD variables to CUDD (actual code taken from PRISM). Added more tests for DD layer. Fixed some bugs in the DD layer.
Former-commit-id: a4b7810137
11 years ago
dehnert
0fce0444f7
Further bugfixes and tests for DD layer.
Former-commit-id: 32ef63f9b1
11 years ago
dehnert
cf5c04065e
Added streaming functionality to DD. More tests, more bugfixes.
Former-commit-id: 3c3078fbdc
11 years ago
dehnert
6b07643c96
Further tests for DD layer and bugfixing.
Former-commit-id: 752a8c55ac
11 years ago
dehnert
a4fec9f080
Started writing functional tests for DD abstraction layer and fixed some bugs on the way.
Former-commit-id: 8a2fc118be
11 years ago
PBerger
0922921b24
Updated cudaForStorm/CMakeLists.txt to make use of the new GIT based version schema.
Added version functions to the Cuda Plugin.
Edited storm.cpp to show version infos for the CUDA Plugin.
Fixed a critical error in basicValueIteration.cu which causes random SEGFAULTs... :P
Streamlined the TopologicalValueIterationNondeterministicLinearEquationSolver.cpp. The SCC group optimizer now returns flat_sets instead of a vector as the sets are ordered, which is required for the Solver to work.
This is now a stable version of StoRM containing a fully wor
Former-commit-id: 47d5c2825c
11 years ago
masawei
2ed6be853b
Fixed two minor bugs.
- 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
11 years ago
PBerger
d3f513b0a0
Added debug output to CUDA Kernel.
Added a performance test for the CUDA stuff.
Former-commit-id: 9953befdea
11 years ago