You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
567 lines
38 KiB
567 lines
38 KiB
#include "src/modelchecker/region/SparseRegionModelChecker.h"
|
|
|
|
#include "src/adapters/CarlAdapter.h"
|
|
#include "src/modelchecker/region/RegionCheckResult.h"
|
|
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|
#include "src/logic/Formulas.h"
|
|
#include "src/models/sparse/StandardRewardModel.h"
|
|
#include "src/settings/SettingsManager.h"
|
|
#include "src/settings/modules/RegionSettings.h"
|
|
#include "src/utility/constants.h"
|
|
#include "src/utility/graph.h"
|
|
#include "src/utility/macros.h"
|
|
|
|
#include "src/exceptions/InvalidArgumentException.h"
|
|
#include "src/exceptions/InvalidPropertyException.h"
|
|
#include "src/exceptions/InvalidStateException.h"
|
|
#include "src/exceptions/InvalidSettingsException.h"
|
|
#include "src/exceptions/NotImplementedException.h"
|
|
#include "src/exceptions/UnexpectedException.h"
|
|
#include "modelchecker/results/CheckResult.h"
|
|
#include "modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|
|
|
namespace storm {
|
|
namespace modelchecker {
|
|
namespace region {
|
|
|
|
SparseRegionModelCheckerSettings::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode const& sampleM,
|
|
storm::settings::modules::RegionSettings::ApproxMode const& appM,
|
|
storm::settings::modules::RegionSettings::SmtMode const& smtM) : sampleMode(sampleM), approxMode(appM), smtMode(smtM) {
|
|
// Intentionally left empty
|
|
}
|
|
|
|
storm::settings::modules::RegionSettings::ApproxMode SparseRegionModelCheckerSettings::getApproxMode() const {
|
|
return this->approxMode;
|
|
}
|
|
|
|
storm::settings::modules::RegionSettings::SampleMode SparseRegionModelCheckerSettings::getSampleMode() const {
|
|
return this->sampleMode;
|
|
}
|
|
|
|
storm::settings::modules::RegionSettings::SmtMode SparseRegionModelCheckerSettings::getSmtMode() const {
|
|
return this->smtMode;
|
|
}
|
|
|
|
bool SparseRegionModelCheckerSettings::doApprox() const {
|
|
return getApproxMode() != storm::settings::modules::RegionSettings::ApproxMode::OFF;
|
|
}
|
|
|
|
bool SparseRegionModelCheckerSettings::doSample() const {
|
|
return getSampleMode() != storm::settings::modules::RegionSettings::SampleMode::OFF;
|
|
}
|
|
|
|
bool SparseRegionModelCheckerSettings::doSmt() const {
|
|
return getSmtMode() != storm::settings::modules::RegionSettings::SmtMode::OFF;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings) :
|
|
model(model),
|
|
specifiedFormula(nullptr),
|
|
settings(settings) {
|
|
STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state.");
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::~SparseRegionModelChecker() {
|
|
//Intentionally left empty
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
std::shared_ptr<ParametricSparseModelType> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getModel() const {
|
|
return this->model;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
std::shared_ptr<storm::logic::OperatorFormula> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormula() const {
|
|
return this->specifiedFormula;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
|
|
return storm::utility::region::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifiedFormulaHasLowerBound() const {
|
|
return storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType());
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
bool const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isComputeRewards() const {
|
|
return computeRewards;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
bool const SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isResultConstant() const {
|
|
return this->constantResult.operator bool();
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
std::shared_ptr<ParametricSparseModelType> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSimpleModel() const {
|
|
return this->simpleModel;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
std::shared_ptr<storm::logic::OperatorFormula> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSimpleFormula() const {
|
|
return this->simpleFormula;
|
|
}
|
|
|
|
// template<typename ParametricSparseModelType, typename ConstantType>
|
|
// SparseRegionModelCheckerSettings& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSettings() {
|
|
// return this->settings;
|
|
// };
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
SparseRegionModelCheckerSettings const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSettings() const {
|
|
return this->settings;
|
|
};
|
|
|
|
|
|
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifyFormula(std::shared_ptr<const storm::logic::Formula> formula) {
|
|
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now();
|
|
STORM_LOG_DEBUG("Specifying the formula " << *formula.get());
|
|
STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled.");
|
|
//Initialize the context for this formula
|
|
if (formula->isProbabilityOperatorFormula()) {
|
|
this->specifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula->asProbabilityOperatorFormula());
|
|
this->computeRewards = false;
|
|
}
|
|
else if (formula->isRewardOperatorFormula()) {
|
|
this->specifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->asRewardOperatorFormula());
|
|
this->computeRewards=true;
|
|
}
|
|
else {
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The specified property " << this->getSpecifiedFormula() << "is not supported");
|
|
}
|
|
this->constantResult = boost::none;
|
|
this->simpleFormula = nullptr;
|
|
this->isApproximationApplicable = false;
|
|
this->approximationModel = nullptr;
|
|
this->samplingModel = nullptr;
|
|
//stuff for statistics:
|
|
this->numOfCheckedRegions=0;
|
|
this->numOfRegionsSolvedThroughSampling=0;
|
|
this->numOfRegionsSolvedThroughApproximation=0;
|
|
this->numOfRegionsSolvedThroughSmt=0;
|
|
this->numOfRegionsExistsBoth=0;
|
|
this->numOfRegionsAllSat=0;
|
|
this->numOfRegionsAllViolated=0;
|
|
this->timeCheckRegion=std::chrono::high_resolution_clock::duration::zero();
|
|
this->timeSampling=std::chrono::high_resolution_clock::duration::zero();
|
|
this->timeApproximation=std::chrono::high_resolution_clock::duration::zero();
|
|
this->timeSmt=std::chrono::high_resolution_clock::duration::zero();
|
|
this->timeComputeReachabilityFunction=std::chrono::high_resolution_clock::duration::zero();
|
|
|
|
|
|
std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now();
|
|
this->preprocess(this->simpleModel, this->simpleFormula, isApproximationApplicable, constantResult);
|
|
std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
|
|
|
|
//TODO: Currently we are not able to detect functions of the form p*q correctly as these functions are not linear but approximation is still applicable.
|
|
//This is just a quick fix to work with such models anyway.
|
|
if(!this->isApproximationApplicable){
|
|
STORM_LOG_ERROR("There are non-linear functions that occur in the given model. Approximation is still correct for functions that are linear w.r.t. a single parameter (assuming the remaining parameters are constants), e.g., p*q is okay. Currently, the implementation is not able to validate this..");
|
|
this->isApproximationApplicable=true;
|
|
}
|
|
|
|
//Check if the approximation and the sampling model needs to be computed
|
|
if(!this->isResultConstant()){
|
|
if(this->isApproximationApplicable && settings.doApprox()){
|
|
initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula());
|
|
}
|
|
if(settings.getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE ||
|
|
(!settings.doSample() && settings.getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
|
|
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
|
|
}
|
|
} else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){
|
|
//In this case, the result is constant but has not been computed yet. so do it now!
|
|
STORM_LOG_DEBUG("The Result is constant and will be computed now.");
|
|
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
|
|
std::map<VariableType, CoefficientType> emptySubstitution;
|
|
this->constantResult = this->getSamplingModel()->computeInitialStateValue(emptySubstitution);
|
|
}
|
|
|
|
//some more information for statistics...
|
|
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now();
|
|
this->timeSpecifyFormula= timeSpecifyFormulaEnd - timeSpecifyFormulaStart;
|
|
this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart;
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula> formula) {
|
|
std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now();
|
|
STORM_LOG_DEBUG("Initializing the Approximation Model...");
|
|
STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Approximation model requested but approximation is not applicable");
|
|
this->approximationModel=std::make_shared<ApproximationModel<ParametricSparseModelType, ConstantType>>(model, formula);
|
|
std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now();
|
|
this->timeInitApproxModel=timeInitApproxModelEnd - timeInitApproxModelStart;
|
|
STORM_LOG_DEBUG("Initialized Approximation Model");
|
|
}
|
|
|
|
template<typename ParametricSparseModelType, typename ConstantType>
|
|
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula> formula) {
|
|
STORM_LOG_DEBUG("Initializing the Sampling Model....");
|
|
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
|
|
this->samplingModel=std::make_shared<SamplingModel<ParametricSparseModelType, ConstantType>>(model, formula);
|
|
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock:
|