Alexander Bork
|
2709b7d828
|
Merge branch 'master' into dftFDEP
|
6 years ago |
|
Alexander Bork
|
10bb42e0f6
|
First version of non-Markovian state elimination for MAs
|
6 years ago |
|
Alexander Bork
|
549774abc9
|
Added state remapping in state elimination
|
6 years ago |
|
Alexander Bork
|
27e65d5669
|
Added construction of the state remapping for elimination of non-Markovian states in MAs
|
6 years ago |
|
Alexander Bork
|
add2a40a62
|
Integrated results of FDEP conflict search in DFT state space generation
|
6 years ago |
|
Alexander Bork
|
3616bdbf13
|
Added two test cases for the FDEP conflict search
|
6 years ago |
|
Alexander Bork
|
e2ef6bc52a
|
Added missing initialization of result vector
|
6 years ago |
|
Alexander Bork
|
589555c75f
|
Moved dynamic behavior computation from builder to DFT and added SEQ and SPARE cases
|
6 years ago |
|
Alexander Bork
|
aa150fc2e3
|
Extended FDEP conflict search by not considering pairs of FDEPs with static behavior
|
6 years ago |
|
Alexander Bork
|
bec75813b1
|
Added computation of dynamic behavior vector for DFTs
|
6 years ago |
|
Alexander Bork
|
39ec751f8d
|
Removed debugging output
|
6 years ago |
|
Alexander Bork
|
9bfc7858d0
|
Added improved upper bound correction
|
6 years ago |
|
Alexander Bork
|
583a880620
|
Adjusted DFT to SMT conversion to deal with constant failures
|
6 years ago |
|
Alexander Bork
|
a0c42fa630
|
Added debugging messages for transformations
|
6 years ago |
|
Alexander Bork
|
1d505d2ee0
|
Added check if DFT transformation is needed
|
6 years ago |
|
Alexander Bork
|
dde18d45eb
|
Added tests for DFT transformator
|
6 years ago |
|
Alexander Bork
|
74aa93d23d
|
Moved elimination of non-binary dependencies from builder to the DFT transformator
|
6 years ago |
|
Alexander Bork
|
12c0a6d72c
|
Added unique constant failure in transformation
|
6 years ago |
|
Alexander Bork
|
69987cc76c
|
Copying of original DFT and changing all constant BEs to be failsafe
|
6 years ago |
|
Alexander Bork
|
f258afa8a2
|
Added basis for DFT transformator
|
6 years ago |
|
Alexander Bork
|
b3cf06d6dd
|
Check in SMT checker that only one BE is constantly failed
|
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
|
e06bb99cc4
|
Changed DEP conflict constraint to avoid double check
|
6 years ago |
|
Alexander Bork
|
baa8a6dbcb
|
Improved conflict search by directly capturing DEPs with same trigger
|
6 years ago |
|
Alexander Bork
|
965c54b76d
|
Fixed error that only one FDEP was required to be active for a possible conflict to be detected
|
6 years ago |
|
Alexander Bork
|
5765824782
|
Reworked SMT result interface
|
6 years ago |
|
Alexander Bork
|
38ccd51ae1
|
Added check for conflicts between dependencies in the DFT
|
6 years ago |
|
Alexander Bork
|
80fc8fb56b
|
Fix for error that checkbound may be large than number of Markovian states
|
6 years ago |
|
Alexander Bork
|
28a878f154
|
Adjusted lower bound correction to new BE distinction
|
6 years ago |
Matthias Volk
|
7995100441
|
Small fixes in DFT tests
|
6 years ago |
|
Matthias Volk
|
521461737a
|
Adaption to changes in BEs
|
6 years ago |
|
Matthias Volk
|
23f1e73137
|
Merge from branch 'dft'
|
6 years ago |
Tim Quatmann
|
63a9b4485b
|
FormulaParserGrammar: Adding support for time-bounded formulas with exact time-bound, e.g., F=12 "target"
|
6 years ago |
|
Alexander Bork
|
f37bcea1ea
|
Added test for bound correction
|
6 years ago |
|
Tim Quatmann
|
b4f652bbc8
|
Reducing the nesting when creating a expression::sum(...).
|
6 years ago |
|
Tim Quatmann
|
a829c52a0d
|
ExpressionParser can now parse round expressions.
|
6 years ago |
|
Tim Quatmann
|
66a7bd5954
|
implemented creation of round expression.
|
6 years ago |
|
Tim Quatmann
|
b70f28b10e
|
Ensured that utility function for rounding always rounds towards infinity.
|
6 years ago |
|
Tim Quatmann
|
0e18046934
|
Fixed translating ceil(x) to mathsat expressions.
|
6 years ago |
|
Tim Quatmann
|
d201580d92
|
Refactored simplification of UnaryNumericalFunctionExpression.
|
6 years ago |
|
Tim Quatmann
|
a34037bff4
|
Added utility function for rounding.
|
6 years ago |
|
Alexander Bork
|
d42dea79c3
|
Added comments to explain the query
|
6 years ago |
|
Alexander Bork
|
74d1bf3c7e
|
Merge remote-tracking branch 'origin/dftSMT' into dftSMT
|
6 years ago |
|
Alexander Bork
|
948485c226
|
Reworked lower bound computation
|
6 years ago |
|
Alexander Bork
|
eeccb2092a
|
Added variables for trigger and resolution timepoints of dependencies
|
6 years ago |
|
Matthias Volk
|
426c293090
|
Travis: disable installation of carl-parser
|
6 years ago |
|
Matthias Volk
|
2d20365674
|
Travis: support for Ubuntu 19.04
|
6 years ago |
|
Matthias Volk
|
75cfa17966
|
Fixed compile issue on Linux
|
6 years ago |
|
Matthias Volk
|
5729066add
|
Merge branch 'master' into dft
|
6 years ago |
