Matthias Volk
|
a99be1bb06
|
Revised relevant events
|
5 years ago |
|
Matthias Volk
|
395081cdf9
|
Moved DFT preprocessing in api functions
|
5 years ago |
|
Matthias Volk
|
190e36605a
|
Refactored computation of relevant events
|
5 years ago |
Alexander Bork
|
605546358b
|
Added option to merge labels of eliminated states into existing states
|
6 years ago |
|
Alexander Bork
|
e28203fbb8
|
Added option to merge labels of eliminated states into existing states
|
6 years ago |
|
Matthias Volk
|
e4e069a98c
|
Slight refactoring of transformations
|
6 years ago |
|
Matthias Volk
|
fab86e8823
|
DFT wellformedness check can be performed stricter as precondition for analysis
|
6 years ago |
|
Matthias Volk
|
39cedc223e
|
Use ValueParsen in DFTJsonParser
|
6 years ago |
|
Alexander Bork
|
a73c2691b6
|
Integration of the new settings in the DFT analysis
|
6 years ago |
|
Alexander Bork
|
ec67166041
|
Decoupled preprocessing and SMT solving in commandline interface
|
6 years ago |
|
Alexander Bork
|
449c513db2
|
Cleanup DFTASFChecker
|
6 years ago |
|
Alexander Bork
|
75d28060cc
|
Moved failure bound computation to decouple it from the SMT checker
|
6 years ago |
|
Alexander Bork
|
9c74bbed24
|
Decoupled FDEP conflict search and SMT solver
|
6 years ago |
|
Alexander Bork
|
ca4dceaae1
|
Added experimental support for constant BEs
|
6 years ago |
|
Alexander Bork
|
31f4683094
|
Added activation for experimental DFT SMT analysis
|
6 years ago |
|
Alexander Bork
|
baa8a6dbcb
|
Improved conflict search by directly capturing DEPs with same trigger
|
6 years ago |
|
Alexander Bork
|
5765824782
|
Reworked SMT result interface
|
6 years ago |
|
Alexander Bork
|
a669c69fc9
|
Added tests for SMT encoding
|
6 years ago |
|
Alexander Bork
|
5d5487140f
|
Fixed bound calculation for SMT encoding
|
6 years ago |
|
Matthias Volk
|
f2c902eedb
|
Set labels, dont care propagation and unique failed state according to relevant events
|
6 years ago |
|
Matthias Volk
|
256137b080
|
Some refactoring
|
6 years ago |
|
Matthias Volk
|
972371c9a2
|
Started on the notion of 'relevant events' for DFT analysis
|
6 years ago |
|
Matthias Volk
|
6dbe2441b9
|
Removed unnecessary members
|
6 years ago |
|
Matthias Volk
|
7a8dbf8828
|
Heuristic is argument for functions in approximation algorithm
|
6 years ago |
|
Matthias Volk
|
5952aa8a6f
|
Set labels, dont care propagation and unique failed state according to relevant events
|
6 years ago |
|
Alexander Bork
|
d06cf59eba
|
Added SMT function to calculate lower bound for number of DFT failures needed for failure of TLE
|
6 years ago |
|
Alexander Bork
|
1976a41298
|
Reworked solver integration
|
6 years ago |
|
Alexander Bork
|
4507b484d5
|
Re-added option to export DFTs to smtlib2 SMT files
|
6 years ago |
|
Alexander Bork
|
29b0c4a78f
|
First version of SMT solver integration for DFT analysis
|
6 years ago |
|
Matthias Volk
|
5f7bf64d44
|
Some refactoring
|
6 years ago |
|
Matthias Volk
|
99651bdc71
|
Started on the notion of 'relevant events' for DFT analysis
|
6 years ago |
|
Matthias Volk
|
2c1855f69a
|
Removed unnecessary members
|
6 years ago |
|
Matthias Volk
|
a410b6d7bc
|
Heuristic is argument for functions in approximation algorithm
|
6 years ago |
|
Matthias Volk
|
1140d96ba5
|
Added well-formedness check for DFTs
|
7 years ago |
|
Matthias Volk
|
f6faf9e3a5
|
Flag for printing information about model generated from DFT
|
7 years ago |
|
Matthias Volk
|
d6d2d96a92
|
Added JaniExportSettings to storm-dft
|
7 years ago |
dehnert
|
6ab7859c84
|
fixing more of Lindas issues
|
7 years ago |
|
Matthias Volk
|
454f9350d7
|
Export proprties in DFT->GSPN->Jani file
|
7 years ago |
|
Matthias Volk
|
cbd3880d87
|
General method for adding transient variables in GSPN->Jani conversion
|
7 years ago |
|
Matthias Volk
|
ce3b63da12
|
Fixed json export settings
|
7 years ago |
|
Matthias Volk
|
48efde755b
|
DFT: export to JSON as string
|
7 years ago |
|
Matthias Volk
|
369d106f99
|
DFT: load json from string
|
7 years ago |
TimQu
|
8f179217d0
|
fixes for storm-dft and storm-gspn
|
7 years ago |
|
TimQu
|
4a7a82627f
|
storm-gspn and storm-dft now use functionalities of storm-conv
|
7 years ago |
|
Alexander Bork
|
ec3cb1a134
|
Added alternative method to calculate priorities for better compatibility with MC4CSLTA
|
7 years ago |
|
Matthias Volk
|
1f221db280
|
Disable transformation of DFT properties to JANI
|
7 years ago |
|
Matthias Volk
|
eea940b625
|
Refactoring for transformation DFT->GSPN->JANI
|
7 years ago |
|
Matthias Volk
|
cf316df35e
|
Added settings for DFT-GSPN transformation
|
7 years ago |
|
Matthias Volk
|
480b1fb8e5
|
Added priorities to GSPN transformation
|
7 years ago |
|
Matthias Volk
|
0674f88cf5
|
Added option for merging DC and Failed places
|
7 years ago |
