Matthias Volk
|
c0075f1cc4
|
Removed unused variable
|
7 years ago |
Alexander Bork
|
3473a930a2
|
Added hint towards uniquefailedbe flag in error message
|
7 years ago |
|
Alexander Bork
|
2ec921a683
|
Added support for constantly failed BEs in the model generation
|
7 years ago |
|
Alexander Bork
|
a257071346
|
Added option to transform a DFT to only use one unique constantly failed BE
|
7 years ago |
|
Alexander Bork
|
541e582934
|
Added support for BEs with probabilities in Galileo parser
|
7 years ago |
|
Matthias Volk
|
39cedc223e
|
Use ValueParsen in DFTJsonParser
|
7 years ago |
Tim Quatmann
|
429c91ff13
|
Added support for parsing fractions in DRN files.
|
7 years ago |
|
Alexander Bork
|
450e074c5b
|
Integrated non-Markovian state elimination into Storm MA modelchecking
|
7 years ago |
|
Alexander Bork
|
a73c2691b6
|
Integration of the new settings in the DFT analysis
|
7 years ago |
|
Alexander Bork
|
ec67166041
|
Decoupled preprocessing and SMT solving in commandline interface
|
7 years ago |
|
Alexander Bork
|
449c513db2
|
Cleanup DFTASFChecker
|
7 years ago |
|
Alexander Bork
|
75d28060cc
|
Moved failure bound computation to decouple it from the SMT checker
|
7 years ago |
|
Alexander Bork
|
9c74bbed24
|
Decoupled FDEP conflict search and SMT solver
|
7 years ago |
|
Alexander Bork
|
ae5c001d24
|
Moved non-Markovian state eliminator to its own class
|
7 years ago |
|
Alexander Bork
|
add2a40a62
|
Integrated results of FDEP conflict search in DFT state space generation
|
7 years ago |
|
Matthias Volk
|
47344f9080
|
Removed unused flat_set includes
|
7 years ago |
|
Alexander Bork
|
e2ef6bc52a
|
Added missing initialization of result vector
|
7 years ago |
|
Alexander Bork
|
589555c75f
|
Moved dynamic behavior computation from builder to DFT and added SEQ and SPARE cases
|
7 years ago |
|
Matthias Volk
|
84467267e0
|
Second try to improve performance for relevant events
|
7 years ago |
|
Alexander Bork
|
aa150fc2e3
|
Extended FDEP conflict search by not considering pairs of FDEPs with static behavior
|
7 years ago |
|
Alexander Bork
|
bec75813b1
|
Added computation of dynamic behavior vector for DFTs
|
7 years ago |
|
Alexander Bork
|
39ec751f8d
|
Removed debugging output
|
7 years ago |
|
Matthias Volk
|
187d47d8ac
|
Try to improve performance for relevant events
|
7 years ago |
|
Alexander Bork
|
9bfc7858d0
|
Added improved upper bound correction
|
7 years ago |
|
Alexander Bork
|
583a880620
|
Adjusted DFT to SMT conversion to deal with constant failures
|
7 years ago |
|
Alexander Bork
|
a0c42fa630
|
Added debugging messages for transformations
|
7 years ago |
|
Matthias Volk
|
d0494d07e6
|
Get settings only once for takeFirstDependency
|
7 years ago |
|
Matthias Volk
|
9c28ed990e
|
Use isBasicElement() instead of type
|
7 years ago |
|
Matthias Volk
|
08859bd3e6
|
Fixed bug in computation of symmetry groups.
Thanks to Enno Ruijters for pointing out this issue.
|
7 years ago |
|
Matthias Volk
|
0dcb271866
|
Added assertions for better debugging
|
7 years ago |
|
Matthias Volk
|
3033d5444c
|
Refactoring
|
7 years ago |
|
Alexander Bork
|
74aa93d23d
|
Moved elimination of non-binary dependencies from builder to the DFT transformator
|
7 years ago |
|
Alexander Bork
|
12c0a6d72c
|
Added unique constant failure in transformation
|
7 years ago |
|
Alexander Bork
|
69987cc76c
|
Copying of original DFT and changing all constant BEs to be failsafe
|
7 years ago |
|
Alexander Bork
|
f258afa8a2
|
Added basis for DFT transformator
|
7 years ago |
|
Alexander Bork
|
b3cf06d6dd
|
Check in SMT checker that only one BE is constantly failed
|
7 years ago |
|
Alexander Bork
|
ca4dceaae1
|
Added experimental support for constant BEs
|
7 years ago |
|
Alexander Bork
|
31f4683094
|
Added activation for experimental DFT SMT analysis
|
7 years ago |
|
Alexander Bork
|
e06bb99cc4
|
Changed DEP conflict constraint to avoid double check
|
7 years ago |
|
Alexander Bork
|
baa8a6dbcb
|
Improved conflict search by directly capturing DEPs with same trigger
|
7 years ago |
|
Alexander Bork
|
965c54b76d
|
Fixed error that only one FDEP was required to be active for a possible conflict to be detected
|
7 years ago |
|
Alexander Bork
|
5765824782
|
Reworked SMT result interface
|
7 years ago |
|
Alexander Bork
|
38ccd51ae1
|
Added check for conflicts between dependencies in the DFT
|
7 years ago |
|
Alexander Bork
|
80fc8fb56b
|
Fix for error that checkbound may be large than number of Markovian states
|
7 years ago |
|
Alexander Bork
|
28a878f154
|
Adjusted lower bound correction to new BE distinction
|
7 years ago |
|
Matthias Volk
|
521461737a
|
Adaption to changes in BEs
|
7 years ago |
|
Alexander Bork
|
d42dea79c3
|
Added comments to explain the query
|
7 years ago |
|
Alexander Bork
|
948485c226
|
Reworked lower bound computation
|
7 years ago |
|
Alexander Bork
|
eeccb2092a
|
Added variables for trigger and resolution timepoints of dependencies
|
7 years ago |
|
Matthias Volk
|
75cfa17966
|
Fixed compile issue on Linux
|
7 years ago |
