Browse Source

Ignore rewards for bisimulation quotienting (of parametric models) if the property to check is not related to rewards.

Former-commit-id: ab9f1d8f3c
tempestpy_adaptions
dehnert 10 years ago
parent
commit
c060377de5
  1. 2
      src/stormParametric.cpp

2
src/stormParametric.cpp

@ -192,7 +192,7 @@ int main(const int argc, const char** argv) {
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
storm::storage::DeterministicModelBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
storm::storage::DeterministicModelBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), keepRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true);
dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
dtmc->printModelInformationToStream(std::cout);

Loading…
Cancel
Save