diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp rename to src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h rename to src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp rename to src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h rename to src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp rename to src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h rename to src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h diff --git a/src/storm/modelchecker/parametric/RegionChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp similarity index 93% rename from src/storm/modelchecker/parametric/RegionChecker.cpp rename to src/storm-pars/modelchecker/region/RegionModelChecker.cpp index 163e28b7a..d01fe5160 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -68,8 +68,8 @@ namespace storm { } template - RegionCheckResult RegionChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) { - RegionCheckResult result = initialResult; + RegionResult RegionChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + RegionResult result = initialResult; // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated instantiationCheckerStopwatch.start(); @@ -120,8 +120,8 @@ namespace storm { } template - RegionCheckResult RegionChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult) { - RegionCheckResult numericResult = analyzeRegion(region, initialResult, false); + RegionResult RegionChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionResult const& initialResult) { + RegionResult numericResult = analyzeRegion(region, initialResult, false); parameterLiftingCheckerStopwatch.start(); if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) { applyHintsToExactChecker(); @@ -159,7 +159,7 @@ namespace storm { template - std::vector, RegionCheckResult>> RegionChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold) { + std::vector, RegionResult>> RegionChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); auto areaOfParameterSpace = region.area(); @@ -167,8 +167,8 @@ namespace storm { auto fractionOfAllSatArea = storm::utility::zero(); auto fractionOfAllViolatedArea = storm::utility::zero(); - std::queue, RegionCheckResult>> unprocessedRegions; - std::vector, RegionCheckResult>> result; + std::queue, RegionResult>> unprocessedRegions; + std::vector, RegionResult>> result; unprocessedRegions.emplace(region, RegionCheckResult::Unknown); uint_fast64_t numOfAnalyzedRegions = 0; numOfCorrectedRegions = 0; @@ -211,7 +211,7 @@ namespace storm { default: std::vector> newRegions; currentRegion.split(currentRegion.getCenterPoint(), newRegions); - RegionCheckResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat : + RegionResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat : ((res == RegionCheckResult::CenterViolated) ? RegionCheckResult::ExistsViolated : RegionCheckResult::Unknown); for(auto& newRegion : newRegions) { @@ -258,7 +258,7 @@ namespace storm { } template - std::string RegionChecker::visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { + std::string RegionChecker::visualizeResult(std::vector, RegionResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { std::stringstream stream; diff --git a/src/storm/modelchecker/parametric/RegionChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h similarity index 80% rename from src/storm/modelchecker/parametric/RegionChecker.h rename to src/storm-pars/modelchecker/region/RegionModelChecker.h index 64bdcd580..377615f1c 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -43,19 +43,19 @@ namespace storm { * Then, we check whether ALL points in the region violate/satisfy the property * */ - RegionCheckResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false); + RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false); /*! * Similar to analyze region but additionaly invokes exact parameter lifting to validate results AllSat or AllViolated */ - RegionCheckResult analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown); + RegionResult analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionCheckResult::Unknown); /*! * Iteratively refines the region until parameter lifting yields a conclusive result (AllSat or AllViolated). * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold */ - std::vector, RegionCheckResult>> performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold); + std::vector, RegionResult>> performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold); - static std::string visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y); + static std::string visualizeResult(std::vector, RegionResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y); protected: SparseModelType const& getConsideredParametricModel() const; diff --git a/src/storm/modelchecker/parametric/RegionCheckResult.cpp b/src/storm-pars/modelchecker/region/RegionResult.cpp similarity index 100% rename from src/storm/modelchecker/parametric/RegionCheckResult.cpp rename to src/storm-pars/modelchecker/region/RegionResult.cpp diff --git a/src/storm/modelchecker/parametric/RegionCheckResult.h b/src/storm-pars/modelchecker/region/RegionResult.h similarity index 100% rename from src/storm/modelchecker/parametric/RegionCheckResult.h rename to src/storm-pars/modelchecker/region/RegionResult.h diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp rename to src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h rename to src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp rename to src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h rename to src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp rename to src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h rename to src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp rename to src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.h b/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseMdpRegionChecker.h rename to src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp similarity index 100% rename from src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp rename to src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h similarity index 100% rename from src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h rename to src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h diff --git a/src/storm/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp similarity index 100% rename from src/storm/settings/modules/ParametricSettings.cpp rename to src/storm-pars/settings/modules/ParametricSettings.cpp diff --git a/src/storm/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h similarity index 64% rename from src/storm/settings/modules/ParametricSettings.h rename to src/storm-pars/settings/modules/ParametricSettings.h index 54f2bbf86..650d7bc3c 100644 --- a/src/storm/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -12,15 +12,6 @@ namespace storm { */ class ParametricSettings : public ModuleSettings { public: - /** - * A type for saving the Smt2EncondingStrategy. - * - * FULL_TRANSITION_SYSTEM: The transition system should be reduced only with very basic operations. - * ONLY_SCC_ENTRY_STATES: Scc elimination should be performed, but no further reduction. - * HIGH_INDEGREE: State elimination but for states with a high indegree. - * RATIONAL_FUNCTION: The smt file should contain only the rational function. - */ - enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION}; /*! * Creates a new set of parametric model checking settings. @@ -42,12 +33,12 @@ namespace storm { /*! * Retrieves whether the parameter space was declared */ - bool isParameterSpaceSet() const; + bool isRegionSet() const; /*! * Retrieves the given parameter spcae */ - std::string getParameterSpace() const; + std::string getRegionString() const; /*! * Retrieves the threshold considered for iterative region refinement. @@ -60,24 +51,6 @@ namespace storm { */ bool isExactValidationSet() const; - /** - * Retrieves whether the encoding of the transition system should be exported to a file. - * @return True iff the smt file should be encoded. - */ - bool exportToSmt2File() const; - - /** - * The path to a file location which should contain the smt2 encoding. - * @return A path to a file location. - */ - std::string exportSmt2Path() const; - - /** - * Retrieves which encoding strategy should be used for generating the smt2 file. - * @return The encoding strategy to be used. - */ - Smt2EncodingStrategy smt2EncodingStrategy() const; - /*! * Retrieves whether or not derivatives of the resulting rational function are to be generated. * @@ -91,7 +64,7 @@ namespace storm { const static std::string encodeSmt2StrategyOptionName; const static std::string exportSmt2DestinationPathOptionName; const static std::string exportResultDestinationPathOptionName; - const static std::string parameterSpaceOptionName; + const static std::string regionOptionName; const static std::string refinementThresholdOptionName; const static std::string exactValidationOptionName; const static std::string derivativesOptionName; diff --git a/src/storm/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp similarity index 100% rename from src/storm/storage/ParameterRegion.cpp rename to src/storm-pars/storage/ParameterRegion.cpp diff --git a/src/storm/storage/ParameterRegion.h b/src/storm-pars/storage/ParameterRegion.h similarity index 100% rename from src/storm/storage/ParameterRegion.h rename to src/storm-pars/storage/ParameterRegion.h diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm-pars/transformer/ParameterLifter.cpp similarity index 100% rename from src/storm/transformer/ParameterLifter.cpp rename to src/storm-pars/transformer/ParameterLifter.cpp diff --git a/src/storm/transformer/ParameterLifter.h b/src/storm-pars/transformer/ParameterLifter.h similarity index 100% rename from src/storm/transformer/ParameterLifter.h rename to src/storm-pars/transformer/ParameterLifter.h diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp similarity index 100% rename from src/storm/transformer/SparseParametricDtmcSimplifier.cpp rename to src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.h b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h similarity index 100% rename from src/storm/transformer/SparseParametricDtmcSimplifier.h rename to src/storm-pars/transformer/SparseParametricDtmcSimplifier.h diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp similarity index 100% rename from src/storm/transformer/SparseParametricMdpSimplifier.cpp rename to src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.h b/src/storm-pars/transformer/SparseParametricMdpSimplifier.h similarity index 100% rename from src/storm/transformer/SparseParametricMdpSimplifier.h rename to src/storm-pars/transformer/SparseParametricMdpSimplifier.h diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp similarity index 100% rename from src/storm/transformer/SparseParametricModelSimplifier.cpp rename to src/storm-pars/transformer/SparseParametricModelSimplifier.cpp diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm-pars/transformer/SparseParametricModelSimplifier.h similarity index 100% rename from src/storm/transformer/SparseParametricModelSimplifier.h rename to src/storm-pars/transformer/SparseParametricModelSimplifier.h diff --git a/src/storm/utility/ModelInstantiator.cpp b/src/storm-pars/utility/ModelInstantiator.cpp similarity index 100% rename from src/storm/utility/ModelInstantiator.cpp rename to src/storm-pars/utility/ModelInstantiator.cpp diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm-pars/utility/ModelInstantiator.h similarity index 100% rename from src/storm/utility/ModelInstantiator.h rename to src/storm-pars/utility/ModelInstantiator.h diff --git a/src/storm/utility/parameterlifting.h b/src/storm-pars/utility/parameterlifting.h similarity index 100% rename from src/storm/utility/parameterlifting.h rename to src/storm-pars/utility/parameterlifting.h diff --git a/src/storm/utility/parametric.cpp b/src/storm-pars/utility/parametric.cpp similarity index 100% rename from src/storm/utility/parametric.cpp rename to src/storm-pars/utility/parametric.cpp diff --git a/src/storm/utility/parametric.h b/src/storm-pars/utility/parametric.h similarity index 100% rename from src/storm/utility/parametric.h rename to src/storm-pars/utility/parametric.h diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 2bc6ec94e..16c42cd7e 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -255,131 +255,5 @@ namespace storm { return result; } - template - std::unique_ptr verifyWithParameterLifting(std::shared_ptr>, std::shared_ptr const&) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter-lifting is unavailable for this data-type."); - } - - template<> - inline std::unique_ptr verifyWithParameterLifting(std::shared_ptr> markovModel, std::shared_ptr const& formula) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Parameter-lifting is currently unavailable from the API."); -// storm::utility::Stopwatch parameterLiftingStopWatch(true); -// std::shared_ptr consideredFormula = formula; -// -// STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(markovModel, formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula); -// -// if (markovModel->isOfType(storm::models::ModelType::Ctmc) || markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { -// STORM_PRINT_AND_LOG("Transforming continuous model to discrete model..."); -// storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula); -// STORM_PRINT_AND_LOG(" done!" << std::endl); -// markovModel->printModelInformationToStream(std::cout); -// } -// -// auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel); -// auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel); -// modelParameters.insert(rewParameters.begin(), rewParameters.end()); -// -// STORM_LOG_THROW(storm::settings::getModule().isParameterSpaceSet(), storm::exceptions::InvalidSettingsException, "Invoked Parameter lifting but no parameter space was defined."); -// auto parameterSpaceAsString = storm::settings::getModule().getParameterSpace(); -// auto parameterSpace = storm::storage::ParameterRegion::parseRegion(parameterSpaceAsString, modelParameters); -// auto refinementThreshold = storm::utility::convertNumber::CoefficientType>(storm::settings::getModule().getRefinementThreshold()); -// std::vector, storm::modelchecker::parametric::RegionCheckResult>> result; -// -// STORM_PRINT_AND_LOG("Performing parameter lifting for property " << *consideredFormula << " with parameter space " << parameterSpace.toString(true) << " and refinement threshold " << storm::utility::convertNumber(refinementThreshold) << " ..." << std::endl); -// -// storm::modelchecker::CheckTask task(*consideredFormula, true); -// std::string resultVisualization; -// -// if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { -// if (storm::settings::getModule().isExactSet()) { -// storm::modelchecker::parametric::SparseDtmcRegionChecker , storm::RationalNumber> regionChecker(*markovModel->template as>()); -// regionChecker.specifyFormula(task); -// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); -// parameterLiftingStopWatch.stop(); -// if (modelParameters.size() == 2) { -// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); -// } -// } else { -// storm::modelchecker::parametric::SparseDtmcRegionChecker , double, storm::RationalNumber> regionChecker(*markovModel->template as>()); -// regionChecker.specifyFormula(task); -// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); -// parameterLiftingStopWatch.stop(); -// if (modelParameters.size() == 2) { -// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); -// } -// } -// } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { -// if (storm::settings::getModule().isExactSet()) { -// storm::modelchecker::parametric::SparseMdpRegionChecker, storm::RationalNumber> regionChecker(*markovModel->template as>()); -// regionChecker.specifyFormula(task); -// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); -// parameterLiftingStopWatch.stop(); -// if (modelParameters.size() == 2) { -// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); -// } -// } else { -// storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*markovModel->template as>()); -// regionChecker.specifyFormula(task); -// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); -// parameterLiftingStopWatch.stop(); -// if (modelParameters.size() == 2) { -// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); -// } -// } -// } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type."); -// } -// -// -// auto satArea = storm::utility::zero::CoefficientType>(); -// auto unsatArea = storm::utility::zero::CoefficientType>(); -// uint_fast64_t numOfSatRegions = 0; -// uint_fast64_t numOfUnsatRegions = 0; -// for (auto const& res : result) { -// switch (res.second) { -// case storm::modelchecker::parametric::RegionCheckResult::AllSat: -// satArea += res.first.area(); -// ++numOfSatRegions; -// break; -// case storm::modelchecker::parametric::RegionCheckResult::AllViolated: -// unsatArea += res.first.area(); -// ++numOfUnsatRegions; -// break; -// default: -// STORM_LOG_ERROR("Unexpected result for region " << res.first.toString(true) << " : " << res.second << "."); -// break; -// } -// } -// typename storm::storage::ParameterRegion::CoefficientType satAreaFraction = satArea / parameterSpace.area(); -// typename storm::storage::ParameterRegion::CoefficientType unsatAreaFraction = unsatArea / parameterSpace.area(); -// STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions and " -// << numOfUnsatRegions << " unsafe regions." << std::endl); -// STORM_PRINT_AND_LOG(storm::utility::convertNumber(satAreaFraction) * 100 << "% of the parameter space is safe, and " -// << storm::utility::convertNumber(unsatAreaFraction) * 100 << "% of the parameter space is unsafe." << std::endl); -// STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl); -// STORM_PRINT_AND_LOG(resultVisualization); -// -// if (storm::settings::getModule().exportResultToFile()) { -// std::string path = storm::settings::getModule().exportResultPath(); -// STORM_PRINT_AND_LOG("Exporting result to path " << path << "." << std::endl); -// std::ofstream filestream; -// storm::utility::openFile(path, filestream); -// -// for (auto const& res : result) { -// switch (res.second) { -// case storm::modelchecker::parametric::RegionCheckResult::AllSat: -// filestream << "safe: " << res.first.toString(true) << std::endl; -// break; -// case storm::modelchecker::parametric::RegionCheckResult::AllViolated: -// filestream << "unsafe: " << res.first.toString(true) << std::endl; -// break; -// default: -// break; -// } -// } -// } -// } - } - } } diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 0f53aa2d3..b28f068c3 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -26,7 +26,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/ParametricSettings.h" #include @@ -658,13 +657,6 @@ namespace storm { std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(formula, true)); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); return result; - }, - [&sparseModel] (std::unique_ptr const& result) { - auto parametricSettings = storm::settings::getModule(); - if (std::is_same::value && sparseModel->isOfType(storm::models::ModelType::Dtmc) && parametricSettings.exportResultToFile()) { - auto dtmc = sparseModel->template as>(); - storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*sparseModel->getInitialStates().begin()], storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); - } }); } diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index a386dc94c..493ea71a2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -30,7 +30,6 @@ #include "storm/settings/modules/GlpkSettings.h" #include "storm/settings/modules/GurobiSettings.h" #include "storm/settings/modules/Smt2SmtSolverSettings.h" -#include "storm/settings/modules/ParametricSettings.h" #include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h" #include "storm/settings/modules/ExplorationSettings.h" #include "storm/settings/modules/ResourceSettings.h" @@ -527,7 +526,6 @@ namespace storm { 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/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index cb42bfd4b..964518b64 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -24,7 +24,6 @@ namespace storm { const std::string CoreSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string CoreSettings::eqSolverOptionName = "eqsolver"; const std::string CoreSettings::lpSolverOptionName = "lpsolver"; - const std::string CoreSettings::parameterLiftingOptionName = "parameterlifting"; const std::string CoreSettings::smtSolverOptionName = "smtsolver"; const std::string CoreSettings::statisticsOptionName = "statistics"; const std::string CoreSettings::statisticsOptionShortName = "stats"; @@ -53,8 +52,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, parameterLiftingOptionName, false, "Sets whether parameter lifting is applied.").build()); - std::vector smtSolvers = {"z3", "mathsat"}; this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); @@ -92,10 +89,6 @@ namespace storm { return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); } - bool CoreSettings::isParameterLiftingSet() const { - return this->getOption(parameterLiftingOptionName).getHasOptionBeenSet(); - } - storm::solver::LpSolverType CoreSettings::getLpSolver() const { std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); if (lpSolverName == "gurobi") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 719449dd2..4f275b3d0 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -81,12 +81,6 @@ namespace storm { */ bool isEquationSolverSet() const; - /*! - * Retrieves whether parameter lifting should be applied. - * @return True iff parameter lifting should be applied. - */ - bool isParameterLiftingSet() const; - /*! * Retrieves the selected LP solver. * @@ -150,7 +144,6 @@ namespace storm { static const std::string dontFixDeadlockOptionShortName; static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; - static const std::string parameterLiftingOptionName; static const std::string smtSolverOptionName; static const std::string statisticsOptionName; static const std::string statisticsOptionShortName;