diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index fb7a8b9a8..747b85874 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -23,39 +23,37 @@ namespace storm { namespace analysis { template - AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { + AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { this->formula = formula; this->matrix = model->getTransitionMatrix(); // Create sample points - auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model); + auto instantiator = utility::ModelInstantiator, models::sparse::Dtmc>(*model); auto matrix = model->getTransitionMatrix(); - std::set variables = storm::models::sparse::getProbabilityParameters(*model); + std::set::type> variables = models::sparse::getProbabilityParameters(*model); - // TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again for (auto i = 0; i < numberOfSamples; ++i) { - auto valuation = storm::utility::parametric::Valuation(); + auto valuation = utility::parametric::Valuation(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { - // TODO: Type // Creates samples between 0 and 1, 1/(#samples+2), 2/(#samples+2), ..., (#samples+1)/(#samples+2) - auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 2))))); + auto val = std::pair::type, typename utility::parametric::CoefficientType::type>((*itr), utility::convertNumber::type>(boost::lexical_cast((i+1)/(double (numberOfSamples + 2))))); valuation.insert(val); } - storm::models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); - auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); - std::unique_ptr checkResult; + models::sparse::Dtmc sampleModel = instantiator.instantiate(valuation); + auto checker = modelchecker::SparseDtmcPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; if (formula->isProbabilityOperatorFormula() && formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { - const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); checkResult = checker.computeUntilProbabilities(Environment(), checkTask); } else if (formula->isProbabilityOperatorFormula() && formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { - const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + STORM_LOG_THROW(false, exceptions::NotSupportedException, "Expecting until or eventually formula"); } auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); @@ -65,38 +63,37 @@ namespace storm { } template - AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { + AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { this->formula = formula; this->matrix = model->getTransitionMatrix(); // Create sample points - auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Mdp>(*model); + auto instantiator = utility::ModelInstantiator, models::sparse::Mdp>(*model); auto matrix = model->getTransitionMatrix(); - std::set variables = storm::models::sparse::getProbabilityParameters(*model); + std::set::type> variables = models::sparse::getProbabilityParameters(*model); - // TODO: sampling part also done in MonotonicityChecker, would be better to use this one instead of creating it again for (auto i = 0; i < numberOfSamples; ++i) { - auto valuation = storm::utility::parametric::Valuation(); + auto valuation = utility::parametric::Valuation(); for (auto itr = variables.begin(); itr != variables.end(); ++itr) { - // TODO: Type - auto val = std::pair((*itr), storm::utility::convertNumber(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); + auto val = std::pair::type, + typename utility::parametric::CoefficientType::type>((*itr), utility::convertNumber::type>(boost::lexical_cast((i+1)/(double (numberOfSamples + 1))))); valuation.insert(val); } - storm::models::sparse::Mdp sampleModel = instantiator.instantiate(valuation); - auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(sampleModel); - std::unique_ptr checkResult; + models::sparse::Mdp sampleModel = instantiator.instantiate(valuation); + auto checker = modelchecker::SparseMdpPrctlModelChecker>(sampleModel); + std::unique_ptr checkResult; if (formula->isProbabilityOperatorFormula() && formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { - const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( (*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula()); checkResult = checker.computeUntilProbabilities(Environment(), checkTask); } else if (formula->isProbabilityOperatorFormula() && formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) { - const storm::modelchecker::CheckTask checkTask = storm::modelchecker::CheckTask( + const modelchecker::CheckTask checkTask = modelchecker::CheckTask( (*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula()); checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + STORM_LOG_THROW(false, exceptions::NotSupportedException, "Expecting until or eventually formula"); } auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult(); @@ -106,16 +103,16 @@ namespace storm { } template - AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { + AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) { auto result = AssumptionStatus::UNKNOWN; - std::set vars = std::set({}); + std::set vars = std::set({}); assumption->gatherVariables(vars); 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); + std::shared_ptr manager = assumption->getManager().getSharedPointer(); + auto valuation = expressions::SimpleValuation(manager); auto values = (*itr); for (auto var = vars.begin(); result == AssumptionStatus::UNKNOWN && var != vars.end(); ++var) { - storm::expressions::Variable par = *var; + expressions::Variable par = *var; auto index = std::stoi(par.getName()); valuation.setRationalValue(par, values[index]); } @@ -128,22 +125,22 @@ namespace storm { } template - AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice) { + AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, Lattice* lattice) { // First check if based on sample points the assumption can be discharged auto result = checkOnSamples(assumption); - assert (result != storm::analysis::AssumptionStatus::VALID); + assert (result != AssumptionStatus::VALID); - if (result == storm::analysis::AssumptionStatus::UNKNOWN) { + if (result == AssumptionStatus::UNKNOWN) { // If result from sample checking was unknown, the assumption might hold, so we continue, // otherwise we return INVALID - std::set vars = std::set({}); + std::set vars = std::set({}); assumption->gatherVariables(vars); STORM_LOG_THROW(assumption->getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::Greater || + expressions::BinaryRelationExpression::RelationType::Greater || assumption->getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::Equal, - storm::exceptions::NotSupportedException, + expressions::BinaryRelationExpression::RelationType::Equal, + exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); // Row with successors of the first state @@ -168,13 +165,13 @@ namespace storm { } if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { - if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater - && lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != storm::analysis::Lattice::UNKNOWN) { + if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater + && lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Lattice::UNKNOWN) { // The assumption should be the greater assumption // If the result is unknown, we cannot compare, also SMTSolver will not help result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, state2succ2); - } else if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) { + } else if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Equal) { // The assumption is equal, the successors are the same, // so if the probability of reaching the successors is the same, we have a valid assumption if (state1succ1->getValue() == state2succ1->getValue()) { @@ -184,21 +181,21 @@ namespace storm { result = AssumptionStatus::UNKNOWN; } } else { - result = validateAssumptionSMTSolver(lattice, assumption); + result = validateAssumptionSMTSolver(assumption, lattice); } } else { - result = validateAssumptionSMTSolver(lattice, assumption); + result = validateAssumptionSMTSolver(assumption, lattice); } } return result; } template - 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, - typename storm::storage::SparseMatrix::iterator state2succ2) { + AssumptionStatus AssumptionChecker::validateAssumptionFunction(Lattice* lattice, + typename storage::SparseMatrix::iterator state1succ1, + typename storage::SparseMatrix::iterator state1succ2, + typename storage::SparseMatrix::iterator state2succ1, + typename storage::SparseMatrix::iterator state2succ2) { assert((state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) || (state1succ1->getColumn() == state2succ2->getColumn() @@ -209,10 +206,10 @@ namespace storm { // 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); - if (comp == storm::analysis::Lattice::ABOVE) { + assert (comp == Lattice::ABOVE || comp == Lattice::BELOW); + if (comp == Lattice::ABOVE) { prob = state1succ1->getValue() - state2succ1->getValue(); - } else if (comp == storm::analysis::Lattice::BELOW) { + } else if (comp == Lattice::BELOW) { prob = state1succ2->getValue() - state2succ2->getValue(); } @@ -220,8 +217,7 @@ namespace storm { // If the result in monotone increasing (decreasing), then choose 0 (1) for the substitutions // This will give the smallest result - // TODO: Type - std::map substitutions; + std::map::type, typename utility::parametric::CoefficientType::type> substitutions; for (auto var : vars) { auto monotonicity = MonotonicityChecker::checkDerivative(prob.derivative(var)); if (monotonicity.first) { @@ -243,9 +239,9 @@ namespace storm { 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()); + AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(std::shared_ptr assumption, Lattice* lattice) { + std::shared_ptr smtSolverFactory = std::make_shared(); + std::shared_ptr manager(new expressions::ExpressionManager()); AssumptionStatus result; auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); @@ -256,8 +252,8 @@ namespace storm { 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; + expressions::Expression exprOrderSucc = manager->boolean(true); + std::set stateVariables; for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { auto varname1 = "s" + std::to_string(itr1->getColumn()); if (!manager->hasVariable(varname1)) { @@ -270,13 +266,13 @@ namespace storm { stateVariables.insert(manager->declareRationalVariable(varname2)); } auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn()); - if (comp == storm::analysis::Lattice::ABOVE) { + if (comp == Lattice::ABOVE) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= manager->getVariable(varname2)); - } else if (comp == storm::analysis::Lattice::BELOW) { + } else if (comp == Lattice::BELOW) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= manager->getVariable(varname2)); - } else if (comp == storm::analysis::Lattice::SAME) { + } else if (comp == Lattice::SAME) { exprOrderSucc = exprOrderSucc && (manager->getVariable(varname1) = manager->getVariable(varname2)); } else { @@ -287,41 +283,39 @@ namespace storm { } if (orderKnown) { - storm::solver::Z3SmtSolver s(*manager); - auto valueTypeToExpression = storm::expressions::RationalFunctionToExpression(manager); - storm::expressions::Expression expr1 = manager->rational(0); + solver::Z3SmtSolver s(*manager); + auto valueTypeToExpression = expressions::RationalFunctionToExpression(manager); + expressions::Expression expr1 = manager->rational(0); for (auto itr1 = row1.begin(); itr1 != row1.end(); ++itr1) { expr1 = expr1 + (valueTypeToExpression.toExpression(itr1->getValue()) * manager->getVariable("s" + std::to_string(itr1->getColumn()))); } - storm::expressions::Expression expr2 = manager->rational(0); + expressions::Expression expr2 = manager->rational(0); for (auto itr2 = row2.begin(); itr2 != row2.end(); ++itr2) { expr2 = expr2 + (valueTypeToExpression.toExpression(itr2->getValue()) * manager->getVariable("s" + std::to_string(itr2->getColumn()))); } // Create expression for the assumption based on the relation to successors // It is the negation of actual assumption - // TODO: use same manager s.t. assumption can be used directly ? - storm::expressions::Expression exprToCheck ; + expressions::Expression exprToCheck ; if (assumption->getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::Greater) { + expressions::BinaryRelationExpression::RelationType::Greater) { exprToCheck = expr1 <= expr2; } else { assert (assumption->getRelationType() == - storm::expressions::BinaryRelationExpression::RelationType::Equal); + expressions::BinaryRelationExpression::RelationType::Equal); exprToCheck = expr1 > expr2; } auto variables = manager->getVariables(); // Bounds for the state probabilities and parameters - storm::expressions::Expression exprBounds = manager->boolean(true); + 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); } } @@ -329,15 +323,14 @@ namespace storm { 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? + assert (s.check() == solver::SmtSolver::CheckResult::Sat); s.add(exprToCheck); auto smtRes = s.check(); - if (smtRes == storm::solver::SmtSolver::CheckResult::Unsat) { + if (smtRes == solver::SmtSolver::CheckResult::Unsat) { // If there is no thing satisfying the negation we are safe. result = AssumptionStatus::VALID; - } else if (smtRes == storm::solver::SmtSolver::CheckResult::Sat) { - assert (smtRes == storm::solver::SmtSolver::CheckResult::Sat); + } else if (smtRes == solver::SmtSolver::CheckResult::Sat) { + assert (smtRes == solver::SmtSolver::CheckResult::Sat); result = AssumptionStatus::INVALID; } else { result = AssumptionStatus::UNKNOWN; @@ -349,6 +342,6 @@ namespace storm { return result; } - template class AssumptionChecker; + template class AssumptionChecker; } } diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 5cde2df72..b7746000f 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -14,6 +14,9 @@ namespace storm { namespace analysis { + /*! + * Constants for status of assumption + */ enum AssumptionStatus { VALID, INVALID, @@ -22,10 +25,6 @@ namespace storm { template class AssumptionChecker { public: - /*! - * Constants for status of assumption - */ - /*! * Constructs an AssumptionChecker based on the number of samples, for the given formula and model. @@ -34,7 +33,7 @@ namespace storm { * @param model The dtmc model to check the formula on. * @param numberOfSamples Number of sample points. */ - AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); + AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); /*! * Constructs an AssumptionChecker based on the number of samples, for the given formula and model. @@ -43,7 +42,7 @@ namespace storm { * @param model The mdp model to check the formula on. * @param numberOfSamples Number of sample points. */ - AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); + AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); /*! * Checks if the assumption holds at the sample points of the AssumptionChecker. @@ -51,7 +50,7 @@ namespace storm { * @param assumption The assumption to check. * @return AssumptionStatus::UNKNOWN or AssumptionStatus::INVALID */ - AssumptionStatus checkOnSamples(std::shared_ptr assumption); + AssumptionStatus checkOnSamples(std::shared_ptr assumption); /*! * Tries to validate an assumption based on the lattice and underlying transition matrix. @@ -60,25 +59,31 @@ namespace storm { * @param lattice The lattice. * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID */ - AssumptionStatus validateAssumption(std::shared_ptr assumption, storm::analysis::Lattice* lattice); + AssumptionStatus validateAssumption(std::shared_ptr assumption, Lattice* lattice); - AssumptionStatus validateAssumptionSMTSolver(storm::analysis::Lattice* lattice, - std::shared_ptr assumption); + /*! + * Tries to validate an assumption based on the lattice, and SMT solving techniques + * + * @param assumption The assumption to validate. + * @param lattice The lattice. + * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID + */ + AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr assumption, Lattice* lattice); private: - std::shared_ptr formula; + std::shared_ptr formula; - storm::storage::SparseMatrix matrix; + storage::SparseMatrix matrix; std::vector> samples; void createSamples(); - 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); + AssumptionStatus validateAssumptionFunction(Lattice* lattice, + typename storage::SparseMatrix::iterator state1succ1, + typename storage::SparseMatrix::iterator state1succ2, + typename storage::SparseMatrix::iterator state2succ1, + typename storage::SparseMatrix::iterator state2succ2); }; }