Browse Source

Fixed incorrect result of canHandleStatic for multi-objective formulas for MDP in hybrid engine and MA in sparse engine.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
ee0e90462f
  1. 1
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  2. 1
      src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

1
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@ -42,6 +42,7 @@ namespace storm {
if (requiresSingleInitialState) { if (requiresSingleInitialState) {
*requiresSingleInitialState = true; *requiresSingleInitialState = true;
} }
return true;
} }
return false; return false;
} }

1
src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@ -46,6 +46,7 @@ namespace storm {
if (requiresSingleInitialState) { if (requiresSingleInitialState) {
*requiresSingleInitialState = true; *requiresSingleInitialState = true;
} }
return true;
} }
return false; return false;
} }

Loading…
Cancel
Save