diff --git a/CHANGELOG.md b/CHANGELOG.md index 52bebe6e8..b05097073 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,7 @@ Version 1.3.x - Fixed linking with Mathsat on macOS - Fixed compilation for macOS mojave - Support for export of MTBDDs from storm +- Support for monotonicity checking of pMCs using the `--monotonicity-analysis` option. Use `--help monotonicity` for all options. ### Version 1.3.0 (2018/12) - Slightly improved scheduler extraction diff --git a/resources/examples/testfiles/pdtmc/simple1.pm b/resources/examples/testfiles/pdtmc/simple1.pm new file mode 100644 index 000000000..597da690d --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple1.pm @@ -0,0 +1,17 @@ +dtmc + +const double p; + +module test + + // local state + s : [0..4] init 0; + + [] s=0 -> p : (s'=1) + (1-p) : (s'=2); + [] s=1 -> p : (s'=3) + (1-p) : (s'=4); + [] s=2 -> p : (s'=4) + (1-p) : (s'=3); + [] s=3 -> 1 : (s'=3); + [] s=4 -> 1 : (s'=4); + +endmodule + diff --git a/resources/examples/testfiles/pdtmc/simple2.pm b/resources/examples/testfiles/pdtmc/simple2.pm new file mode 100644 index 000000000..33002c6ce --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple2.pm @@ -0,0 +1,17 @@ +dtmc + +const double p; + +module test + + // local state + s : [0..4] init 0; + + [] s=0 -> p : (s'=1) + (1-p) : (s'=2); + [] s=1 -> p : (s'=3) + (1-p) : (s'=4); + [] s=2 -> 0.5*p : (s'=3) + (1-0.5*p) : (s'=4); + [] s=3 -> 1 : (s'=3); + [] s=4 -> 1 : (s'=4); + +endmodule + diff --git a/resources/examples/testfiles/pdtmc/simple3.pm b/resources/examples/testfiles/pdtmc/simple3.pm new file mode 100644 index 000000000..18f515800 --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple3.pm @@ -0,0 +1,18 @@ +dtmc + +const double p; + +module test + + // local state + s : [0..5] init 0; + + [] s=0 -> 0.4*p : (s'=1) + (1-p) : (s'=2) + 0.6*p : (s'=3); + [] s=1 -> 0.5*p : (s'=4) + 0.5*p : (s'=3) + (1-p) : (s'=5); + [] s=2 -> 0.3*p : (s'=4) + (1-0.3*p) : (s'=5); + [] s=3 -> 0.7*p : (s'=4) + (1-0.7*p) : (s'=5); + [] s=4 -> 1 : (s'=4); + [] s=5 -> 1 : (s'=5); + +endmodule + diff --git a/resources/examples/testfiles/pdtmc/simple4.pm b/resources/examples/testfiles/pdtmc/simple4.pm new file mode 100644 index 000000000..1bdc3e004 --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple4.pm @@ -0,0 +1,17 @@ +dtmc + +const double p; + +module test + + // local state + s : [0..4] init 0; + + [] s=0 -> p*(1-p) : (s'=1) + (1-p*(1-p)) : (s'=2); + [] s=1 -> p : (s'=3) + (1-p) : (s'=4); + [] s=2 -> (1-p) : (s'=3) + (p) : (s'=4); + [] s=3 -> 1 : (s'=3); + [] s=4 -> 1 : (s'=4); + +endmodule + diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 47d33c0a1..6613030a2 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -371,7 +371,14 @@ namespace storm { result.second = true; } - if (ioSettings.isToNondeterministicModelSet()) { + 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; } @@ -658,6 +665,14 @@ namespace storm { !storm::transformer::NonMarkovianChainTransformer::preservesFormula(*rawFormula)) { STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states."); ignored = true; + } else if (transformationSettings.isToDiscreteTimeModelSet()) { + auto propertyFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getRawFormula()); + auto filterFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getFilter().getStatesFormula()); + if (propertyFormula && filterFormula) { + result = verificationCallback(propertyFormula, filterFormula); + } else { + ignored = true; + } } else { result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 18b27627d..75dba4492 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -1,35 +1,55 @@ +#include "storm-pars/analysis/MonotonicityChecker.h" + +#include "storm-cli-utilities/cli.h" +#include "storm-cli-utilities/model-handling.h" + #include "storm-pars/api/storm-pars.h" +#include "storm-pars/api/region.h" + +#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h" +#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h" + #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/MonotonicitySettings.h" #include "storm-pars/settings/modules/RegionSettings.h" -#include "storm/settings/SettingsManager.h" +#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + #include "storm/api/storm.h" -#include "storm-cli-utilities/cli.h" -#include "storm-cli-utilities/model-handling.h" + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/NotSupportedException.h" + #include "storm/models/ModelBase.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm/solver/stateelimination/NondeterministicModelStateEliminator.h" + +#include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/SymbolicModelDescription.h" + #include "storm/utility/file.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" -#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h" - #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/BisimulationSettings.h" #include "storm/settings/modules/TransformationSettings.h" -#include "storm/exceptions/BaseException.h" -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace pars { - + typedef typename storm::cli::SymbolicInput SymbolicInput; template @@ -37,11 +57,11 @@ namespace storm { SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) { // Intentionally left empty. } - + bool empty() const { return cartesianProducts.empty(); } - + std::vector::type, std::vector::type>>> cartesianProducts; bool graphPreserving; bool exact; @@ -56,7 +76,7 @@ namespace storm { std::shared_ptr model; boost::optional>> formulas; }; - + template std::vector> parseRegions(std::shared_ptr const& model) { std::vector> result; @@ -66,7 +86,7 @@ namespace storm { } return result; } - + template SampleInformation parseSamples(std::shared_ptr const& model, std::string const& sampleString, bool graphPreserving) { STORM_LOG_THROW(!model || model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models."); @@ -75,7 +95,7 @@ namespace storm { if (sampleString.empty()) { return sampleInfo; } - + // Get all parameters from the model. std::set::type> modelParameters; auto const& sparseModel = *model->as>(); @@ -87,14 +107,14 @@ namespace storm { boost::split(cartesianProducts, sampleString, boost::is_any_of(";")); for (auto& product : cartesianProducts) { boost::trim(product); - + // Get the values string for each variable. std::vector valuesForVariables; boost::split(valuesForVariables, product, boost::is_any_of(",")); for (auto& values : valuesForVariables) { boost::trim(values); } - + std::set::type> encounteredParameters; sampleInfo.cartesianProducts.emplace_back(); auto& newCartesianProduct = sampleInfo.cartesianProducts.back(); @@ -105,7 +125,7 @@ namespace storm { boost::trim(variableName); std::string values = varValues.substr(equalsPosition + 1); boost::trim(values); - + bool foundParameter = false; typename utility::parametric::VariableType::type theParameter; for (auto const& parameter : modelParameters) { @@ -118,39 +138,39 @@ namespace storm { } } STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'."); - + std::vector splitValues; boost::split(splitValues, values, boost::is_any_of(":")); STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter."); - + auto& list = newCartesianProduct[theParameter]; - + for (auto& value : splitValues) { boost::trim(value); list.push_back(storm::utility::convertNumber::type>(value)); } } - + STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples."); } - + return sampleInfo; } - + template PreprocessResult preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); auto transformationSettings = storm::settings::getModule(); - + PreprocessResult result(model, false); if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as>()); result.changed = true; } - + if (generalSettings.isBisimulationSet()) { result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as>(), input, bisimulationSettings); result.changed = true; @@ -175,10 +195,10 @@ namespace storm { result.formulas = transformResult.second; result.changed = true; } - + return result; } - + template PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); @@ -207,7 +227,7 @@ namespace storm { } return result; } - + template PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); @@ -219,13 +239,13 @@ namespace storm { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); result = storm::pars::preprocessDdModel(result.model->as>(), input); } - + if (result.changed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; } - + template void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation const* valuation = nullptr) { if (result) { @@ -241,11 +261,11 @@ namespace storm { } ss << entry.first << "=" << entry.second; } - + STORM_PRINT_AND_LOG(" for instance [" << ss.str() << "]"); } STORM_PRINT_AND_LOG(": ") - + auto const* regionCheckResult = dynamic_cast const*>(result.get()); if (regionCheckResult != nullptr) { auto regionSettings = storm::settings::getModule(); @@ -274,7 +294,7 @@ namespace storm { STORM_LOG_ERROR("Property is unsupported by selected engine/settings." << std::endl); } } - + template void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback) { for (auto const& property : properties) { @@ -286,59 +306,59 @@ namespace storm { postprocessingCallback(result); } } - + template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation const& samples) { - + // When samples are provided, we create an instantiation model checker. ModelCheckerType modelchecker(model); - + for (auto const& property : input.properties) { storm::cli::printModelCheckingProperty(property); - + modelchecker.specifyFormula(storm::api::createTask(property.getRawFormula(), true)); modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving); - + storm::utility::parametric::Valuation valuation; - + std::vector::type> parameters; std::vector::type>::const_iterator> iterators; std::vector::type>::const_iterator> iteratorEnds; - + storm::utility::Stopwatch watch(true); for (auto const& product : samples.cartesianProducts) { parameters.clear(); iterators.clear(); iteratorEnds.clear(); - + for (auto const& entry : product) { parameters.push_back(entry.first); iterators.push_back(entry.second.cbegin()); iteratorEnds.push_back(entry.second.cend()); } - + bool done = false; while (!done) { // Read off valuation. for (uint64_t i = 0; i < parameters.size(); ++i) { valuation[parameters[i]] = *iterators[i]; } - + storm::utility::Stopwatch valuationWatch(true); std::unique_ptr result = modelchecker.check(Environment(), valuation); valuationWatch.stop(); - + if (result) { result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); } printInitialStatesResult(result, property, &valuationWatch, &valuation); - + for (uint64_t i = 0; i < parameters.size(); ++i) { ++iterators[i]; if (iterators[i] == iteratorEnds[i]) { // Reset iterator and proceed to move next iterator. iterators[i] = product.at(parameters[i]).cbegin(); - + // If the last iterator was removed, we are done. if (i == parameters.size() - 1) { done = true; @@ -348,15 +368,15 @@ namespace storm { break; } } - + } } - + watch.stop(); STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl); } } - + template void verifyPropertiesAtSamplePoints(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { if (model->isOfType(storm::models::ModelType::Dtmc)) { @@ -369,10 +389,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs."); } } - + template void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { - + if (samples.empty()) { verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { @@ -397,7 +417,7 @@ namespace storm { }); } else { STORM_LOG_TRACE("Sampling the model at given points."); - + if (samples.exact) { verifyPropertiesAtSamplePoints(model, input, samples); } else { @@ -405,7 +425,7 @@ namespace storm { } } } - + template void computeRegionExtremumWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); @@ -438,13 +458,13 @@ namespace storm { template void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); - + auto parametricSettings = storm::settings::getModule(); auto regionSettings = storm::settings::getModule(); - + std::function(std::shared_ptr const& formula)> verificationCallback; std::function const&)> postprocessingCallback; - + STORM_PRINT_AND_LOG(std::endl); if (regionSettings.isHypothesisSet()) { STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); @@ -458,37 +478,37 @@ namespace storm { } auto engine = regionSettings.getRegionCheckEngine(); STORM_PRINT_AND_LOG(" using " << engine); - + // Check the given set of regions with or without refinement if (regionSettings.isRefineSet()) { STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); - boost::optional optionalDepthLimit; - if (regionSettings.isDepthLimitSet()) { - optionalDepthLimit = regionSettings.getDepthLimit(); - } - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); - return result; - }; + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); + boost::optional optionalDepthLimit; + if (regionSettings.isDepthLimitSet()) { + optionalDepthLimit = regionSettings.getDepthLimit(); + } + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); + return result; + }; } else { STORM_PRINT_AND_LOG("." << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); - return result; - }; + std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); + return result; + }; } - + postprocessingCallback = [&] (std::unique_ptr const& result) { - if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); - } - }; - + if (parametricSettings.exportResultToFile()) { + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + } + }; + verifyProperties(input.properties, verificationCallback, postprocessingCallback); } - + template void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { if (regions.empty()) { @@ -544,7 +564,8 @@ namespace storm { storm::pars::verifyWithDdEngine(model->as>(), input, regions, samples); } } - + + template void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); @@ -552,21 +573,24 @@ namespace storm { auto buildSettings = storm::settings::getModule(); auto parSettings = storm::settings::getModule(); - + auto monSettings = storm::settings::getModule(); + auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); - + std::shared_ptr model; if (!buildSettings.isNoBuildModelSet()) { model = storm::cli::buildModel(engine, input, ioSettings); } - + if (model) { model->printModelInformationToStream(std::cout); } - + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - + + + if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); if (preprocessingResult.changed) { @@ -586,15 +610,154 @@ namespace storm { model->printModelInformationToStream(std::cout); } } - + + if (monSettings.isMonotonicityAnalysisSet()) { + // Simplify the model + storm::utility::Stopwatch simplifyingWatch(true); + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto consideredModel = (model->as>()); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*consideredModel); + + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); + STORM_LOG_THROW(formulas.begin()!=formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported"); + + if (!simplifier.simplify(*(formulas[0]))) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + model = simplifier.getSimplifiedModel(); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + auto consideredModel = (model->as>()); + auto simplifier = storm::transformer::SparseParametricMdpSimplifier>(*consideredModel); + + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); + STORM_LOG_THROW(formulas.begin()!=formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported"); + + if (!simplifier.simplify(*(formulas[0]))) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + model = simplifier.getSimplifiedModel(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); + } + + simplifyingWatch.stop(); + STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl); + model->printModelInformationToStream(std::cout); + } + + if (model) { + auto preprocessingResult = storm::pars::preprocessModel(model, input); + if (preprocessingResult.changed) { + model = preprocessingResult.model; + + if (preprocessingResult.formulas) { + std::vector newProperties; + for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) { + auto formula = preprocessingResult.formulas.get().at(i); + STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); + storm::jani::Property property = input.properties.at(i); + newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); + } + input.properties = newProperties; + } + + model->printModelInformationToStream(std::cout); + } + } + + + if (model && monSettings.isSccEliminationSet()) { + storm::utility::Stopwatch eliminationWatch(true); + if (model->isOfType(storm::models::ModelType::Dtmc)) { + STORM_PRINT("Applying scc elimination" << std::endl); + auto sparseModel = model->as>(); + auto matrix = sparseModel->getTransitionMatrix(); + auto backwardsTransitionMatrix = matrix.transpose(); + + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + + storm::storage::BitVector selectedStates(matrix.getRowCount()); + storm::storage::BitVector selfLoopStates(matrix.getRowCount()); + for (size_t i = 0; i < decomposition.size(); ++i) { + auto scc = decomposition.getBlock(i); + if (scc.size() > 1) { + auto statesScc = scc.getStates(); + std::vector entryStates; + for (auto state : statesScc) { + auto row = backwardsTransitionMatrix.getRow(state); + bool found = false; + for (auto backState : row) { + if (!scc.containsState(backState.getColumn())) { + found = true; + } + } + if (found) { + entryStates.push_back(state); + selfLoopStates.set(state); + } else { + selectedStates.set(state); + } + } + + if (entryStates.size() != 1) { + STORM_LOG_THROW(entryStates.size() > 1, storm::exceptions::NotImplementedException, + "state elimination not implemented for scc with more than 1 entry points"); + } + } + } + + storm::storage::FlexibleSparseMatrix flexibleMatrix(matrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardsTransitionMatrix, true); + auto actionRewards = std::vector(matrix.getRowCount(), storm::utility::zero()); + storm::solver::stateelimination::NondeterministicModelStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards); + for(auto state : selectedStates) { + stateEliminator.eliminateState(state, true); + } + for (auto state : selfLoopStates) { + auto row = flexibleMatrix.getRow(state); + stateEliminator.eliminateLoop(state); + } + selectedStates.complement(); + auto keptRows = matrix.getRowFilter(selectedStates); + storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); + // TODO: note that rewards get lost + model = std::make_shared>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates)); + + eliminationWatch.stop(); + STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl); + model->printModelInformationToStream(std::cout); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Unable to perform SCC elimination for monotonicity analysis on MDP: Not mplemented"); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); + } + + } + std::vector> regions = parseRegions(model); + + if (monSettings.isMonotonicityAnalysisSet()) { + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); + // Monotonicity + storm::utility::Stopwatch monotonicityWatch(true); + + STORM_LOG_THROW(regions.size() <= 1, storm::exceptions::InvalidArgumentException, "Monotonicity analysis only allowed on single region"); + storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, regions, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision()); + monotonicityChecker.checkMonotonicity(); + monotonicityWatch.stop(); + STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl + << std::endl); + return; + } + std::string samplesAsString = parSettings.getSamples(); SampleInformation samples; if (!samplesAsString.empty()) { samples = parseSamples(model, samplesAsString, parSettings.isSamplesAreGraphPreservingSet()); samples.exact = parSettings.isSampleExactSet(); } - + if (model) { storm::cli::exportModel(model, input); } @@ -609,18 +772,18 @@ namespace storm { verifyParametricModel(model, input, regions, samples); } } - + void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); - + auto coreSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); - + processInputWithValueTypeAndDdlib(symbolicInput); } diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp new file mode 100644 index 000000000..fce4596ab --- /dev/null +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -0,0 +1,354 @@ +#include +#include "AssumptionChecker.h" + +#include "storm-pars/utility/ModelInstantiator.h" +#include "storm-pars/analysis/MonotonicityChecker.h" + +#include "storm/environment/Environment.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/modelchecker/CheckTask.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/VariableExpression.h" +#include "storm/storage/expressions/RationalFunctionToExpression.h" +#include "storm/utility/constants.h" + +namespace storm { + namespace analysis { + template + AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, storm::storage::ParameterRegion region, uint_fast64_t numberOfSamples) { + this->formula = formula; + this->matrix = model->getTransitionMatrix(); + this->region = region; + + // Create sample points + auto instantiator = utility::ModelInstantiator, models::sparse::Dtmc>(*model); + auto matrix = model->getTransitionMatrix(); + std::set::type> variables = models::sparse::getProbabilityParameters(*model); + + for (uint_fast64_t i = 0; i < numberOfSamples; ++i) { + auto valuation = utility::parametric::Valuation(); + for (auto var: variables) { + auto lb = region.getLowerBoundary(var.name()); + auto ub = region.getUpperBoundary(var.name()); + // Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub + auto val = + std::pair::type, typename utility::parametric::CoefficientType::type> + (var,utility::convertNumber::type>(lb + i*(ub-lb)/(numberOfSamples-1))); + valuation.insert(val); + } + models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); + auto checker = modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); + checkResult = checker.computeUntilProbabilities(Environment(), checkTask); + } else if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); + checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); + } else { + STORM_LOG_THROW(false, exceptions::NotSupportedException, + "Expecting until or eventually formula"); + } + auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); + std::vector values = quantitativeResult.getValueVector(); + samples.push_back(values); + } + } + + template + AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { + STORM_LOG_THROW(false, exceptions::NotImplementedException, "Assumption checking for mdps not yet implemented"); + this->formula = formula; + this->matrix = model->getTransitionMatrix(); + + // Create sample points + auto instantiator = utility::ModelInstantiator, models::sparse::Mdp>(*model); + auto matrix = model->getTransitionMatrix(); + std::set::type> variables = models::sparse::getProbabilityParameters(*model); + + for (auto i = 0; i < numberOfSamples; ++i) { + auto valuation = utility::parametric::Valuation(); + for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + auto val = std::pair::type, + typename utility::parametric::CoefficientType::type>((*itr), utility::convertNumber::type>(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); + valuation.insert(val); + } + models::sparse::Mdp sampleModel = instantiator.instantiate(valuation); + auto checker = modelchecker::SparseMdpPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); + checkResult = checker.computeUntilProbabilities(Environment(), checkTask); + } else if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); + checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); + } else { + STORM_LOG_THROW(false, exceptions::NotSupportedException, + "Expecting until or eventually formula"); + } + auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); + std::vector values = quantitativeResult.getValueVector(); + samples.push_back(values); + } + } + + template + AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { + auto result = AssumptionStatus::UNKNOWN; + std::set vars = std::set({}); + assumption->gatherVariables(vars); + for (auto itr = samples.begin(); result == AssumptionStatus::UNKNOWN && itr != samples.end(); ++itr) { + std::shared_ptr manager = assumption->getManager().getSharedPointer(); + auto valuation = expressions::SimpleValuation(manager); + auto values = (*itr); + for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) { + expressions::Variable par = *var; + auto index = std::stoi(par.getName()); + valuation.setRationalValue(par, values[index]); + } + assert(assumption->hasBooleanType()); + if (!assumption->evaluateAsBool(&valuation)) { + result = AssumptionStatus::INVALID; + } + } + return result; + } + + template + AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, Order* order) { + // First check if based on sample points the assumption can be discharged + auto result = checkOnSamples(assumption); + assert (result != AssumptionStatus::VALID); + + if (result == AssumptionStatus::UNKNOWN) { + // If result from sample checking was unknown, the assumption might hold, so we continue, + // otherwise we return INVALID + std::set vars = std::set({}); + assumption->gatherVariables(vars); + + STORM_LOG_THROW(assumption->getRelationType() == + expressions::BinaryRelationExpression::RelationType::Greater || + assumption->getRelationType() == + expressions::BinaryRelationExpression::RelationType::Equal, + exceptions::NotSupportedException, + "Only Greater Or Equal assumptions supported"); + + // Row with successors of the first state + auto row1 = matrix.getRow( + std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName())); + // Row with successors of the second state + auto row2 = matrix.getRow( + std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName())); + + if (row1.getNumberOfEntries() == 2 && row2.getNumberOfEntries() == 2) { + // If the states have the same successors for which we know the position in the order + // We can check with a function if the assumption holds + + auto state1succ1 = row1.begin(); + auto state1succ2 = (++row1.begin()); + auto state2succ1 = row2.begin(); + auto state2succ2 = (++row2.begin()); + + if (state1succ1->getColumn() == state2succ2->getColumn() + && state2succ1->getColumn() == state1succ2->getColumn()) { + std::swap(state1succ1, state1succ2); + } + + if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { + if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater + && order->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Order::NodeComparison::UNKNOWN) { + // The assumption should be the greater assumption + // If the result is unknown, we cannot compare, also SMTSolver will not help + result = validateAssumptionSMTSolver(assumption, order); + +// result = validateAssumptionFunction(order, state1succ1, state1succ2, state2succ1, +// state2succ2); + } else if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Equal) { + // The assumption is equal, the successors are the same, + // so if the probability of reaching the successors is the same, we have a valid assumption + if (state1succ1->getValue() == state2succ1->getValue()) { + result = AssumptionStatus::VALID; + } + } else { + result = AssumptionStatus::UNKNOWN; + } + } else { + result = validateAssumptionSMTSolver(assumption, order); + } + } else { + result = validateAssumptionSMTSolver(assumption, order); + } + } + return result; + } + + template + AssumptionStatus AssumptionChecker::validateAssumptionFunction(Order* order, + typename storage::SparseMatrix::iterator state1succ1, + typename storage::SparseMatrix::iterator state1succ2, + typename storage::SparseMatrix::iterator state2succ1, + typename storage::SparseMatrix::iterator state2succ2) { + assert((state1succ1->getColumn() == state2succ1->getColumn() + && state1succ2->getColumn() == state2succ2->getColumn()) + || (state1succ1->getColumn() == state2succ2->getColumn() + && state1succ2->getColumn() == state2succ1->getColumn())); + + AssumptionStatus result; + + // Calculate the difference in probability for the "highest" successor state + ValueType prob; + auto comp = order->compare(state1succ1->getColumn(), state1succ2->getColumn()); + assert (comp == Order::NodeComparison::ABOVE || comp == Order::NodeComparison::BELOW); + if (comp == Order::NodeComparison::ABOVE) { + prob = state1succ1->getValue() - state2succ1->getValue(); + } else if (comp == Order::NodeComparison::BELOW) { + prob = state1succ2->getValue() - state2succ2->getValue(); + } + + auto vars = prob.gatherVariables(); + + // If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions + // This will give the smallest result + std::map::type, typename utility::parametric::CoefficientType::type> substitutions; + for (auto var : vars) { + auto monotonicity = MonotonicityChecker::checkDerivative(prob.derivative(var), region); + if (monotonicity.first) { + // monotone increasing + substitutions[var] = 0; + } else if (monotonicity.second) { + // monotone increasing + substitutions[var] = 1; + } else { + result = AssumptionStatus::UNKNOWN; + } + } + + if (prob.evaluate(substitutions) >= 0) { + result = AssumptionStatus::VALID; + } + return result; + } + + + template + AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(std::shared_ptr assumption, Order* order) { + std::shared_ptr smtSolverFactory = std::make_shared(); + std::shared_ptr manager(new expressions::ExpressionManager()); + + AssumptionStatus result; + auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); + auto var2 = assumption->getSecondOperand()->asVariableExpression().getVariableName(); + auto row1 = matrix.getRow(std::stoi(var1)); + auto row2 = matrix.getRow(std::stoi(var2)); + + bool orderKnown = true; + // Check if the order between the different successors is known + // Also start creating expression for order of states + expressions::Expression exprOrderSucc = manager->boolean(true); + std::set stateVariables; + for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { + auto varname1 = "s" + std::to_string(itr1->getColumn()); + if (!manager->hasVariable(varname1)) { + stateVariables.insert(manager->declareRationalVariable(varname1)); + } + for (auto itr2 = row2.begin(); orderKnown && itr2 != row2.end(); ++itr2) { + if (itr1->getColumn() != itr2->getColumn()) { + auto varname2 = "s" + std::to_string(itr2->getColumn()); + if (!manager->hasVariable(varname2)) { + stateVariables.insert(manager->declareRationalVariable(varname2)); + } + auto comp = order->compare(itr1->getColumn(), itr2->getColumn()); + if (comp == Order::NodeComparison::ABOVE) { + exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= + manager->getVariable(varname2)); + } else if (comp == Order::NodeComparison::BELOW) { + exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= + manager->getVariable(varname2)); + } else if (comp == Order::NodeComparison::SAME) { + exprOrderSucc = exprOrderSucc && + (manager->getVariable(varname1) = manager->getVariable(varname2)); + } else { + orderKnown = false; + } + } + } + } + + if (orderKnown) { + solver::Z3SmtSolver s(*manager); + auto valueTypeToExpression = expressions::RationalFunctionToExpression(manager); + expressions::Expression expr1 = manager->rational(0); + for (auto itr1 = row1.begin(); itr1 != row1.end(); ++itr1) { + expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable("s" + std::to_string(itr1->getColumn()))); + } + + expressions::Expression expr2 = manager->rational(0); + for (auto itr2 = row2.begin(); itr2 != row2.end(); ++itr2) { + expr2 = expr2 + (valueTypeToExpression.toExpression(itr2->getValue()) * manager->getVariable("s" + std::to_string(itr2->getColumn()))); + } + + // Create expression for the assumption based on the relation to successors + // It is the negation of actual assumption + expressions::Expression exprToCheck ; + if (assumption->getRelationType() == + expressions::BinaryRelationExpression::RelationType::Greater) { + exprToCheck = expr1 <= expr2; + } else { + assert (assumption->getRelationType() == + expressions::BinaryRelationExpression::RelationType::Equal); + exprToCheck = expr1 != expr2 ; + } + + auto variables = manager->getVariables(); + // Bounds for the state probabilities and parameters + expressions::Expression exprBounds = manager->boolean(true); + for (auto var : variables) { + if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) { + // the var is a state + exprBounds = exprBounds && manager->rational(0) <= var && var <= manager->rational(1); + } else { + // the var is a parameter + auto lb = storm::utility::convertNumber(region.getLowerBoundary(var.getName())); + auto ub = storm::utility::convertNumber(region.getUpperBoundary(var.getName())); + exprBounds = exprBounds && manager->rational(lb) < var && var < manager->rational(ub); + } + } + + s.add(exprOrderSucc); + s.add(exprBounds); + // assert that sorting of successors in the order and the bounds on the expression are at least satisfiable + assert (s.check() == solver::SmtSolver::CheckResult::Sat); + s.add(exprToCheck); + auto smtRes = s.check(); + if (smtRes == solver::SmtSolver::CheckResult::Unsat) { + // If there is no thing satisfying the negation we are safe. + result = AssumptionStatus::VALID; + } else if (smtRes == solver::SmtSolver::CheckResult::Sat) { + assert (smtRes == solver::SmtSolver::CheckResult::Sat); + result = AssumptionStatus::INVALID; + } else { + result = AssumptionStatus::UNKNOWN; + } + } else { + result = AssumptionStatus::UNKNOWN; + } + + return result; + } + + template class AssumptionChecker; + } +} diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h new file mode 100644 index 000000000..802291291 --- /dev/null +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -0,0 +1,90 @@ +#ifndef STORM_ASSUMPTIONCHECKER_H +#define STORM_ASSUMPTIONCHECKER_H + +#include "storm/logic/Formula.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/environment/Environment.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "Order.h" + +namespace storm { + namespace analysis { + /*! + * Constants for status of assumption + */ + enum AssumptionStatus { + VALID, + INVALID, + UNKNOWN, + }; + template + class AssumptionChecker { + public: + + /*! + * Constructs an AssumptionChecker based on the number of samples, for the given formula and model. + * + * @param formula The formula to check. + * @param model The dtmc model to check the formula on. + * @param numberOfSamples Number of sample points. + */ + AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, storm::storage::ParameterRegion region, uint_fast64_t numberOfSamples); + + /*! + * Constructs an AssumptionChecker based on the number of samples, for the given formula and model. + * + * @param formula The formula to check. + * @param model The mdp model to check the formula on. + * @param numberOfSamples Number of sample points. + */ + AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); + + /*! + * Checks if the assumption holds at the sample points of the AssumptionChecker. + * + * @param assumption The assumption to check. + * @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID + */ + AssumptionStatus checkOnSamples(std::shared_ptr assumption); + + /*! + * Tries to validate an assumption based on the order and underlying transition matrix. + * + * @param assumption The assumption to validate. + * @param order The order. + * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID + */ + AssumptionStatus validateAssumption(std::shared_ptr assumption, Order* order); + + /*! + * Tries to validate an assumption based on the order, and SMT solving techniques + * + * @param assumption The assumption to validate. + * @param order The order. + * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID + */ + AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr assumption, Order* order); + + private: + std::shared_ptr formula; + + storage::SparseMatrix matrix; + + std::vector> samples; + + void createSamples(); + + AssumptionStatus validateAssumptionFunction(Order* order, + typename storage::SparseMatrix::iterator state1succ1, + typename storage::SparseMatrix::iterator state1succ2, + typename storage::SparseMatrix::iterator state2succ1, + typename storage::SparseMatrix::iterator state2succ2); + + storm::storage::ParameterRegion region; + + }; + } +} +#endif //STORM_ASSUMPTIONCHECKER_H diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp new file mode 100644 index 000000000..d889e3f13 --- /dev/null +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -0,0 +1,67 @@ +#include "AssumptionMaker.h" + +namespace storm { + namespace analysis { + typedef std::shared_ptr AssumptionType; + template + AssumptionMaker::AssumptionMaker(AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates, bool validate) { + this->numberOfStates = numberOfStates; + this->assumptionChecker = assumptionChecker; + this->validate = validate; + this->expressionManager = std::make_shared(expressions::ExpressionManager()); + for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { + expressionManager->declareRationalVariable(std::to_string(i)); + } + } + + + template + std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order) { + std::map, AssumptionStatus> result; + + expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); + expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); + std::shared_ptr assumption1 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), + expressions::BinaryRelationExpression::RelationType::Greater)); + AssumptionStatus result1; + AssumptionStatus result2; + AssumptionStatus result3; + if (validate) { + result1 = assumptionChecker->validateAssumption(assumption1, order); + } else { + result1 = AssumptionStatus::UNKNOWN; + } + result[assumption1] = result1; + + + std::shared_ptr assumption2 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), + expressions::BinaryRelationExpression::RelationType::Greater)); + + if (validate) { + result2 = assumptionChecker->validateAssumption(assumption2, order); + } else { + result2 = AssumptionStatus::UNKNOWN; + } + result[assumption2] = result2; + + std::shared_ptr assumption3 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), + expressions::BinaryRelationExpression::RelationType::Equal)); + if (validate) { + result3 = assumptionChecker->validateAssumption(assumption3, order); + } else { + result3 = AssumptionStatus::UNKNOWN; + } + result[assumption3] = result3; + + return result; + } + + template class AssumptionMaker; + } +} diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h new file mode 100644 index 000000000..41643fb5a --- /dev/null +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -0,0 +1,51 @@ +#ifndef STORM_ASSUMPTIONMAKER_H +#define STORM_ASSUMPTIONMAKER_H + +#include "AssumptionChecker.h" +#include "Order.h" +#include "OrderExtender.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm-pars/utility/ModelInstantiator.h" + + +namespace storm { + namespace analysis { + + template + class AssumptionMaker { + typedef std::shared_ptr AssumptionType; + public: + /*! + * Constructs AssumptionMaker based on the order extender, the assumption checker and number of states of the mode + * + * @param orderExtender The OrderExtender which needs the assumptions made by the AssumptionMaker. + * @param checker The AssumptionChecker which checks the assumptions at sample points. + * @param numberOfStates The number of states of the model. + */ + AssumptionMaker(AssumptionChecker* checker, uint_fast64_t numberOfStates, bool validate); + + /*! + * Creates assumptions, and checks them if validate in constructor is true. + * Possible results: AssumptionStatus::VALID, AssumptionStatus::INVALID, AssumptionStatus::UNKNOWN + * If validate is false result is always AssumptionStatus::UNKNOWN + * + * @param val1 First state number + * @param val2 Second state number + * @param order The order on which the assumptions are checked + * @return Map with three assumptions, and the validation + */ + std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order); + + private: + AssumptionChecker* assumptionChecker; + + std::shared_ptr expressionManager; + + uint_fast64_t numberOfStates; + + bool validate; + }; + } +} +#endif //STORM_ASSUMPTIONMAKER_H + diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp new file mode 100644 index 000000000..c53609220 --- /dev/null +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -0,0 +1,692 @@ +#include "MonotonicityChecker.h" +#include "storm-pars/analysis/AssumptionMaker.h" +#include "storm-pars/analysis/AssumptionChecker.h" +#include "storm-pars/analysis/Order.h" +#include "storm-pars/analysis/OrderExtender.h" + +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/InvalidOperationException.h" + +#include "storm/utility/Stopwatch.h" +#include "storm/models/ModelType.h" + +#include "storm/api/verification.h" +#include "storm-pars/api/storm-pars.h" + +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h" + + + +namespace storm { + namespace analysis { + template + MonotonicityChecker::MonotonicityChecker(std::shared_ptr model, std::vector> formulas, std::vector> regions, bool validate, uint_fast64_t numberOfSamples, double const& precision) { + assert (model != nullptr); + this->model = model; + this->formulas = formulas; + this->validate = validate; + this->precision = precision; + std::shared_ptr> sparseModel = model->as>(); + + if (regions.size() == 1) { + this->region = *(regions.begin()); + } else { + assert (regions.size() == 0); + typename storm::storage::ParameterRegion::Valuation lowerBoundaries; + typename storm::storage::ParameterRegion::Valuation upperBoundaries; + std::set::VariableType> vars; + vars = storm::models::sparse::getProbabilityParameters(*sparseModel); + for (auto var : vars) { + typename storm::storage::ParameterRegion::CoefficientType lb = storm::utility::convertNumber::CoefficientType>(0 + precision); + typename storm::storage::ParameterRegion::CoefficientType ub = storm::utility::convertNumber::CoefficientType>(1 - precision); + lowerBoundaries.insert(std::make_pair(var, lb)); + upperBoundaries.insert(std::make_pair(var, ub)); + } + this->region = storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); + } + + if (numberOfSamples > 0) { + // sampling + if (model->isOfType(storm::models::ModelType::Dtmc)) { + this->resultCheckOnSamples = std::map::type, std::pair>( + checkOnSamples(model->as>(), numberOfSamples)); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + this->resultCheckOnSamples = std::map::type, std::pair>( + checkOnSamples(model->as>(), numberOfSamples)); + + } + checkSamples= true; + } else { + checkSamples= false; + } + + this->extender = new storm::analysis::OrderExtender(sparseModel); + } + + template + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity() { + auto map = createOrder(); + std::shared_ptr> sparseModel = model->as>(); + auto matrix = sparseModel->getTransitionMatrix(); + return checkMonotonicity(map, matrix); + } + + template + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { + storm::utility::Stopwatch monotonicityCheckWatch(true); + std::map::type, std::pair>> result; + + outfile.open(filename, std::ios_base::app); + + if (map.size() == 0) { + // Nothing is known + outfile << " No assumptions -"; + STORM_PRINT("No valid assumptions, couldn't build a sufficient order"); + if (resultCheckOnSamples.size() != 0) { + STORM_PRINT("\n" << "Based results on samples"); + } else { + outfile << " ?"; + } + + for (auto entry : resultCheckOnSamples) { + if (!entry.second.first && ! entry.second.second) { + outfile << " SX " << entry.first << " "; + } else if (entry.second.first && ! entry.second.second) { + outfile << " SI " << entry.first << " "; + } else if (entry.second.first && entry.second.second) { + outfile << " SC " << entry.first << " "; + } else { + outfile << " SD " << entry.first << " "; + } + } + + } else { + size_t i = 0; + for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { + auto order = itr->first; + + auto addedStates = order->getAddedStates()->getNumberOfSetBits(); + assert (addedStates == order->getAddedStates()->size()); + std::map::type, std::pair> varsMonotone = analyseMonotonicity(i, order, + matrix); + + auto assumptions = itr->second; + if (assumptions.size() > 0) { + bool first = true; + for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { + if (!first) { + outfile << (" ^ "); + } else { + first = false; + } + outfile << (*(*itr2)); + } + outfile << " - "; + } else if (assumptions.size() == 0) { + outfile << "No assumptions - "; + } + + if (varsMonotone.size() == 0) { + outfile << "No params"; + } else { + auto itr2 = varsMonotone.begin(); + while (itr2 != varsMonotone.end()) { + if (checkSamples && + resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && + (!resultCheckOnSamples[itr2->first].first && + !resultCheckOnSamples[itr2->first].second)) { + outfile << "X " << itr2->first; + } else { + if (itr2->second.first && itr2->second.second) { + outfile << "C " << itr2->first; + } else if (itr2->second.first) { + outfile << "I " << itr2->first; + } else if (itr2->second.second) { + outfile << "D " << itr2->first; + } else { + outfile << "? " << itr2->first; + } + } + ++itr2; + if (itr2 != varsMonotone.end()) { + outfile << " "; + } + } + result.insert( + std::pair::type, std::pair>>( + order, varsMonotone)); + } + ++i; + outfile << ";"; + } + } + outfile << ", "; + + monotonicityCheckWatch.stop(); + outfile.close(); + return result; + } + + template + std::map>> MonotonicityChecker::createOrder() { + // Transform to Orders + storm::utility::Stopwatch orderWatch(true); + + // Use parameter lifting modelchecker to get initial min/max values for order creation + storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> plaModelChecker; + std::unique_ptr checkResult; + auto env = Environment(); + + auto formula = formulas[0]; + const storm::modelchecker::CheckTask checkTask + = storm::modelchecker::CheckTask(*formula); + STORM_LOG_THROW(plaModelChecker.canHandle(model, checkTask), storm::exceptions::NotSupportedException, + "Cannot handle this formula"); + plaModelChecker.specify(env, model, checkTask); + + std::unique_ptr minCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Minimize); + std::unique_ptr maxCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Maximize); + auto minRes = minCheck->asExplicitQuantitativeCheckResult(); + auto maxRes = maxCheck->asExplicitQuantitativeCheckResult(); + + std::vector minValues = minRes.getValueVector(); + std::vector maxValues = maxRes.getValueVector(); + // Create initial order + std::tuple criticalTuple = extender->toOrder(formulas, minValues, maxValues); + // Continue based on not (yet) sorted states + std::map>> result; + + auto val1 = std::get<1>(criticalTuple); + auto val2 = std::get<2>(criticalTuple); + auto numberOfStates = model->getNumberOfStates(); + std::vector> assumptions; + + if (val1 == numberOfStates && val2 == numberOfStates) { + result.insert(std::pair>>(std::get<0>(criticalTuple), assumptions)); + } else if (val1 != numberOfStates && val2 != numberOfStates) { + + storm::analysis::AssumptionChecker *assumptionChecker; + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmc = model->as>(); + assumptionChecker = new storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + auto mdp = model->as>(); + assumptionChecker = new storm::analysis::AssumptionChecker(formulas[0], mdp, 3); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, + "Unable to perform monotonicity analysis on the provided model type."); + } + auto assumptionMaker = new storm::analysis::AssumptionMaker(assumptionChecker, numberOfStates, validate); + result = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, val1, val2, assumptions); + } else { + assert(false); + } + orderWatch.stop(); + return result; + } + + template + std::map>> MonotonicityChecker::extendOrderWithAssumptions(storm::analysis::Order* order, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions) { + std::map>> result; + + auto numberOfStates = model->getNumberOfStates(); + if (val1 == numberOfStates || val2 == numberOfStates) { + assert (val1 == val2); + assert (order->getAddedStates()->size() == order->getAddedStates()->getNumberOfSetBits()); + result.insert(std::pair>>(order, assumptions)); + } else { + // Make the three assumptions + auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, order); + assert (assumptionTriple.size() == 3); + auto itr = assumptionTriple.begin(); + auto assumption1 = *itr; + ++itr; + auto assumption2 = *itr; + ++itr; + auto assumption3 = *itr; + + if (assumption1.second != AssumptionStatus::INVALID) { + auto orderCopy = new Order(order); + auto assumptionsCopy = std::vector>(assumptions); + + if (assumption1.second == AssumptionStatus::UNKNOWN) { + // only add assumption to the set of assumptions if it is unknown if it is valid + assumptionsCopy.push_back(assumption1.first); + } + + auto criticalTuple = extender->extendOrder(orderCopy, assumption1.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptionsCopy); + result.insert(map.begin(), map.end()); + } + } + + if (assumption2.second != AssumptionStatus::INVALID) { + auto orderCopy = new Order(order); + auto assumptionsCopy = std::vector>(assumptions); + + if (assumption2.second == AssumptionStatus::UNKNOWN) { + assumptionsCopy.push_back(assumption2.first); + } + + auto criticalTuple = extender->extendOrder(orderCopy, assumption2.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptionsCopy); + result.insert(map.begin(), map.end()); + } + } + + if (assumption3.second != AssumptionStatus::INVALID) { + // Here we can use the original order and assumptions set + if (assumption3.second == AssumptionStatus::UNKNOWN) { + assumptions.push_back(assumption3.first); + } + + auto criticalTuple = extender->extendOrder(order, assumption3.first); + if (somewhereMonotonicity(std::get<0>(criticalTuple))) { + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + std::get<1>(criticalTuple), std::get<2>(criticalTuple), + assumptions); + result.insert(map.begin(), map.end()); + } + } + } + return result; + } + + template + ValueType MonotonicityChecker::getDerivative(ValueType function, typename utility::parametric::VariableType::type var) { + if (function.isConstant()) { + return storm::utility::zero(); + } + if ((derivatives[function]).find(var) == (derivatives[function]).end()) { + (derivatives[function])[var] = function.derivative(var); + } + + return (derivatives[function])[var]; + } + + template + std::map::type, std::pair> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Order* order, storm::storage::SparseMatrix matrix) { + std::map::type, std::pair> varsMonotone; + + // go over all rows, check for each row local monotonicity + for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { + auto row = matrix.getRow(i); + // only enter if you are in a state with at least two successors (so there must be successors, + // and first prob shouldn't be 1) + if (row.begin() != row.end() && !row.begin()->getValue().isOne()) { + std::map transitions; + + // Gather all states which are reached with a non constant probability + auto states = new storm::storage::BitVector(matrix.getColumnCount()); + std::set::type> vars; + for (auto const& entry : row) { + if (!entry.getValue().isConstant()) { + // only analyse take non constant transitions + transitions.insert(std::pair(entry.getColumn(), entry.getValue())); + for (auto const& var:entry.getValue().gatherVariables()) { + vars.insert(var); + states->set(entry.getColumn()); + } + } + } + + // Copy info from checkOnSamples + if (checkSamples) { + for (auto var : vars) { + assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = resultCheckOnSamples[var].first; + varsMonotone[var].second = resultCheckOnSamples[var].second; + } else { + varsMonotone[var].first &= resultCheckOnSamples[var].first; + varsMonotone[var].second &= resultCheckOnSamples[var].second; + } + } + } else { + for (auto var : vars) { + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = true; + varsMonotone[var].second = true; + } + } + } + + + + // Sort the states based on the order + auto sortedStates = order->sortStates(states); + if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) { + // If the states are not all sorted, we still might obtain some monotonicity + for (auto var: vars) { + // current value of monotonicity + std::pair *value = &varsMonotone.find(var)->second; + + // Go over all transitions to successor states, compare all of them + for (auto itr2 = transitions.begin(); (value->first || value->second) + && itr2 != transitions.end(); ++itr2) { + for (auto itr3 = transitions.begin(); (value->first || value->second) + && itr3 != transitions.end(); ++itr3) { + if (itr2->first < itr3->first) { + + auto derivative2 = getDerivative(itr2->second, var); + auto derivative3 = getDerivative(itr3->second, var); + + auto compare = order->compare(itr2->first, itr3->first); + + if (compare == Order::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it + // is sufficient to look at the derivative of itr2. + std::pair mon2; + mon2 = checkDerivative(derivative2, region); + value->first &= mon2.first; + value->second &= mon2.second; + } else if (compare == Order::BELOW) { + // As the second state (itr3) is above the first state (itr2) it + // is sufficient to look at the derivative of itr3. + std::pair mon3; + + mon3 = checkDerivative(derivative3, region); + value->first &= mon3.first; + value->second &= mon3.second; + } else if (compare == Order::SAME) { + // Behaviour doesn't matter, as the states are at the same level. + } else { + // only if derivatives are the same we can continue + if (derivative2 != derivative3) { + // As the relation between the states is unknown, we can't claim + // anything about the monotonicity. + value->first = false; + value->second = false; + } + + } + } + } + } + } + } else { + // The states are all sorted + for (auto var : vars) { + std::pair *value = &varsMonotone.find(var)->second; + bool change = false; + for (auto const &i : sortedStates) { + auto res = checkDerivative(getDerivative(transitions[i], var), region); + change = change || (!(value->first && value->second) // they do not hold both + && ((value->first && !res.first) + || (value->second && !res.second))); + + if (change) { + value->first &= res.second; + value->second &= res.first; + } else { + value->first &= res.first; + value->second &= res.second; + } + if (!value->first && !value->second) { + break; + } + } + + } + } + } + } + return varsMonotone; + } + + template + bool MonotonicityChecker::somewhereMonotonicity(Order* order) { + std::shared_ptr> sparseModel = model->as>(); + auto matrix = sparseModel->getTransitionMatrix(); + + std::map::type, std::pair> varsMonotone; + + for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { + // go over all rows + auto row = matrix.getRow(i); + auto first = (*row.begin()); + if (first.getValue() != ValueType(1)) { + std::map transitions; + + for (auto itr = row.begin(); itr != row.end(); ++itr) { + transitions.insert(std::pair((*itr).getColumn(), (*itr).getValue())); + } + + auto val = first.getValue(); + auto vars = val.gatherVariables(); + // Copy info from checkOnSamples + if (checkSamples) { + for (auto var : vars) { + assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = resultCheckOnSamples[var].first; + varsMonotone[var].second = resultCheckOnSamples[var].second; + } else { + varsMonotone[var].first &= resultCheckOnSamples[var].first; + varsMonotone[var].second &= resultCheckOnSamples[var].second; + } + } + } else { + for (auto var : vars) { + if (varsMonotone.find(var) == varsMonotone.end()) { + varsMonotone[var].first = true; + varsMonotone[var].second = true; + } + } + } + + for (auto var: vars) { + // current value of monotonicity + std::pair *value = &varsMonotone.find(var)->second; + + // Go over all transitions to successor states, compare all of them + for (auto itr2 = transitions.begin(); (value->first || value->second) + && itr2 != transitions.end(); ++itr2) { + for (auto itr3 = transitions.begin(); (value->first || value->second) + && itr3 != transitions.end(); ++itr3) { + if (itr2->first < itr3->first) { + + auto derivative2 = getDerivative(itr2->second, var); + auto derivative3 = getDerivative(itr3->second, var); + + auto compare = order->compare(itr2->first, itr3->first); + + if (compare == Order::ABOVE) { + // As the first state (itr2) is above the second state (itr3) it + // is sufficient to look at the derivative of itr2. + std::pair mon2; + mon2 = checkDerivative(derivative2, region); + value->first &= mon2.first; + value->second &= mon2.second; + } else if (compare == Order::BELOW) { + // As the second state (itr3) is above the first state (itr2) it + // is sufficient to look at the derivative of itr3. + std::pair mon3; + + mon3 = checkDerivative(derivative3, region); + value->first &= mon3.first; + value->second &= mon3.second; + } else if (compare == Order::SAME) { + // Behaviour doesn't matter, as the states are at the same level. + } else { + // As the relation between the states is unknown, we don't do anything + } + } + } + } + } + } + } + + bool result = false; + + for (auto itr = varsMonotone.begin(); !result && itr != varsMonotone.end(); ++itr) { + result = itr->second.first || itr->second.second; + } + return result; + } + + template + std::map::type, std::pair> MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { + storm::utility::Stopwatch samplesWatch(true); + + std::map::type, std::pair> result; + + auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model); + auto matrix = model->getTransitionMatrix(); + std::set::type> variables = storm::models::sparse::getProbabilityParameters(*model); + + // For each of the variables create a model in which we only change the value for this specific variable + for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + double previous = -1; + bool monDecr = true; + bool monIncr = true; + + // Check monotonicity in variable (*itr) by instantiating the model + // all other variables fixed on lb, only increasing (*itr) + for (uint_fast64_t i = 0; (monDecr || monIncr) && i < numberOfSamples; ++i) { + // Create valuation + auto valuation = storm::utility::parametric::Valuation(); + for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { + // Only change value for current variable + if ((*itr) == (*itr2)) { + auto lb = region.getLowerBoundary(itr->name()); + auto ub = region.getUpperBoundary(itr->name()); + // Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub + valuation[*itr2] = utility::convertNumber::type>(lb + i*(ub-lb)/(numberOfSamples-1)); + } else { + auto lb = region.getLowerBoundary(itr->name()); + valuation[*itr2] = utility::convertNumber::type>(lb); + } + } + + // Instantiate model and get result + storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + auto formula = formulas[0]; + if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); + checkResult = checker.computeUntilProbabilities(Environment(), checkTask); + } else if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); + checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "Expecting until or eventually formula"); + } + auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); + std::vector values = quantitativeResult.getValueVector(); + auto initialStates = model->getInitialStates(); + double initial = 0; + // Get total probability from initial states + for (auto j = initialStates.getNextSetIndex(0); j < model->getNumberOfStates(); j = initialStates.getNextSetIndex(j+1)) { + initial += values[j]; + } + // Calculate difference with result for previous valuation + assert (initial >= 0-precision && initial <= 1+precision); + double diff = previous - initial; + assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); + if (previous != -1 && (diff > precision || diff < -precision)) { + monDecr &= diff > precision; // then previous value is larger than the current value from the initial states + monIncr &= diff < -precision; + } + previous = initial; + } + result.insert(std::pair::type, std::pair>(*itr, std::pair(monIncr, monDecr))); + } + + samplesWatch.stop(); + resultCheckOnSamples = result; + return result; + } + + template + std::map::type, std::pair> MonotonicityChecker::checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples) { + storm::utility::Stopwatch samplesWatch(true); + + std::map::type, std::pair> result; + + auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Mdp>(*model); + auto matrix = model->getTransitionMatrix(); + std::set::type> variables = storm::models::sparse::getProbabilityParameters(*model); + + for (auto itr = variables.begin(); itr != variables.end(); ++itr) { + double previous = -1; + bool monDecr = true; + bool monIncr = true; + + for (uint_fast64_t i = 0; i < numberOfSamples; ++i) { + auto valuation = storm::utility::parametric::Valuation(); + for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { + // Only change value for current variable + if ((*itr) == (*itr2)) { + auto val = std::pair::type, typename utility::parametric::CoefficientType::type>( + (*itr2), storm::utility::convertNumber::type>( + boost::lexical_cast((i + 1) / (double(numberOfSamples + 1))))); + valuation.insert(val); + } else { + auto val = std::pair::type, typename utility::parametric::CoefficientType::type>( + (*itr2), storm::utility::convertNumber::type>( + boost::lexical_cast((1) / (double(numberOfSamples + 1))))); + valuation.insert(val); + } + } + storm::models::sparse::Mdp sampleModel = instantiator.instantiate(valuation); + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; + auto formula = formulas[0]; + if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); + checkResult = checker.computeUntilProbabilities(Environment(), checkTask); + } else if (formula->isProbabilityOperatorFormula() && + formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { + const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); + checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "Expecting until or eventually formula"); + } + auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); + std::vector values = quantitativeResult.getValueVector(); + auto initialStates = model->getInitialStates(); + double initial = 0; + for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) { + initial += values[i]; + } + assert (initial >= precision && initial <= 1+precision); + double diff = previous - initial; + assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); + if (previous != -1 && (diff > precision || diff < -precision)) { + monDecr &= diff > precision; // then previous value is larger than the current value from the initial states + monIncr &= diff < -precision; + } + previous = initial; + } + result.insert(std::pair::type, std::pair>(*itr, std::pair(monIncr, monDecr))); + } + + samplesWatch.stop(); + resultCheckOnSamples = result; + return result; + } + + template class MonotonicityChecker; + } +} diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h new file mode 100644 index 000000000..5d32ecf70 --- /dev/null +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -0,0 +1,154 @@ +#ifndef STORM_MONOTONICITYCHECKER_H +#define STORM_MONOTONICITYCHECKER_H + +#include +#include "Order.h" +#include "OrderExtender.h" +#include "AssumptionMaker.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/storage/expressions/RationalFunctionToExpression.h" +#include "storm/utility/constants.h" +#include "storm/models/ModelBase.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/logic/Formula.h" +#include "storm/storage/SparseMatrix.h" +#include "storm-pars/api/region.h" +#include "storm/solver/Z3SmtSolver.h" + + +namespace storm { + namespace analysis { + + template + class MonotonicityChecker { + + public: + /*! + * Constructor of MonotonicityChecker + * @param model the model considered + * @param formula the formula considered + * @param regions the regions to consider + * @param validate whether or not assumptions are to be validated + * @param numberOfSamples number of samples taken for monotonicity checking, default 0, + * if 0 then no check on samples is executed + * @param precision precision on which the samples are compared + */ + MonotonicityChecker(std::shared_ptr model, std::vector> formulas, std::vector> regions, bool validate, uint_fast64_t numberOfSamples=0, double const& precision=0.000001); + + /*! + * Checks for model and formula as provided in constructor for monotonicity + */ + std::map::type, std::pair>> checkMonotonicity(); + + /*! + * Checks if monotonicity can be found in this order. Unordered states are not checked + */ + bool somewhereMonotonicity(storm::analysis::Order* order) ; + + /*! + * Checks if a derivative >=0 or/and <=0 + * @param derivative The derivative you want to check + * @return pair of bools, >= 0 and <= 0 + */ + static std::pair checkDerivative(ValueType derivative, storm::storage::ParameterRegion reg) { + bool monIncr = false; + bool monDecr = false; + + if (derivative.isZero()) { + monIncr = true; + monDecr = true; + } else if (derivative.isConstant()) { + monIncr = derivative.constantPart() >= 0; + monDecr = derivative.constantPart() <= 0; + } else { + + std::shared_ptr smtSolverFactory = std::make_shared(); + std::shared_ptr manager( + new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + + std::set::type> variables = derivative.gatherVariables(); + + + for (auto variable : variables) { + manager->declareRationalVariable(variable.name()); + + } + storm::expressions::Expression exprBounds = manager->boolean(true); + auto managervars = manager->getVariables(); + for (auto var : managervars) { + auto lb = storm::utility::convertNumber(reg.getLowerBoundary(var.getName())); + auto ub = storm::utility::convertNumber(reg.getUpperBoundary(var.getName())); + exprBounds = exprBounds && manager->rational(lb) < var && var < manager->rational(ub); + } + assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat); + + auto converter = storm::expressions::RationalFunctionToExpression(manager); + + // < 0 so not monotone increasing + storm::expressions::Expression exprToCheck = + converter.toExpression(derivative) < manager->rational(0); + s.add(exprBounds); + s.add(exprToCheck); + // If it is unsatisfiable then it should be monotone increasing + monIncr = s.check() == storm::solver::SmtSolver::CheckResult::Unsat; + + // > 0 so not monotone decreasing + exprToCheck = + converter.toExpression(derivative) > manager->rational(0); + + s.reset(); + s.add(exprBounds); + assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat); + s.add(exprToCheck); + monDecr = s.check() == storm::solver::SmtSolver::CheckResult::Unsat; + } + assert (!(monIncr && monDecr) || derivative.isZero()); + + return std::pair(monIncr, monDecr); + } + + private: + std::map::type, std::pair>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + + std::map::type, std::pair> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix matrix) ; + + std::map>> createOrder(); + + std::map::type, std::pair> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + + std::map::type, std::pair> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); + + std::unordered_map::type, ValueType>> derivatives; + + ValueType getDerivative(ValueType function, typename utility::parametric::VariableType::type var); + + std::map>> extendOrderWithAssumptions(Order* order, AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); + + std::shared_ptr model; + + std::vector> formulas; + + bool validate; + + bool checkSamples; + + std::map::type, std::pair> resultCheckOnSamples; + + OrderExtender *extender; + + std::ofstream outfile; + + std::string filename = "monotonicity.txt"; + + double precision; + + storm::storage::ParameterRegion region; + }; + } +} +#endif //STORM_MONOTONICITYCHECKER_H diff --git a/src/storm-pars/analysis/Order.cpp b/src/storm-pars/analysis/Order.cpp new file mode 100644 index 000000000..350cffa29 --- /dev/null +++ b/src/storm-pars/analysis/Order.cpp @@ -0,0 +1,379 @@ +#include +#include +#include "Order.h" + +namespace storm { + namespace analysis { + Order::Order(storm::storage::BitVector* topStates, + storm::storage::BitVector* bottomStates, + storm::storage::BitVector* initialMiddleStates, + uint_fast64_t numberOfStates, + std::vector* statesSorted) { + nodes = std::vector(numberOfStates); + + this->numberOfStates = numberOfStates; + this->addedStates = new storm::storage::BitVector(numberOfStates); + this->doneBuilding = false; + assert (statesSorted != nullptr); + this->statesSorted = *statesSorted; + this->statesToHandle = initialMiddleStates; + + top = new Node(); + bottom = new Node(); + + top->statesAbove = storm::storage::BitVector(numberOfStates); + bottom->statesAbove = storm::storage::BitVector(numberOfStates); + + for (auto const& i : *topStates) { + addedStates->set(i); + bottom->statesAbove.set(i); + top->states.insert(i); + nodes[i] = top; + } + + for (auto const& i : *bottomStates) { + addedStates->set(i); + bottom->states.insert(i); + nodes[i] = bottom; + } + + for (auto const &state : *initialMiddleStates) { + add(state); + } + } + + Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector* statesSorted) { + nodes = std::vector(numberOfStates); + + this->numberOfStates = numberOfStates; + this->addedStates = new storm::storage::BitVector(numberOfStates); + this->doneBuilding = false; + this->statesSorted = *statesSorted; + this->statesToHandle = new storm::storage::BitVector(numberOfStates); + + top = new Node(); + bottom = new Node(); + + top->statesAbove = storm::storage::BitVector(numberOfStates); + bottom->statesAbove = storm::storage::BitVector(numberOfStates); + + addedStates->set(topState); + bottom->statesAbove.set(topState); + top->states.insert(topState); + nodes[topState] = top; + + addedStates->set(bottomState); + bottom->states.insert(bottomState); + nodes[bottomState] = bottom; + assert (addedStates->getNumberOfSetBits() == 2); + } + + Order::Order(Order* order) { + numberOfStates = order->getAddedStates()->size(); + nodes = std::vector(numberOfStates); + addedStates = new storm::storage::BitVector(numberOfStates); + this->doneBuilding = order->getDoneBuilding(); + + auto oldNodes = order->getNodes(); + // Create nodes + for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { + Node *oldNode = (*itr); + if (oldNode != nullptr) { + Node *newNode = new Node(); + newNode->states = oldNode->states; + for (auto const& i : newNode->states) { + addedStates->set(i); + nodes[i] = newNode; + } + if (oldNode == order->getTop()) { + top = newNode; + } else if (oldNode == order->getBottom()) { + bottom = newNode; + } + } + } + assert(*addedStates == *(order->getAddedStates())); + + // set all states above and below + for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { + Node *oldNode = (*itr); + if (oldNode != nullptr) { + Node *newNode = getNode(*(oldNode->states.begin())); + newNode->statesAbove = storm::storage::BitVector((oldNode->statesAbove)); + } + } + + auto statesSortedOrder = order->getStatesSorted(); + for (auto itr = statesSortedOrder.begin(); itr != statesSortedOrder.end(); ++itr) { + this->statesSorted.push_back(*itr); + } + this->statesToHandle = new storm::storage::BitVector(*(order->statesToHandle)); + } + + void Order::addBetween(uint_fast64_t state, Node *above, Node *below) { + assert(!(*addedStates)[state]); + assert(compare(above, below) == ABOVE); + Node *newNode = new Node(); + nodes[state] = newNode; + + newNode->states.insert(state); + newNode->statesAbove = storm::storage::BitVector((above->statesAbove)); + for (auto const& state : above->states) { + newNode->statesAbove.set(state); + } + below->statesAbove.set(state); + addedStates->set(state); + } + + void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { + assert(!(*addedStates)[state]); + assert(compare(above, below) == ABOVE); + + assert (getNode(below)->states.find(below) != getNode(below)->states.end()); + assert (getNode(above)->states.find(above) != getNode(above)->states.end()); + addBetween(state, getNode(above), getNode(below)); + + } + + void Order::addToNode(uint_fast64_t state, Node *node) { + assert(!(*addedStates)[state]); + node->states.insert(state); + nodes[state] = node; + addedStates->set(state); + } + + void Order::add(uint_fast64_t state) { + assert(!(*addedStates)[state]); + addBetween(state, top, bottom); + } + + void Order::addRelationNodes(Order::Node *above, Order::Node * below) { + assert (compare(above, below) == UNKNOWN); + for (auto const& state : above->states) { + below->statesAbove.set(state); + } + below->statesAbove|=((above->statesAbove)); + assert (compare(above, below) == ABOVE); + } + + void Order::addRelation(uint_fast64_t above, uint_fast64_t below) { + addRelationNodes(getNode(above), getNode(below)); + } + + Order::NodeComparison Order::compare(uint_fast64_t state1, uint_fast64_t state2) { + return compare(getNode(state1), getNode(state2)); + } + + Order::NodeComparison Order::compare(Node* node1, Node* node2) { + if (node1 != nullptr && node2 != nullptr) { + if (node1 == node2) { + return SAME; + } + + if (above(node1, node2)) { + assert(!above(node2, node1)); + return ABOVE; + } + + if (above(node2, node1)) { + return BELOW; + } + + // tweak for cyclic pmcs + if (doneBuilding) { + doneBuilding = false; + if (above(node1, node2)) { + assert(!above(node2, node1)); + doneBuilding = true; + return ABOVE; + } + if (above(node2, node1)) { + doneBuilding = true; + return BELOW; + } + } + } + return UNKNOWN; + } + + + bool Order::contains(uint_fast64_t state) { + return state < addedStates->size() && addedStates->get(state); + } + + Order::Node *Order::getNode(uint_fast64_t stateNumber) { + assert (stateNumber < numberOfStates); + return nodes.at(stateNumber); + } + + Order::Node *Order::getTop() { + return top; + } + + Order::Node *Order::getBottom() { + return bottom; + } + + std::vector Order::getNodes() { + return nodes; + } + + storm::storage::BitVector* Order::getAddedStates() { + return addedStates; + } + + bool Order::getDoneBuilding() { + return doneBuilding; + } + + void Order::setDoneBuilding(bool done) { + doneBuilding = done; + } + + std::vector Order::sortStates(storm::storage::BitVector* states) { + uint_fast64_t numberOfSetBits = states->getNumberOfSetBits(); + auto stateSize = states->size(); + auto result = std::vector(numberOfSetBits, stateSize); + for (auto state : *states) { + if (result[0] == stateSize) { + result[0] = state; + } else { + uint_fast64_t i = 0; + bool added = false; + while (i < numberOfSetBits && !added) { + if (result[i] == stateSize) { + result[i] = state; + added = true; + } else { + auto compareRes = compare(state, result[i]); + if (compareRes == ABOVE) { + auto temp = result[i]; + result[i] = state; + for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { + auto temp2 = result[j]; + result[j] = temp; + temp = temp2; + } + added = true; + } else if (compareRes == UNKNOWN) { + break; + } else if (compareRes == SAME) { + ++i; + auto temp = result[i]; + result[i] = state; + for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { + auto temp2 = result[j]; + result[j] = temp; + temp = temp2; + } + added = true; + } + } + ++i; + } + } + } + + return result; + } + + bool Order::above(Node *node1, Node *node2) { + bool found = false; + for (auto const& state : node1->states) { + found = ((node2->statesAbove))[state]; + if (found) { + break; + } + } + + if (!found && !doneBuilding) { + storm::storage::BitVector statesSeen((node2->statesAbove)); + for (auto const &i: (node2->statesAbove)) { + auto nodeI = getNode(i); + if (((nodeI->statesAbove) & statesSeen) != (nodeI->statesAbove)) { + found = above(node1, nodeI, node2, &statesSeen); + } + if (found) { + for (auto const& state:node1->states) { + node2->statesAbove.set(state); + } + break; + } + } + } + return found; + } + + bool Order::above(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2, + storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen) { + bool found = false; + for (auto const& state : node1->states) { + found = ((node2->statesAbove))[state]; + if (found) { + break; + } + } + if (!found) { + nodePrev->statesAbove|=((node2->statesAbove)); + statesSeen->operator|=(((node2->statesAbove))); + + for (auto const &i: node2->statesAbove) { + if (!(*statesSeen)[i]) { + auto nodeI = getNode(i); + if (((nodeI->statesAbove) & *statesSeen) != (nodeI->statesAbove)) { + found = above(node1, nodeI, node2, statesSeen); + } + } + if (found) { + break; + } + + } + } + return found; + } + + void Order::mergeNodes(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2) { + // Merges node2 into node 1 + // everything above n2 also above n1 + node1->statesAbove|=((node2->statesAbove)); + // everything below node 2 also below node 1 + + // add states of node 2 to node 1 + node1->states.insert(node2->states.begin(), node2->states.end()); + + for(auto const& i : node2->states) { + nodes[i] = node1; + } + } + + void Order::merge(uint_fast64_t var1, uint_fast64_t var2) { + mergeNodes(getNode(var1), getNode(var2)); + } + + std::vector Order::getStatesSorted() { + return statesSorted; + } + + uint_fast64_t Order::getNextSortedState() { + if (statesSorted.begin() != statesSorted.end()) { + return *(statesSorted.begin()); + } else { + return numberOfStates; + } + } + + void Order::removeFirstStatesSorted() { + statesSorted.erase(statesSorted.begin()); + } + + void Order::removeStatesSorted(uint_fast64_t state) { + assert(containsStatesSorted(state)); + statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), state)); + } + + bool Order::containsStatesSorted(uint_fast64_t state) { + return std::find(statesSorted.begin(), statesSorted.end(), state) != statesSorted.end(); + } + } +} diff --git a/src/storm-pars/analysis/Order.h b/src/storm-pars/analysis/Order.h new file mode 100644 index 000000000..fa4397498 --- /dev/null +++ b/src/storm-pars/analysis/Order.h @@ -0,0 +1,247 @@ +#ifndef ORDER_ORDER_H +#define ORDER_ORDER_H + +#include +#include +#include +#include +#include + +#include "storm/storage/BitVector.h" + +namespace storm { + namespace analysis { + + class Order { + + public: + /*! + * Constants for comparison of nodes/states + */ + enum NodeComparison { + UNKNOWN, + BELOW, + ABOVE, + SAME, + }; + struct Node { + boost::container::flat_set states; + storm::storage::BitVector statesAbove; + }; + + /*! + * Constructs an order with the given top node and bottom node. + * + * @param topNode The top node of the resulting order. + * @param bottomNode The bottom node of the resulting order. + */ + Order(storm::storage::BitVector* topStates, + storm::storage::BitVector* bottomStates, + storm::storage::BitVector* initialMiddleStates, + uint_fast64_t numberOfStates, + std::vector* statesSorted); + + /*! + * Constructs an order with the given top state and bottom state. + * + * @param top The top state of the resulting order. + * @param bottom The bottom state of the resulting order. + * @param numberOfStates Max number of states in order. + */ + Order(uint_fast64_t top, + uint_fast64_t bottom, + uint_fast64_t numberOfStates, + std::vector* statesSorted); + + /*! + * Constructs a copy of the given order. + * + * @param order The original order. + */ + Order(Order* order); + + /*! + * Adds a node with the given state below node1 and above node2. + * @param state The given state. + * @param node1 The pointer to the node below which a new node (with state) is added + * @param node2 The pointer to the node above which a new node (with state) is added + */ + void addBetween(uint_fast64_t state, Node *node1, Node *node2); + + /*! + * Adds a node with the given state between the nodes of below and above. + * Result: below -> state -> above + * @param state The given state. + * @param above The state number of the state below which a new node (with state) is added + * @param below The state number of the state above which a new node (with state) is added + */ + void addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below); + + /*! + * Adds state to the states of the given node. + * @param state The state which is added. + * @param node The pointer to the node to which state is added, should not be nullptr. + */ + void addToNode(uint_fast64_t state, Node *node); + + /*! + * Adds state between the top and bottom node of the order + * @param state The given state + */ + void add(uint_fast64_t state); + + /*! + * Adds a new relation between two nodes to the order + * @param above The node closest to the top Node of the Order. + * @param below The node closest to the bottom Node of the Order. + */ + void addRelationNodes(storm::analysis::Order::Node *above, storm::analysis::Order::Node * below); + + /*! + * Adds a new relation between two states to the order + * @param above The state closest to the top Node of the Order. + * @param below The state closest to the bottom Node of the Order. + */ + void addRelation(uint_fast64_t above, uint_fast64_t below); + + /*! + * Compares the level of the nodes of the states. + * Behaviour unknown when one or more of the states doesnot occur at any Node in the Order. + * @param state1 The first state. + * @param state2 The second state. + * @return SAME if the nodes are on the same level; + * ABOVE if the node of the first state is closer to top then the node of the second state; + * BELOW if the node of the second state is closer to top then the node of the first state; + * UNKNOWN if it is unclear from the structure of the order how the nodes relate. + */ + Order::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); + + /*! + * Check if state is already in order + * @param state + * @return + */ + bool contains(uint_fast64_t state); + + /*! + * Retrieves the pointer to a Node at which the state occurs. + * + * @param state The number of the state. + * + * @return The pointer to the node of the state, nullptr if the node does not exist. + */ + Node *getNode(uint_fast64_t state); + + /*! + * Retrieves the top node of the order. + * + * @return The top node. + */ + Node* getTop(); + + /*! + * Retrieves the bottom node of the order. + * + * @return The bottom node. + */ + Node* getBottom(); + + /*! + * Returns the vector with the nodes of the order. + * Each index in the vector refers to a state. + * When the state is not yet added at a node, it will contain the nullptr. + * + * @return The vector with nodes of the order. + */ + std::vector getNodes(); + + /*! + * Returns a BitVector in which all added states are set. + * + * @return The BitVector with all added states. + */ + storm::storage::BitVector* getAddedStates(); + + /*! + * Returns true if done building the order. + * @return + */ + bool getDoneBuilding(); + + /*! + * Compares two nodes in the order + * @param node1 + * @param node2 + * @return BELOW, ABOVE, SAME or UNKNOWN + */ + NodeComparison compare(Node* node1, Node* node2); + + /*! + * Sorts the given stats if possible. + * + * @param states Bitvector of the states to sort + * @return Vector with states sorted, length equals number of states to sort. + * If states cannot be sorted, last state of the vector will always equal the length of the BitVector + */ + std::vector sortStates(storm::storage::BitVector* states); + + /*! + * If the order is fully build, this can be set to true. + */ + void setDoneBuilding(bool done); + + /*! + * Prints a string representation of the order to the output stream. + * + * @param out The stream to output to. + */ + void toString(std::ostream &out); + + /*! + * Merges node2 into node1 + * @param node1 + * @param node2 + */ + void mergeNodes(Node* node1, Node* node2); + /*! + * Merges node of var2 into node of var1 + * @param var1 + * @param var2 + */ + void merge(uint_fast64_t var1, uint_fast64_t var2); + + storm::storage::BitVector* statesToHandle; + + uint_fast64_t getNextSortedState(); + + bool containsStatesSorted(uint_fast64_t state); + + void removeFirstStatesSorted(); + + void removeStatesSorted(uint_fast64_t state); + + protected: + std::vector getStatesSorted(); + + private: + std::vector nodes; + + std::vector statesSorted; + + storm::storage::BitVector* addedStates; + + Node* top; + + Node* bottom; + + uint_fast64_t numberOfStates; + + bool above(Node * node1, Node * node2); + + bool above(Node * node1, Node * node2, storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen); + + bool doneBuilding; + }; + } +} +#endif //ORDER_ORDER_H diff --git a/src/storm-pars/analysis/OrderExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp new file mode 100644 index 000000000..636dd8913 --- /dev/null +++ b/src/storm-pars/analysis/OrderExtender.cpp @@ -0,0 +1,490 @@ +// +// Created by Jip Spel on 28.08.18. +// + +#include "OrderExtender.h" +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" +#include +#include +#include "storm/models/sparse/Model.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" + +#include +#include +#include "storm/storage/StronglyConnectedComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponent.h" + +#include "storm/storage/BitVector.h" +#include "storm/utility/macros.h" +#include "storm/utility/Stopwatch.h" + + +namespace storm { + namespace analysis { + + template + OrderExtender::OrderExtender(std::shared_ptr> model) { + this->model = model; + this->matrix = model->getTransitionMatrix(); + this->assumptionSeen = false; + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + + // Build stateMap + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + stateMap[i] = new storm::storage::BitVector(numberOfStates, false); + auto row = matrix.getRow(i); + for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { + // ignore self-loops when there are more transitions + if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { + stateMap[i]->set(rowItr->getColumn(), true); + } + } + } + + // Check if MC contains cycles + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + this->sccs = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + acyclic = true; + for (size_t i = 0; acyclic && i < sccs.size(); ++i) { + acyclic &= sccs.getBlock(i).size() <= 1; + } + } + + template + std::tuple OrderExtender::toOrder(std::vector> formulas) { + STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); + STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() + && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() + || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula"); + + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); + storm::storage::BitVector phiStates; + storm::storage::BitVector psiStates; + if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } else { + phiStates = storm::storage::BitVector(numberOfStates, true); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + + // Get the maybeStates + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector topStates = statesWithProbability01.second; + storm::storage::BitVector bottomStates = statesWithProbability01.first; + + STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); + STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); + + // Transform to Order + auto matrix = this->model->getTransitionMatrix(); + + auto initialMiddleStates = storm::storage::BitVector(numberOfStates); + // Add possible cycle breaking states + if (!acyclic) { + for (size_t i = 0; i < sccs.size(); ++i) { + auto scc = sccs.getBlock(i); + if (scc.size() > 1) { + auto states = scc.getStates(); + // check if the state has already one successor in bottom of top, in that case pick it + for (auto const& state : states) { + auto successors = stateMap[state]; + if (successors->getNumberOfSetBits() == 2) { + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); + auto intersection = bottomStates | topStates; + if (intersection[succ1] || intersection[succ2]) { + initialMiddleStates.set(state); + break; + } + } + } + } + } + } + std::vector statesSorted = storm::utility::graph::getTopologicalSort(matrix); + Order *order = new Order(&topStates, &bottomStates, &initialMiddleStates, numberOfStates, &statesSorted); + + return this->extendOrder(order); + } + + + template + std::tuple OrderExtender::toOrder(std::vector> formulas, std::vector minValues, std::vector maxValues) { + uint_fast64_t numberOfStates = this->model->getNumberOfStates(); + uint_fast64_t bottom = numberOfStates; + uint_fast64_t top = numberOfStates; + std::vector statesSorted = storm::utility::graph::getTopologicalSort(matrix); + Order *order = nullptr; + + for (auto state : statesSorted) { + if ((minValues[numberOfStates - 1 - state] == 1 || maxValues[numberOfStates - 1 - state] == 0) + && minValues[numberOfStates - 1 - state] == maxValues[numberOfStates - 1 - state]) { + if (maxValues[numberOfStates - 1 - state] == 0) { + assert (bottom == numberOfStates); + bottom = state; + } + if (minValues[numberOfStates - 1 - state] == 1) { + assert (top == numberOfStates); + top = state; + } + if (bottom != numberOfStates && top != numberOfStates) { + order = new Order(top, bottom, numberOfStates, &statesSorted); + } + + } else { + assert (order != nullptr); + auto successors = stateMap[state]; + if (successors->getNumberOfSetBits() == 1) { + auto succ = successors->getNextSetIndex(0); + if (succ != state) { + if (!order->contains(succ)) { + order->add(succ); + } + order->addToNode(state, order->getNode(succ)); + } + } else if (successors->getNumberOfSetBits() > 1) { + uint_fast64_t min = numberOfStates; + uint_fast64_t max = numberOfStates; + bool allSorted = true; + + for (auto succ = successors->getNextSetIndex(0); + succ < numberOfStates; succ = successors->getNextSetIndex(succ + 1)) { + if (min == numberOfStates) { + assert (max == numberOfStates); + min = succ; + max = succ; + } else { + if (minValues[numberOfStates - 1 - succ] > maxValues[numberOfStates - 1 - max]) { + max = succ; + } else if (maxValues[numberOfStates - 1 - succ] < minValues[numberOfStates - 1 - min]) { + min = succ; + } else { + allSorted = false; + break; + } + } + } + + if (allSorted && min != max) { + if (order->contains(min) && order->contains(max)) { + assert (order->compare(min,max) == Order::UNKNOWN || order->compare(min,max) == Order::BELOW); + if (order->compare(min, max) == Order::UNKNOWN) { + order->addRelation(max, min); + } + } + if (!order->contains(min)) { + if (order->contains(max)) { + order->addBetween(min, order->getNode(max), order->getBottom()); + } else { + order->add(min); + } + } + if (!order->contains(max)) { + // Because of construction min is in the order + order->addBetween(max, order->getTop(), order->getNode(min)); + } + assert (order->compare(max, min) == Order::ABOVE); + order->addBetween(state, max, min); + } + } + } + } + + assert (order != nullptr); + + // Handle sccs + auto addedStates = order->getAddedStates(); + for (auto scc : sccs) { + if (scc.size() > 1) { + auto states = scc.getStates(); + auto candidate = -1; + for (auto const& state : states) { + if (addedStates->get(state)) { + candidate = -1; + break; + // if there is a state of the scc already present in the order, there is no need to add one. + } + auto successors = stateMap[state]; + if (candidate == -1 && successors->getNumberOfSetBits() == 2) { + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); + if (addedStates->get(succ1) || addedStates->get(succ2)) { + candidate = state; + } + } + } + if (candidate != -1) { + order->add(candidate); + order->statesToHandle->set(candidate); + } + } + } + return this->extendOrder(order); + } + + + template + void OrderExtender::handleAssumption(Order* order, std::shared_ptr assumption) { + assert (assumption != nullptr); + assumptionSeen = true; + + storm::expressions::BinaryRelationExpression expr = *assumption; + assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater + || expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal); + + if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); + storm::expressions::Variable var1 = expr.getFirstOperand()->asVariableExpression().getVariable(); + storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable(); + auto val1 = std::stoul(var1.getName(), nullptr, 0); + auto val2 = std::stoul(var2.getName(), nullptr, 0); + auto comp = order->compare(val1, val2); + + assert (comp == Order::UNKNOWN); + Order::Node *n1 = order->getNode(val1); + Order::Node *n2 = order->getNode(val2); + + if (n1 != nullptr && n2 != nullptr) { + order->mergeNodes(n1,n2); + } else if (n1 != nullptr) { + order->addToNode(val2, n1); + } else if (n2 != nullptr) { + order->addToNode(val1, n2); + } else { + order->add(val1); + order->addToNode(val2, order->getNode(val1)); + } + } else { + assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); + storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); + storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); + auto val1 = std::stoul(largest.getName(), nullptr, 0); + auto val2 = std::stoul(smallest.getName(), nullptr, 0); + auto compareRes = order->compare(val1, val2); + + assert(compareRes == Order::UNKNOWN); + Order::Node *n1 = order->getNode(val1); + Order::Node *n2 = order->getNode(val2); + + if (n1 != nullptr && n2 != nullptr) { + order->addRelationNodes(n1, n2); + } else if (n1 != nullptr) { + order->addBetween(val2, n1, order->getBottom()); + } else if (n2 != nullptr) { + order->addBetween(val1, order->getTop(), n2); + } else { + order->add(val1); + order->addBetween(val2, order->getNode(val1), order->getBottom()); + } + } + } + + template + std::tuple OrderExtender::extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) { + auto numberOfStates = successors->size(); + assert (order->getAddedStates()->size() == numberOfStates); + + if (successors->getNumberOfSetBits() == 1) { + // As there is only one successor the current state and its successor must be at the same nodes. + order->addToNode(stateNumber, order->getNode(successors->getNextSetIndex(0))); + } else if (successors->getNumberOfSetBits() == 2) { + // Otherwise, check how the two states compare, and add if the comparison is possible. + uint_fast64_t successor1 = successors->getNextSetIndex(0); + uint_fast64_t successor2 = successors->getNextSetIndex(successor1 + 1); + + int compareResult = order->compare(successor1, successor2); + if (compareResult == Order::ABOVE) { + // successor 1 is closer to top than successor 2 + order->addBetween(stateNumber, order->getNode(successor1), + order->getNode(successor2)); + } else if (compareResult == Order::BELOW) { + // successor 2 is closer to top than successor 1 + order->addBetween(stateNumber, order->getNode(successor2), + order->getNode(successor1)); + } else if (compareResult == Order::SAME) { + // the successors are at the same level + order->addToNode(stateNumber, order->getNode(successor1)); + } else { + assert(order->compare(successor1, successor2) == Order::UNKNOWN); + return std::make_tuple(order, successor1, successor2); + } + } else if (successors->getNumberOfSetBits() > 2) { + for (auto const& i : *successors) { + for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { + if (order->compare(i,j) == Order::UNKNOWN) { + return std::make_tuple(order, i, j); + } + } + } + + auto highest = successors->getNextSetIndex(0); + auto lowest = highest; + for (auto i = successors->getNextSetIndex(highest+1); i < numberOfStates; i = successors->getNextSetIndex(i+1)) { + if (order->compare(i, highest) == Order::ABOVE) { + highest = i; + } + if (order->compare(lowest, i) == Order::ABOVE) { + lowest = i; + } + } + if (lowest == highest) { + order->addToNode(stateNumber, order->getNode(highest)); + } else { + order->addBetween(stateNumber, order->getNode(highest), order->getNode(lowest)); + } + } + return std::make_tuple(order, numberOfStates, numberOfStates); + } + + + + template + std::tuple OrderExtender::extendOrder(Order* order, std::shared_ptr assumption) { + auto numberOfStates = this->model->getNumberOfStates(); + + if (assumption != nullptr) { + handleAssumption(order, assumption); + } + + auto oldNumberSet = numberOfStates; + while (oldNumberSet != order->getAddedStates()->getNumberOfSetBits()) { + oldNumberSet = order->getAddedStates()->getNumberOfSetBits(); + + // Forward reasoning for cycles; + if (!acyclic) { + auto statesToHandle = order->statesToHandle; + auto stateNumber = statesToHandle->getNextSetIndex(0); + + while (stateNumber != numberOfStates) { + storm::storage::BitVector *successors = stateMap[stateNumber]; + // Checking for states which are already added to the order, and only have one successor left which haven't been added yet + auto succ1 = successors->getNextSetIndex(0); + auto succ2 = successors->getNextSetIndex(succ1 + 1); + + assert (order->contains(stateNumber)); + if (successors->getNumberOfSetBits() == 1) { + if (!order->contains(succ1)) { + order->addToNode(succ1, order->getNode(stateNumber)); + statesToHandle->set(succ1, true); + if (order->containsStatesSorted(succ1)) { + order->removeStatesSorted(succ1); + } + } + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } else if (successors->getNumberOfSetBits() == 2 + && ((order->contains(succ1) && !order->contains(succ2)) + || (!order->contains(succ1) && order->contains(succ2)))) { + + if (!order->contains(succ1)) { + std::swap(succ1, succ2); + } + + auto compare = order->compare(stateNumber, succ1); + if (compare == Order::ABOVE) { + if (order->containsStatesSorted(succ2)) { + order->removeStatesSorted(succ2); + } + order->addBetween(succ2, order->getTop(), order->getNode(stateNumber)); + statesToHandle->set(succ2); + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } else if (compare == Order::BELOW) { + if (order->containsStatesSorted(succ2)) { + order->removeStatesSorted(succ2); + } + order->addBetween(succ2, order->getNode(stateNumber), order->getBottom()); + statesToHandle->set(succ2); + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } else { + // We don't know positions, so we set the current state number to false + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } + + } else if (!((order->contains(succ1) && !order->contains(succ2)) + || (!order->contains(succ1) && order->contains(succ2)))) { + stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); + } else { + statesToHandle->set(stateNumber, false); + stateNumber = statesToHandle->getNextSetIndex(0); + } + } + + } + + // Normal backwardreasoning + auto stateNumber = order->getNextSortedState(); + while (stateNumber != numberOfStates && order->contains(stateNumber)) { + order->removeFirstStatesSorted(); + stateNumber = order->getNextSortedState(); + + if (stateNumber != numberOfStates && order->contains(stateNumber)) { + auto resAllAdded = allSuccAdded(order, stateNumber); + if (!std::get<0>(resAllAdded)) { + return std::make_tuple(order, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); + } + } + } + + if (stateNumber != numberOfStates && !order->contains(stateNumber)) { + auto successors = stateMap[stateNumber]; + + auto result = extendAllSuccAdded(order, stateNumber, successors); + if (std::get<1>(result) != numberOfStates) { + // So we don't know the relation between all successor states + return result; + } else { + assert (order->getNode(stateNumber) != nullptr); + if (!acyclic) { + order->statesToHandle->set(stateNumber); + } + order->removeFirstStatesSorted(); + } + } + assert (stateNumber == numberOfStates || order->getNode(stateNumber) != nullptr); + assert (stateNumber == numberOfStates || order->contains(stateNumber)); + + } + assert (order->getAddedStates()->getNumberOfSetBits() == numberOfStates); + order->setDoneBuilding(true); + return std::make_tuple(order, numberOfStates, numberOfStates); + } + + template + std::tuple OrderExtender::allSuccAdded(storm::analysis::Order *order, uint_fast64_t stateNumber) { + auto successors = stateMap[stateNumber]; + auto numberOfStates = successors->size(); + + if (successors->getNumberOfSetBits() == 1) { + auto succ = successors->getNextSetIndex(0); + return std::make_tuple(order->contains(succ), succ, succ); + } else if (successors->getNumberOfSetBits() > 2) { + for (auto const& i : *successors) { + for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { + if (order->compare(i,j) == Order::UNKNOWN) { + return std::make_tuple(false, i, j); + } + } + } + } + return std::make_tuple(true, numberOfStates, numberOfStates); + + } + + template class OrderExtender; + } +} diff --git a/src/storm-pars/analysis/OrderExtender.h b/src/storm-pars/analysis/OrderExtender.h new file mode 100644 index 000000000..30d3d4137 --- /dev/null +++ b/src/storm-pars/analysis/OrderExtender.h @@ -0,0 +1,83 @@ +#ifndef STORM_LATTICEEXTENDER_H +#define STORM_LATTICEEXTENDER_H + +#include +#include "storm/models/sparse/Dtmc.h" +#include "storm-pars/analysis/Order.h" +#include "storm/api/storm.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponent.h" + + + +namespace storm { + namespace analysis { + + + template + class OrderExtender { + + public: + /*! + * Constructs OrderExtender which can extend an order + * + * @param model The model for which the order should be extended. + */ + OrderExtender(std::shared_ptr> model); + + /*! + * Creates an order based on the given formula. + * + * @param formulas The formulas based on which the order is created, only the first is used. + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple toOrder(std::vector> formulas); + + /*! + * Creates an order based on the given extremal values. + * + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple toOrder(std::vector> formulas, std::vector minValues, std::vector maxValues); + + + /*! + * Extends the order based on the given assumption. + * + * @param order The order. + * @param assumption The assumption on states. + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple extendOrder(storm::analysis::Order* order, std::shared_ptr assumption = nullptr); + + + private: + std::shared_ptr> model; + + std::map stateMap; + + bool acyclic; + + bool assumptionSeen; + + storm::storage::StronglyConnectedComponentDecomposition sccs; + + storm::storage::SparseMatrix matrix; + + void handleAssumption(Order* order, std::shared_ptr assumption); + + std::tuple extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); + + std::tuple allSuccAdded(Order* order, uint_fast64_t stateNumber); + }; + } +} + +#endif //STORM_ORDEREXTENDER_H diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index c032426e5..0ee310b39 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -79,14 +79,14 @@ namespace storm { STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected."); return res.front(); } - + template std::shared_ptr> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { - + STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually..."); std::shared_ptr> consideredModel = model; - + // Treat continuous time models if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); @@ -94,7 +94,7 @@ namespace storm { consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first; STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); } - + // Obtain the region model checker std::shared_ptr> checker; if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) { @@ -104,12 +104,12 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - + checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification); - + return checker; } - + template std::shared_ptr> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index 87635b9bb..8e8592c5e 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -2,6 +2,8 @@ #include "storm-pars/settings/modules/ParametricSettings.h" #include "storm-pars/settings/modules/RegionSettings.h" +#include "storm-pars/settings/modules/MonotonicitySettings.h" + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -29,12 +31,13 @@ namespace storm { namespace settings { void initializeParsSettings(std::string const& name, std::string const& executableName) { storm::settings::mutableManager().setName(name, executableName); - + // Register relevant settings modules. storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pars/settings/modules/MonotonicitySettings.cpp b/src/storm-pars/settings/modules/MonotonicitySettings.cpp new file mode 100644 index 000000000..dd7a91b80 --- /dev/null +++ b/src/storm-pars/settings/modules/MonotonicitySettings.cpp @@ -0,0 +1,54 @@ +#include "storm-pars/settings/modules/MonotonicitySettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string MonotonicitySettings::moduleName = "monotonicity"; + const std::string MonotonicitySettings::monotonicityAnalysis = "monotonicity-analysis"; + const std::string MonotonicitySettings::sccElimination = "mon-elim-scc"; + const std::string MonotonicitySettings::validateAssumptions = "mon-validate-assumptions"; + const std::string MonotonicitySettings::samplesMonotonicityAnalysis = "mon-samples"; + const std::string MonotonicitySettings::precision = "mon-precision"; + + MonotonicitySettings::MonotonicitySettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build()); + + } + + bool MonotonicitySettings::isMonotonicityAnalysisSet() const { + return this->getOption(monotonicityAnalysis).getHasOptionBeenSet(); + } + + bool MonotonicitySettings::isSccEliminationSet() const { + return this->getOption(sccElimination).getHasOptionBeenSet(); + } + + bool MonotonicitySettings::isValidateAssumptionsSet() const { + return this->getOption(validateAssumptions).getHasOptionBeenSet(); + } + + uint_fast64_t MonotonicitySettings::getNumberOfSamples() const { + return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); + } + + double MonotonicitySettings::getMonotonicityAnalysisPrecision() const { + return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble(); + } + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-pars/settings/modules/MonotonicitySettings.h b/src/storm-pars/settings/modules/MonotonicitySettings.h new file mode 100644 index 000000000..f420935cd --- /dev/null +++ b/src/storm-pars/settings/modules/MonotonicitySettings.h @@ -0,0 +1,60 @@ +#ifndef STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ +#define STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ + +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for monotonicity checking. + */ + class MonotonicitySettings : public ModuleSettings { + public: + + /*! + * Creates a new set of monotonicity checking settings. + */ + MonotonicitySettings(); + + /*! + * Retrieves whether monotonicity analysis should be applied. + */ + bool isMonotonicityAnalysisSet() const; + + /*! + * Retrieves whether SCCs in the monotonicity analysis should be eliminated. + */ + bool isSccEliminationSet() const; + + /*! + * Retrieves whether assumptions in monotonicity analysis should be validated + */ + bool isValidateAssumptionsSet() const; + + /*! + * Retrieves the number of samples used for sampling in the monotonicity analysis + */ + uint_fast64_t getNumberOfSamples() const; + + /*! + * Retrieves the precision for the extremal value + */ + double getMonotonicityAnalysisPrecision() const; + + const static std::string moduleName; + + private: + const static std::string monotonicityAnalysis; + const static std::string sccElimination; + const static std::string validateAssumptions; + const static std::string samplesMonotonicityAnalysis; + const static std::string precision; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ */ diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 7ecbd6166..45528844c 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -65,7 +65,7 @@ namespace storm { bool ParametricSettings::isSampleExactSet() const { return this->getOption(sampleExactOptionName).getHasOptionBeenSet(); } - + } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 1f10a4b35..3fe281e4e 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -42,7 +42,7 @@ namespace storm { */ bool transformContinuousModel() const; - /* + /*! * Retrieves whether instead of model checking, only the wellformedness constraints should be obtained. */ bool onlyObtainConstraints() const; @@ -63,7 +63,7 @@ namespace storm { * Retrieves whether samples are to be computed exactly. */ bool isSampleExactSet() const; - + const static std::string moduleName; private: diff --git a/src/storm-pars/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp index 3d9e36c93..68d6e94dc 100644 --- a/src/storm-pars/storage/ParameterRegion.cpp +++ b/src/storm-pars/storage/ParameterRegion.cpp @@ -48,6 +48,16 @@ namespace storm { return (*result).second; } + template + typename ParameterRegion::CoefficientType const& ParameterRegion::getLowerBoundary(const std::string varName) const { + for (auto itr = lowerBoundaries.begin(); itr != lowerBoundaries.end(); ++itr) { + if (itr->first.name().compare(varName) == 0) { + return (*itr).second; + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to find a lower boundary for variableName " << varName << " which is not specified by this region"); + } + template typename ParameterRegion::CoefficientType const& ParameterRegion::getUpperBoundary(VariableType const& variable) const { auto const& result = upperBoundaries.find(variable); @@ -55,6 +65,16 @@ namespace storm { return (*result).second; } + template + typename ParameterRegion::CoefficientType const& ParameterRegion::getUpperBoundary(const std::string varName) const { + for (auto itr = upperBoundaries.begin(); itr != upperBoundaries.end(); ++itr) { + if (itr->first.name().compare(varName) == 0) { + return (*itr).second; + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Tried to find an upper boundary for variableName " << varName << " which is not specified by this region"); + } + template typename ParameterRegion::Valuation const& ParameterRegion::getUpperBoundaries() const { return upperBoundaries; diff --git a/src/storm-pars/storage/ParameterRegion.h b/src/storm-pars/storage/ParameterRegion.h index bcdd86ccb..d4f3ce457 100644 --- a/src/storm-pars/storage/ParameterRegion.h +++ b/src/storm-pars/storage/ParameterRegion.h @@ -24,7 +24,9 @@ namespace storm { std::set const& getVariables() const; CoefficientType const& getLowerBoundary(VariableType const& variable) const; + CoefficientType const& getLowerBoundary(const std::string varName) const; CoefficientType const& getUpperBoundary(VariableType const& variable) const; + CoefficientType const& getUpperBoundary(const std::string varName) const; Valuation const& getLowerBoundaries() const; Valuation const& getUpperBoundaries() const; diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 4dcaf7f61..521aecb75 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -89,6 +89,18 @@ namespace storm { } + template + std::shared_ptr checkAndTransformContinuousToDiscreteTimeFormula(storm::logic::Formula const& formula, std::string const& timeRewardName = "_time") { + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; + if (transformer.preservesFormula(formula)) { + return transformer.checkAndTransformFormulas({formula.asSharedPointer()}, timeRewardName).front(); + } else { + STORM_LOG_ERROR("Unable to transform formula " << formula << " to discrete time."); + } + return nullptr; + } + + /*! * Transforms the given symbolic model to a sparse model. */ diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 8a7030b17..c368a976d 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -107,7 +107,8 @@ namespace storm { #ifdef STORM_HAVE_CARL else if (std::is_same::value && !program.undefinedConstantsAreGraphPreserving()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); + auto undef = program.getUndefinedConstantsAsString(); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted. Undefined constants are: " << undef); } #endif } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 04c7d4256..583f37c7f 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -44,7 +44,6 @@ namespace storm { const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; const std::string IOSettings::propertyOptionShortName = "prop"; - const std::string IOSettings::toNondetOptionName = "to-nondet"; const std::string IOSettings::qvbsInputOptionName = "qvbs"; const std::string IOSettings::qvbsInputOptionShortName = "qvbs"; @@ -90,7 +89,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build()) @@ -266,10 +264,6 @@ namespace storm { return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); } - bool IOSettings::isToNondeterministicModelSet() const { - return this->getOption(toNondetOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isQvbsInputSet() const { return this->getOption(qvbsInputOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 96b419b67..9731a272c 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -290,11 +290,6 @@ namespace storm { * @return The property filter. */ std::string getPropertyFilter() const; - - /*! - * Retrieves whether a DTMC/CTMC should be converted to an MDP/MA - */ - bool isToNondeterministicModelSet() const; /*! * Retrieves whether the input model is to be read from the quantitative verification benchmark set (QVBS) @@ -354,7 +349,6 @@ namespace storm { static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; static const std::string propertyOptionShortName; - static const std::string toNondetOptionName; static const std::string qvbsInputOptionName; static const std::string qvbsInputOptionShortName; static const std::string qvbsRootOptionName; diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp index 75b1c3daf..d948a48d9 100644 --- a/src/storm/settings/modules/TransformationSettings.cpp +++ b/src/storm/settings/modules/TransformationSettings.cpp @@ -12,6 +12,8 @@ namespace storm { const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains"; const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling"; + const std::string TransformationSettings::toNondetOptionName = "to-nondet"; + const std::string TransformationSettings::toDiscreteTimeOptionName = "to-discrete"; TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { @@ -19,6 +21,8 @@ namespace storm { "If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false, "If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, toDiscreteTimeOptionName, false, "If set, CTMCs/MAs are converted to DTMCs/MDPs (which might or might not preserve the provided properties).").setIsAdvanced().build()); } bool TransformationSettings::isChainEliminationSet() const { @@ -29,6 +33,13 @@ namespace storm { return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet(); } + bool TransformationSettings::isToNondeterministicModelSet() const { + return this->getOption(toNondetOptionName).getHasOptionBeenSet(); + } + + bool TransformationSettings::isToDiscreteTimeModelSet() const { + return this->getOption(toDiscreteTimeOptionName).getHasOptionBeenSet(); + } bool TransformationSettings::check() const { // Ensure that labeling preservation is only set if chain elimination is set diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h index ba646c763..00642e5fb 100644 --- a/src/storm/settings/modules/TransformationSettings.h +++ b/src/storm/settings/modules/TransformationSettings.h @@ -34,6 +34,15 @@ namespace storm { */ bool isIgnoreLabelingSet() const; + /*! + * Retrieves whether a DTMC/CTMC should be converted to an MDP/MA + */ + bool isToNondeterministicModelSet() const; + + /*! + * Retrieves whether a CTMC/MA should be converted to a DTMC/MDP + */ + bool isToDiscreteTimeModelSet() const; bool check() const override; @@ -46,6 +55,8 @@ namespace storm { // Define the string names of the options as constants. static const std::string chainEliminationOptionName; static const std::string ignoreLabelingOptionName; + static const std::string toNondetOptionName; + static const std::string toDiscreteTimeOptionName; }; diff --git a/src/storm/solver/stateelimination/EliminatorBase.cpp b/src/storm/solver/stateelimination/EliminatorBase.cpp index 041b610bf..bc523b073 100644 --- a/src/storm/solver/stateelimination/EliminatorBase.cpp +++ b/src/storm/solver/stateelimination/EliminatorBase.cpp @@ -249,7 +249,47 @@ namespace storm { elementsWithEntryInColumnEqualRow.shrink_to_fit(); } } - + + template + void EliminatorBase::eliminateLoop(uint64_t state) { + // Start by finding value of the selfloop. + bool hasEntryInColumn = false; + ValueType columnValue = storm::utility::zero(); + FlexibleRowType& entriesInRow = matrix.getRow(state); + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) { + if (entryIt->getColumn() == state) { + columnValue = entryIt->getValue(); + hasEntryInColumn = true; + } + } + + // Scale all entries in this row. + // Depending on the scaling mode, we scale the other entries of the row. + STORM_LOG_TRACE((hasEntryInColumn ? "State has entry in column." : "State does not have entry in column.")); + if (Mode == ScalingMode::Divide) { + STORM_LOG_ASSERT(hasEntryInColumn, "The scaling mode 'divide' requires an element in the given column."); + STORM_LOG_ASSERT(storm::utility::isZero(columnValue), "The scaling mode 'divide' requires a non-zero element in the given column."); + columnValue = storm::utility::one() / columnValue; + } else if (Mode == ScalingMode::DivideOneMinus) { + if (hasEntryInColumn) { + STORM_LOG_ASSERT(columnValue != storm::utility::one(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column."); + columnValue = storm::utility::one() / (storm::utility::one() - columnValue); + columnValue = storm::utility::simplify(columnValue); + } + } + + if (hasEntryInColumn) { + for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) { + // Scale the entries in a different column, set state transition probability to 0. + if (entryIt->getColumn() != state) { + entryIt->setValue(storm::utility::simplify((ValueType) (entryIt->getValue() * columnValue))); + } else { + entryIt->setValue(storm::utility::zero()); + } + } + } + } + template void EliminatorBase::updateValue(storm::storage::sparse::state_type const&, ValueType const&) { // Intentionally left empty. diff --git a/src/storm/solver/stateelimination/EliminatorBase.h b/src/storm/solver/stateelimination/EliminatorBase.h index 996da58e6..0d66ab18a 100644 --- a/src/storm/solver/stateelimination/EliminatorBase.h +++ b/src/storm/solver/stateelimination/EliminatorBase.h @@ -22,7 +22,9 @@ namespace storm { virtual ~EliminatorBase() = default; void eliminate(uint64_t row, uint64_t column, bool clearRow); - + + void eliminateLoop(uint64_t row); + // Provide virtual methods that can be customized by subclasses to govern side-effect of the elimination. virtual void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability); virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state); diff --git a/src/storm/storage/expressions/RationalFunctionToExpression.cpp b/src/storm/storage/expressions/RationalFunctionToExpression.cpp new file mode 100644 index 000000000..0bbd08038 --- /dev/null +++ b/src/storm/storage/expressions/RationalFunctionToExpression.cpp @@ -0,0 +1,67 @@ +// +// Created by Jip Spel on 24.09.18. +// + +#include "RationalFunctionToExpression.h" +#include "storm/utility/constants.h" + +namespace storm { + namespace expressions { + template + RationalFunctionToExpression::RationalFunctionToExpression(std::shared_ptr manager) : manager(manager) { + // Intentionally left empty. + } + + template + std::shared_ptr RationalFunctionToExpression::getManager() { + return manager; + } + + template + Expression RationalFunctionToExpression::toExpression(ValueType function) { + function.simplify(); + auto varsFunction = function.gatherVariables(); + for (auto var : varsFunction) { + auto varsManager = manager->getVariables(); + bool found = find_if(varsManager.begin(), varsManager.end(), + [&](auto val) -> bool { + return val.getName() == var.name(); + }) != varsManager.end(); + if (!found) { + manager->declareRationalVariable(var.name()); + } + } + + auto denominator = function.denominator(); + if (!denominator.isConstant()) { + STORM_LOG_DEBUG("Expecting the denominator to be constant"); + } + + storm::expressions::Expression result; + if (function.isConstant()) { + result = manager->rational(storm::utility::convertNumber(function.constantPart())); + } else { + auto nominator = function.nominatorAsPolynomial().polynomialWithCoefficient(); + result = manager->rational(storm::utility::convertNumber(nominator.constantPart())); + for (auto itr = nominator.begin(); itr != nominator.end(); ++itr) { + varsFunction.clear(); + itr->gatherVariables(varsFunction); + + storm::expressions::Expression nominatorPartExpr = manager->rational(storm::utility::convertNumber(itr->coeff())); + for (auto var : varsFunction) { + nominatorPartExpr = nominatorPartExpr * (manager->getVariable(var.name())^manager->rational(storm::utility::convertNumber(itr->monomial()->exponentOfVariable(var)))); + } + if (varsFunction.size() >= 1) { + result = result + nominatorPartExpr; + } + } + storm::expressions::Expression denominatorVal = manager->rational(storm::utility::convertNumber(denominator.constantPart())); + result = result / denominatorVal; + } + + return result; + } + + template class RationalFunctionToExpression; + } +} diff --git a/src/storm/storage/expressions/RationalFunctionToExpression.h b/src/storm/storage/expressions/RationalFunctionToExpression.h new file mode 100644 index 000000000..9ba38ccc5 --- /dev/null +++ b/src/storm/storage/expressions/RationalFunctionToExpression.h @@ -0,0 +1,40 @@ +// +// Created by Jip Spel on 24.09.18. +// + +#ifndef STORM_RATIONALFUNCTIONTOEXPRESSION_H +#define STORM_RATIONALFUNCTIONTOEXPRESSION_H + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace expressions { + template + class RationalFunctionToExpression { + public: + RationalFunctionToExpression(std::shared_ptr manager); + + /*! + * Retrieves the manager responsible for the variables of this valuation. + * + * @return The pointer to the manager. + */ + std::shared_ptr getManager(); + + /*! + * Transforms the function into an expression. + * + * @param function The function to transform + * @return The created expression. + */ + Expression toExpression(ValueType function); + + private: + // The manager responsible for the variables of this valuation. + std::shared_ptr manager; + }; + } +} + +#endif //STORM_RATIONALFUNCTIONTOEXPRESSION_H diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 28c5a391d..ba3994449 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite modelchecker utility) +foreach (testsuite analysis modelchecker utility) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp new file mode 100644 index 000000000..fd5e31a85 --- /dev/null +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -0,0 +1,373 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/analysis/AssumptionChecker.h" +#include "storm-pars/analysis/Order.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/storage/ParameterRegion.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +#include "storm-pars/api/region.h" + + +TEST(AssumptionCheckerTest, Brp_no_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + // Create the region + storm::storage::ParameterRegion::Valuation lowerBoundaries; + storm::storage::ParameterRegion::Valuation upperBoundaries; + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= pK <= 0.00001, 0.00001 <= pL <= 0.99999", vars); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + + // Check on samples + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("7"); + expressionManager->declareRationalVariable("5"); + + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + + + storm::storage::BitVector above(8); + above.set(0); + storm::storage::BitVector below(8); + below.set(1); + storm::storage::BitVector initialMiddle(8); + + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 8, &statesSorted); + // Validate assumption + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); +// EXPECT_FALSE(checker.validated(assumption)); + + expressionManager->declareRationalVariable("6"); + expressionManager->declareRationalVariable("8"); + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("6").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("8").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + above = storm::storage::BitVector(13); + above.set(12); + below = storm::storage::BitVector(13); + below.set(9); + initialMiddle = storm::storage::BitVector(13); + + dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 13, &statesSorted); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); +// EXPECT_EQ(checker.validated(assumption)); +// EXPECT_FALSE(checker.valid(assumption)); +} + +TEST(AssumptionCheckerTest, Simple1) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm"; + std::string formulaAsString = "P=? [F s=3]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.99999", vars); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("1"); + expressionManager->declareRationalVariable("2"); + + // Checking on samples + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); +} + +TEST(AssumptionCheckerTest, Simple2) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple2.pm"; + std::string formulaAsString = "P=? [F s=3]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.99999", vars); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("1"); + expressionManager->declareRationalVariable("2"); + + storm::storage::BitVector above(5); + above.set(3); + storm::storage::BitVector below(5); + below.set(4); + storm::storage::BitVector initialMiddle(5); + + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); + + // Checking on samples and validate + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); +} + +TEST(AssumptionCheckerTest, Simple3) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple3.pm"; + std::string formulaAsString = "P=? [F s=4]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(6ul, dtmc->getNumberOfStates()); + ASSERT_EQ(12ul, dtmc->getNumberOfTransitions()); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.99999", vars); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("1"); + expressionManager->declareRationalVariable("2"); + + storm::storage::BitVector above(6); + above.set(4); + storm::storage::BitVector below(6); + below.set(5); + storm::storage::BitVector initialMiddle(6); + + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 6, &statesSorted); + order->add(3); + + // Checking on samples and validate + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); +} + +TEST(AssumptionCheckerTest, Simple4) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple4.pm"; + std::string formulaAsString = "P=? [F s=3]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.4", vars); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("1"); + expressionManager->declareRationalVariable("2"); + + // Order + storm::storage::BitVector above(5); + above.set(3); + storm::storage::BitVector below(5); + below.set(4); + storm::storage::BitVector initialMiddle(5); + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); + + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Greater)); + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); + + assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::Equal)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); + + + +} diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp new file mode 100644 index 000000000..7ede1cc08 --- /dev/null +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -0,0 +1,319 @@ +// +// Created by Jip Spel on 20.09.18. +// + +// TODO: cleanup includes +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/analysis/Order.h" +#include "storm-pars/analysis/AssumptionMaker.h" +#include "storm-pars/analysis/AssumptionChecker.h" +#include "storm-pars/analysis/OrderExtender.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +TEST(AssumptionMakerTest, Brp_without_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); + ASSERT_EQ(183, std::get<1>(criticalTuple)); + ASSERT_EQ(186, std::get<2>(criticalTuple)); + + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); + auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); + + EXPECT_EQ(3, result.size()); + + bool foundFirst = false; + bool foundSecond = false; + bool foundThird = false; + for (auto itr = result.begin(); itr != result.end(); ++itr) { + if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "183") { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundFirst = true; + } else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundSecond = true; + } else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); + foundThird = true; + } else { + EXPECT_TRUE(false); + } + } + EXPECT_TRUE(foundFirst); + EXPECT_TRUE(foundSecond); + EXPECT_TRUE(foundThird); +} + +TEST(AssumptionMakerTest, Brp_without_bisimulation_no_validation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); + ASSERT_EQ(183, std::get<1>(criticalTuple)); + ASSERT_EQ(186, std::get<2>(criticalTuple)); + + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + // This one does not validate the assumptions! + auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), false); + auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); + + EXPECT_EQ(3, result.size()); + + bool foundFirst = false; + bool foundSecond = false; + bool foundThird = false; + for (auto itr = result.begin(); itr != result.end(); ++itr) { + if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "183") { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundFirst = true; + } else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundSecond = true; + } else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); + foundThird = true; + } else { + EXPECT_TRUE(false); + } + } + EXPECT_TRUE(foundFirst); + EXPECT_TRUE(foundSecond); + EXPECT_TRUE(foundThird); +} + +TEST(AssumptionMakerTest, Simple1) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm"; + std::string formulaAsString = "P=? [F s=3]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.999999", vars); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + + storm::storage::BitVector above(5); + above.set(3); + storm::storage::BitVector below(5); + below.set(4); + storm::storage::BitVector initialMiddle(5); + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); + + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); + auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); + + EXPECT_EQ(3, result.size()); + + bool foundFirst = false; + bool foundSecond = false; + bool foundThird = false; + for (auto itr = result.begin(); itr != result.end(); ++itr) { + if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "1") { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundFirst = true; + } else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundSecond = true; + } else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); + foundThird = true; + } else { + EXPECT_TRUE(false); + } + } + EXPECT_TRUE(foundFirst); + EXPECT_TRUE(foundSecond); + EXPECT_TRUE(foundThird); +} + +TEST(AssumptionMakerTest, Simple2) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple2.pm"; + std::string formulaAsString = "P=? [F s=3]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + // Create the region + auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); + auto region = storm::api::parseRegion("0.00001 <= p <= 0.999999", vars); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + + storm::storage::BitVector above(5); + above.set(3); + storm::storage::BitVector below(5); + below.set(4); + storm::storage::BitVector initialMiddle(5); + + std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); + + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); + + auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); + auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); + + auto itr = result.begin(); + + EXPECT_EQ(3, result.size()); + + bool foundFirst = false; + bool foundSecond = false; + bool foundThird = false; + for (auto itr = result.begin(); itr != result.end(); ++itr) { + if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "1") { + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundFirst = true; + } else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); + foundSecond = true; + } else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); + EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); + EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); + EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); + EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); + foundThird = true; + } else { + EXPECT_TRUE(false); + } + } + EXPECT_TRUE(foundFirst); + EXPECT_TRUE(foundSecond); + EXPECT_TRUE(foundThird); +} + diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp new file mode 100644 index 000000000..c83d436b4 --- /dev/null +++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp @@ -0,0 +1,206 @@ +// +// Created by Jip Spel on 20.09.18. +// + +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" +#include "storm-pars/analysis/MonotonicityChecker.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/adapters/RationalFunctionAdapter.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" +TEST(MonotonicityCheckerTest, Derivative_checker) { + + // Create the region + typename storm::storage::ParameterRegion::Valuation lowerBoundaries; + typename storm::storage::ParameterRegion::Valuation upperBoundaries; + auto region = storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); + + // Derivative 0 + auto constFunction = storm::RationalFunction(0); + auto constFunctionRes = storm::analysis::MonotonicityChecker::checkDerivative(constFunction, region); + EXPECT_TRUE(constFunctionRes.first); + EXPECT_TRUE(constFunctionRes.second); + + // Derivative 5 + constFunction = storm::RationalFunction(5); + constFunctionRes = storm::analysis::MonotonicityChecker::checkDerivative(constFunction, region); + EXPECT_TRUE(constFunctionRes.first); + EXPECT_FALSE(constFunctionRes.second); + + // Derivative -4 + constFunction = storm::RationalFunction(storm::RationalFunction(1)-constFunction); + constFunctionRes = storm::analysis::MonotonicityChecker::checkDerivative(constFunction, region); + EXPECT_FALSE(constFunctionRes.first); + EXPECT_TRUE(constFunctionRes.second); + + std::shared_ptr cache = std::make_shared(); + carl::StringParser parser; + parser.setVariables({"p", "q"}); + + // Create the region + auto functionP = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("p"), cache)); + auto functionQ = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("q"), cache)); + + auto varsP = functionP.gatherVariables(); + auto varsQ = functionQ.gatherVariables(); + storm::utility::parametric::Valuation lowerBoundaries2; + storm::utility::parametric::Valuation upperBoundaries2; + for (auto var : varsP) { + typename storm::storage::ParameterRegion::CoefficientType lb = storm::utility::convertNumber::CoefficientType>(0 + 0.000001); + typename storm::storage::ParameterRegion::CoefficientType ub = storm::utility::convertNumber::CoefficientType>(1 - 0.000001); + lowerBoundaries2.emplace(std::make_pair(var, lb)); + upperBoundaries2.emplace(std::make_pair(var, ub)); + } + for (auto var : varsQ) { + typename storm::storage::ParameterRegion::CoefficientType lb = storm::utility::convertNumber::CoefficientType>(0 + 0.000001); + typename storm::storage::ParameterRegion::CoefficientType ub = storm::utility::convertNumber::CoefficientType>(1 - 0.000001); + lowerBoundaries2.emplace(std::make_pair(var, lb)); + upperBoundaries2.emplace(std::make_pair(var, ub)); + } + region = storm::storage::ParameterRegion(std::move(lowerBoundaries2), std::move(upperBoundaries2)); + + // Derivative p + auto function = functionP; + auto functionRes = storm::analysis::MonotonicityChecker::checkDerivative(function, region); + EXPECT_TRUE(functionRes.first); + EXPECT_FALSE(functionRes.second); + + // Derivative 1-p + auto functionDecr = storm::RationalFunction(storm::RationalFunction(1)-function); + auto functionDecrRes = storm::analysis::MonotonicityChecker::checkDerivative(functionDecr, region); + EXPECT_TRUE(functionDecrRes.first); + EXPECT_FALSE(functionDecrRes.second); + + // Derivative 1-2p + auto functionNonMonotonic = storm::RationalFunction(storm::RationalFunction(1)-storm::RationalFunction(2)*function); + auto functionNonMonotonicRes = storm::analysis::MonotonicityChecker::checkDerivative(functionNonMonotonic, region); + EXPECT_FALSE(functionNonMonotonicRes.first); + EXPECT_FALSE(functionNonMonotonicRes.second); + + // Derivative -p + functionDecr = storm::RationalFunction(storm::RationalFunction(0)-function); + functionDecrRes = storm::analysis::MonotonicityChecker::checkDerivative(functionDecr, region); + EXPECT_FALSE(functionDecrRes.first); + EXPECT_TRUE(functionDecrRes.second); + + // Derivative p*q + function = functionP * functionQ ; + functionRes = storm::analysis::MonotonicityChecker::checkDerivative(function, region); + EXPECT_TRUE(functionRes.first); + EXPECT_FALSE(functionRes.second); +} + +TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [true U s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + // Apply bisimulation + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::getModule().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + dtmc = storm::api::performBisimulationMinimization(model, formulas, bisimType)->as>(); + + + // Create the region + typename storm::storage::ParameterRegion::Valuation lowerBoundaries; + typename storm::storage::ParameterRegion::Valuation upperBoundaries; + std::set::VariableType> vars = storm::models::sparse::getProbabilityParameters(*dtmc); + for (auto var : vars) { + typename storm::storage::ParameterRegion::CoefficientType lb = storm::utility::convertNumber::CoefficientType>(0 + 0.000001); + typename storm::storage::ParameterRegion::CoefficientType ub = storm::utility::convertNumber::CoefficientType>(1 - 0.000001); + lowerBoundaries.emplace(std::make_pair(var, lb)); + upperBoundaries.emplace(std::make_pair(var, ub)); + } + auto region = storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); +std::vector> regions = {region}; + + ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); + + storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(dtmc, formulas, regions, true); + auto result = monotonicityChecker.checkMonotonicity(); + EXPECT_EQ(1ul, result.size()); + EXPECT_EQ(2ul, result.begin()->second.size()); + auto monotone = result.begin()->second.begin(); + EXPECT_EQ(true, monotone->second.first); + EXPECT_EQ(false, monotone->second.second); +} + +TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [true U s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + // Apply bisimulation + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::getModule().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + dtmc = storm::api::performBisimulationMinimization(model, formulas, bisimType)->as>(); + + // Create the region + typename storm::storage::ParameterRegion::Valuation lowerBoundaries; + typename storm::storage::ParameterRegion::Valuation upperBoundaries; + std::set::VariableType> vars = storm::models::sparse::getProbabilityParameters(*dtmc); + for (auto var : vars) { + typename storm::storage::ParameterRegion::CoefficientType lb = storm::utility::convertNumber::CoefficientType>(0 + 0.000001); + typename storm::storage::ParameterRegion::CoefficientType ub = storm::utility::convertNumber::CoefficientType>(1 - 0.000001); + lowerBoundaries.emplace(std::make_pair(var, lb)); + upperBoundaries.emplace(std::make_pair(var, ub)); + } + auto region = storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); + std::vector> regions = {region}; + + ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); + + auto monotonicityChecker = storm::analysis::MonotonicityChecker(dtmc, formulas, regions, true, 50); + auto result = monotonicityChecker.checkMonotonicity(); + EXPECT_EQ(1ul, result.size()); + EXPECT_EQ(2ul, result.begin()->second.size()); + auto monotone = result.begin()->second.begin(); + EXPECT_EQ(true, monotone->second.first); + EXPECT_EQ(false, monotone->second.second); +} diff --git a/src/test/storm-pars/analysis/OrderExtenderTest.cpp b/src/test/storm-pars/analysis/OrderExtenderTest.cpp new file mode 100644 index 000000000..50b916b71 --- /dev/null +++ b/src/test/storm-pars/analysis/OrderExtenderTest.cpp @@ -0,0 +1,93 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/analysis/Order.h" +#include "storm-pars/analysis/OrderExtender.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +TEST(OrderExtenderTest, Brp_with_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + + // Apply bisimulation + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (storm::settings::getModule().isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + dtmc = storm::api::performBisimulationMinimization(model, formulas, bisimType)->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); + + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); + EXPECT_EQ(dtmc->getNumberOfStates(), std::get<1>(criticalTuple)); + EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple)); + + auto order = std::get<0>(criticalTuple); + for (uint_fast64_t i = 0; i < dtmc->getNumberOfStates(); ++i) { + EXPECT_TRUE((*order->getAddedStates())[i]); + } + + // Check on some nodes + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7,13)); +} + +TEST(OrderExtenderTest, Brp_without_bisimulation) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P=? [F s=4 & i=N ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); + EXPECT_EQ(183ul, std::get<1>(criticalTuple)); + EXPECT_EQ(186ul, std::get<2>(criticalTuple)); +} + + diff --git a/src/test/storm-pars/analysis/OrderTest.cpp b/src/test/storm-pars/analysis/OrderTest.cpp new file mode 100644 index 000000000..fc5d78709 --- /dev/null +++ b/src/test/storm-pars/analysis/OrderTest.cpp @@ -0,0 +1,173 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" +#include "storm-pars/analysis/Order.h" +#include "storm/storage/BitVector.h" + +TEST(OrderTest, Simple) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + std::vector statesSorted; + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,0)); + EXPECT_EQ(nullptr, order.getNode(2)); + + order.add(2); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(2,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(2,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); + + order.add(3); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,2)); + + order.addToNode(4, order.getNode(2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(4,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,4)); + + order.addBetween(5, order.getNode(0), order.getNode(3)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,5)); + + order.addBetween(6, order.getNode(5), order.getNode(3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,6)); + + order.addRelationNodes(order.getNode(6), order.getNode(4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,6)); + +} + +TEST(OrderTest, copy_order) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + std::vector statesSorted; + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + order.addBetween(5, order.getNode(0), order.getNode(3)); + order.addBetween(6, order.getNode(5), order.getNode(3)); + + + + auto orderCopy = storm::analysis::Order(order); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,0)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(2,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,2)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(2,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,2)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(4,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(4,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(4,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,4)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); + + order.addRelationNodes(order.getNode(6), order.getNode(4)); + orderCopy = storm::analysis::Order(order); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,6)); +} + +TEST(OrderTest, merge_nodes) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + std::vector statesSorted; + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + order.addBetween(5, order.getNode(0), order.getNode(3)); + order.addBetween(6, order.getNode(5), order.getNode(3)); + + order.mergeNodes(order.getNode(4), order.getNode(5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,5)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); +} diff --git a/src/test/storm/storage/ExpressionTest.cpp b/src/test/storm/storage/ExpressionTest.cpp index 27e4e7d7a..98215eba9 100644 --- a/src/test/storm/storage/ExpressionTest.cpp +++ b/src/test/storm/storage/ExpressionTest.cpp @@ -6,7 +6,13 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" #include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" +#include "storm/storage/expressions/RationalFunctionToExpression.h" #include "storm/exceptions/InvalidTypeException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm-parsers/parser/ValueParser.h" +#include "storm/storage/expressions/ToRationalFunctionVisitor.h" + TEST(Expression, FactoryMethodTest) { std::shared_ptr manager(new storm::expressions::ExpressionManager()); @@ -293,27 +299,27 @@ TEST(Expression, SimplificationTest) { storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; storm::expressions::Expression intVarExpression; - - ASSERT_NO_THROW(trueExpression = manager->boolean(true)); - ASSERT_NO_THROW(falseExpression = manager->boolean(false)); - ASSERT_NO_THROW(threeExpression = manager->integer(3)); - ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); - - storm::expressions::Expression tempExpression; - storm::expressions::Expression simplifiedExpression; - ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression); - ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); - EXPECT_TRUE(simplifiedExpression.isTrue()); +ASSERT_NO_THROW(trueExpression = manager->boolean(true)); +ASSERT_NO_THROW(falseExpression = manager->boolean(false)); +ASSERT_NO_THROW(threeExpression = manager->integer(3)); +ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); + +storm::expressions::Expression tempExpression; +storm::expressions::Expression simplifiedExpression; + +ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression); +ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); +EXPECT_TRUE(simplifiedExpression.isTrue()); - ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression); - ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); - EXPECT_TRUE(simplifiedExpression.isFalse()); +ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression); +ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); +EXPECT_TRUE(simplifiedExpression.isFalse()); } TEST(Expression, SimpleEvaluationTest) { std::shared_ptr manager(new storm::expressions::ExpressionManager()); - + storm::expressions::Expression trueExpression; storm::expressions::Expression falseExpression; storm::expressions::Expression threeExpression; @@ -321,7 +327,7 @@ TEST(Expression, SimpleEvaluationTest) { storm::expressions::Expression boolVarExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression rationalVarExpression; - + ASSERT_NO_THROW(trueExpression = manager->boolean(true)); ASSERT_NO_THROW(falseExpression = manager->boolean(false)); ASSERT_NO_THROW(threeExpression = manager->integer(3)); @@ -329,23 +335,23 @@ TEST(Expression, SimpleEvaluationTest) { ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); - + storm::expressions::Expression tempExpression; - + ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); - + ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager)); storm::expressions::SimpleValuation valuation(manager); ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false)); ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0)); ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0)); - + ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3)); EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); - + ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression)); ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); @@ -354,18 +360,67 @@ TEST(Expression, SimpleEvaluationTest) { TEST(Expression, VisitorTest) { std::shared_ptr manager(new storm::expressions::ExpressionManager()); - + storm::expressions::Expression threeExpression; storm::expressions::Expression piExpression; storm::expressions::Expression intVarExpression; storm::expressions::Expression rationalVarExpression; - + ASSERT_NO_THROW(threeExpression = manager->integer(3)); ASSERT_NO_THROW(piExpression = manager->rational(3.14)); ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); - + storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression; storm::expressions::LinearityCheckVisitor visitor; EXPECT_TRUE(visitor.check(tempExpression)); } + +TEST(Expression, RationalFunctionToExpressionTest) { + storm::parser::ValueParser parser; + parser.addParameter("p"); + parser.addParameter("q"); + auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2"); + + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + auto transformer = storm::expressions::RationalFunctionToExpression(manager); + + storm::expressions::Expression expr; + EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); + auto base = storm::expressions::ExpressionEvaluator(*manager); + storm::expressions::ToRationalFunctionVisitor visitor(base); + ASSERT_NO_THROW(rationalFunction.simplify()); + storm::RationalFunction result; + ASSERT_NO_THROW(result = visitor.toRationalFunction(expr)); + ASSERT_NO_THROW(result.simplify()); + EXPECT_EQ(rationalFunction.toString(), result.toString()); + + rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2"); + transformer = storm::expressions::RationalFunctionToExpression(manager); + EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); + ASSERT_NO_THROW(rationalFunction.simplify()); + ASSERT_NO_THROW(result = visitor.toRationalFunction(expr)); + ASSERT_NO_THROW(result.simplify()); + EXPECT_EQ(rationalFunction.toString(), result.toString()); +} + +TEST(Expression, RationalFunctionToExpressionTest_no_params) { + storm::parser::ValueParser parser; + parser.addParameter("p"); + auto rationalFunction1 = parser.parseValue("(p + 380)/3125"); + auto rationalFunction2 = parser.parseValue("(p)/3125"); + auto rationalFunction = rationalFunction1 - rationalFunction2; + + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + auto transformer = storm::expressions::RationalFunctionToExpression(manager); + + storm::expressions::Expression expr; + EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); + auto base = storm::expressions::ExpressionEvaluator(*manager); + storm::expressions::ToRationalFunctionVisitor visitor(base); + ASSERT_NO_THROW(rationalFunction.simplify()); + storm::RationalFunction result; + ASSERT_NO_THROW(result = visitor.toRationalFunction(expr)); + ASSERT_NO_THROW(result.simplify()); + EXPECT_EQ(rationalFunction.toString(), result.toString()); +} \ No newline at end of file