radioGiorgio
|
0e9880c9f8
|
non deterministic transitions based memory structure
|
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 |
Jip Spel
|
6db964363e
|
Update for artifact evaluation ATVA
|
6 years ago |
|
Jip Spel
|
4a1f98a0ba
|
Fix segfaults
|
6 years ago |
Matthias Volk
|
84467267e0
|
Second try to improve performance for relevant events
|
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 |
TimQu
|
6d6dc7c6a7
|
EndComponentEliminatorTest: Fixed expected results since the order of end components changed.
|
6 years ago |
|
Matthias Volk
|
187d47d8ac
|
Try to improve performance for relevant events
|
6 years ago |
|
Tim Quatmann
|
3a8f352329
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
|
Tim Quatmann
|
e06852689c
|
GurobiLpSolver: Fixed rounding of integral results.
|
6 years ago |
|
Tim Quatmann
|
681665c881
|
DetSchedsParetoExplorer: Fixed an assertion.
|
6 years ago |
|
Tim Quatmann
|
834bcebd9c
|
LpChecker: Changed end component formulation. Added validity check.
|
6 years ago |
|
Tim Quatmann
|
e92966c3e4
|
ParetoCourveCheckResult: Print approx. value in case of exact checking.
|
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 |
|
Matthias Volk
|
d0494d07e6
|
Get settings only once for takeFirstDependency
|
6 years ago |
|
Tim Quatmann
|
09ddd4aef9
|
Merge branch 'master' into deterministicScheds
|
6 years ago |
|
Tim Quatmann
|
bc623d1203
|
MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler.
Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration.
|
6 years ago |
|
Tim Quatmann
|
5467043807
|
DeterministicSchedsLpChecker: Only consider end components with value zero for all objectives.
|
6 years ago |
|
Matthias Volk
|
820b48354d
|
Silenced warning
|
6 years ago |
|
Matthias Volk
|
24d0576009
|
Merge from master
|
6 years ago |
|
Matthias Volk
|
9c28ed990e
|
Use isBasicElement() instead of type
|
6 years ago |
|
Matthias Volk
|
51b210a1d6
|
Test case for symmetry reduction
|
6 years ago |
|
Matthias Volk
|
08859bd3e6
|
Fixed bug in computation of symmetry groups.
Thanks to Enno Ruijters for pointing out this issue.
|
6 years ago |
|
Matthias Volk
|
0dcb271866
|
Added assertions for better debugging
|
6 years ago |
|
Matthias Volk
|
3033d5444c
|
Refactoring
|
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 |
|
Tim Quatmann
|
c8ea0f60da
|
JaniBuilder: Fixed several issues that occurred with branch reward expressions over non-transient variables, including GitHub issue #47
|
6 years ago |
|
Tim Quatmann
|
ce9d784c35
|
QCVBS: Fixed models with empty 'open-paremeter-values' entry.
|
6 years ago |
|
TimQu
|
8865857f21
|
Fixed awkward printing of eventually formulas with reward accumulations.
|
6 years ago |
|
Alexander Bork
|
74aa93d23d
|
Moved elimination of non-binary dependencies from builder to the DFT transformator
|
6 years ago |
|
Matthias Volk
|
2779d13d2c
|
Fix for FindDoxygen with CMake 3.12
|
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 |
|
Jip Spel
|
8df0a05ab8
|
Fix assertion
|
6 years ago |
|
Jip Spel
|
2883f81be1
|
Move settings to separate file
|
6 years ago |
|
Matthias Volk
|
49570eb92d
|
Travis: install correct package for dot
|
6 years ago |
|
Jip Spel
|
6b8997c6ba
|
Merge branch 'master' into storm-pars-analysis-monotonicity
|
6 years ago |
|
Matthias Volk
|
719baa58f5
|
Set some more options for Doxygen
|
6 years ago |
|
Matthias Volk
|
b27e7774af
|
Travis: install dot for doxygen generation
|
6 years ago |
|
TimQu
|
c8dd748943
|
DeterministicScheds: Various bug fixes.
|
6 years ago |
|
TimQu
|
19cca3585f
|
PcaaWeightVectorChecker: Initializing weightedPrecision.
|
6 years ago |
|
TimQu
|
4f6822ec1d
|
EndComponentEliminator now provides an entry point where an end component decomposition can be given from outside.
|
6 years ago |
|
TimQu
|
71731e8003
|
Z3LpSolver: Fixed incremental support.
|
6 years ago |
