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
sjunges
3d41c36153
Merge branch 'master' into parametricSystems
Former-commit-id: f6752d5c26
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
sjunges
6bc50e3d76
brp example
Former-commit-id: 06d1553d5f
11 years ago
sjunges
72c804815e
several *small* fixes and better direct encoding
Former-commit-id: 04265d8fb5
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
sjunges
c0b5757e4d
Adding new atomic propositions and attach it to a set of states
Former-commit-id: 2fee551b17
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
sjunges
3387e288f8
Merge branch 'master' into parametricSystems
Former-commit-id: 0c71b31069
11 years ago
sjunges
d4c2657856
Parsing parameteric dtmcs and exporting them to smt2
Former-commit-id: c791625d40
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
dehnert
63601e0b8a
Calling getExpression on an undefined constant is now properly treated with an exception.
Former-commit-id: 2d3e06a20a
11 years ago
dehnert
f1cac96d4c
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: f784694298
11 years ago
dehnert
dc80b987c2
Merge branch 'master' into ddLayerExtensions
Former-commit-id: 9eab593479
11 years ago
dehnert
6078e07476
First version of DD iterator; small test included.
Former-commit-id: 2ec2323886
11 years ago
PBerger
f2383ccfb5
Added missing definitions required for CUDD to compile under 64bit architectures.
Former-commit-id: 4e40ea7ee3
11 years ago
PBerger
0a501b6e76
Added a constructor for GlobalProgramInformation as MSVC fails to default bool to false.
Former-commit-id: bd50a770c8
11 years ago
PBerger
90fc5faca2
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 6bae9c23cf
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
d57a0c9901
Replaced memcpy by std::copy.
Former-commit-id: ef31cf9977
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
3940dbf45c
Accessing index of node via method interface, not member access.
Former-commit-id: d53006d5d4
11 years ago
dehnert
5fe7ffe51a
Added missing function declaration in CUDD'c C++ interface. Started on an iterator for DD valuations.
Former-commit-id: a97ccdec3d
11 years ago
sjunges
7ca6a4edeb
sub part for parameters, working parsing for non parametric systems into a parametric system
Former-commit-id: 7714692e32
11 years ago
sjunges
8142a8e004
some fixes for using something different from doubles for templated value type :)
Former-commit-id: d26d06b265
11 years ago
sjunges
f9a0c94c1b
added options for encoded reachability and parameters
Former-commit-id: 7456b4c0a3
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
masawei
6025dce144
Further work on the formuolas.
- Finished the third and last logic: Csl.
- Note that nothing compiles as of yet. This is due to the removal of the NoBoundOperators wich are expected to be replaced by filters.
Former-commit-id: d26ae768f7
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
sjunges
b654866cb2
Merge branch 'master' into param_dtmc2smt
Former-commit-id: 7eb2effb2f
11 years ago
dehnert
88a5be5b97
Unified some method names.
Former-commit-id: 3cda728bf6
11 years ago
dehnert
cc625a2e00
Added a ton of ifndefs, because MSVC does not yet support defaulting move constructors/assignments.
Former-commit-id: 105792abac
11 years ago
dehnert
164c8225fd
Fixed some minor issues.
Former-commit-id: 80f0ae4c9c
11 years ago
dehnert
7667933caf
First working version of explicit model generation using the new PRISM classes and expressions.
Former-commit-id: e71408cb89
11 years ago
dehnert
d9345b19e9
Further work on adapting explicit model generator to new PRISM classes.
Former-commit-id: 01cefceb52
11 years ago
dehnert
a642ba6e72
Started adapting dependent classes to new PRISM classes.
Former-commit-id: 59155b5fc9
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