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
masawei
0b9198122f
Done with PrCTL.
- Began removing NoBoundFormulas, since they might not be needed anymore. This task will be taken over by filters if they are to be implemented.
Next up: CSL
Former-commit-id: 6164f73737
11 years ago
dehnert
f6587b424d
Further work on PrismParser and the related PRISM classes...
Former-commit-id: be4ae055dd
11 years ago
masawei
b8317b7edf
Working in the new structure of the formula tree.
-Done with LTL.
-Working on PrCTL.
Former-commit-id: 1ec3c6993a
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