From 581410c54b31de8b94ef1c7f0c3c90b7b7dad847 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 11 Sep 2018 11:16:15 +0200 Subject: [PATCH] Add check acyclic --- src/storm-pars-cli/storm-pars.cpp | 172 ++++++++++++++++-------------- 1 file changed, 90 insertions(+), 82 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index d57c4932f..befc25505 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -52,7 +52,7 @@ namespace storm { namespace pars { - + typedef typename storm::cli::SymbolicInput SymbolicInput; template @@ -60,11 +60,11 @@ namespace storm { SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) { // Intentionally left empty. } - + bool empty() const { return cartesianProducts.empty(); } - + std::vector::type, std::vector::type>>> cartesianProducts; bool graphPreserving; bool exact; @@ -79,7 +79,7 @@ namespace storm { } return result; } - + template SampleInformation parseSamples(std::shared_ptr const& model, std::string const& sampleString, bool graphPreserving) { STORM_LOG_THROW(!model || model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models."); @@ -88,7 +88,7 @@ namespace storm { if (sampleString.empty()) { return sampleInfo; } - + // Get all parameters from the model. std::set::type> modelParameters; auto const& sparseModel = *model->as>(); @@ -100,14 +100,14 @@ namespace storm { boost::split(cartesianProducts, sampleString, boost::is_any_of(";")); for (auto& product : cartesianProducts) { boost::trim(product); - + // Get the values string for each variable. std::vector valuesForVariables; boost::split(valuesForVariables, product, boost::is_any_of(",")); for (auto& values : valuesForVariables) { boost::trim(values); } - + std::set::type> encounteredParameters; sampleInfo.cartesianProducts.emplace_back(); auto& newCartesianProduct = sampleInfo.cartesianProducts.back(); @@ -118,7 +118,7 @@ namespace storm { boost::trim(variableName); std::string values = varValues.substr(equalsPosition + 1); boost::trim(values); - + bool foundParameter = false; typename utility::parametric::VariableType::type theParameter; for (auto const& parameter : modelParameters) { @@ -131,56 +131,56 @@ namespace storm { } } STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'."); - + std::vector splitValues; boost::split(splitValues, values, boost::is_any_of(":")); STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter."); - + auto& list = newCartesianProduct[theParameter]; - + for (auto& value : splitValues) { boost::trim(value); list.push_back(storm::utility::convertNumber::type>(value)); } } - + STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples."); } - + return sampleInfo; } - + template std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); - + std::pair, bool> result = std::make_pair(model, false); - + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); result.second = true; } - + if (generalSettings.isBisimulationSet()) { result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); result.second = true; } - + if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); result.second = true; } - + return result; } - + template std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - + std::pair, bool> result = std::make_pair(model, false); - + auto coreSettings = storm::settings::getModule(); if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { // Currently, hybrid engine for parametric models just referrs to building the model symbolically. @@ -195,11 +195,11 @@ namespace storm { } return result; } - + template std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - + std::pair, bool> result = std::make_pair(model, false); if (model->isSparseModel()) { result = storm::pars::preprocessSparseModel(result.first->as>(), input); @@ -207,13 +207,13 @@ namespace storm { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); result = storm::pars::preprocessDdModel(result.first->as>(), input); } - + if (result.second) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; } - + template void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation const* valuation = nullptr) { if (result) { @@ -229,11 +229,11 @@ namespace storm { } ss << entry.first << "=" << entry.second; } - + STORM_PRINT_AND_LOG(" for instance [" << ss.str() << "]"); } STORM_PRINT_AND_LOG(": ") - + auto const* regionCheckResult = dynamic_cast const*>(result.get()); if (regionCheckResult != nullptr) { auto regionSettings = storm::settings::getModule(); @@ -262,7 +262,7 @@ namespace storm { STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); } } - + template void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback) { for (auto const& property : properties) { @@ -274,59 +274,59 @@ namespace storm { postprocessingCallback(result); } } - + template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation const& samples) { - + // When samples are provided, we create an instantiation model checker. ModelCheckerType modelchecker(model); - + for (auto const& property : input.properties) { storm::cli::printModelCheckingProperty(property); - + modelchecker.specifyFormula(storm::api::createTask(property.getRawFormula(), true)); modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving); - + storm::utility::parametric::Valuation valuation; - + std::vector::type> parameters; std::vector::type>::const_iterator> iterators; std::vector::type>::const_iterator> iteratorEnds; - + storm::utility::Stopwatch watch(true); for (auto const& product : samples.cartesianProducts) { parameters.clear(); iterators.clear(); iteratorEnds.clear(); - + for (auto const& entry : product) { parameters.push_back(entry.first); iterators.push_back(entry.second.cbegin()); iteratorEnds.push_back(entry.second.cend()); } - + bool done = false; while (!done) { // Read off valuation. for (uint64_t i = 0; i < parameters.size(); ++i) { valuation[parameters[i]] = *iterators[i]; } - + storm::utility::Stopwatch valuationWatch(true); std::unique_ptr result = modelchecker.check(Environment(), valuation); valuationWatch.stop(); - + if (result) { result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); } printInitialStatesResult(result, property, &valuationWatch, &valuation); - + for (uint64_t i = 0; i < parameters.size(); ++i) { ++iterators[i]; if (iterators[i] == iteratorEnds[i]) { // Reset iterator and proceed to move next iterator. iterators[i] = product.at(parameters[i]).cbegin(); - + // If the last iterator was removed, we are done. if (i == parameters.size() - 1) { done = true; @@ -336,15 +336,15 @@ namespace storm { break; } } - + } } - + watch.stop(); STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl); } } - + template void verifyPropertiesAtSamplePoints(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { if (model->isOfType(storm::models::ModelType::Dtmc)) { @@ -357,10 +357,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs."); } } - + template void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { - + if (samples.empty()) { verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { @@ -380,7 +380,7 @@ namespace storm { }); } else { STORM_LOG_TRACE("Sampling the model at given points."); - + if (samples.exact) { verifyPropertiesAtSamplePoints(model, input, samples); } else { @@ -388,17 +388,17 @@ namespace storm { } } } - + template void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); - + auto parametricSettings = storm::settings::getModule(); auto regionSettings = storm::settings::getModule(); - + std::function(std::shared_ptr const& formula)> verificationCallback; std::function const&)> postprocessingCallback; - + STORM_PRINT_AND_LOG(std::endl); if (regionSettings.isHypothesisSet()) { STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); @@ -412,37 +412,37 @@ namespace storm { } auto engine = regionSettings.getRegionCheckEngine(); STORM_PRINT_AND_LOG(" using " << engine); - + // Check the given set of regions with or without refinement if (regionSettings.isRefineSet()) { STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); - boost::optional optionalDepthLimit; - if (regionSettings.isDepthLimitSet()) { - optionalDepthLimit = regionSettings.getDepthLimit(); - } - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); - return result; - }; + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); + boost::optional optionalDepthLimit; + if (regionSettings.isDepthLimitSet()) { + optionalDepthLimit = regionSettings.getDepthLimit(); + } + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); + return result; + }; } else { STORM_PRINT_AND_LOG("." << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); - return result; - }; + std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); + return result; + }; } - + postprocessingCallback = [&] (std::unique_ptr const& result) { - if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); - } - }; - + if (parametricSettings.exportResultToFile()) { + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + } + }; + verifyProperties(input.properties, verificationCallback, postprocessingCallback); } - + template void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { if (regions.empty()) { @@ -466,19 +466,19 @@ namespace storm { auto buildSettings = storm::settings::getModule(); auto parSettings = storm::settings::getModule(); - + auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); - + std::shared_ptr model; if (!buildSettings.isNoBuildModelSet()) { model = storm::cli::buildModel(engine, input, ioSettings); } - + if (model) { model->printModelInformationToStream(std::cout); } - + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); if (parSettings.isMonotonicityAnalysisSet()) { @@ -527,17 +527,25 @@ namespace storm { if (parSettings.isMonotonicityAnalysisSet()) { std::cout << "Hello, Jip2" << std::endl; + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); std::shared_ptr> sparseModel = model->as>(); + // Check if MC is acyclic + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(sparseModel->getTransitionMatrix(), false, false); + for (auto i = 0; i < decomposition.size(); ++i) { + auto scc = decomposition.getBlock(i); + STORM_LOG_THROW(scc.size() <= 1, storm::exceptions::NotSupportedException, "Cycle found, not supporting cyclic MCs"); + } + + // Transform to Lattices storm::utility::Stopwatch latticeWatch(true); storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); std::tuple criticalPair = extender->toLattice(formulas); - - auto assumptionMaker = storm::analysis::AssumptionMaker(extender, sparseModel->getNumberOfStates()); std::map>> result = assumptionMaker.startMakingAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); + latticeWatch.stop(); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); @@ -559,7 +567,7 @@ namespace storm { samples = parseSamples(model, samplesAsString, parSettings.isSamplesAreGraphPreservingSet()); samples.exact = parSettings.isSampleExactSet(); } - + if (model) { storm::cli::exportModel(model, input); } @@ -574,18 +582,18 @@ namespace storm { verifyParametricModel(model, input, regions, samples); } } - + void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); - + auto coreSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); - + processInputWithValueTypeAndDdlib(symbolicInput); }