sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

adapted region model checkers to new parameterLiftingModelChecker

tempestpy_adaptions
TimQu 8 years ago
parent
c5ebfb74fb
commit
074a1d93a3
6 changed files with 56 additions and 21 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 19
      src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  2. 7
      src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h
  3. 7
      src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
  4. 4
      src/storm/modelchecker/region/SparseMdpRegionModelChecker.h
  5. 18
      src/storm/modelchecker/region/SparseRegionModelChecker.cpp
  6. 22
      src/storm/modelchecker/region/SparseRegionModelChecker.h

19
src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
View File

@ -3,6 +3,7 @@
#include <chrono>
#include <memory>
#include <boost/optional.hpp>
#include <storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h>
#include "storm/adapters/CarlAdapter.h"
#include "storm/logic/Formulas.h"
@ -33,6 +34,7 @@
#include "storm/transformer/SparseParametricDtmcSimplifier.h"
#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
namespace storm {
namespace modelchecker {
@ -427,6 +429,23 @@ namespace storm {
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Sampling Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
STORM_LOG_DEBUG("Initializing the Approx Model....");
std::chrono::high_resolution_clock::time_point timeInitApproximationModelStart = std::chrono::high_resolution_clock::now();
this->approximationModel = std::make_shared<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>>(model);
// replace bounds by optimization direction to obtain a quantitative formula
if(formula->isProbabilityOperatorFormula()) {
auto quantitativeFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
} else {
auto quantitativeFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
}
std::chrono::high_resolution_clock::time_point timeInitApproximationModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Approximation Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::computeReachabilityFunction(storm::models::sparse::Dtmc<ParametricType> const& simpleModel){

7
src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h
View File

@ -62,6 +62,13 @@ namespace storm {
*/
virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
/*!
* initializes the Approx Model
*/
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
private:
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and

7
src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
View File

@ -316,6 +316,13 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkSmt invoked but smt solving has not been implemented for MDPs.");
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
std::cout << "approx model for mdps not implemented" << std::endl;
}
#ifdef STORM_HAVE_CARL
template class SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
#endif

4
src/storm/modelchecker/region/SparseMdpRegionModelChecker.h
View File

@ -85,6 +85,10 @@ namespace storm {
* initializes the Sampling Model
*/
virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
/*!
* initializes the Approx Model
*/
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
};
} //namespace region

18
src/storm/modelchecker/region/SparseRegionModelChecker.cpp
View File

@ -19,6 +19,9 @@
#include "storm/exceptions/UnexpectedException.h"
#include "modelchecker/results/CheckResult.h"
#include "modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/parametric/ParameterRegion.h"
namespace storm {
namespace modelchecker {
@ -191,17 +194,6 @@ namespace storm {
this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> 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>::checkRegions(std::vector<ParameterRegion<ParametricType>>& regions) {
STORM_LOG_DEBUG("Checking " << regions.size() << "regions.");
@ -408,12 +400,12 @@ namespace storm {
return (proveAllSat==this->checkFormulaOnSamplingPoint(region.getSomePoint()));
}
bool computeLowerBounds = (this->specifiedFormulaHasLowerBound() && proveAllSat) || (!this->specifiedFormulaHasLowerBound() && !proveAllSat);
bool formulaSatisfied = this->getApproximationModel()->checkFormulaOnRegion(region, computeLowerBounds);
bool formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximationModel()->check(storm::modelchecker::parametric::ParameterRegion<typename ParametricSparseModelType::ValueType>(region.getLowerBoundaries(), region.getUpperBoundaries()), computeLowerBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->simpleModel->getInitialStates().begin()]);
return (proveAllSat==formulaSatisfied);
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getApproximationModel() {
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getApproximationModel() {
if(this->approximationModel==nullptr){
STORM_LOG_WARN("Approximation model requested but it has not been initialized when specifying the formula. Will initialize it now.");
initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula());

22
src/storm/modelchecker/region/SparseRegionModelChecker.h
View File

@ -2,12 +2,15 @@
#include <ostream>
#include <boost/optional.hpp>
#include <storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h>
#include "storm/utility/region.h"
#include "storm/modelchecker/region/AbstractSparseRegionModelChecker.h"
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/modelchecker/region/ApproximationModel.h"
#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Model.h"
@ -39,7 +42,7 @@ namespace storm {
storm::settings::modules::RegionSettings::ApproxMode approxMode;
storm::settings::modules::RegionSettings::SmtMode smtMode;
};
template<typename ParametricSparseModelType, typename ConstantType>
class SparseRegionModelChecker : public AbstractSparseRegionModelChecker<typename ParametricSparseModelType::ValueType, ConstantType> {
public:
@ -191,7 +194,7 @@ namespace storm {
* Returns the approximation model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> const& getApproximationModel();
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> const& getApproximationModel();
/*!
* Checks the value of the function at some sampling points within the given region.
@ -240,13 +243,18 @@ namespace storm {
// the model that can be instantiated to check the value at a certain point
std::shared_ptr<storm::modelchecker::parametric::SparseInstantiationModelChecker<ParametricSparseModelType, ConstantType>> samplingModel;
private:
/*!
/*!
* initializes the Approximation Model
*
*
* @note does not check whether approximation can be applied
*/
void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula);
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) = 0;
// the model that is used to approximate the reachability values
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> approximationModel;
private:
// The model this model checker is supposed to analyze.
@ -261,8 +269,6 @@ namespace storm {
std::shared_ptr<storm::logic::OperatorFormula const> simpleFormula;
// a flag that is true if approximation is applicable, i.e., there are only linear functions at transitions of the model
bool isApproximationApplicable;
// the model that is used to approximate the reachability values
std::shared_ptr<ApproximationModel<ParametricSparseModelType, ConstantType>> approximationModel;
// a flag that is true iff the resulting reachability function is constant
boost::optional<ConstantType> constantResult;

Write Preview
Loading…
Cancel
Save