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.
78 lines
4.8 KiB
78 lines
4.8 KiB
//
|
|
// Created by Jip Spel on 12.09.18.
|
|
//
|
|
#include "AssumptionChecker.h"
|
|
|
|
#include "storm-pars/utility/ModelInstantiator.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/results/CheckResult.h"
|
|
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|
#include "storm/storage/expressions/SimpleValuation.h"
|
|
#include "storm/storage/expressions/ExpressionManager.h"
|
|
|
|
namespace storm {
|
|
namespace analysis {
|
|
template <typename ValueType>
|
|
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
|
|
this->formula = formula;
|
|
|
|
// Create sample points
|
|
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model.get());
|
|
auto matrix = model->getTransitionMatrix();
|
|
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
|
|
for (auto i = 0; i < numberOfSamples; ++i) {
|
|
auto valuation = storm::utility::parametric::Valuation<ValueType>();
|
|
for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
|
|
auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
|
|
valuation.insert(val);
|
|
}
|
|
storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
|
|
auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>(sampleModel);
|
|
std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
|
|
if (formula->isProbabilityOperatorFormula() &&
|
|
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
|
|
const storm::modelchecker::CheckTask<storm::logic::UntilFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::UntilFormula, double>(
|
|
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula());
|
|
checkResult = checker.computeUntilProbabilities(Environment(), checkTask);
|
|
} else if (formula->isProbabilityOperatorFormula() &&
|
|
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) {
|
|
const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double>(
|
|
(*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<double>();
|
|
std::vector<double> values = quantitativeResult.getValueVector();
|
|
results.push_back(values);
|
|
}
|
|
}
|
|
|
|
template <typename ValueType>
|
|
bool AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
|
|
bool result = true;
|
|
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
|
|
assumption->gatherVariables(vars);
|
|
for (auto itr = results.begin(); result && itr != results.end(); ++itr) {
|
|
std::shared_ptr<storm::expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer();
|
|
auto valuation = storm::expressions::SimpleValuation(manager);
|
|
auto values = (*itr);
|
|
for (auto var = vars.begin(); result && var != vars.end(); ++var) {
|
|
storm::expressions::Variable par = *var;
|
|
auto index = std::stoi(par.getName());
|
|
valuation.setRationalValue(par, values[index]);
|
|
}
|
|
assert(assumption->hasBooleanType());
|
|
result &= assumption->evaluateAsBool(&valuation);
|
|
}
|
|
return result;
|
|
}
|
|
|
|
template class AssumptionChecker<storm::RationalFunction>;
|
|
}
|
|
}
|