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

Fix assumption making and checking and testing

tempestpy_adaptions
Jip Spel 6 years ago
parent
a35cb2643a
commit
f6ea4d38bb
16 changed files with 911 additions and 482 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      resources/examples/testfiles/pdtmc/simple1.pm
  2. 17
      resources/examples/testfiles/pdtmc/simple2.pm
  3. 18
      resources/examples/testfiles/pdtmc/simple3.pm
  4. 12
      src/storm-pars-cli/storm-pars.cpp
  5. 355
      src/storm-pars/analysis/AssumptionChecker.cpp
  6. 51
      src/storm-pars/analysis/AssumptionChecker.h
  7. 28
      src/storm-pars/analysis/AssumptionMaker.cpp
  8. 7
      src/storm-pars/analysis/AssumptionMaker.h
  9. 10
      src/storm-pars/analysis/Lattice.cpp
  10. 55
      src/storm-pars/analysis/Lattice.h
  11. 68
      src/storm-pars/analysis/LatticeExtender.cpp
  12. 291
      src/storm-pars/analysis/MonotonicityChecker.cpp
  13. 71
      src/storm-pars/analysis/MonotonicityChecker.h
  14. 2
      src/storm/storage/expressions/RationalFunctionToExpression.cpp
  15. 194
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  16. 197
      src/test/storm-pars/analysis/AssumptionMakerTest.cpp

17
resources/examples/testfiles/pdtmc/simple1.pm
View File

@ -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

17
resources/examples/testfiles/pdtmc/simple2.pm
View File

@ -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

18
resources/examples/testfiles/pdtmc/simple3.pm
View File

@ -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

12
src/storm-pars-cli/storm-pars.cpp
View File

