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
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
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
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
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
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
masawei
185c2197cb
Fixed up the CslParser.
Next Up: Making the parsers static classes.
Former-commit-id: 247a105078
11 years ago
masawei
b45b52a097
Added the class AbstractRewardPathFormula to the PRCTL formula tree.
- This change splits the path formulas into probabilistic path formulas like Next or Until and reward path formulas like InstantaneousReward or SteadyStateReward.
|- That way it is assured at compile time that no reward path formula can ever be subformula of any probabilistic bound operator and vise versa.
Next up: Adopt changes in the Csl formula tree to the Csl parser.
Former-commit-id: d74c88bbf8
11 years ago
masawei
cf6623c68c
Intruduced legacy support.
- Every PRCTL formula that worked before works now and behaves in the same way. One exception:
|- Formulas of the type Pmin<0.5[Phi] and Rmin<0.5[Psi] result in a parsing error, as the comparison operator already implies the scheduler to be used.
| Also, the modelchecker now actually uses the comparison operator in order to choose the correct scheduler for MDPs.
Former-commit-id: d942d18e7e
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
David_Korzeniewski
37ef3feebb
Fixed return type of addBinaryVariable
Former-commit-id: 44fc99b9a3
11 years ago
David_Korzeniewski
4e6c9b7d6b
Implemented translating z3 expressions to storm expressions
Former-commit-id: 945ce77e35
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
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
masawei
0a2f974983
Added rules to the prctl parser to support filters.
Next up: Make rules for legacy support, make parser static.
Former-commit-id: 4d0c811adb
11 years ago
masawei
a6f20400df
Added similar filters for Ltl and Csl.
- Fixed similar undefined behavior for the MarkovAutomaton Csl modelchecker.
Next up: Make necessary changes to the formula parsers.
Former-commit-id: e8765fe58b
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
David_Korzeniewski
29083cc89c
Implemented asserting expressions and checking satisfiability with z3
Former-commit-id: bb49a49226
11 years ago
David_Korzeniewski
83d2a1c315
Adapted Z3ExpressionAdapter to deletion of constant expressions. Added functionality to autocreate variables in the solver. Added function to get variables and their types from an expression.
Former-commit-id: 29f8e2fb70
11 years ago
David_Korzeniewski
98f87a5e6d
Adapted Z3ExpressionAdapter for new expressions
SmtSolver now not copyable
Former-commit-id: e0d17fd21c
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
David_Korzeniewski
f69b79593c
initial interface for smt solver wrappers
Former-commit-id: e43b7afb3c
11 years ago