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

Clean up assumption checker

tempestpy_adaptions
Jip Spel 6 years ago
parent
0d1ddb6232
commit
3ebd5f0bf6
2 changed files with 92 additions and 94 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 147
      src/storm-pars/analysis/AssumptionChecker.cpp
  2. 39
      src/storm-pars/analysis/AssumptionChecker.h

147
src/storm-pars/analysis/AssumptionChecker.cpp
View File

@ -23,39 +23,37 @@
namespace storm { namespace storm {
namespace analysis { namespace analysis {
template <typename ValueType> 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) {
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
this->formula = formula; this->formula = formula;
this->matrix = model->getTransitionMatrix(); this->matrix = model->getTransitionMatrix();
// Create sample points // Create sample points
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model);
auto instantiator = utility::ModelInstantiator<models::sparse::Dtmc<ValueType>, models::sparse::Dtmc<double>>(*model);
auto matrix = model->getTransitionMatrix(); auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model);
// TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again
for (auto i = 0; i < numberOfSamples; ++i) { for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>();
auto valuation = utility::parametric::Valuation<ValueType>();
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
// TODO: Type
// Creates samples between 0 and 1, 1/(#samples+2), 2/(#samples+2), ..., (#samples+1)/(#samples+2) // Creates samples between 0 and 1, 1/(#samples+2), 2/(#samples+2), ..., (#samples+1)/(#samples+2)
auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 2)))));
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>((*itr), utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 2)))));
valuation.insert(val); 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;
models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
auto checker = modelchecker::SparseDtmcPrctlModelChecker<models::sparse::Dtmc<double>>(sampleModel);
std::unique_ptr<modelchecker::CheckResult> checkResult;
if (formula->isProbabilityOperatorFormula() && if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
const storm::modelchecker::CheckTask<storm::logic::UntilFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::UntilFormula, double>(
const modelchecker::CheckTask<logic::UntilFormula, double> checkTask = modelchecker::CheckTask<logic::UntilFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula());
checkResult = checker.computeUntilProbabilities(Environment(), checkTask); checkResult = checker.computeUntilProbabilities(Environment(), checkTask);
} else if (formula->isProbabilityOperatorFormula() && } else if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) {
const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double>(
const modelchecker::CheckTask<logic::EventuallyFormula, double> checkTask = modelchecker::CheckTask<logic::EventuallyFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula());
checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask);
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
STORM_LOG_THROW(false, exceptions::NotSupportedException,
"Expecting until or eventually formula"); "Expecting until or eventually formula");
} }
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>(); auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
@ -65,38 +63,37 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) {
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) {
this->formula = formula; this->formula = formula;
this->matrix = model->getTransitionMatrix(); this->matrix = model->getTransitionMatrix();
// Create sample points // Create sample points
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model);
auto instantiator = utility::ModelInstantiator<models::sparse::Mdp<ValueType>, models::sparse::Mdp<double>>(*model);
auto matrix = model->getTransitionMatrix(); auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model);
// TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again
for (auto i = 0; i < numberOfSamples; ++i) { for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>();
auto valuation = utility::parametric::Valuation<ValueType>();
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
// TODO: Type
auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type,
typename utility::parametric::CoefficientType<ValueType>::type>((*itr), utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} }
storm::models::sparse::Mdp<double> sampleModel = instantiator.instantiate(valuation);
auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>(sampleModel);
std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
models::sparse::Mdp<double> sampleModel = instantiator.instantiate(valuation);
auto checker = modelchecker::SparseMdpPrctlModelChecker<models::sparse::Mdp<double>>(sampleModel);
std::unique_ptr<modelchecker::CheckResult> checkResult;
if (formula->isProbabilityOperatorFormula() && if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
const storm::modelchecker::CheckTask<storm::logic::UntilFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::UntilFormula, double>(
const modelchecker::CheckTask<logic::UntilFormula, double> checkTask = modelchecker::CheckTask<logic::UntilFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula());
checkResult = checker.computeUntilProbabilities(Environment(), checkTask); checkResult = checker.computeUntilProbabilities(Environment(), checkTask);
} else if (formula->isProbabilityOperatorFormula() && } else if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) {
const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double>(
const modelchecker::CheckTask<logic::EventuallyFormula, double> checkTask = modelchecker::CheckTask<logic::EventuallyFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula());
checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask);
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
STORM_LOG_THROW(false, exceptions::NotSupportedException,
"Expecting until or eventually formula"); "Expecting until or eventually formula");
} }
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>(); auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
@ -106,16 +103,16 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
AssumptionStatus AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<expressions::BinaryRelationExpression> assumption) {
auto result = AssumptionStatus::UNKNOWN; auto result = AssumptionStatus::UNKNOWN;
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
std::set<expressions::Variable> vars = std::set<expressions::Variable>({});
assumption->gatherVariables(vars); assumption->gatherVariables(vars);
for (auto itr = samples.begin(); result == AssumptionStatus::UNKNOWN && itr != samples.end(); ++itr) { for (auto itr = samples.begin(); result == AssumptionStatus::UNKNOWN && itr != samples.end(); ++itr) {
std::shared_ptr<storm::expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer();
auto valuation = storm::expressions::SimpleValuation(manager);
std::shared_ptr<expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer();
auto valuation = expressions::SimpleValuation(manager);
auto values = (*itr); auto values = (*itr);
for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) { for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) {
storm::expressions::Variable par = *var;
expressions::Variable par = *var;
auto index = std::stoi(par.getName()); auto index = std::stoi(par.getName());
valuation.setRationalValue(par, values[index]); valuation.setRationalValue(par, values[index]);
} }
@ -128,22 +125,22 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice) {
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice) {
// First check if based on sample points the assumption can be discharged // First check if based on sample points the assumption can be discharged
auto result = checkOnSamples(assumption); auto result = checkOnSamples(assumption);
assert (result != storm::analysis::AssumptionStatus::VALID);
assert (result != AssumptionStatus::VALID);
if (result == storm::analysis::AssumptionStatus::UNKNOWN) {
if (result == AssumptionStatus::UNKNOWN) {
// If result from sample checking was unknown, the assumption might hold, so we continue, // If result from sample checking was unknown, the assumption might hold, so we continue,
// otherwise we return INVALID // otherwise we return INVALID
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
std::set<expressions::Variable> vars = std::set<expressions::Variable>({});
assumption->gatherVariables(vars); assumption->gatherVariables(vars);
STORM_LOG_THROW(assumption->getRelationType() == STORM_LOG_THROW(assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Greater ||
expressions::BinaryRelationExpression::RelationType::Greater ||
assumption->getRelationType() == assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Equal,
storm::exceptions::NotSupportedException,
expressions::BinaryRelationExpression::RelationType::Equal,
exceptions::NotSupportedException,
"Only Greater Or Equal assumptions supported"); "Only Greater Or Equal assumptions supported");
// Row with successors of the first state // Row with successors of the first state
@ -168,13 +165,13 @@ namespace storm {
} }
if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) {
if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater
&& lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != storm::analysis::Lattice::UNKNOWN) {
if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater
&& lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Lattice::UNKNOWN) {
// The assumption should be the greater assumption // The assumption should be the greater assumption
// If the result is unknown, we cannot compare, also SMTSolver will not help // If the result is unknown, we cannot compare, also SMTSolver will not help
result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1,
state2succ2); state2succ2);
} else if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) {
} else if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Equal) {
// The assumption is equal, the successors are the same, // 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 // so if the probability of reaching the successors is the same, we have a valid assumption
if (state1succ1->getValue() == state2succ1->getValue()) { if (state1succ1->getValue() == state2succ1->getValue()) {
@ -184,21 +181,21 @@ namespace storm {
result = AssumptionStatus::UNKNOWN; result = AssumptionStatus::UNKNOWN;
} }
} else { } else {
result = validateAssumptionSMTSolver(lattice, assumption);
result = validateAssumptionSMTSolver(assumption, lattice);
} }
} else { } else {
result = validateAssumptionSMTSolver(lattice, assumption);
result = validateAssumptionSMTSolver(assumption, lattice);
} }
} }
return result; return result;
} }
template <typename ValueType> template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2) {
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(Lattice* lattice,
typename storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storage::SparseMatrix<ValueType>::iterator state2succ2) {
assert((state1succ1->getColumn() == state2succ1->getColumn() assert((state1succ1->getColumn() == state2succ1->getColumn()
&& state1succ2->getColumn() == state2succ2->getColumn()) && state1succ2->getColumn() == state2succ2->getColumn())
|| (state1succ1->getColumn() == state2succ2->getColumn() || (state1succ1->getColumn() == state2succ2->getColumn()
@ -209,10 +206,10 @@ namespace storm {
// Calculate the difference in probability for the "highest" successor state // Calculate the difference in probability for the "highest" successor state
ValueType prob; ValueType prob;
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn());
assert (comp == storm::analysis::Lattice::ABOVE || comp == storm::analysis::Lattice::BELOW);
if (comp == storm::analysis::Lattice::ABOVE) {
assert (comp == Lattice::ABOVE || comp == Lattice::BELOW);
if (comp == Lattice::ABOVE) {
prob = state1succ1->getValue() - state2succ1->getValue(); prob = state1succ1->getValue() - state2succ1->getValue();
} else if (comp == storm::analysis::Lattice::BELOW) {
} else if (comp == Lattice::BELOW) {
prob = state1succ2->getValue() - state2succ2->getValue(); prob = state1succ2->getValue() - state2succ2->getValue();
} }
@ -220,8 +217,7 @@ namespace storm {
// If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions // If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions
// This will give the smallest result // This will give the smallest result
// TODO: Type
std::map<storm::RationalFunctionVariable, typename ValueType::CoeffType> substitutions;
std::map<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type> substitutions;
for (auto var : vars) { for (auto var : vars) {
auto monotonicity = MonotonicityChecker<ValueType>::checkDerivative(prob.derivative(var)); auto monotonicity = MonotonicityChecker<ValueType>::checkDerivative(prob.derivative(var));
if (monotonicity.first) { if (monotonicity.first) {
@ -243,9 +239,9 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice) {
std::shared_ptr<utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<utility::solver::MathsatSmtSolverFactory>();
std::shared_ptr<expressions::ExpressionManager> manager(new expressions::ExpressionManager());
AssumptionStatus result; AssumptionStatus result;
auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName();
@ -256,8 +252,8 @@ namespace storm {
bool orderKnown = true; bool orderKnown = true;
// Check if the order between the different successors is known // Check if the order between the different successors is known
// Also start creating expression for order of states // Also start creating expression for order of states
storm::expressions::Expression exprOrderSucc = manager->boolean(true);
std::set<storm::expressions::Variable> stateVariables;
expressions::Expression exprOrderSucc = manager->boolean(true);
std::set<expressions::Variable> stateVariables;
for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) {
auto varname1 = "s" + std::to_string(itr1->getColumn()); auto varname1 = "s" + std::to_string(itr1->getColumn());
if (!manager->hasVariable(varname1)) { if (!manager->hasVariable(varname1)) {
@ -270,13 +266,13 @@ namespace storm {
stateVariables.insert(manager->declareRationalVariable(varname2)); stateVariables.insert(manager->declareRationalVariable(varname2));
} }
auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn()); auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn());
if (comp == storm::analysis::Lattice::ABOVE) {
if (comp == Lattice::ABOVE) {
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <=
manager->getVariable(varname2)); manager->getVariable(varname2));
} else if (comp == storm::analysis::Lattice::BELOW) {
} else if (comp == Lattice::BELOW) {
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >=
manager->getVariable(varname2)); manager->getVariable(varname2));
} else if (comp == storm::analysis::Lattice::SAME) {
} else if (comp == Lattice::SAME) {
exprOrderSucc = exprOrderSucc && exprOrderSucc = exprOrderSucc &&
(manager->getVariable(varname1) = manager->getVariable(varname2)); (manager->getVariable(varname1) = manager->getVariable(varname2));
} else { } else {
@ -287,41 +283,39 @@ namespace storm {
} }
if (orderKnown) { if (orderKnown) {
storm::solver::Z3SmtSolver s(*manager);
auto valueTypeToExpression = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::expressions::Expression expr1 = manager->rational(0);
solver::Z3SmtSolver s(*manager);
auto valueTypeToExpression = expressions::RationalFunctionToExpression<ValueType>(manager);
expressions::Expression expr1 = manager->rational(0);
for (auto itr1 = row1.begin(); itr1 != row1.end(); ++itr1) { for (auto itr1 = row1.begin(); itr1 != row1.end(); ++itr1) {
expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable("s" + std::to_string(itr1->getColumn()))); expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable("s" + std::to_string(itr1->getColumn())));
} }
storm::expressions::Expression expr2 = manager->rational(0);
expressions::Expression expr2 = manager->rational(0);
for (auto itr2 = row2.begin(); itr2 != row2.end(); ++itr2) { for (auto itr2 = row2.begin(); itr2 != row2.end(); ++itr2) {
expr2 = expr2 + (valueTypeToExpression.toExpression(itr2->getValue()) * manager->getVariable("s" + std::to_string(itr2->getColumn()))); 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 // Create expression for the assumption based on the relation to successors
// It is the negation of actual assumption // It is the negation of actual assumption
// TODO: use same manager s.t. assumption can be used directly ?
storm::expressions::Expression exprToCheck ;
expressions::Expression exprToCheck ;
if (assumption->getRelationType() == if (assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Greater) {
expressions::BinaryRelationExpression::RelationType::Greater) {
exprToCheck = expr1 <= expr2; exprToCheck = expr1 <= expr2;
} else { } else {
assert (assumption->getRelationType() == assert (assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Equal);
expressions::BinaryRelationExpression::RelationType::Equal);
exprToCheck = expr1 > expr2; exprToCheck = expr1 > expr2;
} }
auto variables = manager->getVariables(); auto variables = manager->getVariables();
// Bounds for the state probabilities and parameters // Bounds for the state probabilities and parameters
storm::expressions::Expression exprBounds = manager->boolean(true);
expressions::Expression exprBounds = manager->boolean(true);
for (auto var : variables) { for (auto var : variables) {
if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) { if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) {
// the var is a state // the var is a state
exprBounds = exprBounds && manager->rational(0) <= var && var <= manager->rational(1); exprBounds = exprBounds && manager->rational(0) <= var && var <= manager->rational(1);
} else { } else {
// the var is a parameter // the var is a parameter
// TODO: graph-preserving
exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1); exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
} }
} }
@ -329,15 +323,14 @@ namespace storm {
s.add(exprOrderSucc); s.add(exprOrderSucc);
s.add(exprBounds); s.add(exprBounds);
// assert that sorting of successors in the lattice and the bounds on the expression are at least satisfiable // assert that sorting of successors in the lattice and the bounds on the expression are at least satisfiable
assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat);
// TODO: kijken of t SAT moet zijn?
assert (s.check() == solver::SmtSolver::CheckResult::Sat);
s.add(exprToCheck); s.add(exprToCheck);
auto smtRes = s.check(); auto smtRes = s.check();
if (smtRes == storm::solver::SmtSolver::CheckResult::Unsat) {
if (smtRes == solver::SmtSolver::CheckResult::Unsat) {
// If there is no thing satisfying the negation we are safe. // If there is no thing satisfying the negation we are safe.
result = AssumptionStatus::VALID; result = AssumptionStatus::VALID;
} else if (smtRes == storm::solver::SmtSolver::CheckResult::Sat) {
assert (smtRes == storm::solver::SmtSolver::CheckResult::Sat);
} else if (smtRes == solver::SmtSolver::CheckResult::Sat) {
assert (smtRes == solver::SmtSolver::CheckResult::Sat);
result = AssumptionStatus::INVALID; result = AssumptionStatus::INVALID;
} else { } else {
result = AssumptionStatus::UNKNOWN; result = AssumptionStatus::UNKNOWN;
@ -349,6 +342,6 @@ namespace storm {
return result; return result;
} }
template class AssumptionChecker<storm::RationalFunction>;
template class AssumptionChecker<RationalFunction>;
} }
} }

39
src/storm-pars/analysis/AssumptionChecker.h
View File

@ -14,6 +14,9 @@
namespace storm { namespace storm {
namespace analysis { namespace analysis {
/*!
* Constants for status of assumption
*/
enum AssumptionStatus { enum AssumptionStatus {
VALID, VALID,
INVALID, INVALID,
@ -22,10 +25,6 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
class AssumptionChecker { class AssumptionChecker {
public: public:
/*!
* Constants for status of assumption
*/
/*! /*!
* Constructs an AssumptionChecker based on the number of samples, for the given formula and model. * Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
@ -34,7 +33,7 @@ namespace storm {
* @param model The dtmc model to check the formula on. * @param model The dtmc model to check the formula on.
* @param numberOfSamples Number of sample points. * @param numberOfSamples Number of sample points.
*/ */
AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
/*! /*!
* Constructs an AssumptionChecker based on the number of samples, for the given formula and model. * Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
@ -43,7 +42,7 @@ namespace storm {
* @param model The mdp model to check the formula on. * @param model The mdp model to check the formula on.
* @param numberOfSamples Number of sample points. * @param numberOfSamples Number of sample points.
*/ */
AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
/*! /*!
* Checks if the assumption holds at the sample points of the AssumptionChecker. * Checks if the assumption holds at the sample points of the AssumptionChecker.
@ -51,7 +50,7 @@ namespace storm {
* @param assumption The assumption to check. * @param assumption The assumption to check.
* @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID * @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID
*/ */
AssumptionStatus checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
AssumptionStatus checkOnSamples(std::shared_ptr<expressions::BinaryRelationExpression> assumption);
/*! /*!
* Tries to validate an assumption based on the lattice and underlying transition matrix. * Tries to validate an assumption based on the lattice and underlying transition matrix.
@ -60,25 +59,31 @@ namespace storm {
* @param lattice The lattice. * @param lattice The lattice.
* @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID
*/ */
AssumptionStatus validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice);
AssumptionStatus validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice);
AssumptionStatus validateAssumptionSMTSolver(storm::analysis::Lattice* lattice,
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
/*!
* Tries to validate an assumption based on the lattice, and SMT solving techniques
*
* @param assumption The assumption to validate.
* @param lattice The lattice.
* @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID
*/
AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice);
private: private:
std::shared_ptr<storm::logic::Formula const> formula;
std::shared_ptr<logic::Formula const> formula;
storm::storage::SparseMatrix<ValueType> matrix;
storage::SparseMatrix<ValueType> matrix;
std::vector<std::vector<double>> samples; std::vector<std::vector<double>> samples;
void createSamples(); void createSamples();
AssumptionStatus validateAssumptionFunction(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2);
AssumptionStatus validateAssumptionFunction(Lattice* lattice,
typename storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storage::SparseMatrix<ValueType>::iterator state2succ2);
}; };
} }

Write Preview
Loading…
Cancel
Save