@ -596,14 +596,12 @@ namespace storm {
}
if (parSettings.isMonotonicityAnalysisSet()) {
std::cout << "Hello, Jip1" << std::endl;
// Simplify the model
storm::utility::Stopwatch simplifyingWatch(true);
std::ofstream outfile;
outfile.open("results.txt", std::ios_base::app);
outfile << ioSettings.getPrismInputFilename() << ", ";
if (model->isOfType(storm::models::ModelType::Dtmc)) {
auto consideredModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(*consideredModel);
@ -635,8 +633,6 @@ namespace storm {
model->printModelInformationToStream(std::cout);
outfile << simplifyingWatch << ", ";
outfile.close();
std::cout << "Bye, Jip1" << std::endl;
}
if (parSettings.isMonotonicityAnalysisSet() && model) {
@ -668,7 +664,8 @@ namespace storm {
auto matrix = sparseModel->getTransitionMatrix();
auto backwardsTransitionMatrix = matrix.transpose();
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, false, false);
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
storm::storage::BitVector selectedStates(matrix.getRowCount());
storm::storage::BitVector selfLoopStates(matrix.getRowCount());
@ -724,8 +721,6 @@ namespace storm {
}
if (parSettings.isMonotonicityAnalysisSet()) {
std::cout << "Hello, Jip2" << std::endl;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
// Monotonicity
@ -740,9 +735,6 @@ namespace storm {
outfile << monotonicityWatch << std::endl;
outfile.close();
std::cout << "Bye, Jip2" << std::endl;
return;
}
std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);

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

@ -5,6 +5,7 @@
#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"
@ -16,8 +17,8 @@
#include "storm/storage/expressions/SimpleValuation.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/VariableExpression.h"
#include "storm/utility/constants.h"
#include "storm/storage/expressions/RationalFunctionToExpression.h"
#include "storm/utility/constants.h"
namespace storm {
namespace analysis {
@ -30,6 +31,8 @@ namespace storm {
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model);
auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
// TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again
for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>();
for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
@ -57,7 +60,7 @@ namespace storm {
}
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
std::vector<double> values = quantitativeResult.getValueVector();
results.push_back(values);
samples.push_back(values);
}
}
@ -70,6 +73,8 @@ namespace storm {
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model);
auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
// TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again
for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>();
for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
@ -96,48 +101,62 @@ namespace storm {
}
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
std::vector<double> values = quantitativeResult.getValueVector();
results.push_back(values);
samples.push_back(values);
}
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
bool result = true;
AssumptionStatus AssumptionChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
auto result = AssumptionStatus::UNKNOWN;
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
assumption->gatherVariables(vars);
for (auto itr = results.begin(); result && itr != results.end(); ++itr) {
for (auto itr = samples.begin(); result == AssumptionStatus::UNKNOWN && itr != samples.end(); ++itr) {
std::shared_ptr<storm::expressions::ExpressionManager const> manager = assumption->getManager().getSharedPointer();
auto valuation = storm::expressions::SimpleValuation(manager);
auto values = (*itr);
for (auto var = vars.begin(); result && var != vars.end(); ++var) {
for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) {
storm::expressions::Variable par = *var;
auto index = std::stoi(par.getName());
valuation.setRationalValue(par, values[index]);
}
assert(assumption->hasBooleanType());
result &= assumption->evaluateAsBool(&valuation);
if (!assumption->evaluateAsBool(&valuation)) {
result = AssumptionStatus::INVALID;
}
}
return result;
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice) {
bool result = validated(assumption);
if (!result) {
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice) {
// First check if based on sample points the assumption can be discharged
auto result = checkOnSamples(assumption);
assert (result != storm::analysis::AssumptionStatus::VALID);
if (result == storm::analysis::AssumptionStatus::UNKNOWN) {
// If result from sample checking was unknown, the assumption might hold, so we continue,
// otherwise we return INVALID
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
assumption->gatherVariables(vars);
STORM_LOG_THROW(assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Greater ||assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Equal,
storm::expressions::BinaryRelationExpression::RelationType::Greater ||
assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Equal,
storm::exceptions::NotSupportedException,
"Only Greater Or Equal assumptions supported");
// TODO: implement validation of equal/greater equations
auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
// 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 lattice
// We can check with a function if the assumption holds
auto state1succ1 = row1.begin();
auto state1succ2 = (++row1.begin());
auto state2succ1 = row2.begin();
@ -149,63 +168,33 @@ namespace storm {
}
if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) {
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn());
if (comp != storm::analysis::Lattice::UNKNOWN) {
if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater
&& lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != storm::analysis::Lattice::UNKNOWN) {
// The assumption should be the greater assumption
// If the result is unknown, we cannot compare, also SMTSolver will not help
result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1,
state2succ2);
if (!result) {
result = validateAssumptionSMTSolver(lattice, state1succ1, state1succ2, state2succ1,
state2succ2);
}
validatedAssumptions.insert(assumption);
if (result) {
validAssumptions.insert(assumption);
} else if (assumption->getRelationType() == storm::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(lattice, assumption);
}
} else {
bool subset = true;
if (row1.getNumberOfEntries() > row2.getNumberOfEntries()) {
std::swap(row1, row2);
}
storm::storage::BitVector stateNumbers(matrix.getColumnCount());
for (auto itr1 = row1.begin(); subset && itr1 != row1.end(); ++itr1) {
bool found = false;
stateNumbers.set(itr1->getColumn());
for (auto itr2 = row2.begin(); !found && itr2 != row2.end(); ++itr2) {
found = itr1->getColumn() == itr2->getColumn();
}
subset &= found;
}
if (subset) {
// Check if they all are in the lattice
bool allInLattice = true;
for (auto i = stateNumbers.getNextSetIndex(0); allInLattice && i < stateNumbers.size(); i = stateNumbers.getNextSetIndex(i+1)) {
for (auto j = stateNumbers.getNextSetIndex(i+1); allInLattice && j < stateNumbers.size(); j = stateNumbers.getNextSetIndex(j+1)) {
auto comp = lattice->compare(i,j);
allInLattice &= comp == storm::analysis::Lattice::ABOVE || comp == storm::analysis::Lattice::BELOW || comp == storm::analysis::Lattice::SAME;
}
}
if (allInLattice) {
result = validateAssumptionSMTSolver(lattice, assumption);
validatedAssumptions.insert(assumption);
if (result) {
validAssumptions.insert(assumption);
}
}
}
result = validateAssumptionSMTSolver(lattice, assumption);
}
}
return result;
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::validateAssumptionFunction(storm::analysis::Lattice* lattice,
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
@ -215,8 +204,9 @@ namespace storm {
|| (state1succ1->getColumn() == state2succ2->getColumn()
&& state1succ2->getColumn() == state2succ1->getColumn()));
bool result = true;
AssumptionStatus result;
// Calculate the difference in probability for the "highest" successor state
ValueType prob;
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn());
assert (comp == storm::analysis::Lattice::ABOVE || comp == storm::analysis::Lattice::BELOW);
@ -227,187 +217,136 @@ namespace storm {
}
auto vars = prob.gatherVariables();
// If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions
// This will give the smallest result
// TODO: Type
std::map<storm::RationalFunctionVariable, typename ValueType::CoeffType> substitutions;
for (auto var : vars) {
auto derivative = prob.derivative(var);
if(derivative.isConstant()) {
if (derivative.constantPart() >= 0) {
substitutions[var] = 0;
} else if (derivative.constantPart() <= 0) {
substitutions[var] = 1;
}
auto monotonicity = MonotonicityChecker<ValueType>::checkDerivative(prob.derivative(var));
if (monotonicity.first) {
// monotone increasing
substitutions[var] = 0;
} else if (monotonicity.second) {
// monotone increasing
substitutions[var] = 1;
} else {
result = false;
result = AssumptionStatus::UNKNOWN;
}
}
// return result && prob.evaluate(substitutions) >= 0;
//TODO check for > and =
return false;
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2) {
assert((state1succ1->getColumn() == state2succ1->getColumn()
&& state1succ2->getColumn() == state2succ2->getColumn())
|| (state1succ1->getColumn() == state2succ2->getColumn()
&& state1succ2->getColumn() == state2succ1->getColumn()));
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);
storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Variable succ1 = manager->declareRationalVariable(std::to_string(state1succ1->getColumn()));
storm::expressions::Variable succ2 = manager->declareRationalVariable(std::to_string(state1succ2->getColumn()));
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn());
storm::expressions::Expression exprGiven;
if (comp == storm::analysis::Lattice::ABOVE) {
exprGiven = succ1 >= succ2;
} else if (comp == storm::analysis::Lattice::BELOW) {
exprGiven = succ1 <= succ2;
} else {
assert (comp != storm::analysis::Lattice::UNKNOWN);
exprGiven = succ1 = succ2;
if (prob.evaluate(substitutions) >= 0) {
result = AssumptionStatus::VALID;
}
auto valueTypeToExpression = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::expressions::Expression exprToCheck =
(valueTypeToExpression.toExpression(state1succ1->getValue())*succ1
+ valueTypeToExpression.toExpression(state1succ2->getValue())*succ2
>= valueTypeToExpression.toExpression(state2succ1->getValue())*succ1
+ valueTypeToExpression.toExpression(state2succ2->getValue())*succ2);
storm::expressions::Expression exprBounds = manager->boolean(true);
auto variables = manager->getVariables();
for (auto var : variables) {
if (var != succ1 && var != succ2) {
// ensure graph-preserving
exprBounds = exprBounds && manager->rational(0) <= var && manager->rational(1) >= var;
} else {
exprBounds = exprBounds && var >= manager->rational(0) && var <= manager->rational(1);
}
}
s.add(exprGiven);
s.add(exprToCheck);
s.add(exprBounds);
smtResult = s.check();
// return smtResult == storm::solver::SmtSolver::CheckResult::Sat;
//TODO check for > and =
return false;
return result;
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
assert (!validated(assumption));
template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
bool result = true;
auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
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));
storm::solver::Z3SmtSolver s(*manager);
bool orderKnown = true;
// Check if the order between the different successors is known
// Also start creating expression for order of states
storm::expressions::Expression exprOrderSucc = manager->boolean(true);
std::set<storm::expressions::Variable> stateVariables;
if (row1.getNumberOfEntries() >= row2.getNumberOfEntries()) {
for (auto itr = row1.begin(); itr != row1.end(); ++itr) {
stateVariables.insert(manager->declareRationalVariable(std::to_string(itr->getColumn())));
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));
}
} else {
for (auto itr = row2.begin(); itr != row2.end(); ++itr) {
stateVariables.insert(manager->declareRationalVariable(std::to_string(itr->getColumn())));
}
}
storm::expressions::Expression exprGiven = manager->boolean(true);
for (auto itr1 = row1.begin(); result && itr1 != row1.end(); ++itr1) {
for (auto itr2 = row1.begin(); result && itr2 != row1.end(); ++itr2) {
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 = lattice->compare(itr1->getColumn(), itr2->getColumn());
if (comp == storm::analysis::Lattice::ABOVE) {
exprGiven = exprGiven && (manager->getVariable(std::to_string(itr1->getColumn())) >=
manager->getVariable(std::to_string(itr2->getColumn())));
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <=
manager->getVariable(varname2));
} else if (comp == storm::analysis::Lattice::BELOW) {
exprGiven = exprGiven && (manager->getVariable(std::to_string(itr1->getColumn())) <=
manager->getVariable(std::to_string(itr2->getColumn())));
exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >=
manager->getVariable(varname2));
} else if (comp == storm::analysis::Lattice::SAME) {
exprOrderSucc = exprOrderSucc &&
(manager->getVariable(varname1) = manager->getVariable(varname2));
} else {
assert (comp != storm::analysis::Lattice::UNKNOWN);
exprGiven = exprGiven &&
(manager->getVariable(std::to_string(itr1->getColumn())) = manager->getVariable(
std::to_string(itr2->getColumn())));
orderKnown = false;
}
}
}
}
auto valueTypeToExpression = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::expressions::Expression expr1 = manager->rational(0);
for (auto itr1 = row1.begin(); result && itr1 != row1.end(); ++itr1) {
expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable(std::to_string(itr1->getColumn())));
}
storm::expressions::Expression expr2 = manager->rational(0);
for (auto itr2 = row2.begin(); result && itr2 != row2.end(); ++itr2) {
expr2 = expr2 + (valueTypeToExpression.toExpression(itr2->getValue()) * manager->getVariable(std::to_string(itr2->getColumn())));
}
storm::expressions::Expression exprToCheck = expr1 >= expr2;
if (orderKnown) {
storm::solver::Z3SmtSolver s(*manager);
auto valueTypeToExpression = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::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())));
}
storm::expressions::Expression exprProb1 = manager->rational(0);
for (auto itr1 = row1.begin(); result && itr1 != row1.end(); ++itr1) {
exprProb1 = exprProb1 + (valueTypeToExpression.toExpression(itr1->getValue()));
}
storm::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())));
}
storm::expressions::Expression exprProb2 = manager->rational(0);
for (auto itr2 = row2.begin(); result && itr2 != row2.end(); ++itr2) {
exprProb2 = exprProb2 + (valueTypeToExpression.toExpression(itr2->getValue()));
}
// Create expression for the assumption based on the relation to successors
// It is the negation of actual assumption
// TODO: use same manager s.t. assumption can be used directly ?
storm::expressions::Expression exprToCheck ;
if (assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Greater) {
exprToCheck = expr1 <= expr2;
} else {
assert (assumption->getRelationType() ==
storm::expressions::BinaryRelationExpression::RelationType::Equal);
exprToCheck = expr1 > expr2;
}
storm::expressions::Expression exprBounds = exprProb1 >= manager->rational(0)
&& exprProb1 <= manager->rational(1)
&& exprProb2 >= manager->rational(0)
&& exprProb2 <= manager->rational(1);
auto variables = manager->getVariables();
// Bounds for the state probabilities and parameters
storm::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
// TODO: graph-preserving
exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
}
}
auto variables = manager->getVariables();
for (auto var : variables) {
if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) {
// ensure graph-preserving
exprBounds = exprBounds && manager->rational(0) <= var && manager->rational(1) >= var;
s.add(exprOrderSucc);
s.add(exprBounds);
// assert that sorting of successors in the lattice and the bounds on the expression are at least satisfiable
assert (s.check() == storm::solver::SmtSolver::CheckResult::Sat);
// TODO: kijken of t SAT moet zijn?
s.add(exprToCheck);
auto smtRes = s.check();
if (smtRes == storm::solver::SmtSolver::CheckResult::Unsat) {
// If there is no thing satisfying the negation we are safe.
result = AssumptionStatus::VALID;
} else if (smtRes == storm::solver::SmtSolver::CheckResult::Sat) {
assert (smtRes == storm::solver::SmtSolver::CheckResult::Sat);
result = AssumptionStatus::INVALID;
} else {
exprBounds = exprBounds && var >= manager->rational(0) && var <= manager->rational(1);
result = AssumptionStatus::UNKNOWN;
}
} else {
result = AssumptionStatus::UNKNOWN;
}
s.add(exprGiven);
s.add(exprBounds);
assert(s.check() == storm::solver::SmtSolver::CheckResult::Sat);
s.add(exprToCheck);
auto smtRes = s.check();
//TODO check for > and =
result = result && smtRes == storm::solver::SmtSolver::CheckResult::Sat;
return false;
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::validated(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
return find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end();
}
template <typename ValueType>
bool AssumptionChecker<ValueType>::valid(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
assert(find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end());
return find(validAssumptions.begin(), validAssumptions.end(), assumption) != validAssumptions.end();
return result;
}
template class AssumptionChecker<storm::RationalFunction>;

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

