diff --git a/resources/examples/testfiles/pdtmc/simple1.pm b/resources/examples/testfiles/pdtmc/simple1.pm new file mode 100644 index 000000000..597da690d --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple1.pm @@ -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 + diff --git a/resources/examples/testfiles/pdtmc/simple2.pm b/resources/examples/testfiles/pdtmc/simple2.pm new file mode 100644 index 000000000..33002c6ce --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple2.pm @@ -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 + diff --git a/resources/examples/testfiles/pdtmc/simple3.pm b/resources/examples/testfiles/pdtmc/simple3.pm new file mode 100644 index 000000000..18f515800 --- /dev/null +++ b/resources/examples/testfiles/pdtmc/simple3.pm @@ -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 + diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 5cd1801a3..01fa208e2 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -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>()); auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*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(matrix, false, false); + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(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> 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> regions = parseRegions(model); diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index e27cd2610..fb7a8b9a8 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -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>(*model); auto matrix = model->getTransitionMatrix(); std::set 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(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { @@ -57,7 +60,7 @@ namespace storm { } auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); std::vector 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>(*model); auto matrix = model->getTransitionMatrix(); std::set 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(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { @@ -96,48 +101,62 @@ namespace storm { } auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); std::vector values = quantitativeResult.getValueVector(); - results.push_back(values); + samples.push_back(values); } } template - bool AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { - bool result = true; + AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { + auto result = AssumptionStatus::UNKNOWN; std::set vars = std::set({}); 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 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 - bool AssumptionChecker::validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice) { - bool result = validated(assumption); - if (!result) { + AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr 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 vars = std::set({}); 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 - bool AssumptionChecker::validateAssumptionFunction(storm::analysis::Lattice* lattice, + AssumptionStatus AssumptionChecker::validateAssumptionFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::iterator state1succ1, typename storm::storage::SparseMatrix::iterator state1succ2, typename storm::storage::SparseMatrix::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 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::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 - bool AssumptionChecker::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, - typename storm::storage::SparseMatrix::iterator state1succ1, - typename storm::storage::SparseMatrix::iterator state1succ2, - typename storm::storage::SparseMatrix::iterator state2succ1, - typename storm::storage::SparseMatrix::iterator state2succ2) { - assert((state1succ1->getColumn() == state2succ1->getColumn() - && state1succ2->getColumn() == state2succ2->getColumn()) - || (state1succ1->getColumn() == state2succ2->getColumn() - && state1succ2->getColumn() == state2succ1->getColumn())); - std::shared_ptr smtSolverFactory = std::make_shared(); - std::shared_ptr 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(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 - bool AssumptionChecker::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, std::shared_ptr assumption) { - assert (!validated(assumption)); + template + AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, std::shared_ptr assumption) { std::shared_ptr smtSolverFactory = std::make_shared(); std::shared_ptr 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 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(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(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 - bool AssumptionChecker::validated(std::shared_ptr assumption) { - return find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end(); - } - - template - bool AssumptionChecker::valid(std::shared_ptr assumption) { - assert(find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end()); - return find(validAssumptions.begin(), validAssumptions.end(), assumption) != validAssumptions.end(); + return result; } template class AssumptionChecker; diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 9ad2aee08..5cde2df72 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -14,9 +14,19 @@ namespace storm { namespace analysis { + enum AssumptionStatus { + VALID, + INVALID, + UNKNOWN, + }; template 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 assumption); + AssumptionStatus checkOnSamples(std::shared_ptr 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 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 assumption); + AssumptionStatus validateAssumption(std::shared_ptr 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 assumption); + AssumptionStatus validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, + std::shared_ptr assumption); private: std::shared_ptr formula; storm::storage::SparseMatrix matrix; - std::vector> results; - - std::set> validatedAssumptions; - - std::set> validAssumptions; + std::vector> samples; - bool validateAssumptionFunction(storm::analysis::Lattice* lattice, - typename storm::storage::SparseMatrix::iterator state1succ1, - typename storm::storage::SparseMatrix::iterator state1succ2, - typename storm::storage::SparseMatrix::iterator state2succ1, - typename storm::storage::SparseMatrix::iterator state2succ2); + void createSamples(); - bool validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, + AssumptionStatus validateAssumptionFunction(storm::analysis::Lattice* lattice, typename storm::storage::SparseMatrix::iterator state1succ1, typename storm::storage::SparseMatrix::iterator state1succ2, typename storm::storage::SparseMatrix::iterator state2succ1, typename storm::storage::SparseMatrix::iterator state2succ2); - bool validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, - std::shared_ptr assumption); }; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 0a5ab376e..e2828db50 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -6,6 +6,7 @@ namespace storm { namespace analysis { + typedef std::shared_ptr AssumptionType; template AssumptionMaker::AssumptionMaker(storm::analysis::AssumptionChecker* 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()); 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 - std::map, bool> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) { - std::map, bool> result; + std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) { + std::map, 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 assumption1 = std::make_shared(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 assumption2 = std::make_shared(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 assumption3 = std::make_shared(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 - std::shared_ptr AssumptionMaker::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(*expressionManager, expressionManager->getBooleanType(), - var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Equal)); - } - - template class AssumptionMaker; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 190559a72..72d0255dc 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -17,6 +17,7 @@ namespace storm { template class AssumptionMaker { + typedef std::shared_ptr 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* checker, uint_fast64_t numberOfStates, bool validate); - std::map, bool> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice); - - std::shared_ptr createEqualAssumption(uint_fast64_t val1, uint_fast64_t val2); + std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice); private: storm::analysis::AssumptionChecker* assumptionChecker; @@ -39,8 +38,6 @@ namespace storm { uint_fast64_t numberOfStates; bool validate; - - }; } } diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 8c14afe49..665d39537 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -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)); + } } } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 8b66c30db..0e1790fc3 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -21,7 +21,6 @@ namespace storm { struct Node { boost::container::flat_set 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 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 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 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 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 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> 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); }; } } diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 0e48ac600..4135e4ded 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -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(model->getTransitionMatrix(), false, false); + storm::storage::StronglyConnectedComponentDecompositionOptions const options; + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(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 LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr 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); } diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 55568ab45..d96c358de 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -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>(); + // TODO initialiseren van sample check if (model != nullptr) { std::shared_ptr> sparseModel = model->as>(); this->extender = new storm::analysis::LatticeExtender(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>( - assumptions); - auto assumptionsCopy2 = std::vector>( - 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>( + assumptions); + auto assumptionsCopy2 = std::vector>( + 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>( +// assumptions); +// auto assumptionsCopy2 = std::vector>( +// 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>( +// assumptions); +// auto assumptionsCopy2 = std::vector>( +// 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 - std::pair MonotonicityChecker::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 smtSolverFactory = std::make_shared(); - std::shared_ptr manager( - new storm::expressions::ExpressionManager()); - - storm::solver::Z3SmtSolver s(*manager); - storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown; - - std::set 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(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(monIncr, monDecr); - } +// template +// std::pair MonotonicityChecker::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 smtSolverFactory = std::make_shared(); +// std::shared_ptr manager( +// new storm::expressions::ExpressionManager()); +// +// storm::solver::Z3SmtSolver s(*manager); +// storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown; +// +// std::set 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(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(monIncr, monDecr); +// } template diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 94cb39ff3..957827f73 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -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 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 smtSolverFactory = std::make_shared(); + std::shared_ptr manager( + new storm::expressions::ExpressionManager()); + + storm::solver::Z3SmtSolver s(*manager); + storm::solver::SmtSolver::CheckResult smtResult = storm::solver::SmtSolver::CheckResult::Unknown; + + std::set 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(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(monIncr, monDecr); + } + private: //TODO: variabele type std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ; @@ -60,8 +129,6 @@ namespace storm { std::map> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); - std::pair checkDerivative(ValueType derivative); - std::unordered_map> derivatives; ValueType getDerivative(ValueType function, carl::Variable var); diff --git a/src/storm/storage/expressions/RationalFunctionToExpression.cpp b/src/storm/storage/expressions/RationalFunctionToExpression.cpp index 81abc8f36..0bbd08038 100644 --- a/src/storm/storage/expressions/RationalFunctionToExpression.cpp +++ b/src/storm/storage/expressions/RationalFunctionToExpression.cpp @@ -28,7 +28,7 @@ namespace storm { return val.getName() == var.name(); }) != varsManager.end(); if (!found) { - manager->declareIntegerVariable(var.name()); + manager->declareRationalVariable(var.name()); } } diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index ab0b25d18..e6b515987 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -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(*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(*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> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 3); + + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("1"); + expressionManager->declareRationalVariable("2"); + + // Checking on samples + auto assumption = std::make_shared( + 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(*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(*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> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 5); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 3); + auto expressionManager = std::make_shared(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(*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(*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(*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> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + ASSERT_EQ(6, dtmc->getNumberOfStates()); + ASSERT_EQ(12, dtmc->getNumberOfTransitions()); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 3); + + auto expressionManager = std::make_shared(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(*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(*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(*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)); +} diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index af6f0213d..a7603ca09 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -56,34 +56,179 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { auto assumptionMaker = storm::analysis::AssumptionMaker(&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> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + 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(formulas[0], dtmc, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(&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> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); + model = simplifier.getSimplifiedModel(); + dtmc = model->as>(); + + 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(formulas[0], dtmc, 3); + auto assumptionMaker = storm::analysis::AssumptionMaker(&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); } +