From cd1bd6b538650bcf912b6fea196d03d7923c32f1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Feb 2017 15:05:05 +0100 Subject: [PATCH] Support for checking multiple dft properties at once --- src/storm-dft-cli/storm-dyftee.cpp | 86 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 358 ++++++++++-------- .../modelchecker/dft/DFTModelChecker.h | 38 +- 3 files changed, 258 insertions(+), 224 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 9a8cd033b..1dfe445e2 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -34,35 +34,44 @@ #include /*! - * Load DFT from filename, build corresponding Model and check against given property. + * Analyse the given DFT according to the given properties. + * We first load the DFT from the given file, then build the corresponding model and last check against the given properties. * - * @param property PCTC formula capturing the property to check. + * @param properties PCTL formulas capturing the properties to check. * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param enableDC Flag whether Don't Care propagation should be used. + * @param approximationError Allowed approximation error. */ template -void analyzeDFT(std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { +void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); - std::shared_ptr> dft; + + // Build DFT from given file. if (dftSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - std::cout << "Running DFT analysis on file " << dftSettings.getDftJsonFilename() << " with property " << property << std::endl; + std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; - std::cout << "Running DFT analysis on file " << dftSettings.getDftFilename() << " with property " << property << std::endl; + std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); } - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property)); - STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas."); + // Build properties + std::string propString = properties[0]; + for (size_t i = 1; i < properties.size(); ++i) { + propString += ";" + properties[i]; + } + std::vector> props = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(propString)); + STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + // Check model storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(*dft, formulas[0], symred, allowModularisation, enableDC, approximationError); + modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError); modelChecker.printTimings(); - modelChecker.printResult(); + modelChecker.printResults(); } /*! @@ -210,43 +219,42 @@ int main(const int argc, const char** argv) { #endif // Set min or max - bool minimal = true; + std::string optimizationDirection = "min"; if (dftSettings.isComputeMaximalValue()) { STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); - minimal = false; + optimizationDirection = "max"; } - // Construct pctlFormula - std::string pctlFormula = ""; - std::string operatorType = ""; - std::string targetFormula = ""; + // Construct properties to check for + std::vector properties; if (generalSettings.isPropertySet()) { - STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - pctlFormula = generalSettings.getProperty(); - } else if (dftSettings.usePropExpectedTime()) { - STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "T"; - targetFormula = "F \"failed\""; - } else if (dftSettings.usePropProbability()) { - STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "P";; - targetFormula = "F \"failed\""; - } else { - STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given."); + properties.push_back(generalSettings.getProperty()); + } + if (dftSettings.usePropExpectedTime()) { + properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropProbability()) { + properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropTimebound()) { std::stringstream stream; - stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\""; - operatorType = "P"; - targetFormula = stream.str(); + stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + properties.push_back(stream.str()); } - - if (!targetFormula.empty()) { - STORM_LOG_ASSERT(pctlFormula.empty(), "Pctl formula not empty."); - pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]"; + if (dftSettings.usePropTimepoints()) { + for (double timepoint : dftSettings.getPropTimepoints()) { + std::stringstream stream; + stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; + properties.push_back(stream.str()); + } + } + + if (properties.empty()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given."); } - - STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty."); + // Set possible approximation error double approximationError = 0.0; if (dftSettings.isApproximationErrorSet()) { approximationError = dftSettings.getApproximationError(); @@ -255,12 +263,12 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); } // All operations have now been performed, so we clean up everything and terminate. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index fadd6d6fe..362c49445 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -13,12 +13,7 @@ namespace storm { namespace modelchecker { template - DFTModelChecker::DFTModelChecker() { - checkResult = storm::utility::zero(); - } - - template - void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + void DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize this->approximationError = approximationError; totalTimer.start(); @@ -29,31 +24,31 @@ namespace storm { // TODO Matthias: check that all paths reach the target state for approximation // Checking DFT - if (formula->isProbabilityOperatorFormula() || !allowModularisation) { - checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError); - } else { - std::shared_ptr> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC); + if (properties[0]->isTimeOperatorFormula() && allowModularisation) { + // Use parallel composition as modularisation approach for expected time + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError); // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - checkResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + for (ValueType result : resultsValue) { + checkResults.push_back(result); + } + } else { + checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError); } totalTimer.stop(); } template - typename DFTModelChecker::dft_result DFTModelChecker::checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { STORM_LOG_TRACE("Check helper called"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool invResults = false; + size_t nrK = 0; // K out of M + size_t nrM = 0; // K out of M // Try modularisation - if(modularisationPossible) { - bool invResults = false; - std::vector> dfts; - size_t nrK = 0; // K out of M - size_t nrM = 0; // K out of M - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -61,7 +56,6 @@ namespace storm { STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); nrK = dfts.size(); nrM = dfts.size(); - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); @@ -70,7 +64,6 @@ namespace storm { nrK = 0; nrM = dfts.size(); invResults = true; - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::VOT: STORM_LOG_TRACE("top modularisation called VOT"); @@ -82,22 +75,29 @@ namespace storm { nrK -= 1; invResults = true; } - modularisationPossible = dfts.size() > 1; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - if (formula->isProbabilityOperatorFormula()) { + // Perform modularisation + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + // TODO Matthias: compute simultaneously + dft_results results; + for (auto property : properties) { + if (!property->isProbabilityOperatorFormula()) { + STORM_LOG_WARN("Could not check property: " << *property); + } else { // Recursively call model checking std::vector res; for(auto const ft : dfts) { - dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0); - res.push_back(boost::get(ftResult)); + // TODO Matthias: allow approximation in modularisation + dft_results ftResults = checkHelper(ft, {property}, symred, true, enableDC, 0.0); + STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); + res.push_back(boost::get(ftResults[0])); } // Combine modularisation results @@ -128,148 +128,138 @@ namespace storm { if(invResults) { result = storm::utility::one() - result; } - return result; + results.push_back(result); } } + return results; + } else { + // No modularisation was possible + return checkDFT(dft, properties, symred, enableDC, approximationError); } - - // If we are here, no modularisation was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - return checkDFT(dft, formula, symred, enableDC, approximationError); } template - std::shared_ptr> DFTModelChecker::buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + // TODO Matthias: use approximation? STORM_LOG_TRACE("Build model via composition"); - // Use parallel composition for CTMCs for expected time - STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool isAnd = true; // Try modularisation - if(modularisationPossible) { - std::vector> dfts; - bool isAnd = true; - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = true; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = false; break; case storm::storage::DFTElementType::VOT: - /*STORM_LOG_TRACE("top modularisation called VOT"); - dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); - */ // TODO enable modularisation for voting gate - modularisationPossible = false; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - bool firstTime = true; - std::shared_ptr> composedModel; - for (auto const ft : dfts) { - STORM_LOG_INFO("Building Model via parallel composition..."); - explorationTimer.start(); + // Perform modularisation via parallel composition + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + bool firstTime = true; + std::shared_ptr> composedModel; + for (auto const ft : dfts) { + STORM_LOG_INFO("Building Model via parallel composition..."); + explorationTimer.start(); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = ft.colourDFT(); + symmetries = ft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = ft.colourDFT(); - symmetries = ft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); + storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + //model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + explorationTimer.stop(); - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - std::shared_ptr> ctmc = model->template as>(); - - ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - - if (firstTime) { - composedModel = ctmc; - firstTime = false; - } else { - composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); - } + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + std::shared_ptr> ctmc = model->template as>(); - // Apply bisimulation - bisimulationTimer.start(); - composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - bisimulationTimer.stop(); - - STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); - if (composedModel->getNumberOfStates() <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } + // Apply bisimulation to new CTMC + bisimulationTimer.start(); + ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + if (firstTime) { + composedModel = ctmc; + firstTime = false; + } else { + composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); } - return composedModel; - } - } - // If we are here, no composition was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - explorationTimer.start(); - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = dft.colourDFT(); - symmetries = dft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); + // Apply bisimulation to parallel composition + bisimulationTimer.start(); + composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + + STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); + if (composedModel->getNumberOfStates() <= 15) { + STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); + } else { + STORM_LOG_TRACE("Transition matrix: too big to print"); + } + } + return composedModel; + } else { + // No composition was possible + explorationTimer.start(); + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - return model->template as>(); + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + //model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + explorationTimer.stop(); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + return model->template as>(); + } } template - typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError) { explorationTimer.start(); // Find symmetries @@ -288,11 +278,18 @@ namespace storm { // Build approximate Markov Automata for lower and upper bound approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::shared_ptr> model; + std::vector newResult; storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - bool probabilityFormula = formula->isProbabilityOperatorFormula(); - STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); + // TODO Matthias: compute approximation for all properties simultaneously? + std::shared_ptr property = properties[0]; + if (properties.size() > 1) { + STORM_LOG_WARN("Computing approximation only for first property: " << *property); + } + + bool probabilityFormula = property->isProbabilityOperatorFormula(); + STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -315,12 +312,11 @@ namespace storm { STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); buildingTimer.stop(); - // Check lower bound - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - ValueType newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult, approxResult.first), "New under-approximation " << newResult << " is smaller than old result " << approxResult.first); - approxResult.first = newResult; + // Check lower bounds + newResult = checkModel(model, {property}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first); + approxResult.first = newResult[0]; // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); @@ -328,11 +324,10 @@ namespace storm { model = builder.getModelApproximation(probabilityFormula ? true : false); buildingTimer.stop(); // Check upper bound - result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult), "New over-approximation " << newResult << " is greater than old result " << approxResult.second); - approxResult.second = newResult; + newResult = checkModel(model, {properties}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); + approxResult.second = newResult[0]; ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); @@ -343,7 +338,9 @@ namespace storm { } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); - return approxResult; + dft_results results; + results.push_back(approxResult); + return results; } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); @@ -365,32 +362,50 @@ namespace storm { explorationTimer.stop(); // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - return result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + dft_results results; + for (ValueType result : resultsValue) { + results.push_back(result); + } + return results; } } template - std::unique_ptr DFTModelChecker::checkModel(std::shared_ptr>& model, std::shared_ptr const& formula) { + std::vector DFTModelChecker::checkModel(std::shared_ptr>& model, property_vector const& properties) { // Bisimulation - bisimulationTimer.start(); if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { + bisimulationTimer.start(); STORM_LOG_INFO("Bisimulation..."); - model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); + bisimulationTimer.stop(); } - bisimulationTimer.stop(); - modelCheckingTimer.start(); // Check the model STORM_LOG_INFO("Model checking..."); - std::unique_ptr result(storm::verifySparseModel(model, formula)); - STORM_LOG_INFO("Model checking done."); - STORM_LOG_ASSERT(result, "Result does not exist."); + modelCheckingTimer.start(); + std::vector results; + + // Check each property + storm::utility::Stopwatch singleModelCheckingTimer; + for (auto property : properties) { + singleModelCheckingTimer.reset(); + singleModelCheckingTimer.start(); + STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); + std::unique_ptr result(storm::verifySparseModel(model, property, true)); + STORM_LOG_ASSERT(result, "Result does not exist."); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl); + results.push_back(resultValue); + singleModelCheckingTimer.stop(); + STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl); + } modelCheckingTimer.stop(); - return result; + STORM_LOG_INFO("Model checking done."); + return results; } template @@ -411,21 +426,30 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Building:\t" << buildingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Bisimulation:\t" << bisimulationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Modelchecking:\t" << modelCheckingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Total:\t\t" << totalTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Exploration:\t" << explorationTimer << "s" << std::endl; + os << "Building:\t" << buildingTimer << "s" << std::endl; + os << "Bisimulation:\t" << bisimulationTimer<< "s" << std::endl; + os << "Modelchecking:\t" << modelCheckingTimer << "s" << std::endl; + os << "Total:\t\t" << totalTimer << "s" << std::endl; } template - void DFTModelChecker::printResult(std::ostream& os) { + void DFTModelChecker::printResults(std::ostream& os) { + bool first = true; os << "Result: ["; - if (this->approximationError > 0.0) { - approximation_result result = boost::get(checkResult); - os << "(" << result.first << ", " << result.second << ")"; - } else { - os << boost::get(checkResult); + for (auto result : checkResults) { + if (!first) { + os << ", "; + } + if (this->approximationError > 0.0) { + approximation_result resultApprox = boost::get(result); + os << "(" << resultApprox.first << ", " << resultApprox.second << ")"; + } else { + os << boost::get(result); + } + if (first) { + first = false; + } } os << "]" << std::endl; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index c714999a8..6991ac888 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -18,26 +18,28 @@ namespace storm { class DFTModelChecker { typedef std::pair approximation_result; - typedef boost::variant dft_result; + typedef std::vector> dft_results; + typedef std::vector> property_vector; public: /*! * Constructor. */ - DFTModelChecker(); + DFTModelChecker() { + } /*! * Main method for checking DFTs. * * @param origDft Original DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation */ - void check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); + void check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); /*! * Print timings of all operations to stream. @@ -51,7 +53,7 @@ namespace storm { * * @param os Output stream to write to. */ - void printResult(std::ostream& os = std::cout); + void printResults(std::ostream& os = std::cout); private: @@ -62,8 +64,8 @@ namespace storm { storm::utility::Stopwatch modelCheckingTimer; storm::utility::Stopwatch totalTimer; - // Model checking result - dft_result checkResult; + // Model checking results + dft_results checkResults; // Allowed error bound for approximation double approximationError; @@ -72,21 +74,21 @@ namespace storm { * Internal helper for model checking a DFT. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * - * @return Model checking result (or in case of approximation two results for lower and upper bound) + * @return Model checking results (or in case of approximation two results for lower and upper bound) */ - dft_result checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError); + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Internal helper for building a CTMC from a DFT via parallel composition. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used @@ -94,30 +96,30 @@ namespace storm { * * @return CTMC representing the DFT */ - std::shared_ptr> buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Check model generated from DFT. * * @param dft The DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * * @return Model checking result */ - dft_result checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError = 0.0); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0); /*! - * Check the given markov model for the given property. + * Check the given markov model for the given properties. * - * @param model Model to check - * @param formula Formula to check for + * @param model Model to check + * @param properties Properties to check for * * @return Model checking result */ - std::unique_ptr checkModel(std::shared_ptr>& model, std::shared_ptr const& formula); + std::vector checkModel(std::shared_ptr>& model, property_vector const& properties); /*! * Checks if the computed approximation is sufficient, i.e.