@ -14,9 +14,19 @@
namespace storm {
namespace analysis {
enum AssumptionStatus {
VALID,
INVALID,
UNKNOWN,
};
template<typename ValueType>
class AssumptionChecker {
public:
/*!
* Constants for status of assumption
*/
/*!
* Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
*
@ -39,60 +49,37 @@ namespace storm {
* Checks if the assumption holds at the sample points of the AssumptionChecker.
*
* @param assumption The assumption to check.
* @return true if the assumption holds at the sample points
* @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID
*/
bool checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
AssumptionStatus checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
/*!
* Tries to validate an assumption based on the lattice and underlying transition matrix.
*
* @param assumption The assumption to validate.
* @param lattice The lattice.
* @return true if the assumption can be validated and holds, false otherwise
*/
bool validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice);
/*!
* Looks up if assumption has been validated.
*
* @param assumption The assumption.
* @return true if the assumption has been validated.
* @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID
*/
bool validated(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
AssumptionStatus validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice);
/*!
* Looks up if assumption is valid. Requires the function to be validated.
*
* @param assumption The assumption.
* @return true if the assumption is valid.
*/
bool valid(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
AssumptionStatus validateAssumptionSMTSolver(storm::analysis::Lattice* lattice,
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
private:
std::shared_ptr<storm::logic::Formula const> formula;
storm::storage::SparseMatrix<ValueType> matrix;
std::vector<std::vector<double>> results;
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> validatedAssumptions;
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> validAssumptions;
std::vector<std::vector<double>> samples;
bool validateAssumptionFunction(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2);
void createSamples();
bool validateAssumptionSMTSolver(storm::analysis::Lattice* lattice,
AssumptionStatus validateAssumptionFunction(storm::analysis::Lattice* lattice,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2);
bool validateAssumptionSMTSolver(storm::analysis::Lattice* lattice,
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
};
}
}

28
src/storm-pars/analysis/AssumptionMaker.cpp
View File

@ -6,6 +6,7 @@
namespace storm {
namespace analysis {
typedef std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionType;
template<typename ValueType>
AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
this->numberOfStates = numberOfStates;
@ -13,51 +14,44 @@ namespace storm {
this->validate = validate;
this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
// TODO: expressenmanager pointer maken die oorspronkelijk in monotonicity checker zit
expressionManager->declareRationalVariable(std::to_string(i));
}
}
template <typename ValueType>
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) {
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> result;
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) {
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> result;
// TODO: alleen maar als validate true is results genereren
storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
bool result1 = (validate && assumptionChecker->validateAssumption(assumption1, lattice) && assumptionChecker->valid(assumption1));
storm::expressions::BinaryRelationExpression::RelationType::Greater));
// TODO: dischargen gebasseerd op monotonicity
auto result1 = assumptionChecker->validateAssumption(assumption1, lattice);
result[assumption1] = result1;
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption2
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
bool result2 = (validate && assumptionChecker->validateAssumption(assumption2, lattice) && assumptionChecker->valid(assumption2));
auto result2 = assumptionChecker->validateAssumption(assumption2, lattice);
result[assumption2] = result2;
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption3
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Equal));
bool result3 = (validate && assumptionChecker->validateAssumption(assumption3, lattice) && assumptionChecker->valid(assumption3));
auto result3 = assumptionChecker->validateAssumption(assumption3, lattice);
result[assumption3] = result3;
return result;
}
template <typename ValueType>
std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionMaker<ValueType>::createEqualAssumption(uint_fast64_t val1, uint_fast64_t val2) {
storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
return std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Equal));
}
template class AssumptionMaker<storm::RationalFunction>;
}
}

