TimQu
6 years ago
42 changed files with 4524 additions and 139 deletions
-
1CHANGELOG.md
-
17resources/examples/testfiles/pdtmc/simple1.pm
-
17resources/examples/testfiles/pdtmc/simple2.pm
-
18resources/examples/testfiles/pdtmc/simple3.pm
-
17resources/examples/testfiles/pdtmc/simple4.pm
-
17src/storm-cli-utilities/model-handling.h
-
337src/storm-pars-cli/storm-pars.cpp
-
354src/storm-pars/analysis/AssumptionChecker.cpp
-
90src/storm-pars/analysis/AssumptionChecker.h
-
67src/storm-pars/analysis/AssumptionMaker.cpp
-
51src/storm-pars/analysis/AssumptionMaker.h
-
692src/storm-pars/analysis/MonotonicityChecker.cpp
-
154src/storm-pars/analysis/MonotonicityChecker.h
-
379src/storm-pars/analysis/Order.cpp
-
247src/storm-pars/analysis/Order.h
-
490src/storm-pars/analysis/OrderExtender.cpp
-
83src/storm-pars/analysis/OrderExtender.h
-
14src/storm-pars/api/region.h
-
5src/storm-pars/settings/ParsSettings.cpp
-
54src/storm-pars/settings/modules/MonotonicitySettings.cpp
-
60src/storm-pars/settings/modules/MonotonicitySettings.h
-
2src/storm-pars/settings/modules/ParametricSettings.cpp
-
4src/storm-pars/settings/modules/ParametricSettings.h
-
20src/storm-pars/storage/ParameterRegion.cpp
-
2src/storm-pars/storage/ParameterRegion.h
-
12src/storm/api/transformation.h
-
3src/storm/generator/PrismNextStateGenerator.cpp
-
6src/storm/settings/modules/IOSettings.cpp
-
6src/storm/settings/modules/IOSettings.h
-
11src/storm/settings/modules/TransformationSettings.cpp
-
11src/storm/settings/modules/TransformationSettings.h
-
42src/storm/solver/stateelimination/EliminatorBase.cpp
-
4src/storm/solver/stateelimination/EliminatorBase.h
-
67src/storm/storage/expressions/RationalFunctionToExpression.cpp
-
40src/storm/storage/expressions/RationalFunctionToExpression.h
-
2src/test/storm-pars/CMakeLists.txt
-
373src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
-
319src/test/storm-pars/analysis/AssumptionMakerTest.cpp
-
206src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
-
93src/test/storm-pars/analysis/OrderExtenderTest.cpp
-
173src/test/storm-pars/analysis/OrderTest.cpp
-
103src/test/storm/storage/ExpressionTest.cpp
@ -0,0 +1,17 @@ |
|||
dtmc |
|||
|
|||
const double p; |
|||
|
|||
module test |
|||
|
|||
// local state |
|||
s : [0..4] init 0; |
|||
|
|||
[] s=0 -> p : (s'=1) + (1-p) : (s'=2); |
|||
[] s=1 -> p : (s'=3) + (1-p) : (s'=4); |
|||
[] s=2 -> p : (s'=4) + (1-p) : (s'=3); |
|||
[] s=3 -> 1 : (s'=3); |
|||
[] s=4 -> 1 : (s'=4); |
|||
|
|||
endmodule |
|||
|
|||
@ -0,0 +1,17 @@ |
|||
dtmc |
|||
|
|||
const double p; |
|||
|
|||
module test |
|||
|
|||
// local state |
|||
s : [0..4] init 0; |
|||
|
|||
[] s=0 -> p : (s'=1) + (1-p) : (s'=2); |
|||
[] s=1 -> p : (s'=3) + (1-p) : (s'=4); |
|||
[] s=2 -> 0.5*p : (s'=3) + (1-0.5*p) : (s'=4); |
|||
[] s=3 -> 1 : (s'=3); |
|||
[] s=4 -> 1 : (s'=4); |
|||
|
|||
endmodule |
|||
|
|||
@ -0,0 +1,18 @@ |
|||
dtmc |
|||
|
|||
const double p; |
|||
|
|||
module test |
|||
|
|||
// local state |
|||
s : [0..5] init 0; |
|||
|
|||
[] s=0 -> 0.4*p : (s'=1) + (1-p) : (s'=2) + 0.6*p : (s'=3); |
|||
[] s=1 -> 0.5*p : (s'=4) + 0.5*p : (s'=3) + (1-p) : (s'=5); |
|||
[] s=2 -> 0.3*p : (s'=4) + (1-0.3*p) : (s'=5); |
|||
[] s=3 -> 0.7*p : (s'=4) + (1-0.7*p) : (s'=5); |
|||
[] s=4 -> 1 : (s'=4); |
|||
[] s=5 -> 1 : (s'=5); |
|||
|
|||
endmodule |
|||
|
|||
@ -0,0 +1,17 @@ |
|||
dtmc |
|||
|
|||
const double p; |
|||
|
|||
module test |
|||
|
|||
// local state |
|||
s : [0..4] init 0; |
|||
|
|||
[] s=0 -> p*(1-p) : (s'=1) + (1-p*(1-p)) : (s'=2); |
|||
[] s=1 -> p : (s'=3) + (1-p) : (s'=4); |
|||
[] s=2 -> (1-p) : (s'=3) + (p) : (s'=4); |
|||
[] s=3 -> 1 : (s'=3); |
|||
[] s=4 -> 1 : (s'=4); |
|||
|
|||
endmodule |
|||
|
|||
@ -0,0 +1,354 @@ |
|||
#include <storm/solver/Z3SmtSolver.h>
|
|||
#include "AssumptionChecker.h"
|
|||
|
|||
#include "storm-pars/utility/ModelInstantiator.h"
|
|||
#include "storm-pars/analysis/MonotonicityChecker.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/prctl/SparseMdpPrctlModelChecker.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"
|
|||
#include "storm/storage/expressions/VariableExpression.h"
|
|||
#include "storm/storage/expressions/RationalFunctionToExpression.h"
|
|||
#include "storm/utility/constants.h"
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
template <typename ValueType> |
|||
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Dtmc<ValueType>> model, storm::storage::ParameterRegion<ValueType> region, uint_fast64_t numberOfSamples) { |
|||
this->formula = formula; |
|||
this->matrix = model->getTransitionMatrix(); |
|||
this->region = region; |
|||
|
|||
// Create sample points
|
|||
auto instantiator = utility::ModelInstantiator<models::sparse::Dtmc<ValueType>, models::sparse::Dtmc<double>>(*model); |
|||
auto matrix = model->getTransitionMatrix(); |
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model); |
|||
|
|||
for (uint_fast64_t i = 0; i < numberOfSamples; ++i) { |
|||
auto valuation = utility::parametric::Valuation<ValueType>(); |
|||
for (auto var: variables) { |
|||
auto lb = region.getLowerBoundary(var.name()); |
|||
auto ub = region.getUpperBoundary(var.name()); |
|||
// Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub
|
|||
auto val = |
|||
std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type> |
|||
(var,utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb + i*(ub-lb)/(numberOfSamples-1))); |
|||
valuation.insert(val); |
|||
} |
|||
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() && |
|||
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { |
|||
const modelchecker::CheckTask<logic::UntilFormula, double> checkTask = modelchecker::CheckTask<logic::UntilFormula, double>( |
|||
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); |
|||
checkResult = checker.computeUntilProbabilities(Environment(), checkTask); |
|||
} else if (formula->isProbabilityOperatorFormula() && |
|||
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { |
|||
const modelchecker::CheckTask<logic::EventuallyFormula, double> checkTask = modelchecker::CheckTask<logic::EventuallyFormula, double>( |
|||
(*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); |
|||
checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); |
|||
} else { |
|||
STORM_LOG_THROW(false, exceptions::NotSupportedException, |
|||
"Expecting until or eventually formula"); |
|||
} |
|||
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>(); |
|||
std::vector<double> values = quantitativeResult.getValueVector(); |
|||
samples.push_back(values); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) { |
|||
STORM_LOG_THROW(false, exceptions::NotImplementedException, "Assumption checking for mdps not yet implemented"); |
|||
this->formula = formula; |
|||
this->matrix = model->getTransitionMatrix(); |
|||
|
|||
// Create sample points
|
|||
auto instantiator = utility::ModelInstantiator<models::sparse::Mdp<ValueType>, models::sparse::Mdp<double>>(*model); |
|||
auto matrix = model->getTransitionMatrix(); |
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model); |
|||
|
|||
for (auto i = 0; i < numberOfSamples; ++i) { |
|||
auto valuation = utility::parametric::Valuation<ValueType>(); |
|||
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { |
|||
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); |
|||
} |
|||
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() && |
|||
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { |
|||
const modelchecker::CheckTask<logic::UntilFormula, double> checkTask = modelchecker::CheckTask<logic::UntilFormula, double>( |
|||
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); |
|||
checkResult = checker.computeUntilProbabilities(Environment(), checkTask); |
|||
} else if (formula->isProbabilityOperatorFormula() && |
|||
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { |
|||
const modelchecker::CheckTask<logic::EventuallyFormula, double> checkTask = modelchecker::CheckTask<logic::EventuallyFormula, double>( |
|||
(*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); |
|||
checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); |
|||
} else { |
|||
STORM_LOG_THROW(false, exceptions::NotSupportedException, |
|||
"Expecting until or eventually formula"); |
|||
} |
|||
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>(); |
|||
std::vector<double> values = quantitativeResult.getValueVector(); |
|||
samples.push_back(values); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
AssumptionStatus AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<expressions::BinaryRelationExpression> assumption) { |
|||
auto result = AssumptionStatus::UNKNOWN; |
|||
std::set<expressions::Variable> vars = std::set<expressions::Variable>({}); |
|||
assumption->gatherVariables(vars); |
|||
for (auto itr = samples.begin(); result == AssumptionStatus::UNKNOWN && itr != samples.end(); ++itr) { |
|||
std::shared_ptr<expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer(); |
|||
auto valuation = expressions::SimpleValuation(manager); |
|||
auto values = (*itr); |
|||
for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) { |
|||
expressions::Variable par = *var; |
|||
auto index = std::stoi(par.getName()); |
|||
valuation.setRationalValue(par, values[index]); |
|||
} |
|||
assert(assumption->hasBooleanType()); |
|||
if (!assumption->evaluateAsBool(&valuation)) { |
|||
result = AssumptionStatus::INVALID; |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order) { |
|||
// First check if based on sample points the assumption can be discharged
|
|||
auto result = checkOnSamples(assumption); |
|||
assert (result != AssumptionStatus::VALID); |
|||
|
|||
if (result == AssumptionStatus::UNKNOWN) { |
|||
// If result from sample checking was unknown, the assumption might hold, so we continue,
|
|||
// otherwise we return INVALID
|
|||
std::set<expressions::Variable> vars = std::set<expressions::Variable>({}); |
|||
assumption->gatherVariables(vars); |
|||
|
|||
STORM_LOG_THROW(assumption->getRelationType() == |
|||
expressions::BinaryRelationExpression::RelationType::Greater || |
|||
assumption->getRelationType() == |
|||
expressions::BinaryRelationExpression::RelationType::Equal, |
|||
exceptions::NotSupportedException, |
|||
"Only Greater Or Equal assumptions supported"); |
|||
|
|||
// Row with successors of the first state
|
|||
auto row1 = matrix.getRow( |
|||
std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName())); |
|||
// Row with successors of the second state
|
|||
auto row2 = matrix.getRow( |
|||
std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName())); |
|||
|
|||
if (row1.getNumberOfEntries() == 2 && row2.getNumberOfEntries() == 2) { |
|||
// If the states have the same successors for which we know the position in the order
|
|||
// We can check with a function if the assumption holds
|
|||
|
|||
auto state1succ1 = row1.begin(); |
|||
auto state1succ2 = (++row1.begin()); |
|||
auto state2succ1 = row2.begin(); |
|||
auto state2succ2 = (++row2.begin()); |
|||
|
|||
if (state1succ1->getColumn() == state2succ2->getColumn() |
|||
&& state2succ1->getColumn() == state1succ2->getColumn()) { |
|||
std::swap(state1succ1, state1succ2); |
|||
} |
|||
|
|||
if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { |
|||
if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater |
|||
&& order->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Order::NodeComparison::UNKNOWN) { |
|||
// The assumption should be the greater assumption
|
|||
// If the result is unknown, we cannot compare, also SMTSolver will not help
|
|||
result = validateAssumptionSMTSolver(assumption, order); |
|||
|
|||
// result = validateAssumptionFunction(order, state1succ1, state1succ2, state2succ1,
|
|||
// state2succ2);
|
|||
} else if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
// 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
|
|||
if (state1succ1->getValue() == state2succ1->getValue()) { |
|||
result = AssumptionStatus::VALID; |
|||
} |
|||
} else { |
|||
result = AssumptionStatus::UNKNOWN; |
|||
} |
|||
} else { |
|||
result = validateAssumptionSMTSolver(assumption, order); |
|||
} |
|||
} else { |
|||
result = validateAssumptionSMTSolver(assumption, order); |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(Order* order, |
|||
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() |
|||
&& state1succ2->getColumn() == state2succ2->getColumn()) |
|||
|| (state1succ1->getColumn() == state2succ2->getColumn() |
|||
&& state1succ2->getColumn() == state2succ1->getColumn())); |
|||
|
|||
AssumptionStatus result; |
|||
|
|||
// Calculate the difference in probability for the "highest" successor state
|
|||
ValueType prob; |
|||
auto comp = order->compare(state1succ1->getColumn(), state1succ2->getColumn()); |
|||
assert (comp == Order::NodeComparison::ABOVE || comp == Order::NodeComparison::BELOW); |
|||
if (comp == Order::NodeComparison::ABOVE) { |
|||
prob = state1succ1->getValue() - state2succ1->getValue(); |
|||
} else if (comp == Order::NodeComparison::BELOW) { |
|||
prob = state1succ2->getValue() - state2succ2->getValue(); |
|||
} |
|||
|
|||
auto vars = prob.gatherVariables(); |
|||
|
|||
// If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions
|
|||
// This will give the smallest result
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type> substitutions; |
|||
for (auto var : vars) { |
|||
auto monotonicity = MonotonicityChecker<ValueType>::checkDerivative(prob.derivative(var), region); |
|||
if (monotonicity.first) { |
|||
// monotone increasing
|
|||
substitutions[var] = 0; |
|||
} else if (monotonicity.second) { |
|||
// monotone increasing
|
|||
substitutions[var] = 1; |
|||
} else { |
|||
result = AssumptionStatus::UNKNOWN; |
|||
} |
|||
} |
|||
|
|||
if (prob.evaluate(substitutions) >= 0) { |
|||
result = AssumptionStatus::VALID; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order) { |
|||
std::shared_ptr<utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<utility::solver::MathsatSmtSolverFactory>(); |
|||
std::shared_ptr<expressions::ExpressionManager> manager(new expressions::ExpressionManager()); |
|||
|
|||
AssumptionStatus result; |
|||
auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); |
|||
auto var2 = assumption->getSecondOperand()->asVariableExpression().getVariableName(); |
|||
auto row1 = matrix.getRow(std::stoi(var1)); |
|||
auto row2 = matrix.getRow(std::stoi(var2)); |
|||
|
|||
bool orderKnown = true; |
|||
// Check if the order between the different successors is known
|
|||
// Also start creating expression for order of states
|
|||
expressions::Expression exprOrderSucc = manager->boolean(true); |
|||
std::set<expressions::Variable> stateVariables; |
|||
for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { |
|||
auto varname1 = "s" + std::to_string(itr1->getColumn()); |
|||
if (!manager->hasVariable(varname1)) { |
|||
stateVariables.insert(manager->declareRationalVariable(varname1)); |
|||
} |
|||
for (auto itr2 = row2.begin(); orderKnown && itr2 != row2.end(); ++itr2) { |
|||
if (itr1->getColumn() != itr2->getColumn()) { |
|||
auto varname2 = "s" + std::to_string(itr2->getColumn()); |
|||
if (!manager->hasVariable(varname2)) { |
|||
stateVariables.insert(manager->declareRationalVariable(varname2)); |
|||
} |
|||
auto comp = order->compare(itr1->getColumn(), itr2->getColumn()); |
|||
if (comp == Order::NodeComparison::ABOVE) { |
|||
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= |
|||
manager->getVariable(varname2)); |
|||
} else if (comp == Order::NodeComparison::BELOW) { |
|||
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= |
|||
manager->getVariable(varname2)); |
|||
} else if (comp == Order::NodeComparison::SAME) { |
|||
exprOrderSucc = exprOrderSucc && |
|||
(manager->getVariable(varname1) = manager->getVariable(varname2)); |
|||
} else { |
|||
orderKnown = false; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
if (orderKnown) { |
|||
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) { |
|||
expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable("s" + std::to_string(itr1->getColumn()))); |
|||
} |
|||
|
|||
expressions::Expression expr2 = manager->rational(0); |
|||
for (auto itr2 = row2.begin(); itr2 != row2.end(); ++itr2) { |
|||
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
|
|||
// It is the negation of actual assumption
|
|||
expressions::Expression exprToCheck ; |
|||
if (assumption->getRelationType() == |
|||
expressions::BinaryRelationExpression::RelationType::Greater) { |
|||
exprToCheck = expr1 <= expr2; |
|||
} else { |
|||
assert (assumption->getRelationType() == |
|||
expressions::BinaryRelationExpression::RelationType::Equal); |
|||
exprToCheck = expr1 != expr2 ; |
|||
} |
|||
|
|||
auto variables = manager->getVariables(); |
|||
// Bounds for the state probabilities and parameters
|
|||
expressions::Expression exprBounds = manager->boolean(true); |
|||
for (auto var : variables) { |
|||
if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) { |
|||
// the var is a state
|
|||
exprBounds = exprBounds && manager->rational(0) <= var && var <= manager->rational(1); |
|||
} else { |
|||
// the var is a parameter
|
|||
auto lb = storm::utility::convertNumber<storm::RationalNumber>(region.getLowerBoundary(var.getName())); |
|||
auto ub = storm::utility::convertNumber<storm::RationalNumber>(region.getUpperBoundary(var.getName())); |
|||
exprBounds = exprBounds && manager->rational(lb) < var && var < manager->rational(ub); |
|||
} |
|||
} |
|||
|
|||
s.add(exprOrderSucc); |
|||
s.add(exprBounds); |
|||
// assert that sorting of successors in the order and the bounds on the expression are at least satisfiable
|
|||
assert (s.check() == solver::SmtSolver::CheckResult::Sat); |
|||
s.add(exprToCheck); |
|||
auto smtRes = s.check(); |
|||
if (smtRes == solver::SmtSolver::CheckResult::Unsat) { |
|||
// If there is no thing satisfying the negation we are safe.
|
|||
result = AssumptionStatus::VALID; |
|||
} else if (smtRes == solver::SmtSolver::CheckResult::Sat) { |
|||
assert (smtRes == solver::SmtSolver::CheckResult::Sat); |
|||
result = AssumptionStatus::INVALID; |
|||
} else { |
|||
result = AssumptionStatus::UNKNOWN; |
|||
} |
|||
} else { |
|||
result = AssumptionStatus::UNKNOWN; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template class AssumptionChecker<RationalFunction>; |
|||
} |
|||
} |
|||
@ -0,0 +1,90 @@ |
|||
#ifndef STORM_ASSUMPTIONCHECKER_H |
|||
#define STORM_ASSUMPTIONCHECKER_H |
|||
|
|||
#include "storm/logic/Formula.h" |
|||
#include "storm/models/sparse/Dtmc.h" |
|||
#include "storm/models/sparse/Mdp.h" |
|||
#include "storm/environment/Environment.h" |
|||
#include "storm/storage/expressions/BinaryRelationExpression.h" |
|||
#include "storm-pars/storage/ParameterRegion.h" |
|||
#include "Order.h" |
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
/*! |
|||
* Constants for status of assumption |
|||
*/ |
|||
enum AssumptionStatus { |
|||
VALID, |
|||
INVALID, |
|||
UNKNOWN, |
|||
}; |
|||
template<typename ValueType> |
|||
class AssumptionChecker { |
|||
public: |
|||
|
|||
/*! |
|||
* Constructs an AssumptionChecker based on the number of samples, for the given formula and model. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param model The dtmc model to check the formula on. |
|||
* @param numberOfSamples Number of sample points. |
|||
*/ |
|||
AssumptionChecker(std::shared_ptr<logic::Formula const> formula, std::shared_ptr<models::sparse::Dtmc<ValueType>> model, storm::storage::ParameterRegion<ValueType> region, uint_fast64_t numberOfSamples); |
|||
|
|||
/*! |
|||
* Constructs an AssumptionChecker based on the number of samples, for the given formula and model. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param model The mdp model to check the formula on. |
|||
* @param numberOfSamples Number of sample points. |
|||
*/ |
|||
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. |
|||
* |
|||
* @param assumption The assumption to check. |
|||
* @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID |
|||
*/ |
|||
AssumptionStatus checkOnSamples(std::shared_ptr<expressions::BinaryRelationExpression> assumption); |
|||
|
|||
/*! |
|||
* Tries to validate an assumption based on the order and underlying transition matrix. |
|||
* |
|||
* @param assumption The assumption to validate. |
|||
* @param order The order. |
|||
* @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID |
|||
*/ |
|||
AssumptionStatus validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order); |
|||
|
|||
/*! |
|||
* Tries to validate an assumption based on the order, and SMT solving techniques |
|||
* |
|||
* @param assumption The assumption to validate. |
|||
* @param order The order. |
|||
* @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID |
|||
*/ |
|||
AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order); |
|||
|
|||
private: |
|||
std::shared_ptr<logic::Formula const> formula; |
|||
|
|||
storage::SparseMatrix<ValueType> matrix; |
|||
|
|||
std::vector<std::vector<double>> samples; |
|||
|
|||
void createSamples(); |
|||
|
|||
AssumptionStatus validateAssumptionFunction(Order* order, |
|||
typename storage::SparseMatrix<ValueType>::iterator state1succ1, |
|||
typename storage::SparseMatrix<ValueType>::iterator state1succ2, |
|||
typename storage::SparseMatrix<ValueType>::iterator state2succ1, |
|||
typename storage::SparseMatrix<ValueType>::iterator state2succ2); |
|||
|
|||
storm::storage::ParameterRegion<ValueType> region; |
|||
|
|||
}; |
|||
} |
|||
} |
|||
#endif //STORM_ASSUMPTIONCHECKER_H |
|||
@ -0,0 +1,67 @@ |
|||
#include "AssumptionMaker.h"
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
typedef std::shared_ptr<expressions::BinaryRelationExpression> AssumptionType; |
|||
template<typename ValueType> |
|||
AssumptionMaker<ValueType>::AssumptionMaker(AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) { |
|||
this->numberOfStates = numberOfStates; |
|||
this->assumptionChecker = assumptionChecker; |
|||
this->validate = validate; |
|||
this->expressionManager = std::make_shared<expressions::ExpressionManager>(expressions::ExpressionManager()); |
|||
for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { |
|||
expressionManager->declareRationalVariable(std::to_string(i)); |
|||
} |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order) { |
|||
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> result; |
|||
|
|||
expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); |
|||
expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); |
|||
std::shared_ptr<expressions::BinaryRelationExpression> assumption1 |
|||
= std::make_shared<expressions::BinaryRelationExpression>(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), |
|||
expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
AssumptionStatus result1; |
|||
AssumptionStatus result2; |
|||
AssumptionStatus result3; |
|||
if (validate) { |
|||
result1 = assumptionChecker->validateAssumption(assumption1, order); |
|||
} else { |
|||
result1 = AssumptionStatus::UNKNOWN; |
|||
} |
|||
result[assumption1] = result1; |
|||
|
|||
|
|||
std::shared_ptr<expressions::BinaryRelationExpression> assumption2 |
|||
= std::make_shared<expressions::BinaryRelationExpression>(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), |
|||
expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
|
|||
if (validate) { |
|||
result2 = assumptionChecker->validateAssumption(assumption2, order); |
|||
} else { |
|||
result2 = AssumptionStatus::UNKNOWN; |
|||
} |
|||
result[assumption2] = result2; |
|||
|
|||
std::shared_ptr<expressions::BinaryRelationExpression> assumption3 |
|||
= std::make_shared<expressions::BinaryRelationExpression>(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), |
|||
expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
if (validate) { |
|||
result3 = assumptionChecker->validateAssumption(assumption3, order); |
|||
} else { |
|||
result3 = AssumptionStatus::UNKNOWN; |
|||
} |
|||
result[assumption3] = result3; |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template class AssumptionMaker<RationalFunction>; |
|||
} |
|||
} |
|||
@ -0,0 +1,51 @@ |
|||
#ifndef STORM_ASSUMPTIONMAKER_H |
|||
#define STORM_ASSUMPTIONMAKER_H |
|||
|
|||
#include "AssumptionChecker.h" |
|||
#include "Order.h" |
|||
#include "OrderExtender.h" |
|||
#include "storm/storage/expressions/BinaryRelationExpression.h" |
|||
#include "storm-pars/utility/ModelInstantiator.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
|
|||
template<typename ValueType> |
|||
class AssumptionMaker { |
|||
typedef std::shared_ptr<expressions::BinaryRelationExpression> AssumptionType; |
|||
public: |
|||
/*! |
|||
* Constructs AssumptionMaker based on the order extender, the assumption checker and number of states of the mode |
|||
* |
|||
* @param orderExtender The OrderExtender which needs the assumptions made by the AssumptionMaker. |
|||
* @param checker The AssumptionChecker which checks the assumptions at sample points. |
|||
* @param numberOfStates The number of states of the model. |
|||
*/ |
|||
AssumptionMaker(AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate); |
|||
|
|||
/*! |
|||
* Creates assumptions, and checks them if validate in constructor is true. |
|||
* Possible results: AssumptionStatus::VALID, AssumptionStatus::INVALID, AssumptionStatus::UNKNOWN |
|||
* If validate is false result is always AssumptionStatus::UNKNOWN |
|||
* |
|||
* @param val1 First state number |
|||
* @param val2 Second state number |
|||
* @param order The order on which the assumptions are checked |
|||
* @return Map with three assumptions, and the validation |
|||
*/ |
|||
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order); |
|||
|
|||
private: |
|||
AssumptionChecker<ValueType>* assumptionChecker; |
|||
|
|||
std::shared_ptr<expressions::ExpressionManager> expressionManager; |
|||
|
|||
uint_fast64_t numberOfStates; |
|||
|
|||
bool validate; |
|||
}; |
|||
} |
|||
} |
|||
#endif //STORM_ASSUMPTIONMAKER_H |
|||
|
|||
@ -0,0 +1,692 @@ |
|||
#include "MonotonicityChecker.h"
|
|||
#include "storm-pars/analysis/AssumptionMaker.h"
|
|||
#include "storm-pars/analysis/AssumptionChecker.h"
|
|||
#include "storm-pars/analysis/Order.h"
|
|||
#include "storm-pars/analysis/OrderExtender.h"
|
|||
|
|||
#include "storm/exceptions/NotSupportedException.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
#include "storm/utility/Stopwatch.h"
|
|||
#include "storm/models/ModelType.h"
|
|||
|
|||
#include "storm/api/verification.h"
|
|||
#include "storm-pars/api/storm-pars.h"
|
|||
|
|||
#include "storm/modelchecker/results/CheckResult.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
|
|||
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
template <typename ValueType> |
|||
MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<storm::storage::ParameterRegion<ValueType>> regions, bool validate, uint_fast64_t numberOfSamples, double const& precision) { |
|||
assert (model != nullptr); |
|||
this->model = model; |
|||
this->formulas = formulas; |
|||
this->validate = validate; |
|||
this->precision = precision; |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); |
|||
|
|||
if (regions.size() == 1) { |
|||
this->region = *(regions.begin()); |
|||
} else { |
|||
assert (regions.size() == 0); |
|||
typename storm::storage::ParameterRegion<ValueType>::Valuation lowerBoundaries; |
|||
typename storm::storage::ParameterRegion<ValueType>::Valuation upperBoundaries; |
|||
std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> vars; |
|||
vars = storm::models::sparse::getProbabilityParameters(*sparseModel); |
|||
for (auto var : vars) { |
|||
typename storm::storage::ParameterRegion<ValueType>::CoefficientType lb = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(0 + precision); |
|||
typename storm::storage::ParameterRegion<ValueType>::CoefficientType ub = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(1 - precision); |
|||
lowerBoundaries.insert(std::make_pair(var, lb)); |
|||
upperBoundaries.insert(std::make_pair(var, ub)); |
|||
} |
|||
this->region = storm::storage::ParameterRegion<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries)); |
|||
} |
|||
|
|||
if (numberOfSamples > 0) { |
|||
// sampling
|
|||
if (model->isOfType(storm::models::ModelType::Dtmc)) { |
|||
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>( |
|||
checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples)); |
|||
} else if (model->isOfType(storm::models::ModelType::Mdp)) { |
|||
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>( |
|||
checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples)); |
|||
|
|||
} |
|||
checkSamples= true; |
|||
} else { |
|||
checkSamples= false; |
|||
} |
|||
|
|||
this->extender = new storm::analysis::OrderExtender<ValueType>(sparseModel); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() { |
|||
auto map = createOrder(); |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); |
|||
auto matrix = sparseModel->getTransitionMatrix(); |
|||
return checkMonotonicity(map, matrix); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) { |
|||
storm::utility::Stopwatch monotonicityCheckWatch(true); |
|||
std::map<storm::analysis::Order *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> result; |
|||
|
|||
outfile.open(filename, std::ios_base::app); |
|||
|
|||
if (map.size() == 0) { |
|||
// Nothing is known
|
|||
outfile << " No assumptions -"; |
|||
STORM_PRINT("No valid assumptions, couldn't build a sufficient order"); |
|||
if (resultCheckOnSamples.size() != 0) { |
|||
STORM_PRINT("\n" << "Based results on samples"); |
|||
} else { |
|||
outfile << " ?"; |
|||
} |
|||
|
|||
for (auto entry : resultCheckOnSamples) { |
|||
if (!entry.second.first && ! entry.second.second) { |
|||
outfile << " SX " << entry.first << " "; |
|||
} else if (entry.second.first && ! entry.second.second) { |
|||
outfile << " SI " << entry.first << " "; |
|||
} else if (entry.second.first && entry.second.second) { |
|||
outfile << " SC " << entry.first << " "; |
|||
} else { |
|||
outfile << " SD " << entry.first << " "; |
|||
} |
|||
} |
|||
|
|||
} else { |
|||
size_t i = 0; |
|||
for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { |
|||
auto order = itr->first; |
|||
|
|||
auto addedStates = order->getAddedStates()->getNumberOfSetBits(); |
|||
assert (addedStates == order->getAddedStates()->size()); |
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, order, |
|||
matrix); |
|||
|
|||
auto assumptions = itr->second; |
|||
if (assumptions.size() > 0) { |
|||
bool first = true; |
|||
for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) { |
|||
if (!first) { |
|||
outfile << (" ^ "); |
|||
} else { |
|||
first = false; |
|||
} |
|||
outfile << (*(*itr2)); |
|||
} |
|||
outfile << " - "; |
|||
} else if (assumptions.size() == 0) { |
|||
outfile << "No assumptions - "; |
|||
} |
|||
|
|||
if (varsMonotone.size() == 0) { |
|||
outfile << "No params"; |
|||
} else { |
|||
auto itr2 = varsMonotone.begin(); |
|||
while (itr2 != varsMonotone.end()) { |
|||
if (checkSamples && |
|||
resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() && |
|||
(!resultCheckOnSamples[itr2->first].first && |
|||
!resultCheckOnSamples[itr2->first].second)) { |
|||
outfile << "X " << itr2->first; |
|||
} else { |
|||
if (itr2->second.first && itr2->second.second) { |
|||
outfile << "C " << itr2->first; |
|||
} else if (itr2->second.first) { |
|||
outfile << "I " << itr2->first; |
|||
} else if (itr2->second.second) { |
|||
outfile << "D " << itr2->first; |
|||
} else { |
|||
outfile << "? " << itr2->first; |
|||
} |
|||
} |
|||
++itr2; |
|||
if (itr2 != varsMonotone.end()) { |
|||
outfile << " "; |
|||
} |
|||
} |
|||
result.insert( |
|||
std::pair<storm::analysis::Order *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>>( |
|||
order, varsMonotone)); |
|||
} |
|||
++i; |
|||
outfile << ";"; |
|||
} |
|||
} |
|||
outfile << ", "; |
|||
|
|||
monotonicityCheckWatch.stop(); |
|||
outfile.close(); |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::createOrder() { |
|||
// Transform to Orders
|
|||
storm::utility::Stopwatch orderWatch(true); |
|||
|
|||
// Use parameter lifting modelchecker to get initial min/max values for order creation
|
|||
storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ValueType>, double> plaModelChecker; |
|||
std::unique_ptr<storm::modelchecker::CheckResult> checkResult; |
|||
auto env = Environment(); |
|||
|
|||
auto formula = formulas[0]; |
|||
const storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask |
|||
= storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula); |
|||
STORM_LOG_THROW(plaModelChecker.canHandle(model, checkTask), storm::exceptions::NotSupportedException, |
|||
"Cannot handle this formula"); |
|||
plaModelChecker.specify(env, model, checkTask); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> minCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Minimize); |
|||
std::unique_ptr<storm::modelchecker::CheckResult> maxCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Maximize); |
|||
auto minRes = minCheck->asExplicitQuantitativeCheckResult<double>(); |
|||
auto maxRes = maxCheck->asExplicitQuantitativeCheckResult<double>(); |
|||
|
|||
std::vector<double> minValues = minRes.getValueVector(); |
|||
std::vector<double> maxValues = maxRes.getValueVector(); |
|||
// Create initial order
|
|||
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues); |
|||
// Continue based on not (yet) sorted states
|
|||
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result; |
|||
|
|||
auto val1 = std::get<1>(criticalTuple); |
|||
auto val2 = std::get<2>(criticalTuple); |
|||
auto numberOfStates = model->getNumberOfStates(); |
|||
std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions; |
|||
|
|||
if (val1 == numberOfStates && val2 == numberOfStates) { |
|||
result.insert(std::pair<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(std::get<0>(criticalTuple), assumptions)); |
|||
} else if (val1 != numberOfStates && val2 != numberOfStates) { |
|||
|
|||
storm::analysis::AssumptionChecker<ValueType> *assumptionChecker; |
|||
if (model->isOfType(storm::models::ModelType::Dtmc)) { |
|||
auto dtmc = model->as<storm::models::sparse::Dtmc<ValueType>>(); |
|||
assumptionChecker = new storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmc, region, 3); |
|||
} else if (model->isOfType(storm::models::ModelType::Mdp)) { |
|||
auto mdp = model->as<storm::models::sparse::Mdp<ValueType>>(); |
|||
assumptionChecker = new storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdp, 3); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, |
|||
"Unable to perform monotonicity analysis on the provided model type."); |
|||
} |
|||
auto assumptionMaker = new storm::analysis::AssumptionMaker<ValueType>(assumptionChecker, numberOfStates, validate); |
|||
result = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, val1, val2, assumptions); |
|||
} else { |
|||
assert(false); |
|||
} |
|||
orderWatch.stop(); |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::extendOrderWithAssumptions(storm::analysis::Order* order, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) { |
|||
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result; |
|||
|
|||
auto numberOfStates = model->getNumberOfStates(); |
|||
if (val1 == numberOfStates || val2 == numberOfStates) { |
|||
assert (val1 == val2); |
|||
assert (order->getAddedStates()->size() == order->getAddedStates()->getNumberOfSetBits()); |
|||
result.insert(std::pair<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(order, assumptions)); |
|||
} else { |
|||
// Make the three assumptions
|
|||
auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, order); |
|||
assert (assumptionTriple.size() == 3); |
|||
auto itr = assumptionTriple.begin(); |
|||
auto assumption1 = *itr; |
|||
++itr; |
|||
auto assumption2 = *itr; |
|||
++itr; |
|||
auto assumption3 = *itr; |
|||
|
|||
if (assumption1.second != AssumptionStatus::INVALID) { |
|||
auto orderCopy = new Order(order); |
|||
auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions); |
|||
|
|||
if (assumption1.second == AssumptionStatus::UNKNOWN) { |
|||
// only add assumption to the set of assumptions if it is unknown if it is valid
|
|||
assumptionsCopy.push_back(assumption1.first); |
|||
} |
|||
|
|||
auto criticalTuple = extender->extendOrder(orderCopy, assumption1.first); |
|||
if (somewhereMonotonicity(std::get<0>(criticalTuple))) { |
|||
auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, |
|||
std::get<1>(criticalTuple), std::get<2>(criticalTuple), |
|||
assumptionsCopy); |
|||
result.insert(map.begin(), map.end()); |
|||
} |
|||
} |
|||
|
|||
if (assumption2.second != AssumptionStatus::INVALID) { |
|||
auto orderCopy = new Order(order); |
|||
auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions); |
|||
|
|||
if (assumption2.second == AssumptionStatus::UNKNOWN) { |
|||
assumptionsCopy.push_back(assumption2.first); |
|||
} |
|||
|
|||
auto criticalTuple = extender->extendOrder(orderCopy, assumption2.first); |
|||
if (somewhereMonotonicity(std::get<0>(criticalTuple))) { |
|||
auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, |
|||
std::get<1>(criticalTuple), std::get<2>(criticalTuple), |
|||
assumptionsCopy); |
|||
result.insert(map.begin(), map.end()); |
|||
} |
|||
} |
|||
|
|||
if (assumption3.second != AssumptionStatus::INVALID) { |
|||
// Here we can use the original order and assumptions set
|
|||
if (assumption3.second == AssumptionStatus::UNKNOWN) { |
|||
assumptions.push_back(assumption3.first); |
|||
} |
|||
|
|||
auto criticalTuple = extender->extendOrder(order, assumption3.first); |
|||
if (somewhereMonotonicity(std::get<0>(criticalTuple))) { |
|||
auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, |
|||
std::get<1>(criticalTuple), std::get<2>(criticalTuple), |
|||
assumptions); |
|||
result.insert(map.begin(), map.end()); |
|||
} |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
ValueType MonotonicityChecker<ValueType>::getDerivative(ValueType function, typename utility::parametric::VariableType<ValueType>::type var) { |
|||
if (function.isConstant()) { |
|||
return storm::utility::zero<ValueType>(); |
|||
} |
|||
if ((derivatives[function]).find(var) == (derivatives[function]).end()) { |
|||
(derivatives[function])[var] = function.derivative(var); |
|||
} |
|||
|
|||
return (derivatives[function])[var]; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Order* order, storm::storage::SparseMatrix<ValueType> matrix) { |
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone; |
|||
|
|||
// go over all rows, check for each row local monotonicity
|
|||
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|||
auto row = matrix.getRow(i); |
|||
// only enter if you are in a state with at least two successors (so there must be successors,
|
|||
// and first prob shouldn't be 1)
|
|||
if (row.begin() != row.end() && !row.begin()->getValue().isOne()) { |
|||
std::map<uint_fast64_t, ValueType> transitions; |
|||
|
|||
// Gather all states which are reached with a non constant probability
|
|||
auto states = new storm::storage::BitVector(matrix.getColumnCount()); |
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> vars; |
|||
for (auto const& entry : row) { |
|||
if (!entry.getValue().isConstant()) { |
|||
// only analyse take non constant transitions
|
|||
transitions.insert(std::pair<uint_fast64_t, ValueType>(entry.getColumn(), entry.getValue())); |
|||
for (auto const& var:entry.getValue().gatherVariables()) { |
|||
vars.insert(var); |
|||
states->set(entry.getColumn()); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Copy info from checkOnSamples
|
|||
if (checkSamples) { |
|||
for (auto var : vars) { |
|||
assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); |
|||
if (varsMonotone.find(var) == varsMonotone.end()) { |
|||
varsMonotone[var].first = resultCheckOnSamples[var].first; |
|||
varsMonotone[var].second = resultCheckOnSamples[var].second; |
|||
} else { |
|||
varsMonotone[var].first &= resultCheckOnSamples[var].first; |
|||
varsMonotone[var].second &= resultCheckOnSamples[var].second; |
|||
} |
|||
} |
|||
} else { |
|||
for (auto var : vars) { |
|||
if (varsMonotone.find(var) == varsMonotone.end()) { |
|||
varsMonotone[var].first = true; |
|||
varsMonotone[var].second = true; |
|||
} |
|||
} |
|||
} |
|||
|
|||
|
|||
|
|||
// Sort the states based on the order
|
|||
auto sortedStates = order->sortStates(states); |
|||
if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) { |
|||
// If the states are not all sorted, we still might obtain some monotonicity
|
|||
for (auto var: vars) { |
|||
// current value of monotonicity
|
|||
std::pair<bool, bool> *value = &varsMonotone.find(var)->second; |
|||
|
|||
// Go over all transitions to successor states, compare all of them
|
|||
for (auto itr2 = transitions.begin(); (value->first || value->second) |
|||
&& itr2 != transitions.end(); ++itr2) { |
|||
for (auto itr3 = transitions.begin(); (value->first || value->second) |
|||
&& itr3 != transitions.end(); ++itr3) { |
|||
if (itr2->first < itr3->first) { |
|||
|
|||
auto derivative2 = getDerivative(itr2->second, var); |
|||
auto derivative3 = getDerivative(itr3->second, var); |
|||
|
|||
auto compare = order->compare(itr2->first, itr3->first); |
|||
|
|||
if (compare == Order::ABOVE) { |
|||
// As the first state (itr2) is above the second state (itr3) it
|
|||
// is sufficient to look at the derivative of itr2.
|
|||
std::pair<bool, bool> mon2; |
|||
mon2 = checkDerivative(derivative2, region); |
|||
value->first &= mon2.first; |
|||
value->second &= mon2.second; |
|||
} else if (compare == Order::BELOW) { |
|||
// As the second state (itr3) is above the first state (itr2) it
|
|||
// is sufficient to look at the derivative of itr3.
|
|||
std::pair<bool, bool> mon3; |
|||
|
|||
mon3 = checkDerivative(derivative3, region); |
|||
value->first &= mon3.first; |
|||
value->second &= mon3.second; |
|||
} else if (compare == Order::SAME) { |
|||
// Behaviour doesn't matter, as the states are at the same level.
|
|||
} else { |
|||
// only if derivatives are the same we can continue
|
|||
if (derivative2 != derivative3) { |
|||
// As the relation between the states is unknown, we can't claim
|
|||
// anything about the monotonicity.
|
|||
value->first = false; |
|||
value->second = false; |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} else { |
|||
// The states are all sorted
|
|||
for (auto var : vars) { |
|||
std::pair<bool, bool> *value = &varsMonotone.find(var)->second; |
|||
bool change = false; |
|||
for (auto const &i : sortedStates) { |
|||
auto res = checkDerivative(getDerivative(transitions[i], var), region); |
|||
change = change || (!(value->first && value->second) // they do not hold both
|
|||
&& ((value->first && !res.first) |
|||
|| (value->second && !res.second))); |
|||
|
|||
if (change) { |
|||
value->first &= res.second; |
|||
value->second &= res.first; |
|||
} else { |
|||
value->first &= res.first; |
|||
value->second &= res.second; |
|||
} |
|||
if (!value->first && !value->second) { |
|||
break; |
|||
} |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
return varsMonotone; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool MonotonicityChecker<ValueType>::somewhereMonotonicity(Order* order) { |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); |
|||
auto matrix = sparseModel->getTransitionMatrix(); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone; |
|||
|
|||
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|||
// go over all rows
|
|||
auto row = matrix.getRow(i); |
|||
auto first = (*row.begin()); |
|||
if (first.getValue() != ValueType(1)) { |
|||
std::map<uint_fast64_t, ValueType> transitions; |
|||
|
|||
for (auto itr = row.begin(); itr != row.end(); ++itr) { |
|||
transitions.insert(std::pair<uint_fast64_t, ValueType>((*itr).getColumn(), (*itr).getValue())); |
|||
} |
|||
|
|||
auto val = first.getValue(); |
|||
auto vars = val.gatherVariables(); |
|||
// Copy info from checkOnSamples
|
|||
if (checkSamples) { |
|||
for (auto var : vars) { |
|||
assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end()); |
|||
if (varsMonotone.find(var) == varsMonotone.end()) { |
|||
varsMonotone[var].first = resultCheckOnSamples[var].first; |
|||
varsMonotone[var].second = resultCheckOnSamples[var].second; |
|||
} else { |
|||
varsMonotone[var].first &= resultCheckOnSamples[var].first; |
|||
varsMonotone[var].second &= resultCheckOnSamples[var].second; |
|||
} |
|||
} |
|||
} else { |
|||
for (auto var : vars) { |
|||
if (varsMonotone.find(var) == varsMonotone.end()) { |
|||
varsMonotone[var].first = true; |
|||
varsMonotone[var].second = true; |
|||
} |
|||
} |
|||
} |
|||
|
|||
for (auto var: vars) { |
|||
// current value of monotonicity
|
|||
std::pair<bool, bool> *value = &varsMonotone.find(var)->second; |
|||
|
|||
// Go over all transitions to successor states, compare all of them
|
|||
for (auto itr2 = transitions.begin(); (value->first || value->second) |
|||
&& itr2 != transitions.end(); ++itr2) { |
|||
for (auto itr3 = transitions.begin(); (value->first || value->second) |
|||
&& itr3 != transitions.end(); ++itr3) { |
|||
if (itr2->first < itr3->first) { |
|||
|
|||
auto derivative2 = getDerivative(itr2->second, var); |
|||
auto derivative3 = getDerivative(itr3->second, var); |
|||
|
|||
auto compare = order->compare(itr2->first, itr3->first); |
|||
|
|||
if (compare == Order::ABOVE) { |
|||
// As the first state (itr2) is above the second state (itr3) it
|
|||
// is sufficient to look at the derivative of itr2.
|
|||
std::pair<bool, bool> mon2; |
|||
mon2 = checkDerivative(derivative2, region); |
|||
value->first &= mon2.first; |
|||
value->second &= mon2.second; |
|||
} else if (compare == Order::BELOW) { |
|||
// As the second state (itr3) is above the first state (itr2) it
|
|||
// is sufficient to look at the derivative of itr3.
|
|||
std::pair<bool, bool> mon3; |
|||
|
|||
mon3 = checkDerivative(derivative3, region); |
|||
value->first &= mon3.first; |
|||
value->second &= mon3.second; |
|||
} else if (compare == Order::SAME) { |
|||
// Behaviour doesn't matter, as the states are at the same level.
|
|||
} else { |
|||
// As the relation between the states is unknown, we don't do anything
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
bool result = false; |
|||
|
|||
for (auto itr = varsMonotone.begin(); !result && itr != varsMonotone.end(); ++itr) { |
|||
result = itr->second.first || itr->second.second; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) { |
|||
storm::utility::Stopwatch samplesWatch(true); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> result; |
|||
|
|||
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model); |
|||
auto matrix = model->getTransitionMatrix(); |
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = storm::models::sparse::getProbabilityParameters(*model); |
|||
|
|||
// For each of the variables create a model in which we only change the value for this specific variable
|
|||
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { |
|||
double previous = -1; |
|||
bool monDecr = true; |
|||
bool monIncr = true; |
|||
|
|||
// Check monotonicity in variable (*itr) by instantiating the model
|
|||
// all other variables fixed on lb, only increasing (*itr)
|
|||
for (uint_fast64_t i = 0; (monDecr || monIncr) && i < numberOfSamples; ++i) { |
|||
// Create valuation
|
|||
auto valuation = storm::utility::parametric::Valuation<ValueType>(); |
|||
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { |
|||
// Only change value for current variable
|
|||
if ((*itr) == (*itr2)) { |
|||
auto lb = region.getLowerBoundary(itr->name()); |
|||
auto ub = region.getUpperBoundary(itr->name()); |
|||
// Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub
|
|||
valuation[*itr2] = utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb + i*(ub-lb)/(numberOfSamples-1)); |
|||
} else { |
|||
auto lb = region.getLowerBoundary(itr->name()); |
|||
valuation[*itr2] = utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb); |
|||
} |
|||
} |
|||
|
|||
// Instantiate model and get result
|
|||
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; |
|||
auto formula = formulas[0]; |
|||
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(); |
|||
auto initialStates = model->getInitialStates(); |
|||
double initial = 0; |
|||
// Get total probability from initial states
|
|||
for (auto j = initialStates.getNextSetIndex(0); j < model->getNumberOfStates(); j = initialStates.getNextSetIndex(j+1)) { |
|||
initial += values[j]; |
|||
} |
|||
// Calculate difference with result for previous valuation
|
|||
assert (initial >= 0-precision && initial <= 1+precision); |
|||
double diff = previous - initial; |
|||
assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); |
|||
if (previous != -1 && (diff > precision || diff < -precision)) { |
|||
monDecr &= diff > precision; // then previous value is larger than the current value from the initial states
|
|||
monIncr &= diff < -precision; |
|||
} |
|||
previous = initial; |
|||
} |
|||
result.insert(std::pair<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr))); |
|||
} |
|||
|
|||
samplesWatch.stop(); |
|||
resultCheckOnSamples = result; |
|||
return result; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) { |
|||
storm::utility::Stopwatch samplesWatch(true); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> result; |
|||
|
|||
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model); |
|||
auto matrix = model->getTransitionMatrix(); |
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = storm::models::sparse::getProbabilityParameters(*model); |
|||
|
|||
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { |
|||
double previous = -1; |
|||
bool monDecr = true; |
|||
bool monIncr = true; |
|||
|
|||
for (uint_fast64_t i = 0; i < numberOfSamples; ++i) { |
|||
auto valuation = storm::utility::parametric::Valuation<ValueType>(); |
|||
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { |
|||
// Only change value for current variable
|
|||
if ((*itr) == (*itr2)) { |
|||
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>( |
|||
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>( |
|||
boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1))))); |
|||
valuation.insert(val); |
|||
} else { |
|||
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>( |
|||
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>( |
|||
boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1))))); |
|||
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; |
|||
auto formula = formulas[0]; |
|||
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(); |
|||
auto initialStates = model->getInitialStates(); |
|||
double initial = 0; |
|||
for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) { |
|||
initial += values[i]; |
|||
} |
|||
assert (initial >= precision && initial <= 1+precision); |
|||
double diff = previous - initial; |
|||
assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision); |
|||
if (previous != -1 && (diff > precision || diff < -precision)) { |
|||
monDecr &= diff > precision; // then previous value is larger than the current value from the initial states
|
|||
monIncr &= diff < -precision; |
|||
} |
|||
previous = initial; |
|||
} |
|||
result.insert(std::pair<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr))); |
|||
} |
|||
|
|||
samplesWatch.stop(); |
|||
resultCheckOnSamples = result; |
|||
return result; |
|||
} |
|||
|
|||
template class MonotonicityChecker<storm::RationalFunction>; |
|||
} |
|||
} |
|||
@ -0,0 +1,154 @@ |
|||
#ifndef STORM_MONOTONICITYCHECKER_H |
|||
#define STORM_MONOTONICITYCHECKER_H |
|||
|
|||
#include <map> |
|||
#include "Order.h" |
|||
#include "OrderExtender.h" |
|||
#include "AssumptionMaker.h" |
|||
#include "storm/storage/expressions/BinaryRelationExpression.h" |
|||
#include "storm/storage/expressions/ExpressionManager.h" |
|||
|
|||
#include "storm/storage/expressions/RationalFunctionToExpression.h" |
|||
#include "storm/utility/constants.h" |
|||
#include "storm/models/ModelBase.h" |
|||
#include "storm/models/sparse/Dtmc.h" |
|||
#include "storm/models/sparse/Mdp.h" |
|||
#include "storm/logic/Formula.h" |
|||
#include "storm/storage/SparseMatrix.h" |
|||
#include "storm-pars/api/region.h" |
|||
#include "storm/solver/Z3SmtSolver.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
|
|||
template <typename ValueType> |
|||
class MonotonicityChecker { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructor of MonotonicityChecker |
|||
* @param model the model considered |
|||
* @param formula the formula considered |
|||
* @param regions the regions to consider |
|||
* @param validate whether or not assumptions are to be validated |
|||
* @param numberOfSamples number of samples taken for monotonicity checking, default 0, |
|||
* if 0 then no check on samples is executed |
|||
* @param precision precision on which the samples are compared |
|||
*/ |
|||
MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<storm::storage::ParameterRegion<ValueType>> regions, bool validate, uint_fast64_t numberOfSamples=0, double const& precision=0.000001); |
|||
|
|||
/*! |
|||
* Checks for model and formula as provided in constructor for monotonicity |
|||
*/ |
|||
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(); |
|||
|
|||
/*! |
|||
* Checks if monotonicity can be found in this order. Unordered states are not checked |
|||
*/ |
|||
bool somewhereMonotonicity(storm::analysis::Order* order) ; |
|||
|
|||
/*! |
|||
* Checks if a derivative >=0 or/and <=0 |
|||
* @param derivative The derivative you want to check |
|||
* @return pair of bools, >= 0 and <= 0 |
|||
*/ |
|||
static std::pair<bool, bool> checkDerivative(ValueType derivative, storm::storage::ParameterRegion<ValueType> reg) { |
|||
bool monIncr = false; |
|||
bool monDecr = false; |
|||
|
|||
if (derivative.isZero()) { |
|||
monIncr = true; |
|||
monDecr = true; |
|||
} else if (derivative.isConstant()) { |
|||
monIncr = derivative.constantPart() >= 0; |
|||
monDecr = derivative.constantPart() <= 0; |
|||
} else { |
|||
|
|||
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()); |
|||
|
|||
storm::solver::Z3SmtSolver s(*manager); |
|||
|
|||
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = derivative.gatherVariables(); |
|||
|
|||
|
|||
for (auto variable : variables) { |
|||
manager->declareRationalVariable(variable.name()); |
|||
|
|||
} |
|||
storm::expressions::Expression exprBounds = manager->boolean(true); |
|||
auto managervars = manager->getVariables(); |
|||
for (auto var : managervars) { |
|||
auto lb = storm::utility::convertNumber<storm::RationalNumber>(reg.getLowerBoundary(var.getName())); |
|||
auto ub = storm::utility::convertNumber<storm::RationalNumber>(reg.getUpperBoundary(var.getName())); |
|||
exprBounds = exprBounds && manager->rational(lb) < var && var < manager->rational(ub); |
|||
} |
|||
assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat); |
|||
|
|||
auto converter = storm::expressions::RationalFunctionToExpression<ValueType>(manager); |
|||
|
|||
// < 0 so not monotone increasing |
|||
storm::expressions::Expression exprToCheck = |
|||
converter.toExpression(derivative) < manager->rational(0); |
|||
s.add(exprBounds); |
|||
s.add(exprToCheck); |
|||
// If it is unsatisfiable then it should be monotone increasing |
|||
monIncr = s.check() == storm::solver::SmtSolver::CheckResult::Unsat; |
|||
|
|||
// > 0 so not monotone decreasing |
|||
exprToCheck = |
|||
converter.toExpression(derivative) > manager->rational(0); |
|||
|
|||
s.reset(); |
|||
s.add(exprBounds); |
|||
assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat); |
|||
s.add(exprToCheck); |
|||
monDecr = s.check() == storm::solver::SmtSolver::CheckResult::Unsat; |
|||
} |
|||
assert (!(monIncr && monDecr) || derivative.isZero()); |
|||
|
|||
return std::pair<bool, bool>(monIncr, monDecr); |
|||
} |
|||
|
|||
private: |
|||
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix<ValueType> matrix) ; |
|||
|
|||
std::map<Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createOrder(); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples); |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples); |
|||
|
|||
std::unordered_map<ValueType, std::unordered_map<typename utility::parametric::VariableType<ValueType>::type, ValueType>> derivatives; |
|||
|
|||
ValueType getDerivative(ValueType function, typename utility::parametric::VariableType<ValueType>::type var); |
|||
|
|||
std::map<Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendOrderWithAssumptions(Order* order, AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions); |
|||
|
|||
std::shared_ptr<storm::models::ModelBase> model; |
|||
|
|||
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; |
|||
|
|||
bool validate; |
|||
|
|||
bool checkSamples; |
|||
|
|||
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> resultCheckOnSamples; |
|||
|
|||
OrderExtender<ValueType> *extender; |
|||
|
|||
std::ofstream outfile; |
|||
|
|||
std::string filename = "monotonicity.txt"; |
|||
|
|||
double precision; |
|||
|
|||
storm::storage::ParameterRegion<ValueType> region; |
|||
}; |
|||
} |
|||
} |
|||
#endif //STORM_MONOTONICITYCHECKER_H |
|||
@ -0,0 +1,379 @@ |
|||
#include <iostream>
|
|||
#include <fstream>
|
|||
#include "Order.h"
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
Order::Order(storm::storage::BitVector* topStates, |
|||
storm::storage::BitVector* bottomStates, |
|||
storm::storage::BitVector* initialMiddleStates, |
|||
uint_fast64_t numberOfStates, |
|||
std::vector<uint_fast64_t>* statesSorted) { |
|||
nodes = std::vector<Node *>(numberOfStates); |
|||
|
|||
this->numberOfStates = numberOfStates; |
|||
this->addedStates = new storm::storage::BitVector(numberOfStates); |
|||
this->doneBuilding = false; |
|||
assert (statesSorted != nullptr); |
|||
this->statesSorted = *statesSorted; |
|||
this->statesToHandle = initialMiddleStates; |
|||
|
|||
top = new Node(); |
|||
bottom = new Node(); |
|||
|
|||
top->statesAbove = storm::storage::BitVector(numberOfStates); |
|||
bottom->statesAbove = storm::storage::BitVector(numberOfStates); |
|||
|
|||
for (auto const& i : *topStates) { |
|||
addedStates->set(i); |
|||
bottom->statesAbove.set(i); |
|||
top->states.insert(i); |
|||
nodes[i] = top; |
|||
} |
|||
|
|||
for (auto const& i : *bottomStates) { |
|||
addedStates->set(i); |
|||
bottom->states.insert(i); |
|||
nodes[i] = bottom; |
|||
} |
|||
|
|||
for (auto const &state : *initialMiddleStates) { |
|||
add(state); |
|||
} |
|||
} |
|||
|
|||
Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector<uint_fast64_t>* statesSorted) { |
|||
nodes = std::vector<Node *>(numberOfStates); |
|||
|
|||
this->numberOfStates = numberOfStates; |
|||
this->addedStates = new storm::storage::BitVector(numberOfStates); |
|||
this->doneBuilding = false; |
|||
this->statesSorted = *statesSorted; |
|||
this->statesToHandle = new storm::storage::BitVector(numberOfStates); |
|||
|
|||
top = new Node(); |
|||
bottom = new Node(); |
|||
|
|||
top->statesAbove = storm::storage::BitVector(numberOfStates); |
|||
bottom->statesAbove = storm::storage::BitVector(numberOfStates); |
|||
|
|||
addedStates->set(topState); |
|||
bottom->statesAbove.set(topState); |
|||
top->states.insert(topState); |
|||
nodes[topState] = top; |
|||
|
|||
addedStates->set(bottomState); |
|||
bottom->states.insert(bottomState); |
|||
nodes[bottomState] = bottom; |
|||
assert (addedStates->getNumberOfSetBits() == 2); |
|||
} |
|||
|
|||
Order::Order(Order* order) { |
|||
numberOfStates = order->getAddedStates()->size(); |
|||
nodes = std::vector<Node *>(numberOfStates); |
|||
addedStates = new storm::storage::BitVector(numberOfStates); |
|||
this->doneBuilding = order->getDoneBuilding(); |
|||
|
|||
auto oldNodes = order->getNodes(); |
|||
// Create nodes
|
|||
for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { |
|||
Node *oldNode = (*itr); |
|||
if (oldNode != nullptr) { |
|||
Node *newNode = new Node(); |
|||
newNode->states = oldNode->states; |
|||
for (auto const& i : newNode->states) { |
|||
addedStates->set(i); |
|||
nodes[i] = newNode; |
|||
} |
|||
if (oldNode == order->getTop()) { |
|||
top = newNode; |
|||
} else if (oldNode == order->getBottom()) { |
|||
bottom = newNode; |
|||
} |
|||
} |
|||
} |
|||
assert(*addedStates == *(order->getAddedStates())); |
|||
|
|||
// set all states above and below
|
|||
for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { |
|||
Node *oldNode = (*itr); |
|||
if (oldNode != nullptr) { |
|||
Node *newNode = getNode(*(oldNode->states.begin())); |
|||
newNode->statesAbove = storm::storage::BitVector((oldNode->statesAbove)); |
|||
} |
|||
} |
|||
|
|||
auto statesSortedOrder = order->getStatesSorted(); |
|||
for (auto itr = statesSortedOrder.begin(); itr != statesSortedOrder.end(); ++itr) { |
|||
this->statesSorted.push_back(*itr); |
|||
} |
|||
this->statesToHandle = new storm::storage::BitVector(*(order->statesToHandle)); |
|||
} |
|||
|
|||
void Order::addBetween(uint_fast64_t state, Node *above, Node *below) { |
|||
assert(!(*addedStates)[state]); |
|||
assert(compare(above, below) == ABOVE); |
|||
Node *newNode = new Node(); |
|||
nodes[state] = newNode; |
|||
|
|||
newNode->states.insert(state); |
|||
newNode->statesAbove = storm::storage::BitVector((above->statesAbove)); |
|||
for (auto const& state : above->states) { |
|||
newNode->statesAbove.set(state); |
|||
} |
|||
below->statesAbove.set(state); |
|||
addedStates->set(state); |
|||
} |
|||
|
|||
void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { |
|||
assert(!(*addedStates)[state]); |
|||
assert(compare(above, below) == ABOVE); |
|||
|
|||
assert (getNode(below)->states.find(below) != getNode(below)->states.end()); |
|||
assert (getNode(above)->states.find(above) != getNode(above)->states.end()); |
|||
addBetween(state, getNode(above), getNode(below)); |
|||
|
|||
} |
|||
|
|||
void Order::addToNode(uint_fast64_t state, Node *node) { |
|||
assert(!(*addedStates)[state]); |
|||
node->states.insert(state); |
|||
nodes[state] = node; |
|||
addedStates->set(state); |
|||
} |
|||
|
|||
void Order::add(uint_fast64_t state) { |
|||
assert(!(*addedStates)[state]); |
|||
addBetween(state, top, bottom); |
|||
} |
|||
|
|||
void Order::addRelationNodes(Order::Node *above, Order::Node * below) { |
|||
assert (compare(above, below) == UNKNOWN); |
|||
for (auto const& state : above->states) { |
|||
below->statesAbove.set(state); |
|||
} |
|||
below->statesAbove|=((above->statesAbove)); |
|||
assert (compare(above, below) == ABOVE); |
|||
} |
|||
|
|||
void Order::addRelation(uint_fast64_t above, uint_fast64_t below) { |
|||
addRelationNodes(getNode(above), getNode(below)); |
|||
} |
|||
|
|||
Order::NodeComparison Order::compare(uint_fast64_t state1, uint_fast64_t state2) { |
|||
return compare(getNode(state1), getNode(state2)); |
|||
} |
|||
|
|||
Order::NodeComparison Order::compare(Node* node1, Node* node2) { |
|||
if (node1 != nullptr && node2 != nullptr) { |
|||
if (node1 == node2) { |
|||
return SAME; |
|||
} |
|||
|
|||
if (above(node1, node2)) { |
|||
assert(!above(node2, node1)); |
|||
return ABOVE; |
|||
} |
|||
|
|||
if (above(node2, node1)) { |
|||
return BELOW; |
|||
} |
|||
|
|||
// tweak for cyclic pmcs
|
|||
if (doneBuilding) { |
|||
doneBuilding = false; |
|||
if (above(node1, node2)) { |
|||
assert(!above(node2, node1)); |
|||
doneBuilding = true; |
|||
return ABOVE; |
|||
} |
|||
if (above(node2, node1)) { |
|||
doneBuilding = true; |
|||
return BELOW; |
|||
} |
|||
} |
|||
} |
|||
return UNKNOWN; |
|||
} |
|||
|
|||
|
|||
bool Order::contains(uint_fast64_t state) { |
|||
return state < addedStates->size() && addedStates->get(state); |
|||
} |
|||
|
|||
Order::Node *Order::getNode(uint_fast64_t stateNumber) { |
|||
assert (stateNumber < numberOfStates); |
|||
return nodes.at(stateNumber); |
|||
} |
|||
|
|||
Order::Node *Order::getTop() { |
|||
return top; |
|||
} |
|||
|
|||
Order::Node *Order::getBottom() { |
|||
return bottom; |
|||
} |
|||
|
|||
std::vector<Order::Node*> Order::getNodes() { |
|||
return nodes; |
|||
} |
|||
|
|||
storm::storage::BitVector* Order::getAddedStates() { |
|||
return addedStates; |
|||
} |
|||
|
|||
bool Order::getDoneBuilding() { |
|||
return doneBuilding; |
|||
} |
|||
|
|||
void Order::setDoneBuilding(bool done) { |
|||
doneBuilding = done; |
|||
} |
|||
|
|||
std::vector<uint_fast64_t> Order::sortStates(storm::storage::BitVector* states) { |
|||
uint_fast64_t numberOfSetBits = states->getNumberOfSetBits(); |
|||
auto stateSize = states->size(); |
|||
auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize); |
|||
for (auto state : *states) { |
|||
if (result[0] == stateSize) { |
|||
result[0] = state; |
|||
} else { |
|||
uint_fast64_t i = 0; |
|||
bool added = false; |
|||
while (i < numberOfSetBits && !added) { |
|||
if (result[i] == stateSize) { |
|||
result[i] = state; |
|||
added = true; |
|||
} else { |
|||
auto compareRes = compare(state, result[i]); |
|||
if (compareRes == ABOVE) { |
|||
auto temp = result[i]; |
|||
result[i] = state; |
|||
for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { |
|||
auto temp2 = result[j]; |
|||
result[j] = temp; |
|||
temp = temp2; |
|||
} |
|||
added = true; |
|||
} else if (compareRes == UNKNOWN) { |
|||
break; |
|||
} else if (compareRes == SAME) { |
|||
++i; |
|||
auto temp = result[i]; |
|||
result[i] = state; |
|||
for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) { |
|||
auto temp2 = result[j]; |
|||
result[j] = temp; |
|||
temp = temp2; |
|||
} |
|||
added = true; |
|||
} |
|||
} |
|||
++i; |
|||
} |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
bool Order::above(Node *node1, Node *node2) { |
|||
bool found = false; |
|||
for (auto const& state : node1->states) { |
|||
found = ((node2->statesAbove))[state]; |
|||
if (found) { |
|||
break; |
|||
} |
|||
} |
|||
|
|||
if (!found && !doneBuilding) { |
|||
storm::storage::BitVector statesSeen((node2->statesAbove)); |
|||
for (auto const &i: (node2->statesAbove)) { |
|||
auto nodeI = getNode(i); |
|||
if (((nodeI->statesAbove) & statesSeen) != (nodeI->statesAbove)) { |
|||
found = above(node1, nodeI, node2, &statesSeen); |
|||
} |
|||
if (found) { |
|||
for (auto const& state:node1->states) { |
|||
node2->statesAbove.set(state); |
|||
} |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
return found; |
|||
} |
|||
|
|||
bool Order::above(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2, |
|||
storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen) { |
|||
bool found = false; |
|||
for (auto const& state : node1->states) { |
|||
found = ((node2->statesAbove))[state]; |
|||
if (found) { |
|||
break; |
|||
} |
|||
} |
|||
if (!found) { |
|||
nodePrev->statesAbove|=((node2->statesAbove)); |
|||
statesSeen->operator|=(((node2->statesAbove))); |
|||
|
|||
for (auto const &i: node2->statesAbove) { |
|||
if (!(*statesSeen)[i]) { |
|||
auto nodeI = getNode(i); |
|||
if (((nodeI->statesAbove) & *statesSeen) != (nodeI->statesAbove)) { |
|||
found = above(node1, nodeI, node2, statesSeen); |
|||
} |
|||
} |
|||
if (found) { |
|||
break; |
|||
} |
|||
|
|||
} |
|||
} |
|||
return found; |
|||
} |
|||
|
|||
void Order::mergeNodes(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2) { |
|||
// Merges node2 into node 1
|
|||
// everything above n2 also above n1
|
|||
node1->statesAbove|=((node2->statesAbove)); |
|||
// everything below node 2 also below node 1
|
|||
|
|||
// add states of node 2 to node 1
|
|||
node1->states.insert(node2->states.begin(), node2->states.end()); |
|||
|
|||
for(auto const& i : node2->states) { |
|||
nodes[i] = node1; |
|||
} |
|||
} |
|||
|
|||
void Order::merge(uint_fast64_t var1, uint_fast64_t var2) { |
|||
mergeNodes(getNode(var1), getNode(var2)); |
|||
} |
|||
|
|||
std::vector<uint_fast64_t> Order::getStatesSorted() { |
|||
return statesSorted; |
|||
} |
|||
|
|||
uint_fast64_t Order::getNextSortedState() { |
|||
if (statesSorted.begin() != statesSorted.end()) { |
|||
return *(statesSorted.begin()); |
|||
} else { |
|||
return numberOfStates; |
|||
} |
|||
} |
|||
|
|||
void Order::removeFirstStatesSorted() { |
|||
statesSorted.erase(statesSorted.begin()); |
|||
} |
|||
|
|||
void Order::removeStatesSorted(uint_fast64_t state) { |
|||
assert(containsStatesSorted(state)); |
|||
statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), state)); |
|||
} |
|||
|
|||
bool Order::containsStatesSorted(uint_fast64_t state) { |
|||
return std::find(statesSorted.begin(), statesSorted.end(), state) != statesSorted.end(); |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,247 @@ |
|||
#ifndef ORDER_ORDER_H |
|||
#define ORDER_ORDER_H |
|||
|
|||
#include <iostream> |
|||
#include <set> |
|||
#include <vector> |
|||
#include <unordered_map> |
|||
#include <boost/container/flat_set.hpp> |
|||
|
|||
#include "storm/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
|
|||
class Order { |
|||
|
|||
public: |
|||
/*! |
|||
* Constants for comparison of nodes/states |
|||
*/ |
|||
enum NodeComparison { |
|||
UNKNOWN, |
|||
BELOW, |
|||
ABOVE, |
|||
SAME, |
|||
}; |
|||
struct Node { |
|||
boost::container::flat_set<uint_fast64_t> states; |
|||
storm::storage::BitVector statesAbove; |
|||
}; |
|||
|
|||
/*! |
|||
* Constructs an order with the given top node and bottom node. |
|||
* |
|||
* @param topNode The top node of the resulting order. |
|||
* @param bottomNode The bottom node of the resulting order. |
|||
*/ |
|||
Order(storm::storage::BitVector* topStates, |
|||
storm::storage::BitVector* bottomStates, |
|||
storm::storage::BitVector* initialMiddleStates, |
|||
uint_fast64_t numberOfStates, |
|||
std::vector<uint_fast64_t>* statesSorted); |
|||
|
|||
/*! |
|||
* Constructs an order with the given top state and bottom state. |
|||
* |
|||
* @param top The top state of the resulting order. |
|||
* @param bottom The bottom state of the resulting order. |
|||
* @param numberOfStates Max number of states in order. |
|||
*/ |
|||
Order(uint_fast64_t top, |
|||
uint_fast64_t bottom, |
|||
uint_fast64_t numberOfStates, |
|||
std::vector<uint_fast64_t>* statesSorted); |
|||
|
|||
/*! |
|||
* Constructs a copy of the given order. |
|||
* |
|||
* @param order The original order. |
|||
*/ |
|||
Order(Order* order); |
|||
|
|||
/*! |
|||
* Adds a node with the given state below node1 and above node2. |
|||
* @param state The given state. |
|||
* @param node1 The pointer to the node below which a new node (with state) is added |
|||
* @param node2 The pointer to the node above which a new node (with state) is added |
|||
*/ |
|||
void addBetween(uint_fast64_t state, Node *node1, Node *node2); |
|||
|
|||
/*! |
|||
* Adds a node with the given state between the nodes of below and above. |
|||
* Result: below -> state -> above |
|||
* @param state The given state. |
|||
* @param above The state number of the state below which a new node (with state) is added |
|||
* @param below The state number of the state above which a new node (with state) is added |
|||
*/ |
|||
void addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below); |
|||
|
|||
/*! |
|||
* Adds state to the states of the given node. |
|||
* @param state The state which is added. |
|||
* @param node The pointer to the node to which state is added, should not be nullptr. |
|||
*/ |
|||
void addToNode(uint_fast64_t state, Node *node); |
|||
|
|||
/*! |
|||
* Adds state between the top and bottom node of the order |
|||
* @param state The given state |
|||
*/ |
|||
void add(uint_fast64_t state); |
|||
|
|||
/*! |
|||
* Adds a new relation between two nodes to the order |
|||
* @param above The node closest to the top Node of the Order. |
|||
* @param below The node closest to the bottom Node of the Order. |
|||
*/ |
|||
void addRelationNodes(storm::analysis::Order::Node *above, storm::analysis::Order::Node * below); |
|||
|
|||
/*! |
|||
* Adds a new relation between two states to the order |
|||
* @param above The state closest to the top Node of the Order. |
|||
* @param below The state closest to the bottom Node of the Order. |
|||
*/ |
|||
void addRelation(uint_fast64_t above, uint_fast64_t below); |
|||
|
|||
/*! |
|||
* Compares the level of the nodes of the states. |
|||
* Behaviour unknown when one or more of the states doesnot occur at any Node in the Order. |
|||
* @param state1 The first state. |
|||
* @param state2 The second state. |
|||
* @return SAME if the nodes are on the same level; |
|||
* ABOVE if the node of the first state is closer to top then the node of the second state; |
|||
* BELOW if the node of the second state is closer to top then the node of the first state; |
|||
* UNKNOWN if it is unclear from the structure of the order how the nodes relate. |
|||
*/ |
|||
Order::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); |
|||
|
|||
/*! |
|||
* Check if state is already in order |
|||
* @param state |
|||
* @return |
|||
*/ |
|||
bool contains(uint_fast64_t state); |
|||
|
|||
/*! |
|||
* Retrieves the pointer to a Node at which the state occurs. |
|||
* |
|||
* @param state The number of the state. |
|||
* |
|||
* @return The pointer to the node of the state, nullptr if the node does not exist. |
|||
*/ |
|||
Node *getNode(uint_fast64_t state); |
|||
|
|||
/*! |
|||
* Retrieves the top node of the order. |
|||
* |
|||
* @return The top node. |
|||
*/ |
|||
Node* getTop(); |
|||
|
|||
/*! |
|||
* Retrieves the bottom node of the order. |
|||
* |
|||
* @return The bottom node. |
|||
*/ |
|||
Node* getBottom(); |
|||
|
|||
/*! |
|||
* Returns the vector with the nodes of the order. |
|||
* Each index in the vector refers to a state. |
|||
* When the state is not yet added at a node, it will contain the nullptr. |
|||
* |
|||
* @return The vector with nodes of the order. |
|||
*/ |
|||
std::vector<Node*> getNodes(); |
|||
|
|||
/*! |
|||
* Returns a BitVector in which all added states are set. |
|||
* |
|||
* @return The BitVector with all added states. |
|||
*/ |
|||
storm::storage::BitVector* getAddedStates(); |
|||
|
|||
/*! |
|||
* Returns true if done building the order. |
|||
* @return |
|||
*/ |
|||
bool getDoneBuilding(); |
|||
|
|||
/*! |
|||
* Compares two nodes in the order |
|||
* @param node1 |
|||
* @param node2 |
|||
* @return BELOW, ABOVE, SAME or UNKNOWN |
|||
*/ |
|||
NodeComparison compare(Node* node1, Node* node2); |
|||
|
|||
/*! |
|||
* Sorts the given stats if possible. |
|||
* |
|||
* @param states Bitvector of the states to sort |
|||
* @return Vector with states sorted, length equals number of states to sort. |
|||
* If states cannot be sorted, last state of the vector will always equal the length of the BitVector |
|||
*/ |
|||
std::vector<uint_fast64_t> sortStates(storm::storage::BitVector* states); |
|||
|
|||
/*! |
|||
* If the order is fully build, this can be set to true. |
|||
*/ |
|||
void setDoneBuilding(bool done); |
|||
|
|||
/*! |
|||
* Prints a string representation of the order to the output stream. |
|||
* |
|||
* @param out The stream to output to. |
|||
*/ |
|||
void toString(std::ostream &out); |
|||
|
|||
/*! |
|||
* Merges node2 into node1 |
|||
* @param node1 |
|||
* @param node2 |
|||
*/ |
|||
void mergeNodes(Node* node1, Node* node2); |
|||
/*! |
|||
* Merges node of var2 into node of var1 |
|||
* @param var1 |
|||
* @param var2 |
|||
*/ |
|||
void merge(uint_fast64_t var1, uint_fast64_t var2); |
|||
|
|||
storm::storage::BitVector* statesToHandle; |
|||
|
|||
uint_fast64_t getNextSortedState(); |
|||
|
|||
bool containsStatesSorted(uint_fast64_t state); |
|||
|
|||
void removeFirstStatesSorted(); |
|||
|
|||
void removeStatesSorted(uint_fast64_t state); |
|||
|
|||
protected: |
|||
std::vector<uint_fast64_t> getStatesSorted(); |
|||
|
|||
private: |
|||
std::vector<Node*> nodes; |
|||
|
|||
std::vector<uint_fast64_t> statesSorted; |
|||
|
|||
storm::storage::BitVector* addedStates; |
|||
|
|||
Node* top; |
|||
|
|||
Node* bottom; |
|||
|
|||
uint_fast64_t numberOfStates; |
|||
|
|||
bool above(Node * node1, Node * node2); |
|||
|
|||
bool above(Node * node1, Node * node2, storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen); |
|||
|
|||
bool doneBuilding; |
|||
}; |
|||
} |
|||
} |
|||
#endif //ORDER_ORDER_H |
|||
@ -0,0 +1,490 @@ |
|||
//
|
|||
// Created by Jip Spel on 28.08.18.
|
|||
//
|
|||
|
|||
#include "OrderExtender.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/graph.h"
|
|||
#include "storm/storage/SparseMatrix.h"
|
|||
#include "storm/utility/graph.h"
|
|||
#include <storm/logic/Formula.h>
|
|||
#include <storm/modelchecker/propositional/SparsePropositionalModelChecker.h>
|
|||
#include "storm/models/sparse/Model.h"
|
|||
#include "storm/modelchecker/results/CheckResult.h"
|
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
|
|||
|
|||
#include "storm/exceptions/NotImplementedException.h"
|
|||
#include "storm/exceptions/NotSupportedException.h"
|
|||
|
|||
#include <set>
|
|||
#include <boost/container/flat_set.hpp>
|
|||
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
|
|||
#include "storm/storage/StronglyConnectedComponent.h"
|
|||
|
|||
#include "storm/storage/BitVector.h"
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/utility/Stopwatch.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
|
|||
template<typename ValueType> |
|||
OrderExtender<ValueType>::OrderExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) { |
|||
this->model = model; |
|||
this->matrix = model->getTransitionMatrix(); |
|||
this->assumptionSeen = false; |
|||
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); |
|||
|
|||
// Build stateMap
|
|||
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { |
|||
stateMap[i] = new storm::storage::BitVector(numberOfStates, false); |
|||
auto row = matrix.getRow(i); |
|||
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { |
|||
// ignore self-loops when there are more transitions
|
|||
if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) { |
|||
stateMap[i]->set(rowItr->getColumn(), true); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Check if MC contains cycles
|
|||
storm::storage::StronglyConnectedComponentDecompositionOptions const options; |
|||
this->sccs = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options); |
|||
acyclic = true; |
|||
for (size_t i = 0; acyclic && i < sccs.size(); ++i) { |
|||
acyclic &= sccs.getBlock(i).size() <= 1; |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) { |
|||
STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); |
|||
STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() |
|||
&& ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() |
|||
|| (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula"); |
|||
|
|||
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); |
|||
|
|||
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model); |
|||
storm::storage::BitVector phiStates; |
|||
storm::storage::BitVector psiStates; |
|||
if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { |
|||
phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
} else { |
|||
phiStates = storm::storage::BitVector(numberOfStates, true); |
|||
psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
} |
|||
|
|||
|
|||
// Get the maybeStates
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); |
|||
storm::storage::BitVector topStates = statesWithProbability01.second; |
|||
storm::storage::BitVector bottomStates = statesWithProbability01.first; |
|||
|
|||
STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); |
|||
STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); |
|||
|
|||
// Transform to Order
|
|||
auto matrix = this->model->getTransitionMatrix(); |
|||
|
|||
auto initialMiddleStates = storm::storage::BitVector(numberOfStates); |
|||
// Add possible cycle breaking states
|
|||
if (!acyclic) { |
|||
for (size_t i = 0; i < sccs.size(); ++i) { |
|||
auto scc = sccs.getBlock(i); |
|||
if (scc.size() > 1) { |
|||
auto states = scc.getStates(); |
|||
// check if the state has already one successor in bottom of top, in that case pick it
|
|||
for (auto const& state : states) { |
|||
auto successors = stateMap[state]; |
|||
if (successors->getNumberOfSetBits() == 2) { |
|||
auto succ1 = successors->getNextSetIndex(0); |
|||
auto succ2 = successors->getNextSetIndex(succ1 + 1); |
|||
auto intersection = bottomStates | topStates; |
|||
if (intersection[succ1] || intersection[succ2]) { |
|||
initialMiddleStates.set(state); |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix); |
|||
Order *order = new Order(&topStates, &bottomStates, &initialMiddleStates, numberOfStates, &statesSorted); |
|||
|
|||
return this->extendOrder(order); |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues) { |
|||
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); |
|||
uint_fast64_t bottom = numberOfStates; |
|||
uint_fast64_t top = numberOfStates; |
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix); |
|||
Order *order = nullptr; |
|||
|
|||
for (auto state : statesSorted) { |
|||
if ((minValues[numberOfStates - 1 - state] == 1 || maxValues[numberOfStates - 1 - state] == 0) |
|||
&& minValues[numberOfStates - 1 - state] == maxValues[numberOfStates - 1 - state]) { |
|||
if (maxValues[numberOfStates - 1 - state] == 0) { |
|||
assert (bottom == numberOfStates); |
|||
bottom = state; |
|||
} |
|||
if (minValues[numberOfStates - 1 - state] == 1) { |
|||
assert (top == numberOfStates); |
|||
top = state; |
|||
} |
|||
if (bottom != numberOfStates && top != numberOfStates) { |
|||
order = new Order(top, bottom, numberOfStates, &statesSorted); |
|||
} |
|||
|
|||
} else { |
|||
assert (order != nullptr); |
|||
auto successors = stateMap[state]; |
|||
if (successors->getNumberOfSetBits() == 1) { |
|||
auto succ = successors->getNextSetIndex(0); |
|||
if (succ != state) { |
|||
if (!order->contains(succ)) { |
|||
order->add(succ); |
|||
} |
|||
order->addToNode(state, order->getNode(succ)); |
|||
} |
|||
} else if (successors->getNumberOfSetBits() > 1) { |
|||
uint_fast64_t min = numberOfStates; |
|||
uint_fast64_t max = numberOfStates; |
|||
bool allSorted = true; |
|||
|
|||
for (auto succ = successors->getNextSetIndex(0); |
|||
succ < numberOfStates; succ = successors->getNextSetIndex(succ + 1)) { |
|||
if (min == numberOfStates) { |
|||
assert (max == numberOfStates); |
|||
min = succ; |
|||
max = succ; |
|||
} else { |
|||
if (minValues[numberOfStates - 1 - succ] > maxValues[numberOfStates - 1 - max]) { |
|||
max = succ; |
|||
} else if (maxValues[numberOfStates - 1 - succ] < minValues[numberOfStates - 1 - min]) { |
|||
min = succ; |
|||
} else { |
|||
allSorted = false; |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
|
|||
if (allSorted && min != max) { |
|||
if (order->contains(min) && order->contains(max)) { |
|||
assert (order->compare(min,max) == Order::UNKNOWN || order->compare(min,max) == Order::BELOW); |
|||
if (order->compare(min, max) == Order::UNKNOWN) { |
|||
order->addRelation(max, min); |
|||
} |
|||
} |
|||
if (!order->contains(min)) { |
|||
if (order->contains(max)) { |
|||
order->addBetween(min, order->getNode(max), order->getBottom()); |
|||
} else { |
|||
order->add(min); |
|||
} |
|||
} |
|||
if (!order->contains(max)) { |
|||
// Because of construction min is in the order
|
|||
order->addBetween(max, order->getTop(), order->getNode(min)); |
|||
} |
|||
assert (order->compare(max, min) == Order::ABOVE); |
|||
order->addBetween(state, max, min); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
assert (order != nullptr); |
|||
|
|||
// Handle sccs
|
|||
auto addedStates = order->getAddedStates(); |
|||
for (auto scc : sccs) { |
|||
if (scc.size() > 1) { |
|||
auto states = scc.getStates(); |
|||
auto candidate = -1; |
|||
for (auto const& state : states) { |
|||
if (addedStates->get(state)) { |
|||
candidate = -1; |
|||
break; |
|||
// if there is a state of the scc already present in the order, there is no need to add one.
|
|||
} |
|||
auto successors = stateMap[state]; |
|||
if (candidate == -1 && successors->getNumberOfSetBits() == 2) { |
|||
auto succ1 = successors->getNextSetIndex(0); |
|||
auto succ2 = successors->getNextSetIndex(succ1 + 1); |
|||
if (addedStates->get(succ1) || addedStates->get(succ2)) { |
|||
candidate = state; |
|||
} |
|||
} |
|||
} |
|||
if (candidate != -1) { |
|||
order->add(candidate); |
|||
order->statesToHandle->set(candidate); |
|||
} |
|||
} |
|||
} |
|||
return this->extendOrder(order); |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
void OrderExtender<ValueType>::handleAssumption(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) { |
|||
assert (assumption != nullptr); |
|||
assumptionSeen = true; |
|||
|
|||
storm::expressions::BinaryRelationExpression expr = *assumption; |
|||
assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater |
|||
|| expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal); |
|||
|
|||
if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); |
|||
storm::expressions::Variable var1 = expr.getFirstOperand()->asVariableExpression().getVariable(); |
|||
storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable(); |
|||
auto val1 = std::stoul(var1.getName(), nullptr, 0); |
|||
auto val2 = std::stoul(var2.getName(), nullptr, 0); |
|||
auto comp = order->compare(val1, val2); |
|||
|
|||
assert (comp == Order::UNKNOWN); |
|||
Order::Node *n1 = order->getNode(val1); |
|||
Order::Node *n2 = order->getNode(val2); |
|||
|
|||
if (n1 != nullptr && n2 != nullptr) { |
|||
order->mergeNodes(n1,n2); |
|||
} else if (n1 != nullptr) { |
|||
order->addToNode(val2, n1); |
|||
} else if (n2 != nullptr) { |
|||
order->addToNode(val1, n2); |
|||
} else { |
|||
order->add(val1); |
|||
order->addToNode(val2, order->getNode(val1)); |
|||
} |
|||
} else { |
|||
assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); |
|||
storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); |
|||
storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); |
|||
auto val1 = std::stoul(largest.getName(), nullptr, 0); |
|||
auto val2 = std::stoul(smallest.getName(), nullptr, 0); |
|||
auto compareRes = order->compare(val1, val2); |
|||
|
|||
assert(compareRes == Order::UNKNOWN); |
|||
Order::Node *n1 = order->getNode(val1); |
|||
Order::Node *n2 = order->getNode(val2); |
|||
|
|||
if (n1 != nullptr && n2 != nullptr) { |
|||
order->addRelationNodes(n1, n2); |
|||
} else if (n1 != nullptr) { |
|||
order->addBetween(val2, n1, order->getBottom()); |
|||
} else if (n2 != nullptr) { |
|||
order->addBetween(val1, order->getTop(), n2); |
|||
} else { |
|||
order->add(val1); |
|||
order->addBetween(val2, order->getNode(val1), order->getBottom()); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) { |
|||
auto numberOfStates = successors->size(); |
|||
assert (order->getAddedStates()->size() == numberOfStates); |
|||
|
|||
if (successors->getNumberOfSetBits() == 1) { |
|||
// As there is only one successor the current state and its successor must be at the same nodes.
|
|||
order->addToNode(stateNumber, order->getNode(successors->getNextSetIndex(0))); |
|||
} else if (successors->getNumberOfSetBits() == 2) { |
|||
// Otherwise, check how the two states compare, and add if the comparison is possible.
|
|||
uint_fast64_t successor1 = successors->getNextSetIndex(0); |
|||
uint_fast64_t successor2 = successors->getNextSetIndex(successor1 + 1); |
|||
|
|||
int compareResult = order->compare(successor1, successor2); |
|||
if (compareResult == Order::ABOVE) { |
|||
// successor 1 is closer to top than successor 2
|
|||
order->addBetween(stateNumber, order->getNode(successor1), |
|||
order->getNode(successor2)); |
|||
} else if (compareResult == Order::BELOW) { |
|||
// successor 2 is closer to top than successor 1
|
|||
order->addBetween(stateNumber, order->getNode(successor2), |
|||
order->getNode(successor1)); |
|||
} else if (compareResult == Order::SAME) { |
|||
// the successors are at the same level
|
|||
order->addToNode(stateNumber, order->getNode(successor1)); |
|||
} else { |
|||
assert(order->compare(successor1, successor2) == Order::UNKNOWN); |
|||
return std::make_tuple(order, successor1, successor2); |
|||
} |
|||
} else if (successors->getNumberOfSetBits() > 2) { |
|||
for (auto const& i : *successors) { |
|||
for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { |
|||
if (order->compare(i,j) == Order::UNKNOWN) { |
|||
return std::make_tuple(order, i, j); |
|||
} |
|||
} |
|||
} |
|||
|
|||
auto highest = successors->getNextSetIndex(0); |
|||
auto lowest = highest; |
|||
for (auto i = successors->getNextSetIndex(highest+1); i < numberOfStates; i = successors->getNextSetIndex(i+1)) { |
|||
if (order->compare(i, highest) == Order::ABOVE) { |
|||
highest = i; |
|||
} |
|||
if (order->compare(lowest, i) == Order::ABOVE) { |
|||
lowest = i; |
|||
} |
|||
} |
|||
if (lowest == highest) { |
|||
order->addToNode(stateNumber, order->getNode(highest)); |
|||
} else { |
|||
order->addBetween(stateNumber, order->getNode(highest), order->getNode(lowest)); |
|||
} |
|||
} |
|||
return std::make_tuple(order, numberOfStates, numberOfStates); |
|||
} |
|||
|
|||
|
|||
|
|||
template <typename ValueType> |
|||
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::extendOrder(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) { |
|||
auto numberOfStates = this->model->getNumberOfStates(); |
|||
|
|||
if (assumption != nullptr) { |
|||
handleAssumption(order, assumption); |
|||
} |
|||
|
|||
auto oldNumberSet = numberOfStates; |
|||
while (oldNumberSet != order->getAddedStates()->getNumberOfSetBits()) { |
|||
oldNumberSet = order->getAddedStates()->getNumberOfSetBits(); |
|||
|
|||
// Forward reasoning for cycles;
|
|||
if (!acyclic) { |
|||
auto statesToHandle = order->statesToHandle; |
|||
auto stateNumber = statesToHandle->getNextSetIndex(0); |
|||
|
|||
while (stateNumber != numberOfStates) { |
|||
storm::storage::BitVector *successors = stateMap[stateNumber]; |
|||
// Checking for states which are already added to the order, and only have one successor left which haven't been added yet
|
|||
auto succ1 = successors->getNextSetIndex(0); |
|||
auto succ2 = successors->getNextSetIndex(succ1 + 1); |
|||
|
|||
assert (order->contains(stateNumber)); |
|||
if (successors->getNumberOfSetBits() == 1) { |
|||
if (!order->contains(succ1)) { |
|||
order->addToNode(succ1, order->getNode(stateNumber)); |
|||
statesToHandle->set(succ1, true); |
|||
if (order->containsStatesSorted(succ1)) { |
|||
order->removeStatesSorted(succ1); |
|||
} |
|||
} |
|||
statesToHandle->set(stateNumber, false); |
|||
stateNumber = statesToHandle->getNextSetIndex(0); |
|||
} else if (successors->getNumberOfSetBits() == 2 |
|||
&& ((order->contains(succ1) && !order->contains(succ2)) |
|||
|| (!order->contains(succ1) && order->contains(succ2)))) { |
|||
|
|||
if (!order->contains(succ1)) { |
|||
std::swap(succ1, succ2); |
|||
} |
|||
|
|||
auto compare = order->compare(stateNumber, succ1); |
|||
if (compare == Order::ABOVE) { |
|||
if (order->containsStatesSorted(succ2)) { |
|||
order->removeStatesSorted(succ2); |
|||
} |
|||
order->addBetween(succ2, order->getTop(), order->getNode(stateNumber)); |
|||
statesToHandle->set(succ2); |
|||
statesToHandle->set(stateNumber, false); |
|||
stateNumber = statesToHandle->getNextSetIndex(0); |
|||
} else if (compare == Order::BELOW) { |
|||
if (order->containsStatesSorted(succ2)) { |
|||
order->removeStatesSorted(succ2); |
|||
} |
|||
order->addBetween(succ2, order->getNode(stateNumber), order->getBottom()); |
|||
statesToHandle->set(succ2); |
|||
statesToHandle->set(stateNumber, false); |
|||
stateNumber = statesToHandle->getNextSetIndex(0); |
|||
} else { |
|||
// We don't know positions, so we set the current state number to false
|
|||
statesToHandle->set(stateNumber, false); |
|||
stateNumber = statesToHandle->getNextSetIndex(0); |
|||
} |
|||
|
|||
} else if (!((order->contains(succ1) && !order->contains(succ2)) |
|||
|| (!order->contains(succ1) && order->contains(succ2)))) { |
|||
stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); |
|||
} else { |
|||
statesToHandle->set(stateNumber, false); |
|||
stateNumber = statesToHandle->getNextSetIndex(0); |
|||
} |
|||
} |
|||
|
|||
} |
|||
|
|||
// Normal backwardreasoning
|
|||
auto stateNumber = order->getNextSortedState(); |
|||
while (stateNumber != numberOfStates && order->contains(stateNumber)) { |
|||
order->removeFirstStatesSorted(); |
|||
stateNumber = order->getNextSortedState(); |
|||
|
|||
if (stateNumber != numberOfStates && order->contains(stateNumber)) { |
|||
auto resAllAdded = allSuccAdded(order, stateNumber); |
|||
if (!std::get<0>(resAllAdded)) { |
|||
return std::make_tuple(order, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); |
|||
} |
|||
} |
|||
} |
|||
|
|||
if (stateNumber != numberOfStates && !order->contains(stateNumber)) { |
|||
auto successors = stateMap[stateNumber]; |
|||
|
|||
auto result = extendAllSuccAdded(order, stateNumber, successors); |
|||
if (std::get<1>(result) != numberOfStates) { |
|||
// So we don't know the relation between all successor states
|
|||
return result; |
|||
} else { |
|||
assert (order->getNode(stateNumber) != nullptr); |
|||
if (!acyclic) { |
|||
order->statesToHandle->set(stateNumber); |
|||
} |
|||
order->removeFirstStatesSorted(); |
|||
} |
|||
} |
|||
assert (stateNumber == numberOfStates || order->getNode(stateNumber) != nullptr); |
|||
assert (stateNumber == numberOfStates || order->contains(stateNumber)); |
|||
|
|||
} |
|||
assert (order->getAddedStates()->getNumberOfSetBits() == numberOfStates); |
|||
order->setDoneBuilding(true); |
|||
return std::make_tuple(order, numberOfStates, numberOfStates); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::tuple<bool, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::allSuccAdded(storm::analysis::Order *order, uint_fast64_t stateNumber) { |
|||
auto successors = stateMap[stateNumber]; |
|||
auto numberOfStates = successors->size(); |
|||
|
|||
if (successors->getNumberOfSetBits() == 1) { |
|||
auto succ = successors->getNextSetIndex(0); |
|||
return std::make_tuple(order->contains(succ), succ, succ); |
|||
} else if (successors->getNumberOfSetBits() > 2) { |
|||
for (auto const& i : *successors) { |
|||
for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { |
|||
if (order->compare(i,j) == Order::UNKNOWN) { |
|||
return std::make_tuple(false, i, j); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
return std::make_tuple(true, numberOfStates, numberOfStates); |
|||
|
|||
} |
|||
|
|||
template class OrderExtender<storm::RationalFunction>; |
|||
} |
|||
} |
|||
@ -0,0 +1,83 @@ |
|||
#ifndef STORM_LATTICEEXTENDER_H |
|||
#define STORM_LATTICEEXTENDER_H |
|||
|
|||
#include <storm/logic/Formula.h> |
|||
#include "storm/models/sparse/Dtmc.h" |
|||
#include "storm-pars/analysis/Order.h" |
|||
#include "storm/api/storm.h" |
|||
#include "storm-pars/storage/ParameterRegion.h" |
|||
#include "storm/storage/StronglyConnectedComponentDecomposition.h" |
|||
#include "storm/storage/StronglyConnectedComponent.h" |
|||
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace analysis { |
|||
|
|||
|
|||
template<typename ValueType> |
|||
class OrderExtender { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructs OrderExtender which can extend an order |
|||
* |
|||
* @param model The model for which the order should be extended. |
|||
*/ |
|||
OrderExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model); |
|||
|
|||
/*! |
|||
* Creates an order based on the given formula. |
|||
* |
|||
* @param formulas The formulas based on which the order is created, only the first is used. |
|||
* @return A triple with a pointer to the order and two states of which the current place in the order |
|||
* is unknown but needed. When the states have as number the number of states, no states are |
|||
* unplaced but needed. |
|||
*/ |
|||
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas); |
|||
|
|||
/*! |
|||
* Creates an order based on the given extremal values. |
|||
* |
|||
* @return A triple with a pointer to the order and two states of which the current place in the order |
|||
* is unknown but needed. When the states have as number the number of states, no states are |
|||
* unplaced but needed. |
|||
*/ |
|||
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues); |
|||
|
|||
|
|||
/*! |
|||
* Extends the order based on the given assumption. |
|||
* |
|||
* @param order The order. |
|||
* @param assumption The assumption on states. |
|||
* @return A triple with a pointer to the order and two states of which the current place in the order |
|||
* is unknown but needed. When the states have as number the number of states, no states are |
|||
* unplaced but needed. |
|||
*/ |
|||
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> extendOrder(storm::analysis::Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr); |
|||
|
|||
|
|||
private: |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; |
|||
|
|||
std::map<uint_fast64_t, storm::storage::BitVector*> stateMap; |
|||
|
|||
bool acyclic; |
|||
|
|||
bool assumptionSeen; |
|||
|
|||
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs; |
|||
|
|||
storm::storage::SparseMatrix<ValueType> matrix; |
|||
|
|||
void handleAssumption(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption); |
|||
|
|||
std::tuple<Order*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); |
|||
|
|||
std::tuple<bool, uint_fast64_t, uint_fast64_t> allSuccAdded(Order* order, uint_fast64_t stateNumber); |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif //STORM_ORDEREXTENDER_H |
|||
@ -0,0 +1,54 @@ |
|||
#include "storm-pars/settings/modules/MonotonicitySettings.h"
|
|||
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/settings/ArgumentBuilder.h"
|
|||
#include "storm/settings/Argument.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/exceptions/IllegalArgumentValueException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string MonotonicitySettings::moduleName = "monotonicity"; |
|||
const std::string MonotonicitySettings::monotonicityAnalysis = "monotonicity-analysis"; |
|||
const std::string MonotonicitySettings::sccElimination = "mon-elim-scc"; |
|||
const std::string MonotonicitySettings::validateAssumptions = "mon-validate-assumptions"; |
|||
const std::string MonotonicitySettings::samplesMonotonicityAnalysis = "mon-samples"; |
|||
const std::string MonotonicitySettings::precision = "mon-precision"; |
|||
|
|||
MonotonicitySettings::MonotonicitySettings() : ModuleSettings(moduleName) { |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").setIsAdvanced().build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").setIsAdvanced().build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").setIsAdvanced().build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples").setIsAdvanced() |
|||
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples").setIsAdvanced() |
|||
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build()); |
|||
|
|||
} |
|||
|
|||
bool MonotonicitySettings::isMonotonicityAnalysisSet() const { |
|||
return this->getOption(monotonicityAnalysis).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool MonotonicitySettings::isSccEliminationSet() const { |
|||
return this->getOption(sccElimination).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool MonotonicitySettings::isValidateAssumptionsSet() const { |
|||
return this->getOption(validateAssumptions).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
uint_fast64_t MonotonicitySettings::getNumberOfSamples() const { |
|||
return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); |
|||
} |
|||
|
|||
double MonotonicitySettings::getMonotonicityAnalysisPrecision() const { |
|||
return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble(); |
|||
} |
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,60 @@ |
|||
#ifndef STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ |
|||
#define STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ |
|||
|
|||
#include "storm/settings/modules/ModuleSettings.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
/*! |
|||
* This class represents the settings for monotonicity checking. |
|||
*/ |
|||
class MonotonicitySettings : public ModuleSettings { |
|||
public: |
|||
|
|||
/*! |
|||
* Creates a new set of monotonicity checking settings. |
|||
*/ |
|||
MonotonicitySettings(); |
|||
|
|||
/*! |
|||
* Retrieves whether monotonicity analysis should be applied. |
|||
*/ |
|||
bool isMonotonicityAnalysisSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether SCCs in the monotonicity analysis should be eliminated. |
|||
*/ |
|||
bool isSccEliminationSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether assumptions in monotonicity analysis should be validated |
|||
*/ |
|||
bool isValidateAssumptionsSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of samples used for sampling in the monotonicity analysis |
|||
*/ |
|||
uint_fast64_t getNumberOfSamples() const; |
|||
|
|||
/*! |
|||
* Retrieves the precision for the extremal value |
|||
*/ |
|||
double getMonotonicityAnalysisPrecision() const; |
|||
|
|||
const static std::string moduleName; |
|||
|
|||
private: |
|||
const static std::string monotonicityAnalysis; |
|||
const static std::string sccElimination; |
|||
const static std::string validateAssumptions; |
|||
const static std::string samplesMonotonicityAnalysis; |
|||
const static std::string precision; |
|||
}; |
|||
|
|||
} // namespace modules |
|||
} // namespace settings |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ */ |
|||
@ -0,0 +1,67 @@ |
|||
//
|
|||
// Created by Jip Spel on 24.09.18.
|
|||
//
|
|||
|
|||
#include "RationalFunctionToExpression.h"
|
|||
#include "storm/utility/constants.h"
|
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
template <typename ValueType> |
|||
RationalFunctionToExpression<ValueType>::RationalFunctionToExpression(std::shared_ptr<ExpressionManager> manager) : manager(manager) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::shared_ptr<ExpressionManager> RationalFunctionToExpression<ValueType>::getManager() { |
|||
return manager; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
Expression RationalFunctionToExpression<ValueType>::toExpression(ValueType function) { |
|||
function.simplify(); |
|||
auto varsFunction = function.gatherVariables(); |
|||
for (auto var : varsFunction) { |
|||
auto varsManager = manager->getVariables(); |
|||
bool found = find_if(varsManager.begin(), varsManager.end(), |
|||
[&](auto val) -> bool { |
|||
return val.getName() == var.name(); |
|||
}) != varsManager.end(); |
|||
if (!found) { |
|||
manager->declareRationalVariable(var.name()); |
|||
} |
|||
} |
|||
|
|||
auto denominator = function.denominator(); |
|||
if (!denominator.isConstant()) { |
|||
STORM_LOG_DEBUG("Expecting the denominator to be constant"); |
|||
} |
|||
|
|||
storm::expressions::Expression result; |
|||
if (function.isConstant()) { |
|||
result = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(function.constantPart())); |
|||
} else { |
|||
auto nominator = function.nominatorAsPolynomial().polynomialWithCoefficient(); |
|||
result = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(nominator.constantPart())); |
|||
for (auto itr = nominator.begin(); itr != nominator.end(); ++itr) { |
|||
varsFunction.clear(); |
|||
itr->gatherVariables(varsFunction); |
|||
|
|||
storm::expressions::Expression nominatorPartExpr = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->coeff())); |
|||
for (auto var : varsFunction) { |
|||
nominatorPartExpr = nominatorPartExpr * (manager->getVariable(var.name())^manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->monomial()->exponentOfVariable(var)))); |
|||
} |
|||
if (varsFunction.size() >= 1) { |
|||
result = result + nominatorPartExpr; |
|||
} |
|||
} |
|||
storm::expressions::Expression denominatorVal = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(denominator.constantPart())); |
|||
result = result / denominatorVal; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template class RationalFunctionToExpression<storm::RationalFunction>; |
|||
} |
|||
} |
|||
@ -0,0 +1,40 @@ |
|||
// |
|||
// Created by Jip Spel on 24.09.18. |
|||
// |
|||
|
|||
#ifndef STORM_RATIONALFUNCTIONTOEXPRESSION_H |
|||
#define STORM_RATIONALFUNCTIONTOEXPRESSION_H |
|||
|
|||
#include "storm/storage/expressions/ExpressionManager.h" |
|||
#include "storm/storage/expressions/Expression.h" |
|||
|
|||
namespace storm { |
|||
namespace expressions { |
|||
template<typename ValueType> |
|||
class RationalFunctionToExpression { |
|||
public: |
|||
RationalFunctionToExpression(std::shared_ptr<ExpressionManager> manager); |
|||
|
|||
/*! |
|||
* Retrieves the manager responsible for the variables of this valuation. |
|||
* |
|||
* @return The pointer to the manager. |
|||
*/ |
|||
std::shared_ptr<ExpressionManager> getManager(); |
|||
|
|||
/*! |
|||
* Transforms the function into an expression. |
|||
* |
|||
* @param function The function to transform |
|||
* @return The created expression. |
|||
*/ |
|||
Expression toExpression(ValueType function); |
|||
|
|||
private: |
|||
// The manager responsible for the variables of this valuation. |
|||
std::shared_ptr<ExpressionManager> manager; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif //STORM_RATIONALFUNCTIONTOEXPRESSION_H |
|||
@ -0,0 +1,373 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "test/storm_gtest.h"
|
|||
|
|||
#include "storm-parsers/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm-parsers/parser/AutoParser.h"
|
|||
#include "storm-parsers/parser/PrismParser.h"
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
#include "storm/api/builder.h"
|
|||
|
|||
#include "storm-pars/analysis/AssumptionChecker.h"
|
|||
#include "storm-pars/analysis/Order.h"
|
|||
#include "storm/storage/expressions/BinaryRelationExpression.h"
|
|||
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
|
|||
#include "storm-pars/storage/ParameterRegion.h"
|
|||
|
|||
#include "storm-pars/api/storm-pars.h"
|
|||
#include "storm/api/storm.h"
|
|||
|
|||
#include "storm-parsers/api/storm-parsers.h"
|
|||
|
|||
#include "storm-pars/api/region.h"
|
|||
|
|||
|
|||
TEST(AssumptionCheckerTest, Brp_no_bisimulation) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [F s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
|
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); |
|||
|
|||
// Create the region
|
|||
storm::storage::ParameterRegion<storm::RationalFunction>::Valuation lowerBoundaries; |
|||
storm::storage::ParameterRegion<storm::RationalFunction>::Valuation upperBoundaries; |
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.00001, 0.00001 <= pL <= 0.99999", vars); |
|||
|
|||
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
|
|||
// Check on samples
|
|||
auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager()); |
|||
expressionManager->declareRationalVariable("7"); |
|||
expressionManager->declareRationalVariable("5"); |
|||
|
|||
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
|
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
|
|||
|
|||
storm::storage::BitVector above(8); |
|||
above.set(0); |
|||
storm::storage::BitVector below(8); |
|||
below.set(1); |
|||
storm::storage::BitVector initialMiddle(8); |
|||
|
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 8, &statesSorted); |
|||
// Validate assumption
|
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); |
|||
// EXPECT_FALSE(checker.validated(assumption));
|
|||
|
|||
expressionManager->declareRationalVariable("6"); |
|||
expressionManager->declareRationalVariable("8"); |
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("6").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("8").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
above = storm::storage::BitVector(13); |
|||
above.set(12); |
|||
below = storm::storage::BitVector(13); |
|||
below.set(9); |
|||
initialMiddle = storm::storage::BitVector(13); |
|||
|
|||
dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 13, &statesSorted); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); |
|||
// EXPECT_EQ(checker.validated(assumption));
|
|||
// EXPECT_FALSE(checker.valid(assumption));
|
|||
} |
|||
|
|||
TEST(AssumptionCheckerTest, Simple1) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm"; |
|||
std::string formulaAsString = "P=? [F s=3]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars); |
|||
|
|||
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
|
|||
auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager()); |
|||
expressionManager->declareRationalVariable("1"); |
|||
expressionManager->declareRationalVariable("2"); |
|||
|
|||
// Checking on samples
|
|||
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
} |
|||
|
|||
TEST(AssumptionCheckerTest, Simple2) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple2.pm"; |
|||
std::string formulaAsString = "P=? [F s=3]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars); |
|||
|
|||
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
|
|||
auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager()); |
|||
expressionManager->declareRationalVariable("1"); |
|||
expressionManager->declareRationalVariable("2"); |
|||
|
|||
storm::storage::BitVector above(5); |
|||
above.set(3); |
|||
storm::storage::BitVector below(5); |
|||
below.set(4); |
|||
storm::storage::BitVector initialMiddle(5); |
|||
|
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); |
|||
|
|||
// Checking on samples and validate
|
|||
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
|
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
} |
|||
|
|||
TEST(AssumptionCheckerTest, Simple3) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple3.pm"; |
|||
std::string formulaAsString = "P=? [F s=4]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(6ul, dtmc->getNumberOfStates()); |
|||
ASSERT_EQ(12ul, dtmc->getNumberOfTransitions()); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars); |
|||
|
|||
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
|
|||
auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager()); |
|||
expressionManager->declareRationalVariable("1"); |
|||
expressionManager->declareRationalVariable("2"); |
|||
|
|||
storm::storage::BitVector above(6); |
|||
above.set(4); |
|||
storm::storage::BitVector below(6); |
|||
below.set(5); |
|||
storm::storage::BitVector initialMiddle(6); |
|||
|
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 6, &statesSorted); |
|||
order->add(3); |
|||
|
|||
// Checking on samples and validate
|
|||
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
} |
|||
|
|||
TEST(AssumptionCheckerTest, Simple4) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple4.pm"; |
|||
std::string formulaAsString = "P=? [F s=3]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.4", vars); |
|||
|
|||
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
|
|||
auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager()); |
|||
expressionManager->declareRationalVariable("1"); |
|||
expressionManager->declareRationalVariable("2"); |
|||
|
|||
// Order
|
|||
storm::storage::BitVector above(5); |
|||
above.set(3); |
|||
storm::storage::BitVector below(5); |
|||
below.set(4); |
|||
storm::storage::BitVector initialMiddle(5); |
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); |
|||
|
|||
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Greater)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
|
|||
assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( |
|||
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), |
|||
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), |
|||
expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), |
|||
storm::expressions::BinaryRelationExpression::RelationType::Equal)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); |
|||
|
|||
|
|||
|
|||
} |
|||
@ -0,0 +1,319 @@ |
|||
//
|
|||
// Created by Jip Spel on 20.09.18.
|
|||
//
|
|||
|
|||
// TODO: cleanup includes
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "test/storm_gtest.h"
|
|||
|
|||
#include "storm-parsers/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm-parsers/parser/AutoParser.h"
|
|||
#include "storm-parsers/parser/PrismParser.h"
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
#include "storm/api/builder.h"
|
|||
|
|||
#include "storm-pars/analysis/Order.h"
|
|||
#include "storm-pars/analysis/AssumptionMaker.h"
|
|||
#include "storm-pars/analysis/AssumptionChecker.h"
|
|||
#include "storm-pars/analysis/OrderExtender.h"
|
|||
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
|
|||
|
|||
#include "storm-pars/api/storm-pars.h"
|
|||
#include "storm/api/storm.h"
|
|||
|
|||
#include "storm-parsers/api/storm-parsers.h"
|
|||
|
|||
TEST(AssumptionMakerTest, Brp_without_bisimulation) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [F s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); |
|||
|
|||
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc); |
|||
auto criticalTuple = extender->toOrder(formulas); |
|||
ASSERT_EQ(183, std::get<1>(criticalTuple)); |
|||
ASSERT_EQ(186, std::get<2>(criticalTuple)); |
|||
|
|||
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true); |
|||
auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); |
|||
|
|||
EXPECT_EQ(3, result.size()); |
|||
|
|||
bool foundFirst = false; |
|||
bool foundSecond = false; |
|||
bool foundThird = false; |
|||
for (auto itr = result.begin(); itr != result.end(); ++itr) { |
|||
if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "183") { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundFirst = true; |
|||
} else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundSecond = true; |
|||
} else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); |
|||
foundThird = true; |
|||
} else { |
|||
EXPECT_TRUE(false); |
|||
} |
|||
} |
|||
EXPECT_TRUE(foundFirst); |
|||
EXPECT_TRUE(foundSecond); |
|||
EXPECT_TRUE(foundThird); |
|||
} |
|||
|
|||
TEST(AssumptionMakerTest, Brp_without_bisimulation_no_validation) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [F s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); |
|||
|
|||
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc); |
|||
auto criticalTuple = extender->toOrder(formulas); |
|||
ASSERT_EQ(183, std::get<1>(criticalTuple)); |
|||
ASSERT_EQ(186, std::get<2>(criticalTuple)); |
|||
|
|||
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
// This one does not validate the assumptions!
|
|||
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), false); |
|||
auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); |
|||
|
|||
EXPECT_EQ(3, result.size()); |
|||
|
|||
bool foundFirst = false; |
|||
bool foundSecond = false; |
|||
bool foundThird = false; |
|||
for (auto itr = result.begin(); itr != result.end(); ++itr) { |
|||
if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "183") { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundFirst = true; |
|||
} else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundSecond = true; |
|||
} else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); |
|||
foundThird = true; |
|||
} else { |
|||
EXPECT_TRUE(false); |
|||
} |
|||
} |
|||
EXPECT_TRUE(foundFirst); |
|||
EXPECT_TRUE(foundSecond); |
|||
EXPECT_TRUE(foundThird); |
|||
} |
|||
|
|||
TEST(AssumptionMakerTest, Simple1) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm"; |
|||
std::string formulaAsString = "P=? [F s=3]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 5); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); |
|||
|
|||
storm::storage::BitVector above(5); |
|||
above.set(3); |
|||
storm::storage::BitVector below(5); |
|||
below.set(4); |
|||
storm::storage::BitVector initialMiddle(5); |
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); |
|||
|
|||
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true); |
|||
auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); |
|||
|
|||
EXPECT_EQ(3, result.size()); |
|||
|
|||
bool foundFirst = false; |
|||
bool foundSecond = false; |
|||
bool foundThird = false; |
|||
for (auto itr = result.begin(); itr != result.end(); ++itr) { |
|||
if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "1") { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundFirst = true; |
|||
} else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundSecond = true; |
|||
} else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); |
|||
foundThird = true; |
|||
} else { |
|||
EXPECT_TRUE(false); |
|||
} |
|||
} |
|||
EXPECT_TRUE(foundFirst); |
|||
EXPECT_TRUE(foundSecond); |
|||
EXPECT_TRUE(foundThird); |
|||
} |
|||
|
|||
TEST(AssumptionMakerTest, Simple2) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple2.pm"; |
|||
std::string formulaAsString = "P=? [F s=3]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
// Create the region
|
|||
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 5); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); |
|||
|
|||
storm::storage::BitVector above(5); |
|||
above.set(3); |
|||
storm::storage::BitVector below(5); |
|||
below.set(4); |
|||
storm::storage::BitVector initialMiddle(5); |
|||
|
|||
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); |
|||
|
|||
auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); |
|||
|
|||
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, region, 3); |
|||
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true); |
|||
auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); |
|||
|
|||
auto itr = result.begin(); |
|||
|
|||
EXPECT_EQ(3, result.size()); |
|||
|
|||
bool foundFirst = false; |
|||
bool foundSecond = false; |
|||
bool foundThird = false; |
|||
for (auto itr = result.begin(); itr != result.end(); ++itr) { |
|||
if (!foundFirst && itr->first->getFirstOperand()->asVariableExpression().getVariable().getName() == "1") { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundFirst = true; |
|||
} else if (!foundSecond && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType()); |
|||
foundSecond = true; |
|||
} else if (!foundThird && itr->first->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { |
|||
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, itr->second); |
|||
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); |
|||
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); |
|||
EXPECT_EQ("2", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ("1", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); |
|||
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType()); |
|||
foundThird = true; |
|||
} else { |
|||
EXPECT_TRUE(false); |
|||
} |
|||
} |
|||
EXPECT_TRUE(foundFirst); |
|||
EXPECT_TRUE(foundSecond); |
|||
EXPECT_TRUE(foundThird); |
|||
} |
|||
|
|||
@ -0,0 +1,206 @@ |
|||
//
|
|||
// Created by Jip Spel on 20.09.18.
|
|||
//
|
|||
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "test/storm_gtest.h"
|
|||
#include "storm-pars/analysis/MonotonicityChecker.h"
|
|||
#include "storm/storage/expressions/BinaryRelationExpression.h"
|
|||
#include "storm/storage/SparseMatrix.h"
|
|||
#include "storm/adapters/RationalFunctionAdapter.h"
|
|||
|
|||
#include "storm-parsers/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm-parsers/parser/AutoParser.h"
|
|||
#include "storm-parsers/parser/PrismParser.h"
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
#include "storm/api/builder.h"
|
|||
|
|||
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
|
|||
|
|||
#include "storm-pars/api/storm-pars.h"
|
|||
#include "storm/api/storm.h"
|
|||
|
|||
#include "storm-parsers/api/storm-parsers.h"
|
|||
TEST(MonotonicityCheckerTest, Derivative_checker) { |
|||
|
|||
// Create the region
|
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation lowerBoundaries; |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation upperBoundaries; |
|||
auto region = storm::storage::ParameterRegion<storm::RationalFunction>(std::move(lowerBoundaries), std::move(upperBoundaries)); |
|||
|
|||
// Derivative 0
|
|||
auto constFunction = storm::RationalFunction(0); |
|||
auto constFunctionRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(constFunction, region); |
|||
EXPECT_TRUE(constFunctionRes.first); |
|||
EXPECT_TRUE(constFunctionRes.second); |
|||
|
|||
// Derivative 5
|
|||
constFunction = storm::RationalFunction(5); |
|||
constFunctionRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(constFunction, region); |
|||
EXPECT_TRUE(constFunctionRes.first); |
|||
EXPECT_FALSE(constFunctionRes.second); |
|||
|
|||
// Derivative -4
|
|||
constFunction = storm::RationalFunction(storm::RationalFunction(1)-constFunction); |
|||
constFunctionRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(constFunction, region); |
|||
EXPECT_FALSE(constFunctionRes.first); |
|||
EXPECT_TRUE(constFunctionRes.second); |
|||
|
|||
std::shared_ptr<storm::RawPolynomialCache> cache = std::make_shared<storm::RawPolynomialCache>(); |
|||
carl::StringParser parser; |
|||
parser.setVariables({"p", "q"}); |
|||
|
|||
// Create the region
|
|||
auto functionP = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("p"), cache)); |
|||
auto functionQ = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("q"), cache)); |
|||
|
|||
auto varsP = functionP.gatherVariables(); |
|||
auto varsQ = functionQ.gatherVariables(); |
|||
storm::utility::parametric::Valuation<storm::RationalFunction> lowerBoundaries2; |
|||
storm::utility::parametric::Valuation<storm::RationalFunction> upperBoundaries2; |
|||
for (auto var : varsP) { |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType lb = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(0 + 0.000001); |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType ub = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(1 - 0.000001); |
|||
lowerBoundaries2.emplace(std::make_pair(var, lb)); |
|||
upperBoundaries2.emplace(std::make_pair(var, ub)); |
|||
} |
|||
for (auto var : varsQ) { |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType lb = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(0 + 0.000001); |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType ub = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(1 - 0.000001); |
|||
lowerBoundaries2.emplace(std::make_pair(var, lb)); |
|||
upperBoundaries2.emplace(std::make_pair(var, ub)); |
|||
} |
|||
region = storm::storage::ParameterRegion<storm::RationalFunction>(std::move(lowerBoundaries2), std::move(upperBoundaries2)); |
|||
|
|||
// Derivative p
|
|||
auto function = functionP; |
|||
auto functionRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(function, region); |
|||
EXPECT_TRUE(functionRes.first); |
|||
EXPECT_FALSE(functionRes.second); |
|||
|
|||
// Derivative 1-p
|
|||
auto functionDecr = storm::RationalFunction(storm::RationalFunction(1)-function); |
|||
auto functionDecrRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(functionDecr, region); |
|||
EXPECT_TRUE(functionDecrRes.first); |
|||
EXPECT_FALSE(functionDecrRes.second); |
|||
|
|||
// Derivative 1-2p
|
|||
auto functionNonMonotonic = storm::RationalFunction(storm::RationalFunction(1)-storm::RationalFunction(2)*function); |
|||
auto functionNonMonotonicRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(functionNonMonotonic, region); |
|||
EXPECT_FALSE(functionNonMonotonicRes.first); |
|||
EXPECT_FALSE(functionNonMonotonicRes.second); |
|||
|
|||
// Derivative -p
|
|||
functionDecr = storm::RationalFunction(storm::RationalFunction(0)-function); |
|||
functionDecrRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(functionDecr, region); |
|||
EXPECT_FALSE(functionDecrRes.first); |
|||
EXPECT_TRUE(functionDecrRes.second); |
|||
|
|||
// Derivative p*q
|
|||
function = functionP * functionQ ; |
|||
functionRes = storm::analysis::MonotonicityChecker<storm::RationalFunction>::checkDerivative(function, region); |
|||
EXPECT_TRUE(functionRes.first); |
|||
EXPECT_FALSE(functionRes.second); |
|||
} |
|||
|
|||
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [true U s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
|
|||
// Apply bisimulation
|
|||
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; |
|||
if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) { |
|||
bisimType = storm::storage::BisimulationType::Weak; |
|||
} |
|||
|
|||
dtmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
|
|||
// Create the region
|
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation lowerBoundaries; |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation upperBoundaries; |
|||
std::set<typename storm::storage::ParameterRegion<storm::RationalFunction>::VariableType> vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
for (auto var : vars) { |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType lb = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(0 + 0.000001); |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType ub = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(1 - 0.000001); |
|||
lowerBoundaries.emplace(std::make_pair(var, lb)); |
|||
upperBoundaries.emplace(std::make_pair(var, ub)); |
|||
} |
|||
auto region = storm::storage::ParameterRegion<storm::RationalFunction>(std::move(lowerBoundaries), std::move(upperBoundaries)); |
|||
std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region}; |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); |
|||
|
|||
storm::analysis::MonotonicityChecker<storm::RationalFunction> monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true); |
|||
auto result = monotonicityChecker.checkMonotonicity(); |
|||
EXPECT_EQ(1ul, result.size()); |
|||
EXPECT_EQ(2ul, result.begin()->second.size()); |
|||
auto monotone = result.begin()->second.begin(); |
|||
EXPECT_EQ(true, monotone->second.first); |
|||
EXPECT_EQ(false, monotone->second.second); |
|||
} |
|||
|
|||
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [true U s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
|
|||
// Apply bisimulation
|
|||
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; |
|||
if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) { |
|||
bisimType = storm::storage::BisimulationType::Weak; |
|||
} |
|||
|
|||
dtmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
// Create the region
|
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation lowerBoundaries; |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation upperBoundaries; |
|||
std::set<typename storm::storage::ParameterRegion<storm::RationalFunction>::VariableType> vars = storm::models::sparse::getProbabilityParameters(*dtmc); |
|||
for (auto var : vars) { |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType lb = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(0 + 0.000001); |
|||
typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType ub = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(1 - 0.000001); |
|||
lowerBoundaries.emplace(std::make_pair(var, lb)); |
|||
upperBoundaries.emplace(std::make_pair(var, ub)); |
|||
} |
|||
auto region = storm::storage::ParameterRegion<storm::RationalFunction>(std::move(lowerBoundaries), std::move(upperBoundaries)); |
|||
std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region}; |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); |
|||
|
|||
auto monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true, 50); |
|||
auto result = monotonicityChecker.checkMonotonicity(); |
|||
EXPECT_EQ(1ul, result.size()); |
|||
EXPECT_EQ(2ul, result.begin()->second.size()); |
|||
auto monotone = result.begin()->second.begin(); |
|||
EXPECT_EQ(true, monotone->second.first); |
|||
EXPECT_EQ(false, monotone->second.second); |
|||
} |
|||
@ -0,0 +1,93 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "test/storm_gtest.h"
|
|||
|
|||
#include "storm-parsers/parser/FormulaParser.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "storm-parsers/parser/AutoParser.h"
|
|||
#include "storm-parsers/parser/PrismParser.h"
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
#include "storm/api/builder.h"
|
|||
|
|||
#include "storm-pars/analysis/Order.h"
|
|||
#include "storm-pars/analysis/OrderExtender.h"
|
|||
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
|
|||
|
|||
#include "storm-pars/api/storm-pars.h"
|
|||
#include "storm/api/storm.h"
|
|||
|
|||
#include "storm-parsers/api/storm-parsers.h"
|
|||
|
|||
TEST(OrderExtenderTest, Brp_with_bisimulation) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [F s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
|
|||
// Apply bisimulation
|
|||
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; |
|||
if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) { |
|||
bisimType = storm::storage::BisimulationType::Weak; |
|||
} |
|||
|
|||
dtmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); |
|||
|
|||
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc); |
|||
auto criticalTuple = extender->toOrder(formulas); |
|||
EXPECT_EQ(dtmc->getNumberOfStates(), std::get<1>(criticalTuple)); |
|||
EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple)); |
|||
|
|||
auto order = std::get<0>(criticalTuple); |
|||
for (uint_fast64_t i = 0; i < dtmc->getNumberOfStates(); ++i) { |
|||
EXPECT_TRUE((*order->getAddedStates())[i]); |
|||
} |
|||
|
|||
// Check on some nodes
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7,13)); |
|||
} |
|||
|
|||
TEST(OrderExtenderTest, Brp_without_bisimulation) { |
|||
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; |
|||
std::string formulaAsString = "P=? [F s=4 & i=N ]"; |
|||
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
|
|||
|
|||
// Program and formula
|
|||
storm::prism::Program program = storm::api::parseProgram(programFile); |
|||
program = storm::utility::prism::preprocess(program, constantsAsString); |
|||
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc); |
|||
ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); |
|||
model = simplifier.getSimplifiedModel(); |
|||
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); |
|||
|
|||
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc); |
|||
auto criticalTuple = extender->toOrder(formulas); |
|||
EXPECT_EQ(183ul, std::get<1>(criticalTuple)); |
|||
EXPECT_EQ(186ul, std::get<2>(criticalTuple)); |
|||
} |
|||
|
|||
|
|||
@ -0,0 +1,173 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "test/storm_gtest.h"
|
|||
#include "storm-pars/analysis/Order.h"
|
|||
#include "storm/storage/BitVector.h"
|
|||
|
|||
TEST(OrderTest, Simple) { |
|||
auto numberOfStates = 7; |
|||
auto above = storm::storage::BitVector(numberOfStates); |
|||
above.set(0); |
|||
auto below = storm::storage::BitVector(numberOfStates); |
|||
below.set(1); |
|||
auto initialMiddle = storm::storage::BitVector(numberOfStates); |
|||
std::vector<uint_fast64_t> statesSorted; |
|||
|
|||
auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,0)); |
|||
EXPECT_EQ(nullptr, order.getNode(2)); |
|||
|
|||
order.add(2); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(2,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(2,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); |
|||
|
|||
order.add(3); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,2)); |
|||
|
|||
order.addToNode(4, order.getNode(2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(4,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,4)); |
|||
|
|||
order.addBetween(5, order.getNode(0), order.getNode(3)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(5,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,5)); |
|||
|
|||
order.addBetween(6, order.getNode(5), order.getNode(3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,6)); |
|||
|
|||
order.addRelationNodes(order.getNode(6), order.getNode(4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,6)); |
|||
|
|||
} |
|||
|
|||
TEST(OrderTest, copy_order) { |
|||
auto numberOfStates = 7; |
|||
auto above = storm::storage::BitVector(numberOfStates); |
|||
above.set(0); |
|||
auto below = storm::storage::BitVector(numberOfStates); |
|||
below.set(1); |
|||
auto initialMiddle = storm::storage::BitVector(numberOfStates); |
|||
std::vector<uint_fast64_t> statesSorted; |
|||
|
|||
auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); |
|||
order.add(2); |
|||
order.add(3); |
|||
order.addToNode(4, order.getNode(2)); |
|||
order.addBetween(5, order.getNode(0), order.getNode(3)); |
|||
order.addBetween(6, order.getNode(5), order.getNode(3)); |
|||
|
|||
|
|||
|
|||
auto orderCopy = storm::analysis::Order(order); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,0)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(2,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,2)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(2,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,2)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(4,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(4,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(4,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,4)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(5,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); |
|||
|
|||
order.addRelationNodes(order.getNode(6), order.getNode(4)); |
|||
orderCopy = storm::analysis::Order(order); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,0)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,1)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,3)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,6)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,6)); |
|||
} |
|||
|
|||
TEST(OrderTest, merge_nodes) { |
|||
auto numberOfStates = 7; |
|||
auto above = storm::storage::BitVector(numberOfStates); |
|||
above.set(0); |
|||
auto below = storm::storage::BitVector(numberOfStates); |
|||
below.set(1); |
|||
auto initialMiddle = storm::storage::BitVector(numberOfStates); |
|||
std::vector<uint_fast64_t> statesSorted; |
|||
|
|||
auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, &statesSorted); |
|||
order.add(2); |
|||
order.add(3); |
|||
order.addToNode(4, order.getNode(2)); |
|||
order.addBetween(5, order.getNode(0), order.getNode(3)); |
|||
order.addBetween(6, order.getNode(5), order.getNode(3)); |
|||
|
|||
order.mergeNodes(order.getNode(4), order.getNode(5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,5)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); |
|||
|
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); |
|||
EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue