dehnert
|
084bb14acd
|
Bugfix for expression parser.
Former-commit-id: 2b03856c86
|
11 years ago |
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
|
dd73387ed1
|
Add missing case.
Former-commit-id: b30aa3bc0d
|
11 years ago |
dehnert
|
72cc5f2188
|
Added 'power' as a binary operator in expression classes and expression grammar.
Former-commit-id: c58321709e
|
11 years ago |
dehnert
|
478f5ee38c
|
Started separating expression parsing from PRISM model parsing.
Former-commit-id: 84d1354f97
|
11 years ago |
dehnert
|
28eed65a0d
|
Fixed a reference to a non-existant option.
Former-commit-id: 02020513cc
|
11 years ago |
PBerger
|
5503e91bb3
|
Added detailed time measurement using std::chrono, leading to more useful information for comparison against Prism, etc.
Former-commit-id: 98e3e8e097
|
11 years ago |
PBerger
|
7ab2a84c0f
|
Small beauty fixes to the Cudd Interface
Former-commit-id: 631d5a20bd
|
11 years ago |
PBerger
|
03399375f8
|
Fixed an unintended 32bit shift being expanded to 64 bit
Former-commit-id: b2adc2a5ba
|
11 years ago |
PBerger
|
b5cb0cde1d
|
Fixed a typo in the StormOptions.cpp
Former-commit-id: a23d47d112
|
11 years ago |
PBerger
|
b7ad4398e2
|
Fixed an error in the interface of the LpSolvers.
Former-commit-id: 65e415efb2
|
11 years ago |
dehnert
|
63f55b38f0
|
Removed debug output that was - of course - never there. (You saw nothing!)
Former-commit-id: 9249928f54
|
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
|
e79fa50999
|
Changed naming of DD variables belonging to one meta variable slightly: only integer-valued meta variables now get a '.i' suffix to denote their i-th bit.
Former-commit-id: 771312ac31
|
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 |
dehnert
|
1513241985
|
Added functions for more efficiently retrieving the DD for 'greater than constant', 'greater or equal than constant' and 'notZero'.
Former-commit-id: 9d80c29f27
|
11 years ago |
dehnert
|
b1f22c1747
|
Added shortcut DD interface to compute \'greaterZero\' on a DD.
Former-commit-id: 65585533fd
|
11 years ago |
dehnert
|
9e506f40bc
|
Some fixes for MSVC. :P
Former-commit-id: 1429e54f73
|
11 years ago |
dehnert
|
6a2d75d68d
|
Some changes in anticipation of integrating MEDDLY.
Former-commit-id: 0f7a71ec9b
|
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
|
66d6fa3bb4
|
Fixed wrong type.
Former-commit-id: 59e08c3669
|
11 years ago |
dehnert
|
686618e6e2
|
Added missing header to (hopefully) fix MSVC problems.
Former-commit-id: 0247ce1e35
|
11 years ago |
dehnert
|
9e746549a8
|
Fully adapted MILP-based counterexample generator to new LP solver interface.
Former-commit-id: 83f3b8c507
|
11 years ago |
dehnert
|
db4721ce3a
|
Started adapting MILP-based counterexample generator to new LP solver interface.
Former-commit-id: b571d744db
|
11 years ago |
dehnert
|
d80586b4aa
|
Adapted MA model checker to new LP solver interface (LRA computation).
Former-commit-id: b23b72c851
|
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
|
d5c2f9248f
|
Finished linear coefficient visitor and adapted glpk solver to new expression-based LP solver interface.
Former-commit-id: ba1d3a912f
|
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
|
ab89716286
|
Merge branch 'master' into lpsolverInterface
Former-commit-id: 09c7d170b8
|
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
|
f60ea09cf4
|
Valuations now have methods to check whether they contain a given identifier.
Former-commit-id: 541c27d543
|
11 years ago |
dehnert
|
024b98978f
|
Made internal changes to SimpleValuations to (hopefully) make it nice and fast.
Former-commit-id: 1e9f18f522
|
11 years ago |
dehnert
|
3158d19123
|
Started working on adapting LP solver interface to new expressions.
Former-commit-id: 6131736a7f
|
11 years ago |
dehnert
|
9d3e78ab89
|
Cudd now gets 2GB instead of 2MB by default.
Former-commit-id: 06cf809493
|
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
|
2d8cc2efcd
|
Added reordering functionality to DD interface.
Former-commit-id: ffb8ad62f1
|
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
|
a0df98a6eb
|
Removed unnecessary virtual keyword in Expression class.
Former-commit-id: f879cd579e
|
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
|
d00cf794f1
|
Fixed wrong invocation of option system so all tests pass again, sorry about that, Philipp. :)
Former-commit-id: 475923edc4
|
11 years ago |
dehnert
|
9b31033d05
|
Added options for Cudd manager to set precision, reordering technique and maxmem.
Former-commit-id: c18bfab518
|
11 years ago |
dehnert
|
3667261429
|
Merge branch 'master' into PrismParserErrorHandling
Former-commit-id: 5f7743942c
|
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
|
83f9832e2d
|
Added type check visitor to validate types of identifiers in expressions. Started writing validation method on PRISM program class.
Former-commit-id: 6416bea711
|
11 years ago |
dehnert
|
873d80cd2d
|
If a module is renamed from some other module, this is now kept track of in the respective PRISM classes.
Former-commit-id: c07e25ac55
|
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
|
6f9dd7107d
|
Added universal abstraction function to DD layer.
Former-commit-id: 56e5d62b5a
|
11 years ago |