dehnert
|
9a7c24372e
|
Added crude version of 'dump to explicit format' for Dtmcs.
Former-commit-id: bbe6195046
|
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 |
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 |
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 |
dehnert
|
f6587b424d
|
Further work on PrismParser and the related PRISM classes...
Former-commit-id: be4ae055dd
|
11 years ago |
dehnert
|
e67eb05309
|
Changed internal data structures of PRISM classes slightly. Added classs for certain ingredients that were represented as primitives before.
Former-commit-id: bdc61e88a5
|
11 years ago |
dehnert
|
cac8a50e90
|
Further work on PRISM grammar (commit to switch workplace).
Former-commit-id: 2969fe50a3
|
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 |
sjunges
|
8ca5ac176e
|
fixed spelling in comment: breath-first search
Former-commit-id: 21e719734b
|
11 years ago |
dehnert
|
cc0c327668
|
Removed superfluous grammars and started working on making one PRISM grammar to rule them all.
Former-commit-id: 375acb4699
|
11 years ago |
dehnert
|
41b31df0ab
|
Added small tests for implies/iff in expressions.
Former-commit-id: 3d90be7596
|
11 years ago |
dehnert
|
d87c79d0f6
|
Added implies/iff to expression classes. Finished reworking PRISM classes.
Former-commit-id: ca202042ed
|
11 years ago |
dehnert
|
d88876d0cd
|
PRISM classes almost adapted to new expression classes. TODO: source file of PRISM program.
Former-commit-id: 929a78684d
|
11 years ago |