diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f1ad5f36e..f0ec400fe 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -53,19 +53,19 @@ namespace storm { namespace cli { - - + + struct SymbolicInput { // The symbolic model description. boost::optional model; - + // The original properties to check. std::vector properties; - + // The preprocessed properties to check (in case they needed amendment). boost::optional> preprocessedProperties; }; - + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { auto buildSettings = storm::settings::getModule(); if (ioSettings.isPrismOrJaniInputSet()) { @@ -93,7 +93,7 @@ namespace storm { STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); } } - + void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { if (ioSettings.isPropertySet()) { std::vector newProperties; @@ -102,11 +102,11 @@ namespace storm { } else { newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter); } - + input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); } } - + SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings) { // Parse the model input SymbolicInput input; @@ -118,21 +118,21 @@ namespace storm { input.properties = std::move(janiInput.second); modelParsingWatch.stop(); STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); - + // Parse additional properties boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); parseProperties(ioSettings, input, propertyFilter); - + // Substitute constant definitions auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex())); input.model = input.model.get().preprocess(constantDefinitions); if (!input.properties.empty()) { input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions); } - + return input; } - + SymbolicInput parseSymbolicInput() { auto ioSettings = storm::settings::getModule(); if (ioSettings.isQvbsInputSet()) { @@ -140,25 +140,25 @@ namespace storm { } else { // Parse the property filter, if any is given. boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); - + SymbolicInput input; parseSymbolicModelDescription(ioSettings, input); parseProperties(ioSettings, input, propertyFilter); return input; } } - + struct ModelProcessingInformation { - + // The engine to use storm::utility::Engine engine; - + // If set, bisimulation will be applied. bool applyBisimulation; - + // If set, a transformation to Jani will be enforced bool transformToJani; - + // Which data type is to be used for numbers ... enum class ValueType { FinitePrecision, @@ -167,34 +167,34 @@ namespace storm { }; ValueType buildValueType; // ... during model building ValueType verificationValueType; // ... during model verification - + // The Dd library to be used storm::dd::DdType ddType; - + // The environment used during model checking storm::Environment env; - + // A flag which is set to true, if the settings were detected to be compatible. // If this is false, it could be that the query can not be handled. bool isCompatible; }; - + void getModelProcessingInformationAutomatic(SymbolicInput const& input, ModelProcessingInformation& mpi) { auto hints = storm::settings::getModule(); - + STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); std::vector const& properties = input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties; STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a property."); STORM_LOG_WARN_COND(properties.size() == 1, "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered."); - + storm::utility::AutomaticSettings as; if (hints.isNumberStatesSet()) { as.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); } else { as.predict(input.model->asJaniModel(), properties.front()); } - + mpi.engine = as.getEngine(); if (as.enableBisimulation()) { mpi.applyBisimulation = true; @@ -209,7 +209,7 @@ namespace storm { << "\t exact=" << (mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision) << std::noboolalpha << std::endl); } - + /*! * Sets the model processing information based on the given input. * Finding the right model processing information might require a conversion to jani. @@ -221,13 +221,13 @@ namespace storm { auto coreSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); - + // Set the engine. mpi.engine = coreSettings.getEngine(); - + // Set whether bisimulation is to be used. mpi.applyBisimulation = generalSettings.isBisimulationSet(); - + // Set the value type used for numeric values if (generalSettings.isParametricSet()) { mpi.verificationValueType = ModelProcessingInformation::ValueType::Parametric; @@ -237,7 +237,7 @@ namespace storm { mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecision; } auto originalVerificationValueType = mpi.verificationValueType; - + // Since the remaining settings could depend on the ones above, we need apply the automatic engine now. bool useAutomatic = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Automatic; if (useAutomatic) { @@ -263,7 +263,7 @@ namespace storm { } } } - + // Check whether these settings are compatible with the provided input. if (input.model) { auto checkCompatibleSettings = [&mpi, &input] { @@ -294,7 +294,7 @@ namespace storm { // If there is no input model, nothing has to be done, actually mpi.isCompatible = true; } - + // Set whether a transformation to jani is required or necessary mpi.transformToJani = ioSettings.isPrismToJaniSet(); if (input.model) { @@ -317,7 +317,7 @@ namespace storm { STORM_LOG_WARN("Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied."); } } - + // Set the Dd library mpi.ddType = coreSettings.getDdLibraryType(); if (mpi.ddType == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue()) { @@ -328,7 +328,7 @@ namespace storm { } return mpi; } - + void ensureNoUndefinedPropertyConstants(std::vector const& properties) { // Make sure there are no undefined constants remaining in any property. for (auto const& property : properties) { @@ -342,18 +342,18 @@ namespace storm { } } } - + std::pair preprocessSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); - + SymbolicInput output = input; - + // Preprocess properties (if requested) if (ioSettings.isPropertiesAsMultiSet()) { STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException, "Can not translate properties to multi-objective formula because no properties were specified."); output.properties = {storm::api::createMultiObjectiveProperty(output.properties)}; } - + // Substitute constant definitions in symbolic input. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); std::map constantDefinitions; @@ -368,7 +368,7 @@ namespace storm { auto transformedJani = std::make_shared(); ModelProcessingInformation mpi = getModelProcessingInformation(output, transformedJani); - + // Check whether conversion for PRISM to JANI is requested or necessary. if (output.model && output.model.get().isPrismProgram()) { if (mpi.transformToJani) { @@ -378,16 +378,16 @@ namespace storm { } else { storm::prism::Program const& model = output.model.get().asPrismProgram(); auto modelAndProperties = model.toJani(output.properties); - + output.model = modelAndProperties.first; - + if (!modelAndProperties.second.empty()) { output.preprocessedProperties = std::move(modelAndProperties.second); } } } } - + if (output.model && output.model.get().isJaniModel()) { storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(storm::utility::getBuilderType(mpi.engine)); storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures); @@ -395,7 +395,7 @@ namespace storm { return {output, mpi}; } - + void exportSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); if (input.model && input.model.get().isJaniModel()) { @@ -405,25 +405,25 @@ namespace storm { } } } - + std::vector> createFormulasToRespect(std::vector const& properties) { std::vector> result = storm::api::extractFormulasFromProperties(properties); - + for (auto const& property : properties) { if (!property.getFilter().getStatesFormula()->isInitialFormula()) { result.push_back(property.getFilter().getStatesFormula()); } } - + return result; } - + template std::shared_ptr buildModelDd(SymbolicInput const& input) { auto buildSettings = storm::settings::getModule(); return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet()); } - + template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings, bool useJit) { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); @@ -462,7 +462,7 @@ namespace storm { return storm::api::buildSparseModel(input.model.get(), options, useJit, storm::settings::getModule().isDoctorSet()); } - + template std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings, storm::settings::modules::BuildSettings const& buildSettings) { std::shared_ptr result; @@ -478,7 +478,7 @@ namespace storm { } return result; } - + template std::shared_ptr buildModel(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings, ModelProcessingInformation const& mpi) { storm::utility::Stopwatch modelBuildingWatch(true); @@ -496,24 +496,24 @@ namespace storm { STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = buildModelExplicit(ioSettings, buildSettings); } - + modelBuildingWatch.stop(); if (result) { STORM_PRINT("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); } - + return result; } - + template std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { auto transformationSettings = storm::settings::getModule(); auto debugSettings = storm::settings::getModule(); - + std::shared_ptr> result = model; model->close(); STORM_LOG_WARN_COND(!debugSettings.isAdditionalChecksSet() || !model->containsZenoCycle(), "MA contains a Zeno cycle. Model checking results cannot be trusted."); - + if (model->isConvertibleToCtmc()) { STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead."); result = model->convertToCtmc(); @@ -526,18 +526,18 @@ namespace storm { return result; } - + template std::shared_ptr> preprocessSparseModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; if (bisimulationSettings.isWeakBisimulationSet()) { bisimType = storm::storage::BisimulationType::Weak; } - + STORM_LOG_INFO("Performing bisimulation minimization..."); return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); } - + template std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto bisimulationSettings = storm::settings::getModule(); @@ -545,36 +545,36 @@ namespace storm { auto transformationSettings = storm::settings::getModule(); std::pair>, bool> result = std::make_pair(model, false); - + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); result.second = true; } - + if (mpi.applyBisimulation) { result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); result.second = true; } - + if (transformationSettings.isToDiscreteTimeModelSet()) { // TODO: we should also transform the properties at this point. STORM_LOG_WARN_COND(!model->hasRewardModel("_time"), "Scheduled transformation to discrete time model, but a reward model named '_time' is already present in this model. We might take the wrong reward model later."); result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first), storm::api::extractFormulasFromProperties(input.properties)).first; result.second = true; } - + if (transformationSettings.isToNondeterministicModelSet()) { result.first = storm::api::transformToNondeterministicModel(std::move(*result.first)); result.second = true; } - + return result; } - + template void exportSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); - + if (ioSettings.isExportExplicitSet()) { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector(), !ioSettings.isExplicitExportPlaceholdersDisabled()); } @@ -582,12 +582,12 @@ namespace storm { if (ioSettings.isExportDdSet()) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drdd format is only supported for DDs."); } - + if (ioSettings.isExportDotSet()) { storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); } } - + template void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); @@ -604,7 +604,7 @@ namespace storm { storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportDotFilename()); } } - + template void exportModel(std::shared_ptr const& model, SymbolicInput const& input) { if (model->isSparseModel()) { @@ -613,13 +613,13 @@ namespace storm { exportDdModel(model->as>(), input); } } - + template typename std::enable_if::value, std::shared_ptr>>::type preprocessDdMarkovAutomaton(std::shared_ptr> const& model) { return model; } - + template typename std::enable_if::value, std::shared_ptr>>::type preprocessDdMarkovAutomaton(std::shared_ptr> const& model) { @@ -630,11 +630,11 @@ namespace storm { return model; } } - + template std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings, ModelProcessingInformation const& mpi) { STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation."); - + auto quotientFormat = bisimulationSettings.getQuotientFormat(); if (mpi.engine == storm::utility::Engine::DdSparse && quotientFormat != storm::dd::bisimulation::QuotientFormat::Sparse && bisimulationSettings.isQuotientFormatSetFromDefaultValue()) { STORM_LOG_INFO("Setting bisimulation quotient format to 'sparse'."); @@ -643,17 +643,17 @@ namespace storm { STORM_LOG_INFO("Performing bisimulation minimization..."); return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode(), quotientFormat); } - + template std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto bisimulationSettings = storm::settings::getModule(); std::pair>, bool> intermediateResult = std::make_pair(model, false); - + if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as>()); intermediateResult.second = true; } - + std::unique_ptr>, bool>> result; auto symbolicModel = intermediateResult.first->template as>(); if (mpi.applyBisimulation) { @@ -662,11 +662,11 @@ namespace storm { } else { result = std::make_unique>, bool>>(symbolicModel->template toValueType(), !std::is_same::value); } - + if (result && result->first->isSymbolicModel() && mpi.engine == storm::utility::Engine::DdSparse) { // Mark as changed. result->second = true; - + std::shared_ptr> symbolicModel = result->first->template as>(); std::vector> formulas; for (auto const& property : input.properties) { @@ -675,14 +675,14 @@ namespace storm { result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas); STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type."); } - + return *result; } - + template std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { storm::utility::Stopwatch preprocessingWatch(true); - + std::pair, bool> result = std::make_pair(model, false); if (model->isSparseModel()) { result = preprocessSparseModel(result.first->as>(), input, mpi); @@ -690,19 +690,19 @@ namespace storm { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); result = preprocessDdModel(result.first->as>(), input, mpi); } - + preprocessingWatch.stop(); - + if (result.second) { STORM_PRINT(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; } - + void printComputingCounterexample(storm::jani::Property const& property) { STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); } - + void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { if (counterexample) { STORM_PRINT(*counterexample << std::endl); @@ -713,16 +713,16 @@ namespace storm { STORM_PRINT(" failed." << std::endl); } } - + template void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type."); } - + template <> void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { typedef double ValueType; - + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); auto sparseModel = model->as>(); for (auto& rewModel : sparseModel->getRewardModels()) { @@ -730,7 +730,7 @@ namespace storm { } STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models."); - + auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); @@ -772,7 +772,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); } } - + template void printFilteredResult(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { if (result->isQuantitative()) { @@ -835,11 +835,14 @@ namespace storm { } STORM_PRINT(std::endl); } - + void printModelCheckingProperty(storm::jani::Property const& property) { + if(property.isShieldingProperty()) { + STORM_PRINT(std::endl << "Creating a " << property.getShieldingExpression()->typeToString() << " shield for:"); + } STORM_PRINT(std::endl << "Model checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ..." << std::endl); } - + template void printResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { if (result) { @@ -854,15 +857,15 @@ namespace storm { STORM_LOG_ERROR("Property is unsupported by selected engine/settings." << std::endl); } } - + struct PostprocessingIdentity { void operator()(std::unique_ptr const&) { // Intentionally left empty. } }; - + template - void verifyProperties(SymbolicInput const& input, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + void verifyProperties(SymbolicInput const& input, std::function(std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { auto transformationSettings = storm::settings::getModule(); auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties; for (auto const& property : properties) { @@ -880,13 +883,15 @@ namespace storm { auto propertyFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getRawFormula()); auto filterFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getFilter().getStatesFormula()); if (propertyFormula && filterFormula) { - result = verificationCallback(propertyFormula, filterFormula); + STORM_LOG_WARN_COND(!property.isShieldingProperty(), "The creation of shields for continuous time models is currently not supported."); + result = verificationCallback(propertyFormula, filterFormula, nullptr); } else { ignored = true; } } else { result = verificationCallback(property.getRawFormula(), - property.getFilter().getStatesFormula()); + property.getFilter().getStatesFormula(), + property.getShieldingExpression()); } } catch (storm::exceptions::BaseException const& ex) { STORM_LOG_WARN("Cannot handle property: " << ex.what()); @@ -898,20 +903,20 @@ namespace storm { } } } - + std::vector parseConstraints(storm::expressions::ExpressionManager const& expressionManager, std::string const& constraintsString) { std::vector constraints; - + std::vector constraintsAsStrings; boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(",")); - + storm::parser::ExpressionParser expressionParser(expressionManager); std::unordered_map variableMapping; for (auto const& variableTypePair : expressionManager) { variableMapping[variableTypePair.first.getName()] = variableTypePair.first; } expressionParser.setIdentifierMapping(variableMapping); - + for (auto const& constraintString : constraintsAsStrings) { if (constraintString.empty()) { continue; @@ -921,32 +926,32 @@ namespace storm { STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << "."); constraints.emplace_back(constraint); } - + return constraints; } - + std::vector> parseInjectedRefinementPredicates(storm::expressions::ExpressionManager const& expressionManager, std::string const& refinementPredicatesString) { std::vector> injectedRefinementPredicates; - + storm::parser::ExpressionParser expressionParser(expressionManager); std::unordered_map variableMapping; for (auto const& variableTypePair : expressionManager) { variableMapping[variableTypePair.first.getName()] = variableTypePair.first; } expressionParser.setIdentifierMapping(variableMapping); - + std::vector predicateGroupsAsStrings; boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";")); - + if (!predicateGroupsAsStrings.empty()) { for (auto const& predicateGroupString : predicateGroupsAsStrings) { if (predicateGroupString.empty()) { continue; } - + std::vector predicatesAsStrings; boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":")); - + if (!predicatesAsStrings.empty()) { injectedRefinementPredicates.emplace_back(); for (auto const& predicateString : predicatesAsStrings) { @@ -954,55 +959,58 @@ namespace storm { STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); injectedRefinementPredicates.back().emplace_back(predicate); } - + STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException, "Expecting non-empty list of predicates to inject for each (mentioned) refinement step."); - + // Finally reverse the list, because we take the predicates from the back. std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end()); } } - + // Finally reverse the list, because we take the predicates from the back. std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end()); } - + return injectedRefinementPredicates; } - + template void verifyWithAbstractionRefinementEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule(); storm::api::AbstractionRefinementOptions options(parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()), parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates())); - verifyProperties(input, [&input,&options,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input,&options,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); return storm::api::verifyWithAbstractionRefinementEngine(mpi.env, input.model.get(), storm::api::createTask(formula, true), options); }); } - + template void verifyWithExplorationEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input, [&input,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); return storm::api::verifyWithExplorationEngine(mpi.env, input.model.get(), storm::api::createTask(formula, true)); }); } - + template void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto sparseModel = model->as>(); auto const& ioSettings = storm::settings::getModule(); - auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + auto verificationCallback = [&sparseModel,&ioSettings,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldingExpression) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); + if(shieldingExpression) { + task.setShieldingExpression(shieldingExpression); + } if (ioSettings.isExportSchedulerSet()) { task.setProduceSchedulers(true); } std::unique_ptr result = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, task); - + std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique(sparseModel->getInitialStates()); @@ -1057,16 +1065,16 @@ namespace storm { STORM_PRINT("Time for model checking: " << watch << "." << std::endl); } } - + template void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { - verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); - + auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithHybridEngine(mpi.env, symbolicModel, task); - + std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); @@ -1079,16 +1087,16 @@ namespace storm { return result; }); } - + template void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { - verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); - + auto symbolicModel = model->as>(); std::unique_ptr result = storm::api::verifyWithDdEngine(mpi.env, symbolicModel, storm::api::createTask(formula, true)); - + std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); @@ -1101,16 +1109,16 @@ namespace storm { return result; }); } - + template void verifyWithAbstractionRefinementEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { - verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states, std::shared_ptr const& shieldExpression) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); auto symbolicModel = model->as>(); return storm::api::verifyWithAbstractionRefinementEngine(mpi.env, symbolicModel, storm::api::createTask(formula, true)); }); } - + template typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { if (mpi.engine == storm::utility::Engine::Hybrid) { @@ -1121,12 +1129,12 @@ namespace storm { verifyWithAbstractionRefinementEngine(model, input, mpi); } } - + template typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const&, SymbolicInput const&, ModelProcessingInformation const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type."); } - + template void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { if (model->isSparseModel()) { @@ -1136,7 +1144,7 @@ namespace storm { verifySymbolicModel(model, input, mpi); } } - + template std::shared_ptr buildPreprocessModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto ioSettings = storm::settings::getModule(); @@ -1145,13 +1153,13 @@ namespace storm { if (!buildSettings.isNoBuildModelSet()) { model = buildModel(input, ioSettings, mpi); } - + if (model) { model->printModelInformationToStream(std::cout); } - + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - + if (model) { auto preprocessingResult = preprocessModel(model, input, mpi); if (preprocessingResult.second) { @@ -1170,7 +1178,7 @@ namespace storm { } return model; } - + template void processInputWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto abstractionSettings = storm::settings::getModule(); @@ -1192,10 +1200,10 @@ namespace storm { } } } - + template void processInputWithValueType(SymbolicInput const& input, ModelProcessingInformation const& mpi) { - + if (mpi.ddType == storm::dd::DdType::CUDD) { STORM_LOG_ASSERT(mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision && mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && (std::is_same::value), "Unexpected value type for Dd library cudd."); processInputWithValueTypeAndDdlib(input, mpi); diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp index 485a4bb18..d37d18a57 100644 --- a/src/storm-parsers/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -18,7 +18,7 @@ namespace storm { namespace parser { - + FormulaParser::FormulaParser() : manager(new storm::expressions::ExpressionManager()), grammar(new FormulaParserGrammar(manager)) { // Intentionally left empty. } @@ -40,25 +40,25 @@ namespace storm { FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) { other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); } - + FormulaParser& FormulaParser::operator=(FormulaParser const& other) { this->manager = other.manager; this->grammar = std::shared_ptr(new FormulaParserGrammar(this->manager)); other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); return *this; } - + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { std::vector property = parseFromString(formulaString); STORM_LOG_THROW(property.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << property.size() << " instead."); return property.front().getRawFormula(); } - + std::vector FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. std::ifstream inputFileStream; storm::utility::openFile(filename, inputFileStream); - + std::vector properties; // Now try to parse the contents of the file. @@ -75,15 +75,15 @@ namespace storm { storm::utility::closeFile(inputFileStream); return properties; } - + std::vector FormulaParser::parseFromString(std::string const& formulaString) const { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); - + // Create empty result; std::vector result; - + // Create grammar. try { // Start parsing. @@ -93,15 +93,14 @@ namespace storm { } catch (qi::expectation_failure const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); } - return result; } - + void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { // Record the mapping and hand it over to the grammar. this->identifiers_.add(identifier, expression); grammar->addIdentifierExpression(identifier, expression); } - + } // namespace parser } // namespace storm diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 9d5f0283e..3aba843be 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -140,19 +140,37 @@ namespace storm { gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); + shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + + shieldExpression.name("shield expression"); + + shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | + qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | + qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); + shieldingType.name("shielding type"); + + probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; + probability.name("double between 0 and 1"); + + shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + shieldComparison.name("shield comparison type"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula.name("state formula"); formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); + + constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -164,30 +182,30 @@ namespace storm { start.name("start"); // Enable the following lines to print debug output for most the rules. -// debug(start); -// debug(constantDefinition); -// debug(stateFormula); -// debug(orStateFormula); -// debug(andStateFormula); -// debug(probabilityOperator); -// debug(rewardOperator); -// debug(longRunAverageOperator); -// debug(timeOperator); -// debug(pathFormulaWithoutUntil); -// debug(pathFormula); -// debug(conditionalFormula); -// debug(nextFormula); -// debug(globallyFormula); -// debug(eventuallyFormula); -// debug(atomicStateFormula); -// debug(booleanLiteralFormula); -// debug(labelFormula); -// debug(expressionFormula); -// debug(rewardPathFormula); -// debug(cumulativeRewardFormula); -// debug(totalRewardFormula); -// debug(instantaneousRewardFormula); -// debug(multiFormula); + //debug(start); + //debug(constantDefinition); + //debug(stateFormula); + //debug(orStateFormula); + //debug(andStateFormula); + //debug(probabilityOperator); + //debug(rewardOperator); + //debug(longRunAverageOperator); + //debug(timeOperator); + //debug(pathFormulaWithoutUntil); + //debug(pathFormula); + //debug(conditionalFormula); + //debug(nextFormula); + //debug(globallyFormula); + //debug(eventuallyFormula); + //debug(atomicStateFormula); + //debug(booleanLiteralFormula); + //debug(labelFormula); + //debug(expressionFormula); + //debug(rewardPathFormula); + //debug(cumulativeRewardFormula); + //debug(totalRewardFormula); + //debug(instantaneousRewardFormula); + //debug(multiFormula); // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -490,6 +508,29 @@ namespace storm { } } + std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { + return std::make_pair(comparisonType, value); + } + + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { + if(comparisonStruct.is_initialized()) { + STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored."); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); + } else { + STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)"); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); + } + } + + storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldExpression) { + ++propertyCount; + if (propertyName) { + return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula), shieldExpression); + } else { + return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula), shieldExpression); + } + } + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 9ea0e5355..35ac56b6b 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -202,12 +202,20 @@ namespace storm { qi::rule(), Skipper> quantileFormula; qi::rule(), Skipper> gameFormula; + qi::rule(), Skipper> shieldExpression; + qi::rule shieldingType; + qi::rule probability; + qi::rule, qi::locals, Skipper> shieldComparison; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); @@ -243,6 +251,7 @@ namespace storm { std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldingExpression); // An error handler function. phoenix::function handler; diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 72399c314..48918990b 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -139,9 +139,9 @@ namespace storm { if (actionCount > 0) { parseActions(parsedStructure.at("actions"), model); } - + Scope scope(name); - + // Parse constants ConstantsMap constants; scope.constants = &constants; @@ -157,7 +157,7 @@ namespace storm { constants.emplace(constant->getName(), &model.getConstants().back()); } } - + // Parse variables size_t variablesCount = parsedStructure.count("variables"); STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables."); @@ -170,7 +170,7 @@ namespace storm { globalVars.emplace(variable->getName(), &model.addVariable(*variable)); } } - + uint64_t funDeclCount = parsedStructure.count("functions"); STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Model '" << name << "' has more than one list of functions"); FunctionsMap globalFuns; @@ -196,7 +196,7 @@ namespace storm { globalFuns[funDef.getName()] = &model.addFunctionDefinition(funDef); } } - + // Parse Automata STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given"); STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array"); @@ -215,7 +215,7 @@ namespace storm { std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); model.finalize(); - + // Parse properties storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); @@ -243,14 +243,14 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description); return { parseFormula(model, propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - + template std::vector> JaniParser::parseBinaryFormulaArguments(storm::jani::Model& model, Json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description); STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description); return { parseFormula(model, propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(model, propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - + template storm::jani::PropertyInterval JaniParser::parsePropertyInterval(Json const& piStructure, Scope const& scope) { storm::jani::PropertyInterval pi; @@ -260,11 +260,11 @@ namespace storm { if (piStructure.count("lower-exclusive") > 0) { STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); pi.lowerBoundStrict = piStructure.at("lower-exclusive"); - + } if (piStructure.count("upper") > 0) { pi.upperBound = parseExpression(piStructure.at("upper"), scope.refine("Upper bound for property interval")); - + } if (piStructure.count("upper-exclusive") > 0) { STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); @@ -293,7 +293,7 @@ namespace storm { } return storm::logic::RewardAccumulation(accSteps, accTime, accExit); } - + void insertLowerUpperTimeBounds(std::vector>& lowerBounds, std::vector>& upperBounds, storm::jani::PropertyInterval const& pi) { if (pi.hasLowerBound()) { lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); @@ -334,7 +334,7 @@ namespace storm { } if (propertyStructure.count("op") == 1) { std::string opString = getString(propertyStructure.at("op"), "Operation description"); - + if(opString == "Pmin" || opString == "Pmax") { std::vector> args = parseUnaryFormulaArgument(model, propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); assert(args.size() == 1); @@ -342,7 +342,7 @@ namespace storm { opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; return std::make_shared(args[0], opInfo); - + } else if (opString == "∀" || opString == "∃") { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description); @@ -352,7 +352,7 @@ namespace storm { storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), scope.refine("Reward expression")); STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description); std::string rewardName = rewExpr.toString(); - + storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; @@ -361,7 +361,7 @@ namespace storm { if (propertyStructure.count("accumulate") > 0) { rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); } - + bool time = false; if (propertyStructure.count("step-instant") > 0) { STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + scope.description); @@ -455,7 +455,7 @@ namespace storm { } auto subformula = std::make_shared(rewardAccumulation); return std::make_shared(subformula, rewardName, opInfo); - + } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector> args; @@ -467,7 +467,7 @@ namespace storm { args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } - + std::vector> lowerBounds, upperBounds; std::vector tbReferences; if (propertyStructure.count("step-bounds") > 0) { @@ -557,7 +557,7 @@ namespace storm { } else if (opString == ">") { ct = storm::logic::ComparisonType::Greater; } - + std::vector const leftRight = {"left", "right"}; for (uint64_t i = 0; i < 2; ++i) { if (propertyStructure.at(leftRight[i]).count("op") > 0) { @@ -598,7 +598,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Looking for operator for formula " << propertyStructure.dump() << ", but did not find one"); } } - + template storm::jani::Property JaniParser::parseProperty(storm::jani::Model& model, Json const& propertyStructure, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); @@ -612,7 +612,7 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); // Parse filter expression. Json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); @@ -641,7 +641,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); } - + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); std::shared_ptr statesFormula; if (expressionStructure.at("states").count("op") > 0) { @@ -663,7 +663,7 @@ namespace storm { STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(model, expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); - return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, nullptr, comment); } template @@ -681,11 +681,11 @@ namespace storm { definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name)); assert(definingExpression.isInitialized()); } - + STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration."); ParsedType type; parseType(type, constantStructure.at("type"), name, scope); - + STORM_LOG_THROW(type.basicType.is_initialized(), storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") has unexpected type"); storm::expressions::Variable var; switch (type.basicType.get()) { @@ -710,10 +710,10 @@ namespace storm { constraintExpression = var.getExpression() <= type.bounds->second; } } - + return std::make_shared(name, std::move(var), definingExpression, constraintExpression); } - + template void JaniParser::parseType(ParsedType& result, Json const& typeStructure, std::string variableName, Scope const& scope) { if (typeStructure.is_string()) { @@ -779,7 +779,7 @@ namespace storm { } } } - + template storm::jani::FunctionDefinition JaniParser::parseFunctionDefinition(Json const& functionDefinitionStructure, Scope const& scope, bool firstPass, std::string const& parameterNamePrefix) { STORM_LOG_THROW(functionDefinitionStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Function definition (scope: " + scope.description + ") must have a name"); @@ -787,7 +787,7 @@ namespace storm { STORM_LOG_THROW(functionDefinitionStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) type-declaration."); ParsedType type; parseType(type, functionDefinitionStructure.at("type"), functionName, scope); - + std::unordered_map parameterNameToVariableMap; std::vector parameters; if (!firstPass && functionDefinitionStructure.count("parameters") > 0) { @@ -799,13 +799,13 @@ namespace storm { STORM_LOG_THROW(parameterStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one type."); parseType(parameterType, parameterStructure.at("type"), parameterName, scope.refine("parameter declaration of parameter " + std::to_string(parameters.size()) + " of function definition " + functionName)); STORM_LOG_WARN_COND(!parameterType.bounds.is_initialized(), "Bounds on parameter" + parameterName + " of function definition " + functionName + " will be ignored."); - + std::string exprParameterName = parameterNamePrefix + functionName + VARIABLE_AUTOMATON_DELIMITER + parameterName; parameters.push_back(expressionManager->declareVariable(exprParameterName, parameterType.expressionType)); parameterNameToVariableMap.emplace(parameterName, parameters.back()); } } - + STORM_LOG_THROW(functionDefinitionStructure.count("body") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) body."); storm::expressions::Expression functionBody; if (!firstPass) { @@ -815,7 +815,7 @@ namespace storm { return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody); } - + template std::shared_ptr JaniParser::parseVariable(Json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix) { STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scope.description + ") must have a name"); @@ -845,7 +845,7 @@ namespace storm { } else { assert(!transientVar); } - + bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues; if (type.basicType) { switch (type.basicType.get()) { @@ -945,7 +945,7 @@ namespace storm { } return result; } - + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ")."); } @@ -988,7 +988,7 @@ namespace storm { void ensureIntegerType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) { STORM_LOG_THROW(expr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << "."); } - + /** * Helper for parse expression. */ @@ -1411,7 +1411,7 @@ namespace storm { localFuns[funDef.getName()] = &automaton.addFunctionDefinition(funDef); } } - + STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations."); std::unordered_map locIds; for(auto const& locEntry : automatonStructure.at("locations")) { @@ -1500,7 +1500,7 @@ namespace storm { templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex)); } } - + // destinations STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'"); std::vector> destinationLocationsAndProbabilities; @@ -1550,7 +1550,7 @@ namespace storm { return automaton; } - + template std::vector parseSyncVectors(typename JaniParser::Json const& syncVectorStructure) { std::vector syncVectors; @@ -1586,9 +1586,9 @@ namespace storm { } return std::shared_ptr(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get(), inputEnabledActions)); } - + STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump()); - + if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) { // We might have an automaton. STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition"); @@ -1598,9 +1598,9 @@ namespace storm { return std::shared_ptr(new storm::jani::AutomatonComposition(name)); } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported"); - + } - + std::vector> compositions; for (auto const& elemDecl : compositionStructure.at("elements")) { if(!allowRecursion) { @@ -1608,17 +1608,17 @@ namespace storm { } compositions.push_back(parseComposition(elemDecl)); } - + STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once"); std::vector syncVectors; if (compositionStructure.count("syncs") > 0) { syncVectors = parseSyncVectors(compositionStructure.at("syncs")); } - + return std::shared_ptr(new storm::jani::ParallelComposition(compositions, syncVectors)); - + } - + template class JaniParser; template class JaniParser; } diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index bd07cb013..9b134c069 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -37,19 +37,19 @@ namespace storm { reducedPropertyNames.insert(property.getName()); } } - + if (reducedPropertyNames.size() < propertyNameSet.size()) { std::set missingProperties; std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin())); STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << "."); } - + return result; } else { return properties; } } - + std::vector> extractFormulasFromProperties(std::vector const& properties) { std::vector> formulas; for (auto const& prop : properties) { @@ -57,7 +57,7 @@ namespace storm { } return formulas; } - + storm::jani::Property createMultiObjectiveProperty(std::vector const& properties) { std::set undefConstants; std::string name = ""; @@ -67,9 +67,10 @@ namespace storm { name += prop.getName(); comment += prop.getComment(); STORM_LOG_WARN_COND(prop.getFilter().isDefault(), "Non-default property filter of property " + prop.getName() + " will be dropped during conversion to multi-objective property."); + STORM_LOG_WARN_COND(!prop.isShieldingProperty(), "Shielding of multi-objective property is not possible yet. Dropping expression: '" + prop.getShieldingExpression()->toString() + "'."); } auto multiFormula = std::make_shared(extractFormulasFromProperties(properties)); - return storm::jani::Property(name, multiFormula, undefConstants, comment); + return storm::jani::Property(name, multiFormula, undefConstants, nullptr, comment); } } } diff --git a/src/storm/environment/solver/MultiplierEnvironment.cpp b/src/storm/environment/solver/MultiplierEnvironment.cpp index 0dd7f031a..08e0dea5b 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.cpp +++ b/src/storm/environment/solver/MultiplierEnvironment.cpp @@ -29,13 +29,4 @@ namespace storm { type = value; typeSetFromDefault = isSetFromDefault; } - - void MultiplierEnvironment::setOptimizationDirectionOverride(storm::storage::BitVector optDirOverride) { - optimizationDirectionOverride = optDirOverride; - } - - boost::optional const& MultiplierEnvironment::getOptimizationDirectionOverride() const { - return optimizationDirectionOverride; - } - } diff --git a/src/storm/environment/solver/MultiplierEnvironment.h b/src/storm/environment/solver/MultiplierEnvironment.h index 945b62602..f851feca3 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.h +++ b/src/storm/environment/solver/MultiplierEnvironment.h @@ -18,14 +18,8 @@ namespace storm { storm::solver::MultiplierType const& getType() const; bool const& isTypeSetFromDefault() const; void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false); - - void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride); - boost::optional const& getOptimizationDirectionOverride() const; - private: storm::solver::MultiplierType type; bool typeSetFromDefault; - - boost::optional optimizationDirectionOverride = boost::none; }; } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 9169b89f4..2528e6c9a 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -15,25 +15,25 @@ namespace storm { RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { // Intentionally left empty } - + std::shared_ptr RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } - + void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector& properties) const { for (auto& p : properties) { eliminateRewardAccumulations(p); } } - + void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::jani::Property& property) const { auto formula = eliminateRewardAccumulations(*property.getFilter().getFormula()); auto states = eliminateRewardAccumulations(*property.getFilter().getStatesFormula()); storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states); - property = storm::jani::Property(property.getName(), storm::jani::FilterExpression(formula, property.getFilter().getFilterType(), states), property.getUndefinedConstants(), property.getComment()); + property = storm::jani::Property(property.getName(), storm::jani::FilterExpression(formula, property.getFilter().getFilterType(), states), property.getUndefinedConstants(), property.getShieldingExpression(), property.getComment()); } - + boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; @@ -68,7 +68,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); } } - + boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { boost::optional rewAcc; STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); @@ -90,7 +90,7 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); } - + boost::any RewardAccumulationEliminationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); @@ -100,7 +100,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); } } - + boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { @@ -120,12 +120,12 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); } - + boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, f.getOptionalRewardModelName())); return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - + boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); @@ -135,11 +135,11 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); } } - + bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); storm::jani::RewardModelInformation info(model, rewardModelName.get()); - + if ((info.hasActionRewards() || info.hasTransitionRewards()) && !accumulation.isStepsSet()) { return false; } diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp new file mode 100644 index 000000000..a9cbeb088 --- /dev/null +++ b/src/storm/logic/ShieldExpression.cpp @@ -0,0 +1,80 @@ +#include "storm/logic/ShieldExpression.h" + +#include + +namespace storm { + namespace logic { + ShieldExpression::ShieldExpression() {} + + ShieldExpression::ShieldExpression(ShieldingType type, std::string filename) : type(type), filename(filename) { + //Intentionally left empty + } + + ShieldExpression::ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value) : type(type), filename(filename), comparison(comparison), value(value) { + //Intentionally left empty + } + + bool ShieldExpression::isRelative() const { + return comparison == storm::logic::ShieldComparison::Relative; + } + + bool ShieldExpression::isPreSafetyShield() const { + return type == storm::logic::ShieldingType::PreSafety; + } + + bool ShieldExpression::isPostSafetyShield() const { + return type == storm::logic::ShieldingType::PostSafety; + } + + bool ShieldExpression::isOptimalShield() const { + return type == storm::logic::ShieldingType::Optimal; + } + + double ShieldExpression::getValue() const { + return value; + } + + std::string ShieldExpression::typeToString() const { + switch(type) { + case storm::logic::ShieldingType::PostSafety: return "PostSafety"; + case storm::logic::ShieldingType::PreSafety: return "PreSafety"; + case storm::logic::ShieldingType::Optimal: return "Optimal"; + } + } + + std::string ShieldExpression::comparisonToString() const { + switch(comparison) { + case storm::logic::ShieldComparison::Absolute: return "gamma"; + case storm::logic::ShieldComparison::Relative: return "lambda"; + } + } + + std::string ShieldExpression::toString() const { + return "<" + typeToString() + ", " + comparisonToString() + "=" + std::to_string(value) + ">"; + } + + std::string ShieldExpression::prettify() const { + std::string prettyString = ""; + std::string comparisonType = isRelative() ? "relative" : "absolute"; + switch(type) { + case storm::logic::ShieldingType::PostSafety: prettyString += "Post-Safety"; break; + case storm::logic::ShieldingType::PreSafety: prettyString += "Pre-Safety"; break; + case storm::logic::ShieldingType::Optimal: prettyString += "Optimal"; break; + } + prettyString += "-Shield "; + if(!(type == storm::logic::ShieldingType::Optimal)) { + prettyString += "with " + comparisonType + " comparison (" + comparisonToString() + " = " + std::to_string(value) + "):"; + } + return prettyString; + } + + std::string ShieldExpression::getFilename() const { + return filename; + } + + std::ostream& operator<<(std::ostream& out, ShieldExpression const& shieldExpression) { + out << shieldExpression.toString(); + return out; + } + } +} diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h new file mode 100644 index 000000000..b214f3baa --- /dev/null +++ b/src/storm/logic/ShieldExpression.h @@ -0,0 +1,45 @@ +#pragma once + +#include +#include + +namespace storm { + namespace logic { + + enum class ShieldingType { + PostSafety, + PreSafety, + Optimal + }; + + enum class ShieldComparison { Absolute, Relative }; + + class ShieldExpression { + public: + ShieldExpression(); + ShieldExpression(ShieldingType type, std::string filename); + ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value); + + bool isRelative() const; + bool isPreSafetyShield() const; + bool isPostSafetyShield() const; + bool isOptimalShield() const; + + double getValue() const; + + std::string typeToString() const; + std::string comparisonToString() const; + std::string toString() const; + std::string prettify() const; + std::string getFilename() const; + friend std::ostream& operator<<(std::ostream& stream, ShieldExpression const& shieldExpression); + + private: + ShieldingType type; + ShieldComparison comparison; + double value; + + std::string filename; + }; + } +} diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 6598d5a85..b42e8c3f8 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -10,6 +10,7 @@ #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" #include "storm/logic/PlayerCoalition.h" +#include "storm/logic/ShieldExpression.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/exceptions/InvalidOperationException.h" @@ -19,13 +20,13 @@ namespace storm { namespace logic { class Formula; } - + namespace modelchecker { - + enum class CheckType { Probabilities, Rewards }; - + /* * This class is used to customize the checking process of a formula. */ @@ -34,7 +35,7 @@ namespace storm { public: template friend class CheckTask; - + /*! * Creates a task object with the default options for the given formula. */ @@ -42,10 +43,10 @@ namespace storm { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; this->produceSchedulers = false; this->qualitative = false; - + updateOperatorInformation(); } - + /*! * Copies the check task from the source while replacing the formula with the new one. In particular, this * changes the formula type of the check task object. @@ -54,9 +55,10 @@ namespace storm { CheckTask substituteFormula(NewFormulaType const& newFormula) const { CheckTask result(newFormula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); result.updateOperatorInformation(); + if(isShieldingTask()) result.setShieldingExpression(getShieldingExpression()); return result; } - + /*! * If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula. * Calling this method has no effect if the provided formula is not an operator formula. @@ -67,20 +69,20 @@ namespace storm { if (operatorFormula.hasOptimalityType()) { this->optimizationDirection = operatorFormula.getOptimalityType(); } - + if (operatorFormula.hasBound()) { this->bound = operatorFormula.getBound(); } - + if (operatorFormula.hasOptimalityType()) { this->optimizationDirection = operatorFormula.getOptimalityType(); } else if (operatorFormula.hasBound()) { this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; } - + if (formula.get().isProbabilityOperatorFormula()) { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.get().asProbabilityOperatorFormula(); - + if (probabilityOperatorFormula.hasBound()) { if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs())) { this->qualitative = true; @@ -89,7 +91,7 @@ namespace storm { } else if (formula.get().isRewardOperatorFormula()) { storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.get().asRewardOperatorFormula(); this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); - + if (rewardOperatorFormula.hasBound()) { if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs())) { this->qualitative = true; @@ -107,49 +109,49 @@ namespace storm { CheckTask convertValueType() const { return CheckTask(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); } - + /*! * Retrieves the formula from this task. */ FormulaType const& getFormula() const { return formula.get(); } - + /*! * Retrieves whether an optimization direction was set. */ bool isOptimizationDirectionSet() const { return static_cast(optimizationDirection); } - + /*! * Retrieves the optimization direction (if set). */ storm::OptimizationDirection const& getOptimizationDirection() const { return optimizationDirection.get(); } - + /*! * Sets the optimization direction. */ void setOptimizationDirection(storm::OptimizationDirection const& dir) { optimizationDirection = dir; } - + /*! * Retrieves whether a player coalition was set. */ bool isPlayerCoalitionSet() const { return static_cast(playerCoalition); } - + /*! * Retrieves the player coalition (if set). */ storm::logic::PlayerCoalition const& getPlayerCoalition() const { return playerCoalition.get(); } - + /*! * Sets the player coalition. */ @@ -157,28 +159,28 @@ namespace storm { playerCoalition = coalition; return *this; } - + /*! * Retrieves whether a reward model was set. */ bool isRewardModelSet() const { return static_cast(rewardModel); } - + /*! * Retrieves the reward model over which to perform the checking (if set). */ std::string const& getRewardModel() const { return rewardModel.get(); } - + /*! * Retrieves whether only the initial states are relevant in the computation. */ bool isOnlyInitialStatesRelevantSet() const { return onlyInitialStatesRelevant; } - + /*! * Sets whether only initial states are relevant. */ @@ -186,14 +188,37 @@ namespace storm { this->onlyInitialStatesRelevant = value; return *this; } - + + /* + * Returns whether this is a task for which a shield should be produced. + */ + bool isShieldingTask() const { + return static_cast(shieldingExpression); + } + + /* + * Retrieves the associated shielding expression. + */ + std::shared_ptr getShieldingExpression() const { + return shieldingExpression.get(); + } + + /* + * Sets the shielding expression for this check task. + */ + CheckTask& setShieldingExpression(std::shared_ptr const& shieldingExpression) { + this->shieldingExpression = shieldingExpression; + this->produceSchedulers = true; + return *this; + } + /*! * Retrieves whether there is a bound with which the values for the states will be compared. */ bool isBoundSet() const { return static_cast(bound); } - + /*! * Retrieves the value of the bound (if set). */ @@ -201,14 +226,14 @@ namespace storm { STORM_LOG_THROW(!bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << bound.get().threshold << "' as it contains undefined constants."); return storm::utility::convertNumber(bound.get().threshold.evaluateAsRational()); } - + /*! * Retrieves the comparison type of the bound (if set). */ storm::logic::ComparisonType const& getBoundComparisonType() const { return bound.get().comparisonType; } - + /*! * Retrieves the bound (if set). */ @@ -238,46 +263,46 @@ namespace storm { void setQualitative(bool value) { qualitative = value; } - + /*! * Sets whether to produce schedulers (if supported). */ void setProduceSchedulers(bool produceSchedulers = true) { this->produceSchedulers = produceSchedulers; } - + /*! * Retrieves whether scheduler(s) are to be produced (if supported). */ bool isProduceSchedulersSet() const { return produceSchedulers; } - + /*! * sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ void setHint(std::shared_ptr const& hint) { this->hint = hint; } - + /*! * Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ ModelCheckerHint const& getHint() const { return *hint; } - + ModelCheckerHint& getHint() { return *hint; } - + /*! * Conversion operator that strips the type of the formula. */ operator CheckTask() const { return this->substituteFormula(this->getFormula()); } - + private: /*! * Creates a task object with the given options. @@ -297,36 +322,39 @@ namespace storm { CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional playerCoalition, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint) : formula(formula), optimizationDirection(optimizationDirection), playerCoalition(playerCoalition), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) { // Intentionally left empty. } - + // The formula that is to be checked. std::reference_wrapper formula; - + // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection; - + // If set, the given coalitions of players will be assumed. boost::optional playerCoalition; // If set, the reward property has to be interpreted over this model. boost::optional rewardModel; - + // If set to true, the model checker may decide to only compute the values for the initial states. bool onlyInitialStatesRelevant; + // The according ShieldExpression. + boost::optional> shieldingExpression; + // The bound with which the states will be compared. boost::optional bound; - + // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; - + // If supported by the model checker and the model formalism, schedulers to achieve a value will be produced // if this flag is set. bool produceSchedulers; - + // A hint that might contain information that speeds up the modelchecking process (if supported by the model checker) std::shared_ptr hint; }; - + } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index c14a9ba93..d9e2681a6 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -116,7 +116,7 @@ namespace storm { if (this->isContinuousTime()) { STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games."); } else { - storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor); + storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor, nullptr, nullptr, &statesOfCoalition); return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 28ace1d81..15c12ba95 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -26,7 +26,7 @@ namespace storm { namespace internal { template - LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) { + LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates, storm::storage::BitVector const* statesOfCoalition) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false), _statesOfCoalition(statesOfCoalition) { setComponent(component); // Run through the component and collect some data: @@ -167,6 +167,9 @@ namespace storm { if (env.solver().lra().isMaximalIterationCountSet()) { maxIter = env.solver().lra().getMaximalIterationCount(); } + if(gameNondetTs()) { + STORM_LOG_ASSERT(_statesOfCoalition != nullptr, "Tried to solve LRA problem for a game, but coalition states have not been set."); + } // start the iterations ValueType result = storm::utility::zero(); @@ -218,13 +221,10 @@ namespace storm { } performIterationStep(env, dir, choices); } - std::cout << "result (" << iter << " steps):" << std::endl; - storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); - for(int i = 0; i < xNew().size() ; i++ ) { - std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl; - //if(i == 50) {std::cout << "only showing top 50 lines"; break; } + if(gameNondetTs()) { + storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); + result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ? } - if(gameNondetTs()) result = xOld().at(0) * _uniformizationRate; // TODO is "init" always going to be .at(0) ? return result; } @@ -386,10 +386,10 @@ namespace storm { } } else if(gameNondetTs()) { // TODO DRYness? exact same behaviour as case above? if (choices == nullptr) { - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew()); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), nullptr, _statesOfCoalition); } else { std::vector tsChoices(_TsTransitions.getRowGroupCount()); - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices, _statesOfCoalition); setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? } } else { diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index c800a9976..abd1576de 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -8,12 +8,12 @@ namespace storm { class Environment; - - + + namespace modelchecker { namespace helper { namespace internal { - + /*! * Specifies differnt kinds of transition types with which this helper can be used * Ts means timed states (cf. Markovian states in a Markov Automaton) and Is means instant states (cf. probabilistic states in a Markov automaton). @@ -45,7 +45,7 @@ namespace storm { public: /// Function mapping from indices to values typedef std::function ValueGetter; - + /*! * Initializes a new VI helper for the provided MEC or BSCC * @param component the MEC or BSCC @@ -55,7 +55,7 @@ namespace storm { * @param exitRates The exit rates of the timed states (relevant for continuous time models). If nullptr, all rates are assumed to be 1 (which corresponds to a discrete time model) * @note All indices and vectors must be w.r.t. the states as described by the provided transition matrix */ - LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates = nullptr, std::vector const* exitRates = nullptr); + LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates = nullptr, std::vector const* exitRates = nullptr, storm::storage::BitVector const* statesOfCoalition = nullptr); /*! * Performs value iteration with the given state- and action values. @@ -69,9 +69,9 @@ namespace storm { * @note it is possible to call this method multiple times with different values. However, other changes to the environment or the optimization direction might not have the expected effect due to caching. */ ValueType performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); - + private: - + /*! * Initializes the value iterations with the provided values. * Resets all information from potential previous calls. @@ -80,7 +80,7 @@ namespace storm { * @param stateValueGetter Function that returns for each global choice index (w.r.t. the input transitions) the value (e.g. reward) for that choice */ void initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr); - + /*! * Performs a single iteration step. * @param env The environment. @@ -90,41 +90,41 @@ namespace storm { * @pre when calling this the first time, initializeNewValues must have been called before. Moreover, prepareNextIteration must be called between two calls of this. */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); - + struct ConvergenceCheckResult { bool isPrecisionAchieved; ValueType currentValue; }; - + /*! * Checks whether the curently computed value achieves the desired precision */ ConvergenceCheckResult checkConvergence(bool relative, ValueType precision) const; - + /*! * Must be called between two calls of performIterationStep. */ void prepareNextIteration(Environment const& env); - + /// Prepares the necessary solvers and multipliers for doing the iterations. void prepareSolversAndMultipliers(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr); - + void setInputModelChoices(std::vector& choices, std::vector const& localMecChoices, bool setChoiceZeroToMarkovianStates = false, bool setChoiceZeroToProbabilisticStates = false) const; - + /// Returns true iff the given state is a timed state bool isTimedState(uint64_t const& inputModelStateIndex) const; - + /// The result for timed states of the most recent iteration std::vector& xNew(); std::vector const& xNew() const; - + /// The result for timed states of the previous iteration std::vector& xOld(); std::vector const& xOld() const; /// @return true iff there potentially is a nondeterministic choice at timed states bool nondetTs() const; - + /// @return true iff there potentially is a nondeterministic choice at instant states. Returns false if there are no instant states. bool nondetIs() const; @@ -132,14 +132,15 @@ namespace storm { bool gameNondetTs() const; void setComponent(ComponentType component); - + // We need to make sure that states/choices will be processed in ascending order typedef std::map> InternalComponentType; - + InternalComponentType _component; storm::storage::SparseMatrix const& _transitionMatrix; storm::storage::BitVector const* _timedStates; // e.g. Markovian states of a Markov automaton. + storm::storage::BitVector const* _statesOfCoalition; bool _hasInstantStates; ValueType _uniformizationRate; storm::storage::SparseMatrix _TsTransitions, _TsToIsTransitions, _IsTransitions, _IsToTsTransitions; @@ -154,4 +155,4 @@ namespace storm { } } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index d40c5ade0..97efcc3bc 100644 --- a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -9,31 +9,31 @@ namespace storm { namespace storage { class BitVector; } - + namespace modelchecker { namespace helper { template struct MDPSparseModelCheckingHelperReturnType { - + MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; - + MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr>&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { // Intentionally left empty. } - + virtual ~MDPSparseModelCheckingHelperReturnType() { // Intentionally left empty. } - + // The values computed for the states. std::vector values; - + // A scheduler, if it was computed. std::unique_ptr> scheduler; }; } - + } } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 774ef0014..08f8c614d 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -24,6 +24,8 @@ #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/shields/shield-handling.h" + #include "storm/settings/modules/GeneralSettings.h" #include "storm/exceptions/InvalidStateException.h" @@ -65,6 +67,8 @@ namespace storm { storm::logic::Formula const& subFormula = gameFormula.getSubformula(); statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition()); + std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl; + statesOfCoalition.complement(); if (subFormula.isRewardOperatorFormula()) { return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); @@ -143,7 +147,9 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); - if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + if(checkTask.isShieldingTask()) { + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), statesOfCoalition); + } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -157,7 +163,9 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); - if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + if(checkTask.isShieldingTask()) { + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), statesOfCoalition); + } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } return result; @@ -184,6 +192,9 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if(checkTask.isShieldingTask()) { + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), statesOfCoalition); + } return result; } @@ -195,17 +206,17 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set."); - auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition()); - std::cout << "Found " << coalitionStates.getNumberOfSetBits() << " states in coalition." << std::endl; storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); - if (checkTask.isProduceSchedulersSet()) { + if(checkTask.isShieldingTask()) { + tempest::shields::createOptimalShield(std::make_shared>(this->getModel()), helper.getProducedOptimalChoices(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), statesOfCoalition, statesOfCoalition); + } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } + return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h b/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h new file mode 100644 index 000000000..17f96ad9c --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include "storm/storage/Scheduler.h" + +namespace storm { + namespace storage { + class BitVector; + } + + namespace modelchecker { + namespace helper { + template + struct SMGSparseModelCheckingHelperReturnType { + + SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType const&) = delete; + SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType&&) = default; + + SMGSparseModelCheckingHelperReturnType(std::vector&& values, storm::storage::BitVector&& relevantStates = nullptr, std::unique_ptr>&& scheduler = nullptr, std::vector&& choiceValues = nullptr) : values(std::move(values)), relevantStates(relevantStates), scheduler(std::move(scheduler)), choiceValues(std::move(choiceValues)) { + // Intentionally left empty. + } + + virtual ~SMGSparseModelCheckingHelperReturnType() { + // Intentionally left empty. + } + + // The values computed for the states. + std::vector values; + + // The relevant states for which choice values have been computed. + storm::storage::BitVector relevantStates; + + // A scheduler, if it was computed. + std::unique_ptr> scheduler; + + // The values computed for the available choices. + std::vector choiceValues; + }; + } + + } +} diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ca6e53ea2..a57a0ccef 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -14,20 +14,18 @@ namespace storm { namespace helper { template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // TODO add Kwiatkowska original reference - // TODO FIX solver min max mess - auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); // Initialize the solution vector. std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -43,12 +41,17 @@ namespace storm { } viHelper.performValueIteration(env, x, b, goal.direction()); + //if(goal.isShieldingTask()) { + if(true) { + viHelper.getChoiceValues(env, x, constrainedChoiceValues); + } viHelper.fillResultVector(x, relevantStates, psiStates); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } - return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template @@ -72,7 +75,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // the idea is to implement the definition of globally as in the formula: // G psi = not(F(not psi)) = not(true U (not psi)) // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again @@ -82,11 +85,14 @@ namespace storm { for (auto& element : result.values) { element = storm::utility::one() - element; } + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } return result; } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { // create vector x for result, bitvector allStates with a true for each state and a vector b for the probability to get to state psi std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); @@ -100,14 +106,19 @@ namespace storm { // create multiplier and execute the calculation for 1 step auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + //if(goal.isShieldingTask()) { + if (true) { + multiplier->multiply(env, x, &b, choiceValues); + } multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition); - STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); - return MDPSparseModelCheckingHelperReturnType(std::move(x)); + return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(allStates), nullptr, std::move(choiceValues)); } template - MDPSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); @@ -137,17 +148,17 @@ namespace storm { if(upperBound > 0) { viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); -/* if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - - }*/ } + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); viHelper.fillResultVector(x, relevantStates); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - STORM_LOG_DEBUG("x = " << x); + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + } - return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index e6a36f2af..5258104dc 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -9,7 +9,7 @@ #include "storm/utility/solver.h" #include "storm/solver/SolveGoal.h" -#include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h" +#include "storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h" namespace storm { @@ -34,15 +34,13 @@ namespace storm { template class SparseSmgRpatlHelper { public: - // TODO should probably be renamed in the future: - - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); - static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); - static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); - static MDPSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); - + static SMGSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static SMGSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static SMGSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); + static SMGSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); + static void expandChoiceValues(std::vector const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector const& constrainedChoiceValues, std::vector& choiceValues); }; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 9a4db040e..33bb6dfe2 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -73,6 +73,21 @@ namespace storm { result = filledVector; } + template + void BoundedGloballyGameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + template void BoundedGloballyGameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index d2eb985dc..78d499265 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -30,6 +30,11 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index e0fd4eee8..58a42a397 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -8,8 +8,6 @@ #include "storm/utility/SignalHandler.h" #include "storm/utility/vector.h" -// TODO this will undergo major refactoring as soon as we implement model checking of further properties - namespace storm { namespace modelchecker { namespace helper { @@ -21,10 +19,6 @@ namespace storm { template void GameViHelper::prepareSolversAndMultipliers(const Environment& env) { - // TODO we get whole transitionmatrix and psistates DONE IN smgrpatlhelper - // -> clip statesofcoalition - // -> compute b vector from psiStates - // -> clip transitionmatrix and create multiplier _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; @@ -75,29 +69,16 @@ namespace storm { } _x1IsCurrent = !_x1IsCurrent; - // multiplyandreducegaussseidel - // Ax + b if (choices == nullptr) { - //STORM_LOG_DEBUG("\n" << _transitionMatrix); - //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld())); - //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b)); - //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew())); _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); - //std::cin.get(); } else { - // Also keep track of the choices made. _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); } // compare applyPointwise storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(storm::solver::maximize(dir)) { - if(a > b) return a; - else return b; - } else { - if(a > b) return a; - else return b; - } + if(a > b) return a; + else return b; }); } @@ -129,13 +110,11 @@ namespace storm { return false; } } - // TODO needs checking return true; } template - void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) - { + void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); uint bitIndex = 0; for(uint i = 0; i < filledVector.size(); i++) { @@ -150,6 +129,21 @@ namespace storm { result = filledVector; } + template + void GameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; @@ -184,6 +178,11 @@ namespace storm { return scheduler; } + template + void GameViHelper::getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues) { + _multiplier->multiply(env, x, &_b, choiceValues); + } + template std::vector& GameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 3a1343f90..00eca9fe6 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -30,6 +30,11 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ @@ -42,6 +47,7 @@ namespace storm { storm::storage::Scheduler extractScheduler() const; + void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp new file mode 100644 index 000000000..779f3b894 --- /dev/null +++ b/src/storm/shields/AbstractShield.cpp @@ -0,0 +1,43 @@ +#include "storm/shields/AbstractShield.h" + +#include + +namespace tempest { + namespace shields { + + template + AbstractShield::AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : rowGroupIndices(rowGroupIndices), shieldingExpression(shieldingExpression), optimizationDirection(optimizationDirection), relevantStates(relevantStates), coalitionStates(coalitionStates) { + // Intentionally left empty. + } + + template + AbstractShield::~AbstractShield() { + // Intentionally left empty. + } + + template + std::vector AbstractShield::computeRowGroupSizes() { + std::vector rowGroupSizes(this->rowGroupIndices.size() - 1); + for(uint rowGroupStartIndex = 0; rowGroupStartIndex < rowGroupSizes.size(); rowGroupStartIndex++) { + rowGroupSizes.at(rowGroupStartIndex) = this->rowGroupIndices[rowGroupStartIndex + 1] - this->rowGroupIndices[rowGroupStartIndex]; + } + return rowGroupSizes; + } + + template + storm::OptimizationDirection AbstractShield::getOptimizationDirection() { + return optimizationDirection; + } + + template + std::string AbstractShield::getClassName() const { + return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); + } + + // Explicitly instantiate appropriate + template class AbstractShield::index_type>; +#ifdef STORM_HAVE_CARL + template class AbstractShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h new file mode 100644 index 000000000..d93da4407 --- /dev/null +++ b/src/storm/shields/AbstractShield.h @@ -0,0 +1,62 @@ +#pragma once + +#include +#include +#include +#include + +#include "storm/storage/Scheduler.h" +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/Distribution.h" + +#include "storm/utility/constants.h" + +#include "storm/solver/OptimizationDirection.h" + +#include "storm/logic/ShieldExpression.h" + +namespace tempest { + namespace shields { + namespace utility { + template + struct ChoiceFilter { + bool operator()(ValueType v, ValueType max, double shieldValue) { + Compare compare; + if(relative) return compare(v, max * shieldValue); + else return compare(v, shieldValue); + } + }; + } + + template + class AbstractShield { + public: + typedef IndexType index_type; + typedef ValueType value_type; + + virtual ~AbstractShield() = 0; + + /*! + * Computes the sizes of the row groups based on the indices given. + */ + std::vector computeRowGroupSizes(); + + storm::OptimizationDirection getOptimizationDirection(); + + std::string getClassName() const; + + protected: + AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + + std::vector rowGroupIndices; + //std::vector choiceValues; + + std::shared_ptr shieldingExpression; + storm::OptimizationDirection optimizationDirection; + + storm::storage::BitVector relevantStates; + boost::optional coalitionStates; + }; + } +} diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp new file mode 100644 index 000000000..0bd26908d --- /dev/null +++ b/src/storm/shields/OptimalShield.cpp @@ -0,0 +1,35 @@ +#include "storm/shields/OptimalShield.h" + +#include + +namespace tempest { + namespace shields { + + template + OptimalShield::OptimalShield(std::vector const& rowGroupIndices, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), precomputedChoices(precomputedChoices) { + // Intentionally left empty. + } + + template + storm::storage::OptimalScheduler OptimalShield::construct() { + storm::storage::OptimalScheduler shield(this->rowGroupIndices.size() - 1); + // TODO Needs fixing as soon as we support MDPs + if(this->coalitionStates.is_initialized()) { + this->relevantStates = ~this->relevantStates; + } + for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { + if(this->relevantStates.get(state)) { + shield.setChoice(precomputedChoices[state], state); + } else { + shield.setChoice(storm::storage::Distribution(), state); + } + } + return shield; + } + // Explicitly instantiate appropriate + template class OptimalShield::index_type>; +#ifdef STORM_HAVE_CARL + template class OptimalShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/OptimalShield.h b/src/storm/shields/OptimalShield.h new file mode 100644 index 000000000..03bff3542 --- /dev/null +++ b/src/storm/shields/OptimalShield.h @@ -0,0 +1,19 @@ +#pragma once + +#include "storm/shields/AbstractShield.h" +#include "storm/storage/OptimalScheduler.h" + +namespace tempest { + namespace shields { + + template + class OptimalShield : public AbstractShield { + public: + OptimalShield(std::vector const& rowGroupIndices, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + + storm::storage::OptimalScheduler construct(); + private: + std::vector precomputedChoices; + }; + } +} diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp new file mode 100644 index 000000000..9c639c010 --- /dev/null +++ b/src/storm/shields/PostSafetyShield.cpp @@ -0,0 +1,73 @@ +#include "storm/shields/PostSafetyShield.h" + +#include + +namespace tempest { + namespace shields { + + template + PostSafetyShield::PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { + // Intentionally left empty. + } + + template + storm::storage::PostScheduler PostSafetyShield::construct() { + if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } else { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } + } + + template + template + storm::storage::PostScheduler PostSafetyShield::constructWithCompareType() { + tempest::shields::utility::ChoiceFilter choiceFilter; + storm::storage::PostScheduler shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes()); + auto choice_it = this->choiceValues.begin(); + if(this->coalitionStates.is_initialized()) { + this->relevantStates &= this->coalitionStates.get(); + } + for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; + if(this->relevantStates.get(state)) { + auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; + ValueType maxProbability = *(choice_it + maxProbabilityIndex); + if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { + STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); + shield.setChoice(0, storm::storage::Distribution(), state); + choice_it += rowGroupSize; + continue; + } + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + storm::storage::Distribution actionDistribution; + if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { + actionDistribution.addProbability(choice, 1); + } else { + actionDistribution.addProbability(maxProbabilityIndex, 1); + } + shield.setChoice(choice, storm::storage::SchedulerChoice(actionDistribution), state); + } + } else { + shield.setChoice(0, storm::storage::Distribution(), state); + choice_it += rowGroupSize; + } + } + return shield; + } + + // Explicitly instantiate appropriate + template class PostSafetyShield::index_type>; +#ifdef STORM_HAVE_CARL + template class PostSafetyShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/PostSafetyShield.h b/src/storm/shields/PostSafetyShield.h new file mode 100644 index 000000000..6f04e53c3 --- /dev/null +++ b/src/storm/shields/PostSafetyShield.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/shields/AbstractShield.h" +#include "storm/storage/PostScheduler.h" + +namespace tempest { + namespace shields { + + template + class PostSafetyShield : public AbstractShield { + public: + PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + + storm::storage::PostScheduler construct(); + template + storm::storage::PostScheduler constructWithCompareType(); + private: + std::vector choiceValues; + }; + } +} diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp new file mode 100644 index 000000000..abbc50ae7 --- /dev/null +++ b/src/storm/shields/PreSafetyShield.cpp @@ -0,0 +1,70 @@ +#include "storm/shields/PreSafetyShield.h" + +#include + +namespace tempest { + namespace shields { + + template + PreSafetyShield::PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates), choiceValues(choiceValues) { + // Intentionally left empty. + } + + template + storm::storage::PreScheduler PreSafetyShield::construct() { + if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } else { + if(this->shieldingExpression->isRelative()) { + return constructWithCompareType, true>(); + } else { + return constructWithCompareType, false>(); + } + } + } + + template + template + storm::storage::PreScheduler PreSafetyShield::constructWithCompareType() { + tempest::shields::utility::ChoiceFilter choiceFilter; + storm::storage::PreScheduler shield(this->rowGroupIndices.size() - 1); + auto choice_it = this->choiceValues.begin(); + if(this->coalitionStates.is_initialized()) { + this->relevantStates &= this->coalitionStates.get(); + } + for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; + if(this->relevantStates.get(state)) { + storm::storage::Distribution actionDistribution; + ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); + if(!relative && !choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { + STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); + shield.setChoice(storm::storage::Distribution(), state); + choice_it += rowGroupSize; + continue; + } + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { + actionDistribution.addProbability(choice, *choice_it); + } + } + shield.setChoice(storm::storage::SchedulerChoice(actionDistribution), state); + + } else { + shield.setChoice(storm::storage::Distribution(), state); + choice_it += rowGroupSize; + } + } + return shield; + } + // Explicitly instantiate appropriate + template class PreSafetyShield::index_type>; +#ifdef STORM_HAVE_CARL + template class PreSafetyShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/PreSafetyShield.h b/src/storm/shields/PreSafetyShield.h new file mode 100644 index 000000000..8a4667bf2 --- /dev/null +++ b/src/storm/shields/PreSafetyShield.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/shields/AbstractShield.h" +#include "storm/storage/PreScheduler.h" + +namespace tempest { + namespace shields { + + template + class PreSafetyShield : public AbstractShield { + public: + PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + + storm::storage::PreScheduler construct(); + template + storm::storage::PreScheduler constructWithCompareType(); + private: + std::vector choiceValues; + }; + } +} diff --git a/src/storm/shields/shield-handling.h b/src/storm/shields/shield-handling.h new file mode 100644 index 000000000..ef4686334 --- /dev/null +++ b/src/storm/shields/shield-handling.h @@ -0,0 +1,60 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/Scheduler.h" +#include "storm/storage/BitVector.h" + +#include "storm/logic/ShieldExpression.h" + +#include "storm/shields/AbstractShield.h" +#include "storm/shields/PreSafetyShield.h" +#include "storm/shields/PostSafetyShield.h" +#include "storm/shields/OptimalShield.h" + +#include "storm/io/file.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidArgumentException.h" + + +namespace tempest { + namespace shields { + std::string shieldFilename(std::shared_ptr const& shieldingExpression) { + return shieldingExpression->getFilename() + ".shield"; + } + + template + void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { + std::ofstream stream; + storm::utility::openFile(shieldFilename(shieldingExpression), stream); + if(shieldingExpression->isPreSafetyShield()) { + PreSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + shield.construct().printToStream(stream, shieldingExpression, model); + } else if(shieldingExpression->isPostSafetyShield()) { + PostSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + shield.construct().printToStream(stream, shieldingExpression, model); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); + storm::utility::closeFile(stream); + } + storm::utility::closeFile(stream); + } + + template + void createOptimalShield(std::shared_ptr> model, std::vector const& precomputedChoices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { + std::ofstream stream; + storm::utility::openFile(shieldFilename(shieldingExpression), stream); + if(shieldingExpression->isOptimalShield()) { + OptimalShield shield(model->getTransitionMatrix().getRowGroupIndices(), precomputedChoices, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); + shield.construct().printToStream(stream, shieldingExpression, model); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown Shielding Type: " + shieldingExpression->typeToString()); + storm::utility::closeFile(stream); + } + storm::utility::closeFile(stream); + } + } +} diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index e36ce7e74..e28e1ceae 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -88,7 +88,7 @@ namespace storm { } template - void GmmxxMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { initialize(); std::vector* target = &result; if (&x == &result) { @@ -110,7 +110,7 @@ namespace storm { } template - void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { initialize(); multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, dirOverride, backwards); } @@ -135,7 +135,7 @@ namespace storm { } template - void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { bool isOverridden = (dirOverride && !dirOverride->empty()) ? true : false; if (dir == storm::OptimizationDirection::Minimize) { if(isOverridden) { @@ -170,7 +170,7 @@ namespace storm { template template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -304,7 +304,7 @@ namespace storm { template<> template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } @@ -330,7 +330,7 @@ namespace storm { template class TbbMultAddReduceFunctor { public: - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -429,12 +429,12 @@ namespace storm { std::vector const* b; std::vector& result; std::vector* choices; - boost::optional dirOverride = boost::none; + boost::optional const dirOverride = boost::none; }; #endif template - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { #ifdef STORM_HAVE_INTELTBB if (dir == storm::OptimizationDirection::Minimize) { tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride)); @@ -448,7 +448,7 @@ namespace storm { } template<> - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } diff --git a/src/storm/solver/GmmxxMultiplier.h b/src/storm/solver/GmmxxMultiplier.h index 77050f8aa..b3f65d282 100644 --- a/src/storm/solver/GmmxxMultiplier.h +++ b/src/storm/solver/GmmxxMultiplier.h @@ -25,8 +25,8 @@ namespace storm { virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; - virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override; + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const override; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void clearCache() const override; @@ -37,11 +37,11 @@ namespace storm { void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; - void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const; + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; + void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const; template - void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; mutable gmm::csr_matrix gmmMatrix; }; diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index a0533b06d..97eb22bb8 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -30,12 +30,12 @@ namespace storm { } template - void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices, dirOverride); } template - void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, dirOverride, backwards); } @@ -55,7 +55,7 @@ namespace storm { } template - void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector* dirOverride) const { + void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector const* dirOverride) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index 7662d355c..4127a6625 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -70,8 +70,8 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. * @param choices If given, the choices made in the reduction process are written to this vector. */ - void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; - virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const = 0; + void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const = 0; /*! * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups @@ -88,8 +88,8 @@ namespace storm { * @param choices If given, the choices made in the reduction process are written to this vector. * @param backwards if true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup. */ - void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const = 0; + void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -117,7 +117,7 @@ namespace storm { * to the number of rows of A. * @param n The number of times to perform the multiplication. */ - void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector* dirOverride = nullptr) const; + void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector const* dirOverride = nullptr) const; /*! * Multiplies the row with the given index with x and adds the result to the provided value diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 26dad0b22..17df1faa3 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -16,12 +16,12 @@ namespace storm { namespace solver { - + template NativeMultiplier::NativeMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { // Intentionally left empty. } - + template bool NativeMultiplier::parallelize(Environment const& env) const { #ifdef STORM_HAVE_INTELTBB @@ -30,7 +30,7 @@ namespace storm { return false; #endif } - + template void NativeMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { std::vector* target = &result; @@ -51,7 +51,7 @@ namespace storm { std::swap(result, *this->cachedVector); } } - + template void NativeMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards) const { if (backwards) { @@ -62,7 +62,7 @@ namespace storm { } template - void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { std::vector* target = &result; if (&x == &result) { if (this->cachedVector) { @@ -83,7 +83,7 @@ namespace storm { } template - void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { if (backwards) { this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices, dirOverride); } else { @@ -112,7 +112,7 @@ namespace storm { } template - void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices, dirOverride); } @@ -127,7 +127,7 @@ namespace storm { } template - void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { #ifdef STORM_HAVE_INTELTBB this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices, dirOverride); #else @@ -141,6 +141,6 @@ namespace storm { template class NativeMultiplier; template class NativeMultiplier; #endif - + } } diff --git a/src/storm/solver/NativeMultiplier.h b/src/storm/solver/NativeMultiplier.h index 62ae47d07..532ec2cc9 100644 --- a/src/storm/solver/NativeMultiplier.h +++ b/src/storm/solver/NativeMultiplier.h @@ -20,8 +20,8 @@ namespace storm { virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; - virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override; + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const override; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const override; @@ -30,10 +30,10 @@ namespace storm { void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; }; diff --git a/src/storm/storage/OptimalScheduler.cpp b/src/storm/storage/OptimalScheduler.cpp new file mode 100644 index 000000000..982c2e6fa --- /dev/null +++ b/src/storm/storage/OptimalScheduler.cpp @@ -0,0 +1,112 @@ +#include "storm/utility/vector.h" +#include "storm/storage/OptimalScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace storage { + template + OptimalScheduler::OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + } + + template + OptimalScheduler::OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + } + + template + void OptimalScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == this->schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + STORM_LOG_THROW(this->isMemorylessScheduler(), storm::exceptions::InvalidOperationException, "The given scheduler is incompatible."); + + bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); + bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); + bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); + uint_fast64_t widthOfStates = std::to_string(this->schedulerChoices.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(this->schedulerChoices.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; + + out << "___________________________________________________________________" << std::endl; + out << shieldingExpression->prettify() << std::endl; + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + out << std::setw(widthOfStates) << "model state:" << " " << "choice"; + if(choiceLabelsGiven) { + out << " [: (]"; + } else { + out << " [: ()}"; + } + out << ":" << std::endl; + for (uint_fast64_t state = 0; state < this->schedulerChoices.front().size(); ++state) { + std::stringstream stateString; + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + ++numOfSkippedStatesWithUniqueChoice; + continue; + } + + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < this->getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; + } else { + stateString << std::setw(widthOfStates) << ""; + stateString << " "; + } + + // Print choice info + SchedulerChoice const& choice = this->schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + stateString << "; "; + } + stateString << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + } else { + stateString << choiceProbPair.first; + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + stateString << ")"; + } + } else { + if(!this->printUndefinedChoices) continue; + stateString << "undefined."; + } + + // Todo: print memory updates + out << stateString.str(); + out << std::endl; + } + } + if (numOfSkippedStatesWithUniqueChoice > 0) { + out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; + } + out << "___________________________________________________________________" << std::endl; + } + + template class OptimalScheduler; +#ifdef STORM_HAVE_CARL + template class OptimalScheduler; +#endif + } +} diff --git a/src/storm/storage/OptimalScheduler.h b/src/storm/storage/OptimalScheduler.h new file mode 100644 index 000000000..827676bbd --- /dev/null +++ b/src/storm/storage/OptimalScheduler.h @@ -0,0 +1,42 @@ +#pragma once + +#include +#include +#include +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/Scheduler.h" +#include "storm/logic/ShieldExpression.h" + +namespace storm { + namespace storage { + + /* + * TODO needs obvious changes in all comment blocks + * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i + * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). + * A Choice can be undefined, deterministic + */ + template + class OptimalScheduler : public Scheduler { + public: + typedef uint_fast64_t OldChoice; + /*! + * Initializes a scheduler for the given number of model states. + * + * @param numberOfModelStates number of model states + * @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless. + */ + OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); + OptimalScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + + /*! + * Prints the scheduler to the given output stream. + * @param out The output stream + * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) + * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. + * Requires a model to be given. + */ + void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + }; + } +} diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp new file mode 100644 index 000000000..2e4392891 --- /dev/null +++ b/src/storm/storage/PostScheduler.cpp @@ -0,0 +1,145 @@ +#include "storm/utility/vector.h" +#include "storm/storage/PostScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace storage { + + template + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + STORM_LOG_DEBUG(numberOfChoicesPerState.size() << " " << numberOfModelStates); + STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); + for(uint state = 0; state < numberOfModelStates; state++) { + schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); + } + numberOfChoices = 0; + for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) + numberOfChoices += *it; + this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices; + this->numOfDeterministicChoices = 0; + } + + template + PostScheduler::PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + STORM_LOG_ASSERT(numberOfChoicesPerState.size() == numberOfModelStates, "Need to know amount of choices per model state"); + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoiceMapping = std::vector>>>(numOfMemoryStates, std::vector>>(numberOfModelStates)); + for(uint state = 0; state < numberOfModelStates; state++) { + schedulerChoiceMapping[0][state].resize(numberOfChoicesPerState[state]); + } + numberOfChoices = 0; + for(std::vector::iterator it = numberOfChoicesPerState.begin(); it != numberOfChoicesPerState.end(); ++it) + numberOfChoices += *it; + this->numOfUndefinedChoices = numOfMemoryStates * numberOfChoices; + this->numOfDeterministicChoices = 0; + } + + template + void PostScheduler::setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState == 0, "Currently we do not support PostScheduler with memory"); + STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); + + schedulerChoiceMapping[memoryState][modelState][oldChoice] = newChoice; + } + + template + SchedulerChoice const& PostScheduler::getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState < this->getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < schedulerChoiceMapping[memoryState].size(), "Illegal model state index"); + return schedulerChoiceMapping[memoryState][modelState][oldChoice]; + } + + + template + bool PostScheduler::isDeterministicScheduler() const { + return true; + } + + template + bool PostScheduler::isMemorylessScheduler() const { + return true; + } + + template + void PostScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(this->isMemorylessScheduler(), storm::exceptions::InvalidOperationException, "The given scheduler is incompatible."); + + bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); + bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); + bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); + uint_fast64_t widthOfStates = std::to_string(schedulerChoiceMapping.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(schedulerChoiceMapping.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + out << "___________________________________________________________________" << std::endl; + out << shieldingExpression->prettify() << std::endl; + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + out << std::setw(widthOfStates) << "model state:" << " " << "correction"; + if(choiceLabelsGiven) { + out << " [ {action label}: {corrected action label}]"; + } else { + out << " [: ()}"; + } + out << ":" << std::endl; + uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; + for (uint_fast64_t state = 0; state < schedulerChoiceMapping.front().size(); ++state) { + std::stringstream stateString; + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstChoiceIndex = true; + for(uint choiceIndex = 0; choiceIndex < schedulerChoiceMapping[0][state].size(); choiceIndex++) { + SchedulerChoice const& choice = schedulerChoiceMapping[0][state][choiceIndex]; + if(firstChoiceIndex) { + firstChoiceIndex = false; + } else { + stateString << "; "; + } + if (choice.isDefined()) { + auto choiceProbPair = *(choice.getChoiceAsDistribution().begin()); + if(choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceIndex); + stateString << std::to_string(choiceIndex) << " {" << boost::join(choiceLabels, ", ") << "}: "; + } else { + stateString << std::to_string(choiceIndex) << ": "; + } + //stateString << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + } else { + stateString << choiceProbPair.first; + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + + } else { + if(!this->printUndefinedChoices) goto skipStatesWithUndefinedChoices; + stateString << "undefined."; + } + // Todo: print memory updates + } + out << stateString.str() << std::endl; + // jump to label if we find one undefined choice. + skipStatesWithUndefinedChoices:; + } + } + + template class PostScheduler; +#ifdef STORM_HAVE_CARL + template class PostScheduler; +#endif + } +} diff --git a/src/storm/storage/PostScheduler.h b/src/storm/storage/PostScheduler.h new file mode 100644 index 000000000..57c194fa6 --- /dev/null +++ b/src/storm/storage/PostScheduler.h @@ -0,0 +1,101 @@ +#pragma once + +#include +#include +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/Scheduler.h" +#include "storm/logic/ShieldExpression.h" + +namespace storm { + namespace storage { + + /* + * TODO needs obvious changes in all comment blocks + * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i + * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). + * A Choice can be undefined, deterministic + */ + template + class PostScheduler : public Scheduler { + public: + typedef uint_fast64_t OldChoice; + /*! + * Initializes a scheduler for the given number of model states. + * + * @param numberOfModelStates number of model states + * @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless. + */ + PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional const& memoryStructure = boost::none); + PostScheduler(uint_fast64_t numberOfModelStates, std::vector numberOfChoicesPerState, boost::optional&& memoryStructure); + + /*! + * Sets the choice defined by the scheduler for the given state. + * + * @param choice The choice to set for the given state. + * @param modelState The state of the model for which to set the choice. + * @param memoryState The state of the memoryStructure for which to set the choice. + */ + void setChoice(OldChoice const& oldChoice, SchedulerChoice const& newChoice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); + + /*! + * Is the scheduler defined on the states indicated by the selected-states bitvector? + */ + bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const; + + /*! + * Clears the choice defined by the scheduler for the given state. + * + * @param modelState The state of the model for which to clear the choice. + * @param memoryState The state of the memoryStructure for which to clear the choice. + */ + void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); + + /*! + * Gets the choice defined by the scheduler for the given model and memory state. + * + * @param state The state for which to get the choice. + * @param memoryState the memory state which we consider. + */ + SchedulerChoice const& getChoice(uint_fast64_t modelState, OldChoice oldChoice, uint_fast64_t memoryState = 0) ; + + /*! + * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state + */ + //storm::storage::BitVector computeActionSupport(std::vector const& nondeterministicChoiceIndicies) const; + + /*! + * Retrieves whether all defined choices are deterministic + */ + bool isDeterministicScheduler() const; + + /*! + * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) + */ + bool isMemorylessScheduler() const; + + /*! + * Retrieves the number of memory states this scheduler considers. + */ + //uint_fast64_t getNumberOfMemoryStates() const; + + /*! + * Retrieves the memory structure associated with this scheduler + */ + //boost::optional const& getMemoryStructure() const; + + /*! + * Prints the scheduler to the given output stream. + * @param out The output stream + * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) + * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. + * Requires a model to be given. + */ + void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + private: + std::vector>>> schedulerChoiceMapping; + + std::vector numberOfChoicesPerState; + uint_fast64_t numberOfChoices; + }; + } +} diff --git a/src/storm/storage/PreScheduler.cpp b/src/storm/storage/PreScheduler.cpp new file mode 100644 index 000000000..0f1cf775d --- /dev/null +++ b/src/storm/storage/PreScheduler.cpp @@ -0,0 +1,112 @@ +#include "storm/utility/vector.h" +#include "storm/storage/PreScheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace storage { + template + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : Scheduler(numberOfModelStates, memoryStructure) { + } + + template + PreScheduler::PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : Scheduler(numberOfModelStates, std::move(memoryStructure)) { + } + + template + void PreScheduler::printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == this->schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + STORM_LOG_THROW(this->isMemorylessScheduler(), storm::exceptions::InvalidOperationException, "The given scheduler is incompatible."); + + bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); + bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); + bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); + uint_fast64_t widthOfStates = std::to_string(this->schedulerChoices.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(this->schedulerChoices.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); + uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; + + out << "___________________________________________________________________" << std::endl; + out << shieldingExpression->prettify() << std::endl; + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + out << std::setw(widthOfStates) << "model state:" << " " << "choice(s)"; + if(choiceLabelsGiven) { + out << " [: (]"; + } else { + out << " [: ()}"; + } + out << ":" << std::endl; + for (uint_fast64_t state = 0; state < this->schedulerChoices.front().size(); ++state) { + std::stringstream stateString; + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + ++numOfSkippedStatesWithUniqueChoice; + continue; + } + + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < this->getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; + } else { + stateString << std::setw(widthOfStates) << ""; + stateString << " "; + } + + // Print choice info + SchedulerChoice const& choice = this->schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + stateString << "; "; + } + stateString << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + } else { + stateString << choiceProbPair.first; + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } + stateString << ")"; + } + } else { + if(!this->printUndefinedChoices) continue; + stateString << "undefined."; + } + + // Todo: print memory updates + out << stateString.str(); + out << std::endl; + } + } + if (numOfSkippedStatesWithUniqueChoice > 0) { + out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; + } + out << "___________________________________________________________________" << std::endl; + } + + template class PreScheduler; +#ifdef STORM_HAVE_CARL + template class PreScheduler; +#endif + } +} diff --git a/src/storm/storage/PreScheduler.h b/src/storm/storage/PreScheduler.h new file mode 100644 index 000000000..8207456e1 --- /dev/null +++ b/src/storm/storage/PreScheduler.h @@ -0,0 +1,42 @@ +#pragma once + +#include +#include +#include +#include "storm/storage/SchedulerChoice.h" +#include "storm/storage/Scheduler.h" +#include "storm/logic/ShieldExpression.h" + +namespace storm { + namespace storage { + + /* + * TODO needs obvious changes in all comment blocks + * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i + * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). + * A Choice can be undefined, deterministic + */ + template + class PreScheduler : public Scheduler { + public: + typedef uint_fast64_t OldChoice; + /*! + * Initializes a scheduler for the given number of model states. + * + * @param numberOfModelStates number of model states + * @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless. + */ + PreScheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); + PreScheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + + /*! + * Prints the scheduler to the given output stream. + * @param out The output stream + * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) + * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. + * Requires a model to be given. + */ + void printToStream(std::ostream& out, std::shared_ptr shieldingExpression, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + }; + } +} diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 59db79429..c53d1f015 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -8,7 +8,7 @@ namespace storm { namespace storage { - + template Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; @@ -16,7 +16,7 @@ namespace storm { numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; } - + template Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1; @@ -24,7 +24,7 @@ namespace storm { numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; } - + template void Scheduler::setChoice(SchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); @@ -50,7 +50,7 @@ namespace storm { ++numOfDeterministicChoices; } } - + schedulerChoice = choice; } @@ -71,7 +71,7 @@ namespace storm { STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); setChoice(SchedulerChoice(), modelState, memoryState); } - + template SchedulerChoice const& Scheduler::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); @@ -96,17 +96,17 @@ namespace storm { } return result; } - + template bool Scheduler::isPartialScheduler() const { return numOfUndefinedChoices != 0; } - + template bool Scheduler::isDeterministicScheduler() const { return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; } - + template bool Scheduler::isMemorylessScheduler() const { return getNumberOfMemoryStates() == 1; @@ -125,7 +125,7 @@ namespace storm { template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); - + bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling(); bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); @@ -135,7 +135,7 @@ namespace storm { } widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; - + out << "___________________________________________________________________" << std::endl; out << (isPartialScheduler() ? "Partially" : "Fully") << " defined "; out << (isMemorylessScheduler() ? "memoryless " : ""); @@ -146,76 +146,79 @@ namespace storm { out << ":" << std::endl; STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; - for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { - // Check whether the state is skipped - if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { - ++numOfSkippedStatesWithUniqueChoice; - continue; - } - - // Print the state info - if (stateValuationsGiven) { - out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { + std::stringstream stateString; + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + ++numOfSkippedStatesWithUniqueChoice; + continue; + } + + // Print the state info + if (stateValuationsGiven) { + stateString << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + stateString << std::setw(widthOfStates) << state; + } + stateString << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; } else { - out << std::setw(widthOfStates) << state; + stateString << std::setw(widthOfStates) << ""; + stateString << " "; } - out << " "; - - bool firstMemoryState = true; - for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { - // Indent if this is not the first memory state - if (firstMemoryState) { - firstMemoryState = false; + // Print the memory state info + if (!isMemorylessScheduler()) { + stateString << "m" << std::setw(8) << memoryState; + } + + // Print choice info + SchedulerChoice const& choice = schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + if (choice.isDeterministic()) { + if (choiceOriginsGiven) { + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + } else { + stateString << choice.getDeterministicChoice(); + } + if (choiceLabelsGiven) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; + } } else { - out << std::setw(widthOfStates) << ""; - out << " "; - } - // Print the memory state info - if (!isMemorylessScheduler()) { - out << "m" << std::setw(8) << memoryState; - } - - // Print choice info - SchedulerChoice const& choice = schedulerChoices[memoryState][state]; - if (choice.isDefined()) { - if (choice.isDeterministic()) { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + stateString << " + "; + } + stateString << choiceProbPair.second << ": ("; if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + stateString << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); } else { - out << choice.getDeterministicChoice(); + stateString << choiceProbPair.first; } if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - } else { - bool firstChoice = true; - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - if (firstChoice) { - firstChoice = false; - } else { - out << " + "; - } - out << choiceProbPair.second << ": ("; - if (choiceOriginsGiven) { - out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); - } else { - out << choiceProbPair.first; - } - if (choiceLabelsGiven) { - auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); - out << " {" << boost::join(choiceLabels, ", ") << "}"; - } - out << ")"; + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + stateString << " {" << boost::join(choiceLabels, ", ") << "}"; } + stateString << ")"; } - } else { - out << "undefined."; } - - // Todo: print memory updates - out << std::endl; + } else { + if(!printUndefinedChoices) continue; + stateString << "undefined."; } + + // Todo: print memory updates + out << stateString.str(); + out << std::endl; + } } if (numOfSkippedStatesWithUniqueChoice > 0) { out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; @@ -271,10 +274,15 @@ namespace storm { out << output.dump(4); } + template + void Scheduler::setPrintUndefinedChoices(bool value) { + printUndefinedChoices = value; + } + template class Scheduler; template class Scheduler; template class Scheduler; template class Scheduler; - + } } diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 492a7a2f3..43c7bb1cb 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -1,14 +1,15 @@ #pragma once #include +#include + #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/SchedulerChoice.h" namespace storm { - - namespace storage { - + template + class PostScheduler; /* * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). @@ -17,7 +18,8 @@ namespace storm { template class Scheduler { public: - + friend class PostScheduler; + /*! * Initializes a scheduler for the given number of model states. * @@ -26,7 +28,7 @@ namespace storm { */ Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); - + /*! * Sets the choice defined by the scheduler for the given state. * @@ -40,7 +42,7 @@ namespace storm { * Is the scheduler defined on the states indicated by the selected-states bitvector? */ bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const; - + /*! * Clears the choice defined by the scheduler for the given state. * @@ -48,7 +50,7 @@ namespace storm { * @param memoryState The state of the memoryStructure for which to clear the choice. */ void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); - + /*! * Gets the choice defined by the scheduler for the given model and memory state. * @@ -66,22 +68,22 @@ namespace storm { * Retrieves whether there is a pair of model and memory state for which the choice is undefined. */ bool isPartialScheduler() const; - + /*! * Retrieves whether all defined choices are deterministic */ bool isDeterministicScheduler() const; - + /*! * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) */ bool isMemorylessScheduler() const; - + /*! * Retrieves the number of memory states this scheduler considers. */ uint_fast64_t getNumberOfMemoryStates() const; - + /*! * Retrieves the memory structure associated with this scheduler */ @@ -101,7 +103,7 @@ namespace storm { } return newScheduler; } - + /*! * Prints the scheduler to the given output stream. * @param out The output stream @@ -111,19 +113,22 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; - + /*! * Prints the scheduler in json format to the given output stream. */ void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; - - private: - + + void setPrintUndefinedChoices(bool value = true); + + protected: + boost::optional memoryStructure; std::vector>> schedulerChoices; + + bool printUndefinedChoices = false; uint_fast64_t numOfUndefinedChoices; uint_fast64_t numOfDeterministicChoices; }; } } - diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 84b8fa306..7f2e7e1d6 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1753,7 +1753,7 @@ namespace storm { #endif template - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == OptimizationDirection::Minimize) { multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); @@ -1771,7 +1771,7 @@ namespace storm { template template - void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; auto elementIt = this->begin(); auto rowGroupIt = rowGroupIndices.begin(); @@ -1862,13 +1862,13 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif template - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == storm::OptimizationDirection::Minimize) { multiplyAndReduceBackward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); @@ -1886,7 +1886,7 @@ namespace storm { template template - void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; auto elementIt = this->end() - 1; auto rowGroupIt = rowGroupIndices.end() - 2; @@ -1972,7 +1972,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif @@ -1985,7 +1985,7 @@ namespace storm { typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices), dirOverride(dirOverride) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -2092,7 +2092,7 @@ namespace storm { }; template - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == storm::OptimizationDirection::Minimize) { tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride)); @@ -2110,14 +2110,14 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif #endif template - void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { // If the vector and the result are aliases, we need and temporary vector. std::vector* target; diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 8346e5554..0043f5c01 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -35,19 +35,19 @@ namespace storm { namespace storm { namespace storage { - + // Forward declare matrix class. template class SparseMatrix; - + typedef uint_fast64_t SparseMatrixIndexType; - + template class MatrixEntry { public: typedef IndexType index_type; typedef ValueType value_type; - + /*! * Constructs a matrix entry with the given column and value. * @@ -55,14 +55,14 @@ namespace storm { * @param value The value of the matrix entry. */ MatrixEntry(index_type column, value_type value); - + /*! * Move-constructs the matrix entry fro the given column-value pair. * * @param pair The column-value pair from which to move-construct the matrix entry. */ MatrixEntry(std::pair&& pair); - + MatrixEntry() = default; MatrixEntry(MatrixEntry const& other) = default; MatrixEntry& operator=(MatrixEntry const& other) = default; @@ -70,59 +70,59 @@ namespace storm { MatrixEntry(MatrixEntry&& other) = default; MatrixEntry& operator=(MatrixEntry&& other) = default; #endif - + /*! * Retrieves the column of the matrix entry. * * @return The column of the matrix entry. */ index_type const& getColumn() const; - + /*! * Sets the column of the current entry. * * @param column The column to set for this entry. */ void setColumn(index_type const& column); - + /*! * Retrieves the value of the matrix entry. * * @return The value of the matrix entry. */ value_type const& getValue() const; - + /*! * Sets the value of the entry in the matrix. * * @param value The value that is to be set for this entry. */ void setValue(value_type const& value); - + /*! * Retrieves a pair of column and value that characterizes this entry. * * @return A column-value pair that characterizes this entry. */ std::pair const& getColumnValuePair() const; - + /*! * Multiplies the entry with the given factor and returns the result. * * @param factor The factor with which to multiply the entry. */ MatrixEntry operator*(value_type factor) const; - + bool operator==(MatrixEntry const& other) const; bool operator!=(MatrixEntry const& other) const; - + template friend std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); private: // The actual matrix entry. std::pair entry; }; - + /*! * Computes the hash value of a matrix entry. */ @@ -133,7 +133,7 @@ namespace storm { boost::hash_combine(seed, matrixEntry.getValue()); return seed; } - + /*! * A class that can be used to build a sparse matrix by adding value by value. */ @@ -142,7 +142,7 @@ namespace storm { public: typedef SparseMatrixIndexType index_type; typedef ValueType value_type; - + /*! * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. * The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are @@ -159,7 +159,7 @@ namespace storm { * has a custom row grouping. */ SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0); - + /*! * Moves the contents of the given matrix into the matrix builder so that its contents can be modified again. * This is, for example, useful if rows need to be added to the matrix. @@ -167,7 +167,7 @@ namespace storm { * @param matrix The matrix that is to be made editable again. */ SparseMatrixBuilder(SparseMatrix&& matrix); - + /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, * a call to finalize(false) is mandatory. @@ -182,7 +182,7 @@ namespace storm { * @param value The value that is to be set at the specified row and column. */ void addNextValue(index_type row, index_type column, value_type const& value); - + /*! * Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row * group are added. @@ -190,7 +190,7 @@ namespace storm { * @param startingRow The starting row of the new row group. */ void newRowGroup(index_type startingRow); - + /* * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix * may now be used. This must be called after all entries have been added to the matrix via addNextValue. @@ -211,10 +211,10 @@ namespace storm { * groups added this way will be empty. */ SparseMatrix build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0); - + /*! * Retrieves the most recently used row. - * + * * @return The most recently used row. */ index_type getLastRow() const; @@ -232,7 +232,7 @@ namespace storm { * @return The most recently used row. */ index_type getLastColumn() const; - + /*! * Replaces all columns with id > offset according to replacements. * Every state with id offset+i is replaced by the id in replacements[i]. @@ -242,7 +242,7 @@ namespace storm { * @param offset Offset to add to each id in vector index. */ void replaceColumns(std::vector const& replacements, index_type offset); - + /*! * Makes sure that a diagonal entry will be inserted at the given row. * All other entries of this row must be set immediately after calling this (without setting values at other rows in between) @@ -251,72 +251,72 @@ namespace storm { * If addNextValue is called on the given row and the diagonal column, we take the sum of the two values provided to addDiagonalEntry and addNextValue */ void addDiagonalEntry(index_type row, ValueType const& value); - + private: // A flag indicating whether a row count was set upon construction. bool initialRowCountSet; - + // The row count that was initially set (if any). index_type initialRowCount; - + // A flag indicating whether a column count was set upon construction. bool initialColumnCountSet; // The column count that was initially set (if any). index_type initialColumnCount; - + // A flag indicating whether an entry count was set upon construction. bool initialEntryCountSet; - + // The number of entries in the matrix. index_type initialEntryCount; - + // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix. bool forceInitialDimensions; - + // A flag indicating whether the builder is to construct a custom row grouping for the matrix. bool hasCustomRowGrouping; - + // A flag indicating whether the number of row groups was set upon construction. bool initialRowGroupCountSet; - + // The number of row groups in the matrix. index_type initialRowGroupCount; - + // The vector that stores the row-group indices (if they are non-trivial). boost::optional> rowGroupIndices; - + // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; - + // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; - + // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix // with preallocated storage. index_type currentEntryCount; - + // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a // matrix. index_type lastRow; - + // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an // entry into a matrix. index_type lastColumn; - + // Stores the highest column at which an entry was inserted into the matrix. index_type highestColumn; - + // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroupCount; - + boost::optional pendingDiagonalEntry; }; - + /*! * A class that holds a possibly non-square matrix in the compressed row storage format. That is, it is supposed * to store non-zero entries only, but zeros may be explicitly stored if necessary for certain operations. @@ -340,12 +340,12 @@ namespace storm { friend class storm::adapters::StormAdapter; friend class storm::solver::TopologicalCudaValueIterationMinMaxLinearEquationSolver; friend class SparseMatrixBuilder; - + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; typedef typename std::vector>::iterator iterator; typedef typename std::vector>::const_iterator const_iterator; - + /*! * This class represents a number of consecutive rows of the matrix. */ @@ -359,32 +359,32 @@ namespace storm { * @param entryCount The number of entrys in the rows. */ rows(iterator begin, index_type entryCount); - + /*! * Retrieves an iterator that points to the beginning of the rows. * * @return An iterator that points to the beginning of the rows. */ iterator begin(); - + /*! * Retrieves an iterator that points past the last entry of the rows. * * @return An iterator that points past the last entry of the rows. */ iterator end(); - + /*! * Retrieves the number of entries in the rows. * * @return The number of entries in the rows. */ index_type getNumberOfEntries() const; - + private: // The pointer to the columnd and value of the first entry. iterator beginIterator; - + // The number of non-zero entries in the rows. index_type entryCount; }; @@ -402,55 +402,55 @@ namespace storm { * @param entryCount The number of entrys in the rows. */ const_rows(const_iterator begin, index_type entryCount); - + /*! * Retrieves an iterator that points to the beginning of the rows. * * @return An iterator that points to the beginning of the rows. */ const_iterator begin() const; - + /*! * Retrieves an iterator that points past the last entry of the rows. * * @return An iterator that points past the last entry of the rows. */ const_iterator end() const; - + /*! * Retrieves the number of entries in the rows. * * @return The number of entries in the rows. */ index_type getNumberOfEntries() const; - + private: // The pointer to the column and value of the first entry. const_iterator beginIterator; - + // The number of non-zero entries in the rows. index_type entryCount; }; - + /*! * An enum representing the internal state of the matrix. After creation, the matrix is UNINITIALIZED. * Only after a call to finalize(), the status of the matrix is set to INITIALIZED and the matrix can be * used. */ enum MatrixStatus { UNINITIALIZED, INITIALIZED }; - + /*! * Constructs an empty sparse matrix. */ SparseMatrix(); - + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * * @param other The matrix from which to copy the content. */ SparseMatrix(SparseMatrix const& other); - + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * @@ -459,14 +459,14 @@ namespace storm { * exist in the original matrix, they are inserted and set to value zero. */ SparseMatrix(SparseMatrix const& other, bool insertDiagonalElements); - + /*! * Constructs a sparse matrix by moving the contents of the given matrix to the newly created one. * * @param other The matrix from which to move the content. */ SparseMatrix(SparseMatrix&& other); - + /*! * Constructs a sparse matrix by copying the given contents. * @@ -476,7 +476,7 @@ namespace storm { * @param rowGroupIndices The vector representing the row groups in the matrix. */ SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, boost::optional> const& rowGroupIndices); - + /*! * Constructs a sparse matrix by moving the given contents. * @@ -493,14 +493,14 @@ namespace storm { * @param other The matrix from which to copy-assign. */ SparseMatrix& operator=(SparseMatrix const& other); - + /*! * Assigns the contents of the given matrix to the current one by moving its contents. * * @param other The matrix from which to move to contents. */ SparseMatrix& operator=(SparseMatrix&& other); - + /*! * Determines whether the current and the given matrix are semantically equal. * @@ -508,28 +508,28 @@ namespace storm { * @return True iff the given matrix is semantically equal to the current one. */ bool operator==(SparseMatrix const& other) const; - + /*! * Returns the number of rows of the matrix. * * @return The number of rows of the matrix. */ index_type getRowCount() const; - + /*! * Returns the number of columns of the matrix. * * @return The number of columns of the matrix. */ index_type getColumnCount() const; - + /*! * Returns the number of entries in the matrix. * * @return The number of entries in the matrix. */ index_type getEntryCount() const; - + /*! * Returns the number of entries in the given row group of the matrix. * @@ -550,7 +550,7 @@ namespace storm { * Recompute the nonzero entry count */ void updateNonzeroEntryCount() const; - + /*! * Recomputes the number of columns and the number of non-zero entries. */ @@ -562,14 +562,14 @@ namespace storm { * @param difference Difference between old and new nonzero entry count. */ void updateNonzeroEntryCount(std::make_signed::type difference); - + /*! * Returns the number of row groups in the matrix. * * @return The number of row groups in the matrix. */ index_type getRowGroupCount() const; - + /*! * Returns the size of the given row group. * @@ -577,31 +577,31 @@ namespace storm { * @return The number of rows that belong to the given row group. */ index_type getRowGroupSize(index_type group) const; - + /*! * Returns the size of the largest row group of the matrix */ index_type getSizeOfLargestRowGroup() const; - + /*! * Returns the total number of rows that are in one of the specified row groups. */ index_type getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const; - + /*! * Returns the grouping of rows of this matrix. * * @return The grouping of rows of this matrix. */ std::vector const& getRowGroupIndices() const; - + /*! * Swaps the grouping of rows of this matrix. * * @return The old grouping of rows of this matrix. */ std::vector swapRowGroupIndices(std::vector&& newRowGrouping); - + /*! * Sets the row grouping to the given one. * @note It is assumed that the new row grouping is non-trivial. @@ -609,14 +609,14 @@ namespace storm { * @param newRowGroupIndices The new row group indices. */ void setRowGroupIndices(std::vector const& newRowGroupIndices); - + /*! * Retrieves whether the matrix has a trivial row grouping. * * @return True iff the matrix has a trivial row grouping. */ bool hasTrivialRowGrouping() const; - + /*! * Makes the row grouping of this matrix trivial. * Has no effect when the row grouping is already trivial. @@ -630,7 +630,7 @@ namespace storm { * @return a bit vector that is true at position i iff the row group of row i is selected. */ storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint) const; - + /*! * Returns the indices of all rows that * * are in a selected group and @@ -641,7 +641,7 @@ namespace storm { * @return a bit vector that is true at position i iff row i satisfies the constraints. */ storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const; - + /*! * Returns the indices of all row groups selected by the row constraints * @@ -650,21 +650,21 @@ namespace storm { * @return a bit vector that is true at position i iff row i satisfies the constraints. */ storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const; - + /*! * This function makes the given rows absorbing. * * @param rows A bit vector indicating which rows are to be made absorbing. */ void makeRowsAbsorbing(storm::storage::BitVector const& rows); - + /*! * This function makes the groups of rows given by the bit vector absorbing. * * @param rowGroupConstraint A bit vector indicating which row groups to make absorbing. */ void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint); - + /*! * This function makes the given row Dirac. This means that all entries will be set to 0 except the one * at the specified column, which is set to 1 instead. @@ -673,14 +673,14 @@ namespace storm { * @param column The index of the column whose value is to be set to 1. */ void makeRowDirac(index_type row, index_type column); - + /* * Sums the entries in all rows. * * @return The vector of sums of the entries in the respective rows. */ std::vector getRowSumVector() const; - + /* * Sums the entries in the given row and columns. * @@ -689,7 +689,7 @@ namespace storm { * @return The sum of the entries in the given row and columns. */ value_type getConstrainedRowSum(index_type row, storm::storage::BitVector const& columns) const; - + /*! * Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those * entries are added that are in selected columns. @@ -700,7 +700,7 @@ namespace storm { * @return A vector whose elements are the sums of the selected columns in each row. */ std::vector getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; - + /*! * Computes a vector whose entries represent the sums of selected columns for all rows in selected row * groups. @@ -711,7 +711,7 @@ namespace storm { * groups. */ std::vector getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; - + /*! * Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not * set to one in the given bit vector. @@ -728,10 +728,10 @@ namespace storm { * by the constraints are kept and all others are dropped. */ SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const; - + /*! - * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. - * + * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. + * * @param rowsToKeep A bit vector indicating which rows to keep. * @param allowEmptyRowGroups if set to true, the result can potentially have empty row groups. * Otherwise, it is asserted that there are no empty row groups. @@ -757,7 +757,7 @@ namespace storm { * @param rowFilter the selected rows */ SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; - + /*! * Removes all zero entries from this. */ @@ -770,19 +770,19 @@ namespace storm { * @return True if the rows have identical entries. */ bool compareRows(index_type i1, index_type i2) const; - + /*! * Finds duplicate rows in a rowgroup. */ BitVector duplicateRowsInRowgroups() const; - + /** * Swaps the two rows. * @param row1 Index of first row * @param row2 Index of second row */ void swapRows(index_type const& row1, index_type const& row2); - + /*! * Selects exactly one row from each row group of this matrix and returns the resulting matrix. * @@ -791,7 +791,7 @@ namespace storm { * @return A submatrix of the current matrix by selecting one row out of each row group. */ SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; - + /*! * Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily often and with an arbitrary order * The resulting matrix will have a trivial row grouping. @@ -802,7 +802,7 @@ namespace storm { * @return A matrix which rows are selected from this matrix according to the given index sequence */ SparseMatrix selectRowsFromRowIndexSequence(std::vector const& rowIndexSequence, bool insertDiagonalEntries = true) const; - + /*! * Transposes the matrix. * @@ -812,7 +812,7 @@ namespace storm { * @return A sparse matrix that represents the transpose of this matrix. */ storm::storage::SparseMatrix transpose(bool joinGroups = false, bool keepZeros = false) const; - + /*! * Transposes the matrix w.r.t. the selected rows. * This is equivalent to selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros) but avoids creating one intermediate matrix. @@ -822,7 +822,7 @@ namespace storm { * */ SparseMatrix transposeSelectedRowsFromRowGroups(std::vector const& rowGroupChoices, bool keepZeros = false) const; - + /*! * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). */ @@ -833,24 +833,24 @@ namespace storm { * Requires the matrix to contain each diagonal entry and to be square. */ void invertDiagonal(); - + /*! * Negates (w.r.t. addition) all entries that are not on the diagonal. */ void negateAllNonDiagonalEntries(); - + /*! * Sets all diagonal elements to zero. */ void deleteDiagonalEntries(); - + /*! * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. * * @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal D^-1 (as a vector). */ std::pair, std::vector> getJacobiDecomposition() const; - + /*! * Performs a pointwise multiplication of the entries in the given row of this matrix and the entries of * the given row of the other matrix and returns the sum. @@ -862,8 +862,8 @@ namespace storm { */ template ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix const& otherMatrix, index_type const& row) const; - - + + /*! * Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector * containing the sum of the entries in each row of the resulting matrix. @@ -876,7 +876,7 @@ namespace storm { */ template std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - + /*! * Multiplies the matrix with the given vector and writes the result to the given result vector. * @@ -886,13 +886,13 @@ namespace storm { * @return The product of the matrix and the given vector as the content of the given result vector. */ void multiplyWithVector(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; - + void multiplyWithVectorForward(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; void multiplyWithVectorBackward(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; #ifdef STORM_HAVE_INTELTBB void multiplyWithVectorParallel(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; #endif - + /*! * Multiplies the matrix with the given vector, reduces it according to the given direction and and writes * the result to the given result vector. @@ -907,19 +907,19 @@ namespace storm { * the 'new' choice has a value strictly better (wrt. to the optimization direction) value. * @return The resulting vector the content of the given result vector. */ - void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; - void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; - void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; #ifdef STORM_HAVE_INTELTBB - void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; #endif /*! @@ -937,11 +937,11 @@ namespace storm { * @param vector The vector with which the matrix is to be multiplied. This vector is interpreted as being * a row vector. * @param result The vector that is supposed to hold the result of the multiplication after the operation. - * @return The product of the matrix and the given vector as the content of the given result vector. The + * @return The product of the matrix and the given vector as the content of the given result vector. The * result is to be interpreted as a row vector. */ void multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const; - + /*! * Scales each row of the matrix, i.e., multiplies each element in row i with factors[i] * @@ -955,7 +955,7 @@ namespace storm { * @param divisors The divisors with which each row is divided. */ void divideRowsInPlace(std::vector const& divisors); - + /*! * Performs one step of the successive over-relaxation technique. * @@ -975,7 +975,7 @@ namespace storm { * @param result The vector to which to write the result. */ void performWalkerChaeStep(std::vector const& x, std::vector const& columnSums, std::vector const& b, std::vector const& ax, std::vector& result) const; - + /*! * Computes the sum of the entries in a given row. * @@ -983,21 +983,21 @@ namespace storm { * @return The sum of the selected row. */ value_type getRowSum(index_type row) const; - + /*! * Returns the number of non-constant entries */ index_type getNonconstantEntryCount() const; - + /*! * Returns the number of rowGroups that contain a non-constant value */ index_type getNonconstantRowGroupCount() const; - + /*! * Checks for each row whether it sums to one. */ - bool isProbabilistic() const; + bool isProbabilistic() const; /*! * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix * of B if B has no entries in position where A has none. Additionally, the matrices must be of equal size. @@ -1007,10 +1007,10 @@ namespace storm { */ template bool isSubmatrixOf(SparseMatrix const& matrix) const; - + // Returns true if the matrix is the identity matrix bool isIdentityMatrix() const; - + template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); @@ -1018,7 +1018,7 @@ namespace storm { * Returns a string describing the dimensions of the matrix. */ std::string getDimensionsAsString() const; - + /*! * Prints the matrix in a dense format, as also used by e.g. Matlab. * Notice that the format does not support multiple rows in a rowgroup. @@ -1026,14 +1026,14 @@ namespace storm { * @out The stream to output to. */ void printAsMatlabMatrix(std::ostream& out) const; - + /*! * Calculates a hash value over all values contained in the matrix. * * @return size_t A hash value for this matrix. */ std::size_t hash() const; - + /*! * Returns an object representing the consecutive rows given by the parameters. * @@ -1067,7 +1067,7 @@ namespace storm { * @return An object representing the given row. */ rows getRow(index_type row); - + /*! * Returns an object representing the offset'th row in the rowgroup * @param rowGroup the row group @@ -1075,7 +1075,7 @@ namespace storm { * @return An object representing the given row. */ const_rows getRow(index_type rowGroup, index_type offset) const; - + /*! * Returns an object representing the offset'th row in the rowgroup * @param rowGroup the row group @@ -1083,7 +1083,7 @@ namespace storm { * @return An object representing the given row. */ rows getRow(index_type rowGroup, index_type offset); - + /*! * Returns an object representing the given row group. * @@ -1091,7 +1091,7 @@ namespace storm { * @return An object representing the given row group. */ const_rows getRowGroup(index_type rowGroup) const; - + /*! * Returns an object representing the given row group. * @@ -1099,7 +1099,7 @@ namespace storm { * @return An object representing the given row group. */ rows getRowGroup(index_type rowGroup); - + /*! * Retrieves an iterator that points to the beginning of the given row. * @@ -1107,7 +1107,7 @@ namespace storm { * @return An iterator that points to the beginning of the given row. */ const_iterator begin(index_type row = 0) const; - + /*! * Retrieves an iterator that points to the beginning of the given row. * @@ -1115,7 +1115,7 @@ namespace storm { * @return An iterator that points to the beginning of the given row. */ iterator begin(index_type row = 0); - + /*! * Retrieves an iterator that points past the end of the given row. * @@ -1138,14 +1138,14 @@ namespace storm { * @return An iterator that points past the end of the last row of the matrix. */ const_iterator end() const; - + /*! * Retrieves an iterator that points past the end of the last row of the matrix. * * @return An iterator that points past the end of the last row of the matrix. */ iterator end(); - + /*! * Returns a copy of the matrix with the chosen internal data type */ @@ -1163,7 +1163,7 @@ namespace storm { return SparseMatrix(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices)); } - + private: /*! * Creates a submatrix of the current matrix by keeping only row groups and columns in the given row group @@ -1178,39 +1178,39 @@ namespace storm { * given by the row group constraint are kept and all others are dropped. */ SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const; - + // The number of rows of the matrix. index_type rowCount; - + // The number of columns of the matrix. mutable index_type columnCount; - + // The number of entries in the matrix. index_type entryCount; - + // The number of nonzero entries in the matrix. mutable index_type nonzeroEntryCount; - + // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; - + // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; - + // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet // there may be row group indices, because they were requested from the outside. bool trivialRowGrouping; - + // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly. mutable boost::optional> rowGroupIndices; }; - + #ifdef STORM_HAVE_CARL std::set getVariables(SparseMatrix const& matrix); #endif - + } // namespace storage } // namespace storm diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index add01f24d..1f13eb1f1 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -2,18 +2,18 @@ namespace storm { namespace jani { - + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << *fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; } - - Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) { + + Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::shared_ptr const& shieldingExpression, std::string const& comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { // Intentionally left empty. } - - Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment) - : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants) { + + Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::shared_ptr const& shieldingExpression, std::string const& comment) + : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { // Intentionally left empty. } @@ -24,7 +24,7 @@ namespace storm { std::string const& Property::getComment() const { return this->comment; } - + std::string Property::asPrismSyntax() const { std::stringstream stream; if (!this->getName().empty()) { @@ -41,13 +41,13 @@ namespace storm { stream << ")"; } stream << ";"; - + if (!this->getComment().empty()) { stream << " // " << this->getComment(); } return stream.str(); } - + Property Property::substitute(std::map const& substitution) const { std::set remainingUndefinedConstants; for (auto const& constant : undefinedConstants) { @@ -55,52 +55,61 @@ namespace storm { remainingUndefinedConstants.insert(constant); } } - return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, comment); + return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, getShieldingExpression(), comment); } - + Property Property::substitute(std::function const& substitutionFunction) const { std::set remainingUndefinedConstants; for (auto const& constant : undefinedConstants) { substitutionFunction(constant.getExpression()).getBaseExpression().gatherVariables(remainingUndefinedConstants); } - return Property(name, filterExpression.substitute(substitutionFunction), remainingUndefinedConstants, comment); + return Property(name, filterExpression.substitute(substitutionFunction), remainingUndefinedConstants, getShieldingExpression(), comment); } - + Property Property::substituteLabels(std::map const& substitution) const { - return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment); + return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, getShieldingExpression(), comment); } - + Property Property::substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { - return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, comment); + return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, getShieldingExpression(), comment); } - + Property Property::clone() const { - return Property(name, filterExpression.clone(), undefinedConstants, comment); + return Property(name, filterExpression.clone(), undefinedConstants, getShieldingExpression(), comment); } - + FilterExpression const& Property::getFilter() const { return this->filterExpression; } - + std::shared_ptr Property::getRawFormula() const { return this->filterExpression.getFormula(); } - + + bool Property::isShieldingProperty() const { + return shieldingExpression != boost::none && shieldingExpression.get() != nullptr; + } + + std::shared_ptr Property::getShieldingExpression() const { + if(!isShieldingProperty()) return nullptr; + return shieldingExpression.get(); + } + std::set const& Property::getUndefinedConstants() const { return undefinedConstants; } - + bool Property::containsUndefinedConstants() const { return !undefinedConstants.empty(); } - + std::set Property::getUsedVariablesAndConstants() const { auto res = getUndefinedConstants(); getFilter().getFormula()->gatherUsedVariables(res); getFilter().getStatesFormula()->gatherUsedVariables(res); return res; } - + std::set Property::getUsedLabels() const { std::set res; auto labFormSet = getFilter().getFormula()->getAtomicLabelFormulas(); @@ -113,15 +122,15 @@ namespace storm { } return res; } - + void Property::gatherReferencedRewardModels(std::set& rewardModelNames) const { getFilter().getFormula()->gatherReferencedRewardModels(rewardModelNames); getFilter().getStatesFormula()->gatherReferencedRewardModels(rewardModelNames); } - + std::ostream& operator<<(std::ostream& os, Property const& p) { return os << "(" << p.getName() << "): " << p.getFilter(); } - + } } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 757db04a8..4f3805afe 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -2,19 +2,22 @@ #include +#include + #include "storm/modelchecker/results/FilterType.h" #include "storm/logic/Formulas.h" #include "storm/logic/FragmentSpecification.h" #include "storm/logic/CloneVisitor.h" +#include "storm/logic/ShieldExpression.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace jani { - + /** - * Property intervals as per Jani Specification. + * Property intervals as per Jani Specification. * Currently mainly used to help parsing. */ struct PropertyInterval { @@ -22,29 +25,29 @@ namespace storm { bool lowerBoundStrict = false; storm::expressions::Expression upperBound; bool upperBoundStrict = false; - + bool hasLowerBound() const { return lowerBound.isInitialized(); } - + bool hasUpperBound() const { return upperBound.isInitialized(); } }; - - + + class FilterExpression { public: FilterExpression() = default; - + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr const& statesFormula = std::make_shared("init")) : formula(formula), ft(ft), statesFormula(statesFormula) { STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula."); } - + std::shared_ptr const& getFormula() const { return formula; } - + std::shared_ptr const& getStatesFormula() const { return statesFormula; } @@ -52,104 +55,111 @@ namespace storm { storm::modelchecker::FilterType getFilterType() const { return ft; } - + bool isDefault() const { return (ft == storm::modelchecker::FilterType::VALUES) && statesFormula && statesFormula->isInitialFormula(); } - + FilterExpression substitute(std::map const& substitution) const { return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution)); } - + FilterExpression substitute(std::function const& substitutionFunction) const { return FilterExpression(formula->substitute(substitutionFunction), ft, statesFormula->substitute(substitutionFunction)); } - + FilterExpression substituteLabels(std::map const& labelSubstitution) const { return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution)); } - + FilterExpression substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { return FilterExpression(formula->substituteRewardModelNames(rewardModelNameSubstitution), ft, statesFormula->substituteRewardModelNames(rewardModelNameSubstitution)); } - + FilterExpression clone() const { storm::logic::CloneVisitor cv; return FilterExpression(cv.clone(*formula), ft, cv.clone(*statesFormula)); } - + private: // For now, we assume that the states are always the initial states. std::shared_ptr formula; storm::modelchecker::FilterType ft; std::shared_ptr statesFormula; }; - - + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe); - - - + + + class Property { public: Property() = default; - + /** * Constructs the property * @param name the name * @param formula the formula representation * @param undefinedConstants the undefined constants used in the property + * @param shieldingExpression An optional expression for a shield to be created * @param comment An optional comment */ - Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment = ""); - + Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::shared_ptr const& shieldExpression = nullptr, std::string const& comment = ""); + /** * Constructs the property * @param name the name * @param formula the formula representation + * @param shieldingExpression An optional expression for a shield to be created * @param comment An optional comment */ - Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment = ""); - + Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::shared_ptr const& shieldExpression = nullptr, std::string const& comment = ""); + /** * Get the provided name * @return the name */ std::string const& getName() const; - + /** * Get the provided comment, if any * @return the comment */ std::string const& getComment() const; - + Property substitute(std::map const& substitution) const; Property substitute(std::function const& substitutionFunction) const; Property substituteLabels(std::map const& labelSubstitution) const; Property substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const; Property clone() const; - + FilterExpression const& getFilter() const; - + std::string asPrismSyntax() const; - + std::set const& getUndefinedConstants() const; bool containsUndefinedConstants() const; std::set getUsedVariablesAndConstants() const; std::set getUsedLabels() const; void gatherReferencedRewardModels(std::set& rewardModelNames) const; - + std::shared_ptr getRawFormula() const; - + + bool isShieldingProperty() const; + std::shared_ptr getShieldingExpression() const; + private: std::string name; std::string comment; FilterExpression filterExpression; std::set undefinedConstants; + + // TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here. + boost::optional> shieldingExpression = boost::none; }; - - + + std::ostream& operator<<(std::ostream& os, Property const& p); } } - diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index e5fceec44..e0f353b8d 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -24,7 +24,7 @@ namespace storm { namespace storage { template class MatrixEntry; } - + template struct NumberTraits; @@ -35,41 +35,79 @@ namespace storm { struct ElementLess { typedef std::less type; }; - + struct DoubleLess { bool operator()(double a, double b) const { return (a == 0.0 && b > 0.0) || (b - a > 1e-17); } }; - + template<> struct ElementLess { typedef DoubleLess type; }; + template + struct ElementLessEqual { + typedef std::less_equal type; + }; + + struct DoubleLessEqual { + bool operator()(double a, double b) const { + return (a == 0.0 && b >= 0.0) || std::fabs(a - b) < 1e-17 || (b - a >= 1e-17); + } + }; + + template<> + struct ElementLessEqual { + typedef DoubleLessEqual type; + }; + template struct ElementGreater { typedef std::greater type; }; - + struct DoubleGreater { bool operator()(double a, double b) const { return (b == 0.0 && a > 0.0) || (a - b > 1e-17); } }; - + template<> struct ElementGreater { typedef DoubleGreater type; }; + + template + struct ElementGreaterEqual { + typedef std::greater_equal type; + }; + + struct DoubleGreaterEqual { + bool operator()(double a, double b) const { + return (b == 0.0 && a >= 0.0) || std::fabs(a - b) < 1e-17 || (a - b > 1e-17); + } + }; + + template<> + struct ElementGreaterEqual { + typedef DoubleGreaterEqual type; + }; } - + template using ElementLess = typename detail::ElementLess::type; template using ElementGreater = typename detail::ElementGreater::type; + template + using ElementLessEqual = typename detail::ElementLessEqual::type; + + template + using ElementGreaterEqual = typename detail::ElementGreaterEqual::type; + template ValueType one(); @@ -84,7 +122,7 @@ namespace storm { template bool isZero(ValueType const& a); - + template bool isNan(ValueType const& a); @@ -93,7 +131,7 @@ namespace storm { template bool isAlmostOne(ValueType const& a); - + template bool isConstant(ValueType const& a); @@ -105,7 +143,7 @@ namespace storm { template TargetType convertNumber(SourceType const& number); - + template std::pair asFraction(ValueType const& number); @@ -114,28 +152,28 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template std::pair minmax(std::vector const& values); - + template ValueType minimum(std::vector const& values); - + template ValueType maximum(std::vector const& values); - + template< typename K, typename ValueType> std::pair minmax(std::map const& values); - + template< typename K, typename ValueType> ValueType minimum(std::map const& values); - + template ValueType maximum(std::map const& values); - + template ValueType pow(ValueType const& value, int_fast64_t exponent); @@ -147,7 +185,7 @@ namespace storm { template ValueType sqrt(ValueType const& number); - + template ValueType abs(ValueType const& number); @@ -183,7 +221,7 @@ namespace storm { template IntegerType mod(IntegerType const& first, IntegerType const& second); - + template std::string to_string(ValueType const& value); }