7
src/storm-pars/analysis/AssumptionMaker.h
View File

@ -17,6 +17,7 @@ namespace storm {
template<typename ValueType>
class AssumptionMaker {
typedef std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionType;
public:
/*!
* Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the model.
@ -27,9 +28,7 @@ namespace storm {
*/
AssumptionMaker( storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice);
std::shared_ptr<storm::expressions::BinaryRelationExpression> createEqualAssumption(uint_fast64_t val1, uint_fast64_t val2);
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice);
private:
storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
@ -39,8 +38,6 @@ namespace storm {
uint_fast64_t numberOfStates;
bool validate;
};
}
}

10
src/storm-pars/analysis/Lattice.cpp
View File

@ -80,7 +80,6 @@ namespace storm {
}
void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {
// std::cout << "Adding " << state << " between " << *(above->states.begin()) << " and " << *(below->states.begin()) << std::endl;
assert(!(*addedStates)[state]);
assert(compare(above, below) == ABOVE);
@ -97,7 +96,6 @@ namespace storm {
}
void Lattice::addToNode(uint_fast64_t state, Node *node) {
// std::cout << "Adding " << state << " to " << *(node->states.begin()) << std::endl;
assert(!(*addedStates)[state]);
node->states.insert(state);
nodes[state] = node;
@ -118,6 +116,10 @@ namespace storm {
assert (compare(above, below) == ABOVE);
}
void Lattice::addRelation(uint_fast64_t above, uint_fast64_t below) {
addRelationNodes(getNode(above), getNode(below));
}
int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
return compare(getNode(state1), getNode(state2));
}
@ -366,5 +368,9 @@ namespace storm {
nodes[i] = node1;
}
}
void Lattice::merge(uint_fast64_t var1, uint_fast64_t var2) {
mergeNodes(getNode(var1), getNode(var2));
}
}
}

