diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index f01fe0936..2b07436f5 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -167,9 +167,10 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - - std::tuple>, boost::optional>, boost::optional, boost::optional, boost::optional> result = computeReachabilityProbability(*dtmc, filterFormula); - storm::RationalFunction valueFunction = std::get<0>(result); + + storm::modelchecker::reachability::SparseSccModelChecker modelchecker; + + storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, filterFormula); STORM_PRINT_AND_LOG(std::endl << "computed value " << valueFunction << std::endl); // Get variables from parameter definitions in prism program. @@ -190,11 +191,11 @@ int main(const int argc, const char** argv) { storm::utility::exportParametricMcResult(valueFunction, constraintCollector); } - if (storm::settings::parametricSettings().exportToSmt2File() && std::get<1>(result) && std::get<2>(result) && std::get<3>(result) && std::get<4>(result) && std::get<5>(result)) { - storm::modelchecker::reachability::DirectEncoding dec; - storm::utility::exportStringStreamToFile(dec.encodeAsSmt2(std::get<1>(result).get(), std::get<2>(result).get(), parameters, std::get<3>(result).get(), carl::rationalize(std::get<4>(result).get()), std::get<5>(result).get()), "out.smt"); - } - +// if (storm::settings::parametricSettings().exportToSmt2File() && std::get<1>(result) && std::get<2>(result) && std::get<3>(result) && std::get<4>(result) && std::get<5>(result)) { +// storm::modelchecker::reachability::DirectEncoding dec; +// storm::utility::exportStringStreamToFile(dec.encodeAsSmt2(std::get<1>(result).get(), std::get<2>(result).get(), parameters, std::get<3>(result).get(), carl::rationalize(std::get<4>(result).get()), std::get<5>(result).get()), "out.smt"); +// } + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); return 0;