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
David_Korzeniewski
c3a71d5915
Merge branch 'master' into SmtSolvers
Conflicts:
src/storage/expressions/Expression.cpp
Former-commit-id: 151d48f807
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
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
2cb34d6e6b
Merge branch 'master' into SmtSolvers
Former-commit-id: c3550e8ad9
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
David_Korzeniewski
4cb346f8ce
Merge branch 'master' into SmtSolvers
Former-commit-id: 7fca03c3ab
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
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
dehnert
d0d80cf5e1
Started on making the PrismParser more robust.
Former-commit-id: 7ce1351d0c
11 years ago
masawei
2f5f8c0918
PrctlFilter is operational but not yet complete (proper standard output missing).
- General function of the filters: The filter as an abstraction layer between the control flow and the formula/modelchecker.
|- It has a formula as child but is not a formula itself.
|- It invokes the modelchecking process on the child formula and manipulates the result.
|- For the purpose of result manipulation it keeps a list of filter actions.
|- Each action manipulates the result in a certain way. For example: It returns only the results for states 25 to 140.
|- Furthermore the printing of the result to standard out and the log is no longer done by the modelchecker but by the filter.
|- That way the tasks of each class becomes more clear: Modelchecker to compute the results, filter to prepare the computed results for write out.
- Battled with a major design problem: How to integrate the optimizing operator (aka. min or max probs for non-det. models) into the filter scheme.
|- It is now integrated as a separate filter action, which does not touch the results but hold the flag determining whether to maximize or to minimize.
|- This action must be the innermost filter action (i.e. the first list entry) to have any effect.
|- This is combined with a special fuction of the modelchecker that manipulates the mutable minimizationStack calculates the modelchecking result and resets the stack to its original state.
|- This way the information whether to min, to max or not to try is managed by the filter and propagated as needed.
|- Remark: Fixed a major risk of undefined behavior in the SparseMdpPrctlModelChecker.
|- If the formula to be checked did not have a NoBoundFormula as root then the minimumOperatorStack would be empty and minimumOperatorStack.top() would result in undefined behavior.
|- Added tests whether the stack is empty before trying to read out the possibly non existant top element.
Next up: Implement similar filters for LTL and CSL and try to get it compiled.
Former-commit-id: 577998e027
11 years ago
dehnert
5816bd8860
Bugfix for explicit model adapter: empty choice labeling was not created for automatically added self-loops.
Former-commit-id: 6c63c28f59
11 years ago
masawei
299390cef5
Started on the filters.
- Got the general structure down.
- Now writing the output functions.
Next up: Finish the basic filter functionality.
Former-commit-id: 91daa0a9f7
11 years ago
dehnert
44ba492fe7
CuddDdManager now sets tolerance to 1e-15.
Former-commit-id: bfc985b5de
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
5b06259a05
Added ite operator for DDs in abstraction layer.
Former-commit-id: b1bc85e9e3
11 years ago
dehnert
3eb8f8e328
Bugfix: valuations now correctly store the given initial value for boolean variables.
Former-commit-id: a23f014303
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