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

Added toExpression functions for SMT constraints

main
Alexander Bork 7 years ago
parent
7cab3985c0
commit
fc9befbe9e
3 changed files with 95 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
  2. 4
      src/storm-dft/modelchecker/dft/DFTASFChecker.h
  3. 94
      src/storm-dft/modelchecker/dft/SmtConstraint.cpp

23
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
View File

@ -4,6 +4,7 @@
#include "storm/utility/file.h"
#include "storm/utility/bitoperations.h"
#include "storm-parsers/parser/ExpressionCreator.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/Type.h"
@ -123,12 +124,6 @@ namespace storm {
// Handle dependencies
addMarkovianConstraints();
//TODO Move this out of convert method
// Toplevel element will not fail (part of constraint 13)
constraints.push_back(std::make_shared<IsConstantValue>(timePointVariables.at(dft.getTopLevelIndex()), notFailed));
constraints.back()->setDescription("Toplevel element should not fail");
}
// Constraint Generator Functions
@ -434,10 +429,12 @@ namespace storm {
storm::utility::closeFile(stream);
}
void DFTASFChecker::toSolver() {
std::vector<storm::solver::SmtSolver::CheckResult> DFTASFChecker::toSolver() {
std::vector<storm::solver::SmtSolver::CheckResult> resultVector;
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(
*manager);
//Add variables to manager
for (auto const &timeVarEntry : timePointVariables) {
manager->declareIntegerVariable(varNames[timeVarEntry.second]);
}
@ -452,11 +449,21 @@ namespace storm {
manager->declareIntegerVariable(varNames[tmpVar]);
}
}
// Add constraints to solver
for (auto const &constraint : constraints) {
solver->add(constraint->toExpression(varNames, manager));
}
// Set backtracking marker to check several properties without reconstructing DFT encoding
solver->push();
// Constraint that toplevel element will not fail (part of constraint 13)
std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
timePointVariables.at(dft.getTopLevelIndex()), notFailed);
solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
resultVector.push_back(solver->check());
solver->pop();
//TODO Add porperties to check
return resultVector;
}
}
}

4
src/storm-dft/modelchecker/dft/DFTASFChecker.h
View File

@ -4,6 +4,7 @@
#include <vector>
#include <unordered_map>
#include "storm/solver/SmtSolver.h"
#include "SmtConstraint.h"
#include "storm-dft/storage/dft/DFT.h"
#include "storm/utility/solver.h"
@ -35,7 +36,8 @@ namespace storm {
*/
void convert();
void toFile(std::string const&);
void toSolver();
std::vector<storm::solver::SmtSolver::CheckResult> toSolver();
private:
uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;

94
src/storm-dft/modelchecker/dft/SmtConstraint.cpp
View File

@ -1,4 +1,5 @@
#include "DFTASFChecker.h"
#include <storm/storage/expressions/ExpressionManager.h>
#include <string>
namespace storm {
@ -36,7 +37,16 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
std::vector<storm::expressions::Expression> outerAnd;
std::vector<storm::expressions::Expression> innerOr;
for (auto const &ovi : varIndices) {
outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) >=
manager->getVariableExpression(varNames.at(ovi))));
innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) ==
manager->getVariableExpression(varNames.at(ovi))));
}
outerAnd.push_back(disjunction(innerOr));
return conjunction(outerAnd);
}
private:
@ -76,7 +86,16 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
std::vector<storm::expressions::Expression> outerAnd;
std::vector<storm::expressions::Expression> innerOr;
for (auto const &ovi : varIndices) {
outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) <=
manager->getVariableExpression(varNames.at(ovi))));
innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) ==
manager->getVariableExpression(varNames.at(ovi))));
}
outerAnd.push_back(disjunction(innerOr));
return conjunction(outerAnd);
}
private:
@ -105,7 +124,8 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return (manager->getVariableExpression(varNames.at(varIndex)) >= lowerBound) &&
(manager->getVariableExpression(varNames.at(varIndex)) <= upperBound);
}
private:
@ -139,7 +159,15 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
if (constraints.empty()) {
return manager->boolean(true);
} else {
std::vector<storm::expressions::Expression> conjuncts;
for (auto const &c : constraints) {
conjuncts.push_back(c->toExpression(varNames, manager));
}
return conjunction(conjuncts);
}
}
private:
@ -172,7 +200,15 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
if (constraints.empty()) {
return manager->boolean(false);
} else {
std::vector<storm::expressions::Expression> disjuncts;
for (auto const &c : constraints) {
disjuncts.push_back(c->toExpression(varNames, manager));
}
return disjunction(disjuncts);
}
}
private:
@ -194,7 +230,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return implies(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager));
}
private:
@ -216,7 +252,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return iff(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager));
}
private:
@ -241,7 +277,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->boolean(value);
}
private:
@ -270,7 +306,11 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
if (value) {
return manager->getVariableExpression(varNames.at(varIndex));
} else {
return !(manager->getVariableExpression(varNames.at(varIndex)));
}
}
private:
@ -296,7 +336,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->getVariableExpression(varNames.at(varIndex)) == manager->integer(value);
}
private:
@ -322,7 +362,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->getVariableExpression(varNames.at(varIndex)) < value;
}
private:
@ -347,7 +387,7 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->getVariableExpression(varNames.at(varIndex)) <= value;
}
private:
@ -370,7 +410,8 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->getVariableExpression(varNames.at(var1Index)) ==
manager->getVariableExpression(varNames.at(var2Index));
}
private:
@ -393,7 +434,8 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return manager->getVariableExpression(varNames.at(var1Index)) <
manager->getVariableExpression(varNames.at(var2Index));
}
private:
@ -427,7 +469,16 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
std::vector<storm::expressions::Expression> conjuncts;
for (uint64_t i = 0; i < varIndices.size(); ++i) {
for (uint64_t j = i + 1; j < varIndices.size(); ++j) {
// check all elements pairwise for inequality
conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i))) !=
manager->getVariableExpression(varNames.at(varIndices.at(j))));
}
}
// take the conjunction of all pairwise inequalities
return conjunction(conjuncts);
}
private:
@ -455,9 +506,16 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
std::vector<storm::expressions::Expression> conjuncts;
for (uint64_t i = 1; i < varIndices.size(); ++i) {
conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i - 1))) <=
manager->getVariableExpression(varNames.at(varIndices.at(i))));
}
// take the conjunction of all pairwise inequalities
return conjunction(conjuncts);
}
private:
std::vector<uint64_t> varIndices;
};
@ -479,7 +537,9 @@ namespace storm {
storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
//TODO
return ite(ifConstraint->toExpression(varNames, manager),
thenConstraint->toExpression(varNames, manager),
elseConstraint->toExpression(varNames, manager));
}
private:

Write Preview
Loading…
Cancel
Save