55
src/storm-pars/analysis/Lattice.h
View File

@ -21,7 +21,6 @@ namespace storm {
struct Node {
boost::container::flat_set<uint_fast64_t> states;
storm::storage::BitVector statesAbove;
// storm::storage::BitVector statesBelow;
};
/*!
@ -70,6 +69,13 @@ namespace storm {
*/
void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below);
/*!
* Adds a new relation between two nodes to the lattice
* @param above The node closest to the top Node of the Lattice.
* @param below The node closest to the bottom Node of the Lattice.
*/
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 Lattice.
@ -128,37 +134,6 @@ namespace storm {
std::vector<uint_fast64_t> sortStates(storm::storage::BitVector* states);
// /*!
// * Returns a set with the nodes which are above the state.
// *
// * @param state The state number.
// * @return The set with all nodes which are above the state.
// */
// std::set<Lattice::Node*> getAbove(uint_fast64_t state);
//
// /*!
// * Returns a set with the nodes which are below the state.
// *
// * @param state The state number.
// * @return The set with all nodes which are below the state.
// */
// std::set<Lattice::Node*> getBelow(uint_fast64_t state);
//
// /*!
// * Returns a set with the nodes which are above the node.
// *
// * @param node The node.
// * @return The set with all nodes which are above the node.
// */
// std::set<Lattice::Node*> getAbove(Lattice::Node* node);
//
// /*!
// * Returns a set with the nodes which are below the node.
// *
// * @param node The node.
// * @return The set with all nodes which are below the node.
// */
// std::set<Lattice::Node*> getBelow(Lattice::Node* node);
void setDoneBuilding(bool done);
/*!
@ -181,6 +156,13 @@ namespace storm {
* @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);
/*!
* Constants for comparison of nodes/states
@ -207,18 +189,9 @@ namespace storm {
bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen);
std::unordered_map<uint_fast64_t, std::unordered_map<uint_fast64_t, uint_fast64_t>> comparisons;
bool doneBuilding;
// void setStatesAbove(Node* node, uint_fast64_t state, bool alreadyInitialized);
// void setStatesBelow(Node* node, uint_fast64_t state, bool alreadyInitialized);
// void setStatesAbove(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized);
// void setStatesBelow(storm::analysis::Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized);
};
}
}

68
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -72,7 +72,8 @@ namespace storm {
auto initialMiddleStates = storm::storage::BitVector(numberOfStates);
// Check if MC contains cycles
// TODO maybe move to other place?
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(model->getTransitionMatrix(), false, false);
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(model->getTransitionMatrix(), options);
acyclic = true;
for (auto i = 0; acyclic && i < decomposition.size(); ++i) {
acyclic &= decomposition.getBlock(i).size() <= 1;
@ -80,6 +81,7 @@ namespace storm {
if (acyclic) {
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
} else {
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
@ -241,7 +243,6 @@ namespace storm {
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
auto numberOfStates = this->model->getNumberOfStates();
if (assumption != nullptr) {
handleAssumption(lattice, assumption);
}
@ -328,6 +329,7 @@ namespace storm {
auto addedStates = lattice->getAddedStates();
if (assumptionSeen) {
statesToHandle = addedStates;
// TODO: statesSorted =
}
auto stateNumber = statesToHandle->getNextSetIndex(0);
while (stateNumber != numberOfStates) {
@ -342,6 +344,7 @@ namespace storm {
if (!(*addedStates)[succ1]) {
lattice->addToNode(succ1, lattice->getNode(stateNumber));
statesToHandle->set(succ1, true);
statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), succ1));
}
statesToHandle->set(stateNumber, false);
stateNumber = statesToHandle->getNextSetIndex(0);
@ -355,11 +358,13 @@ namespace storm {
auto compare = lattice->compare(stateNumber, succ1);
if (compare == Lattice::ABOVE) {
statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), succ2));
lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber));
statesToHandle->set(succ2);
statesToHandle->set(stateNumber, false);
stateNumber = statesToHandle->getNextSetIndex(0);
} else if (compare == Lattice::BELOW) {
statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), succ2));
lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom());
statesToHandle->set(succ2);
statesToHandle->set(stateNumber, false);
@ -379,27 +384,58 @@ namespace storm {
}
}
addedStates = lattice->getAddedStates();
auto notAddedStates = addedStates->operator~();
for (auto stateNumber : notAddedStates) {
// Iterate over all not yet added states
storm::storage::BitVector* successors = stateMap[stateNumber];
// addedStates = lattice->getAddedStates();
// auto notAddedStates = addedStates->operator~();
if (!assumptionSeen) {
stateNumber = *(statesSorted.begin());
while (stateNumber != numberOfStates && (*(lattice->getAddedStates()))[stateNumber]) {
statesSorted.erase(statesSorted.begin());
stateNumber = *(statesSorted.begin());
}
// Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false);
if ((*successors & *addedStates) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) {
return result;
if (stateNumber == numberOfStates) {
assert(false);
}
storm::storage::BitVector* successors = stateMap[stateNumber];
// Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false);
if ((*successors & *addedStates) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) {
return result;
}
statesToHandle->set(stateNumber);
}
} else {
addedStates = lattice->getAddedStates();
auto notAddedStates = addedStates->operator~();
for (auto stateNumber : notAddedStates) {
// Iterate over all not yet added states
storm::storage::BitVector* successors = stateMap[stateNumber];
// Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false);
if ((*successors & *addedStates) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) {
return result;
}
statesToHandle->set(stateNumber);
}
}
statesToHandle->set(stateNumber);
}
}
// if nothing changed and there are states left, then add a state between top and bottom
if (oldNumberSet == lattice->getAddedStates()->getNumberOfSetBits() && oldNumberSet != numberOfStates) {
auto stateNumber = lattice->getAddedStates()->getNextUnsetIndex(0);
if (assumptionSeen) {
stateNumber = lattice->getAddedStates()->getNextUnsetIndex(0);
} else {
stateNumber = *(statesSorted.begin());//lattice->getAddedStates()->getNextUnsetIndex(0);
}
statesSorted.erase(statesSorted.begin());
lattice->add(stateNumber);
statesToHandle->set(stateNumber);
}

291
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -22,11 +22,7 @@
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm/solver/Z3SmtSolver.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/RationalFunctionToExpression.h"
#include "storm/utility/constants.h"
namespace storm {
namespace analysis {
@ -37,6 +33,7 @@ namespace storm {
this->formulas = formulas;
this->validate = validate;
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>();
// TODO initialiseren van sample check
if (model != nullptr) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
this->extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
@ -204,12 +201,12 @@ namespace storm {
} else if (validSomewhere) {
auto itr2 = varsMonotone.begin();
while (itr2 != varsMonotone.end()) {
// if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
// (!resultCheckOnSamples[itr2->first].first &&
// !resultCheckOnSamples[itr2->first].second)) {
// // STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl);
// outfile << "X " << itr2->first;
// } else {
if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
(!resultCheckOnSamples[itr2->first].first &&
!resultCheckOnSamples[itr2->first].second)) {
// STORM_PRINT(" - Not monotone in: " << itr2->first << std::endl);
outfile << "X " << itr2->first;
} else {
if (itr2->second.first && itr2->second.second) {
// STORM_PRINT(" - Constant in" << itr2->first << std::endl);
outfile << "C " << itr2->first;
@ -224,7 +221,7 @@ namespace storm {
// STORM_PRINT(" - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl);
outfile << "? " << itr2->first;
}
// }
}
++itr2;
if (itr2 != varsMonotone.end()) {
outfile << " ";
@ -313,44 +310,81 @@ namespace storm {
++itr;
auto assumption3 = *itr;
if (!assumption1.second && !assumption2.second && !assumption3.second) {
// Both assumption cannot be validated, so we need to keep them both
// TODO: hier niet verder gaan als je iets gevonden hebt?
auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
assumptions);
auto assumptionsCopy2 = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
assumptions);
auto latticeCopy = new storm::analysis::Lattice(lattice);
auto latticeCopy2 = new storm::analysis::Lattice(lattice);
assumptions.push_back(assumption1.first);
assumptionsCopy.push_back(assumption2.first);
assumptionsCopy2.push_back(assumption2.first);
auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptions);
result.insert(map.begin(), map.end());
}
auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
assumptions);
auto assumptionsCopy2 = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
assumptions);
criticalTuple = extender->extendLattice(latticeCopy, assumption2.first);
if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptionsCopy);
result.insert(map.begin(), map.end());
}
criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first);
if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptionsCopy2);
result.insert(map.begin(), map.end());
}
auto latticeCopy = new storm::analysis::Lattice(lattice);
auto latticeCopy2 = new storm::analysis::Lattice(lattice);
assumptions.push_back(assumption1.first);
assumptionsCopy.push_back(assumption2.first);
assumptionsCopy2.push_back(assumption3.first);
auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
if (assumption1.second != AssumptionStatus::INVALID && somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptions);
result.insert(map.begin(), map.end());
}
// TODO: checkend at ie niet invalid is
criticalTuple = extender->extendLattice(latticeCopy, assumption2.first);
if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptionsCopy);
result.insert(map.begin(), map.end());
}
criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first);
if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
std::get<1>(criticalTuple), std::get<2>(criticalTuple),
assumptionsCopy2);
result.insert(map.begin(), map.end());
}
// } else if (assumption1.second && assumption2.second) {
// assert (false);
// if (!assumption1.second && !assumption2.second && !assumption3.second) {
// // Both assumption cannot be validated, so we need to keep them both
// // TODO: hier niet verder gaan als je iets gevonden hebt?
// auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
// assumptions);
// auto assumptionsCopy2 = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
// assumptions);
// auto latticeCopy = new storm::analysis::Lattice(lattice);
// auto latticeCopy2 = new storm::analysis::Lattice(lattice);
// assumptions.push_back(assumption1.first);
// assumptionsCopy.push_back(assumption2.first);
// assumptionsCopy2.push_back(assumption3.first);
//
// auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptions);
// result.insert(map.begin(), map.end());
// }
//
// criticalTuple = extender->extendLattice(latticeCopy, assumption2.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptionsCopy);
// result.insert(map.begin(), map.end());
// }
// criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptionsCopy2);
// result.insert(map.begin(), map.end());
// }
//// }
// } else if (!assumption3.second && assumption1.second && assumption2.second) {
//// assert (false);
// //TODO Both assumptions hold --> should not happen if we change it to < instead of <=
// auto assumption = assumptionMaker->createEqualAssumption(val1, val2);
// if (!validate) {
@ -361,9 +395,9 @@ namespace storm {
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
// }
// } else if (assumption1.second) {
// } else if (!assumption3.second && !assumption2.second && assumption1.second) {
// if (!validate) {
// assert(false);
//// assert(false);
// assumptions.push_back(assumption1.first);
// }
// // if validate is true and both hold, then they must be valid, so no need to add to assumptions
@ -374,8 +408,8 @@ namespace storm {
// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
// }
//
// } else {
// assert (assumption2.second);
// } else if (!assumption3.second && !assumption1.second && assumption2.second){
//// assert (assumption2.second);
// if (!validate) {
// assumptions.push_back(assumption2.first);
// }
@ -384,6 +418,43 @@ namespace storm {
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
// }
// } else {
// // TODO: should not happen
// STORM_LOG_WARN("All assumptions are true");// {" << *(assumption1.first) <<", " << *(assumption2.first) << ", " << *(assumption3.first) << "}" << std::endl);
// // Both assumption cannot be validated, so we need to keep them both
// // TODO: hier niet verder gaan als je iets gevonden hebt?
// auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
// assumptions);
// auto assumptionsCopy2 = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
// assumptions);
// auto latticeCopy = new storm::analysis::Lattice(lattice);
// auto latticeCopy2 = new storm::analysis::Lattice(lattice);
// assumptions.push_back(assumption1.first);
// assumptionsCopy.push_back(assumption2.first);
// assumptionsCopy2.push_back(assumption2.first);
//
// auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptions);
// result.insert(map.begin(), map.end());
// }
//
// criticalTuple = extender->extendLattice(latticeCopy, assumption2.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptionsCopy);
// result.insert(map.begin(), map.end());
// }
// criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first);
// if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
// auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
// std::get<1>(criticalTuple), std::get<2>(criticalTuple),
// assumptionsCopy2);
// result.insert(map.begin(), map.end());
// }
// }
}
return result;
@ -538,65 +609,65 @@ namespace storm {
return varsMonotone;
}
template <typename ValueType>
std::pair<bool, bool> MonotonicityChecker<ValueType>::checkDerivative(ValueType derivative) {
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);
storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
std::set<carl::Variable> 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) {
exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
}
auto converter = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::expressions::Expression exprToCheck1 =
converter.toExpression(derivative) >= manager->rational(0);
s.add(exprBounds);
s.add(exprToCheck1);
smtResult = s.check();
monIncr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
storm::expressions::Expression exprToCheck2 =
converter.toExpression(derivative) <= manager->rational(0);
s.reset();
smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
s.add(exprBounds);
s.add(exprToCheck2);
smtResult = s.check();
monDecr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
if (monIncr && monDecr) {
monIncr = false;
monDecr = false;
}
}
assert (!(monIncr && monDecr) || derivative.isZero());
return std::pair<bool, bool>(monIncr, monDecr);
}
// template <typename ValueType>
// std::pair<bool, bool> MonotonicityChecker<ValueType>::checkDerivative(ValueType derivative) {
// 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);
// storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
//
// std::set<carl::Variable> 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) {
// exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
// }
//
// auto converter = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
//
// storm::expressions::Expression exprToCheck1 =
// converter.toExpression(derivative) >= manager->rational(0);
// s.add(exprBounds);
// s.add(exprToCheck1);
// smtResult = s.check();
// monIncr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
//
// storm::expressions::Expression exprToCheck2 =
// converter.toExpression(derivative) <= manager->rational(0);
// s.reset();
// smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
// s.add(exprBounds);
// s.add(exprToCheck2);
// smtResult = s.check();
// monDecr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
// if (monIncr && monDecr) {
// monIncr = false;
// monDecr = false;
// }
// }
// assert (!(monIncr && monDecr) || derivative.isZero());
//
// return std::pair<bool, bool>(monIncr, monDecr);
// }
template <typename ValueType>

71
src/storm-pars/analysis/MonotonicityChecker.h
View File

@ -10,7 +10,10 @@
#include "LatticeExtender.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 "carl/core/Variable.h"
#include "storm/models/ModelBase.h"
#include "storm/models/sparse/Dtmc.h"
@ -18,6 +21,8 @@
#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 {
@ -50,6 +55,70 @@ namespace storm {
*/
bool somewhereMonotonicity(storm::analysis::Lattice* lattice) ;
/*!
* 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) {
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);
storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
std::set<carl::Variable> 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) {
exprBounds = exprBounds && manager->rational(0) < var && var < manager->rational(1);
}
auto converter = storm::expressions::RationalFunctionToExpression<ValueType>(manager);
storm::expressions::Expression exprToCheck1 =
converter.toExpression(derivative) >= manager->rational(0);
s.add(exprBounds);
s.add(exprToCheck1);
smtResult = s.check();
monIncr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
storm::expressions::Expression exprToCheck2 =
converter.toExpression(derivative) <= manager->rational(0);
s.reset();
smtResult = storm::solver::SmtSolver::CheckResult::Unknown;
s.add(exprBounds);
s.add(exprToCheck2);
smtResult = s.check();
monDecr = smtResult == storm::solver::SmtSolver::CheckResult::Sat;
if (monIncr && monDecr) {
monIncr = false;
monDecr = false;
}
}
assert (!(monIncr && monDecr) || derivative.isZero());
return std::pair<bool, bool>(monIncr, monDecr);
}
private:
//TODO: variabele type
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
@ -60,8 +129,6 @@ namespace storm {
std::map<carl::Variable, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
std::pair<bool, bool> checkDerivative(ValueType derivative);
std::unordered_map<ValueType, std::unordered_map<carl::Variable, ValueType>> derivatives;
ValueType getDerivative(ValueType function, carl::Variable var);

2
src/storm/storage/expressions/RationalFunctionToExpression.cpp
View File

@ -28,7 +28,7 @@ namespace storm {
return val.getName() == var.name();
}) != varsManager.end();
if (!found) {
manager->declareIntegerVariable(var.name());
manager->declareRationalVariable(var.name());
}
}

194
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View File

@ -27,7 +27,6 @@
#include "storm-parsers/api/storm-parsers.h"
// TODO: extend for cases in which checkOnSamples and validateAssumption return true
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 ]";
@ -59,22 +58,24 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
EXPECT_TRUE(checker.checkOnSamples(assumption));
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("7").getExpression().getBaseExpressionPointer(),
expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::Greater));
EXPECT_TRUE(checker.checkOnSamples(assumption));
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_FALSE(checker.checkOnSamples(assumption));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption));
storm::storage::BitVector above(8);
above.set(0);
@ -84,8 +85,8 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
auto dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 8);
// Validate assumption
EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice));
EXPECT_FALSE(checker.validated(assumption));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice));
// EXPECT_FALSE(checker.validated(assumption));
expressionManager->declareRationalVariable("6");
expressionManager->declareRationalVariable("8");
@ -100,12 +101,181 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
below.set(9);
initialMiddle = storm::storage::BitVector(13);
dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 13);
EXPECT_FALSE(checker.checkOnSamples(assumption));
EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice));
EXPECT_TRUE(checker.validated(assumption));
EXPECT_FALSE(checker.valid(assumption));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice));
// 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(), 5);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8);
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 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(), 5);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8);
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 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);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
// 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, lattice));
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, lattice));
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, lattice));
}
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(6, dtmc->getNumberOfStates());
ASSERT_EQ(12, dtmc->getNumberOfTransitions());
auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 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);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 6);
lattice->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, lattice));
EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(lattice,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));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(lattice, 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));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice));
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(lattice,assumption));
}

197
src/test/storm-pars/analysis/AssumptionMakerTest.cpp
View File

@ -56,34 +56,179 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) {
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));
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() == "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, 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>>();
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);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);
auto result = assumptionMaker.createAndCheckAssumption(1, 2, lattice);
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);
}
auto var1 = itr->first->getManager().getVariable("183");
auto var2 = itr->first->getManager().getVariable("186");
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>>();
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);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);
auto result = assumptionMaker.createAndCheckAssumption(1, 2, lattice);
auto itr = result.begin();
EXPECT_EQ(3, result.size());
EXPECT_EQ(false, itr->second);
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
EXPECT_EQ(var1, itr->first->getFirstOperand()->asVariableExpression().getVariable());
EXPECT_EQ(var2, itr->first->getSecondOperand()->asVariableExpression().getVariable());
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType());
++itr;
EXPECT_EQ(false, itr->second);
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable());
EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable());
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType());
++itr;
EXPECT_EQ(false, itr->second);
EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable());
EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable());
EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType());
// TODO: createEqualsAssumption checken
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);
}
Write Preview
Loading…
Cancel
Save