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

First working version of MaxSAT-based minimal command counterexample generation. 

Former-commit-id: 6dc49157f9
main
dehnert 12 years ago
parent
b6ff62e689
commit
629448c312
6 changed files with 183 additions and 57 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. 21
      counterexamples.h
  2. 22
      src/adapters/ExplicitModelAdapter.h
  3. 8
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  4. 133
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  5. 34
      src/storm.cpp
  6. 22
      src/utility/IRUtility.h

21
counterexamples.h
View File

@ -0,0 +1,21 @@
/*
* vector.h
*
* Created on: 06.12.2012
* Author: Christian Dehnert
*/
#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_
#define STORM_UTILITY_COUNTEREXAMPLE_H_
namespace storm {
namespace utility {
namespace counterexample{
} // namespace counterexample
} // namespace utility
} // namespace storm
#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */

22
src/adapters/ExplicitModelAdapter.h
View File

@ -125,28 +125,6 @@ namespace storm {
}
private:
/*!
* Sets some boolean variable in the given state object.
*
* @param state The state to modify.
* @param index The index of the boolean variable to modify.
* @param value The new value of the variable.
*/
static void setValue(StateType* state, uint_fast64_t index, bool value) {
std::get<0>(*state)[index] = value;
}
/*!
* Set some integer variable in the given state object.
*
* @param state The state to modify.
* @param index index of the integer variable to modify.
* @param value The new value of the variable.
*/
static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) {
std::get<1>(*state)[index] = value;
}
/*!
* Transforms a state into a somewhat readable string.
*

8
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -1084,12 +1084,12 @@ namespace storm {
* @param model The Gurobi model.
* @param variableInformation A struct with information about the variables of the model.
*/
static std::unordered_set<uint_fast64_t> getUsedLabelsInSolution(GRBenv* env, GRBmodel* model, VariableInformation const& variableInformation) {
static std::set<uint_fast64_t> getUsedLabelsInSolution(GRBenv* env, GRBmodel* model, VariableInformation const& variableInformation) {
int error = 0;
// Check whether the model was optimized, so we can read off the solution.
if (checkGurobiModelIsOptimized(env, model)) {
std::unordered_set<uint_fast64_t> result;
std::set<uint_fast64_t> result;
double value = 0;
for (auto labelVariablePair : variableInformation.labelToVariableIndexMap) {
@ -1202,7 +1202,7 @@ namespace storm {
public:
static std::unordered_set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
static std::set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
#ifdef STORM_HAVE_GUROBI
// (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabels()) {
@ -1239,7 +1239,7 @@ namespace storm {
optimizeModel(environmentModelPair.first, environmentModelPair.second);
// (4.5) Read off result from variables.
std::unordered_set<uint_fast64_t> usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation);
std::set<uint_fast64_t> usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation);
// Display achieved probability.
std::pair<uint_fast64_t, double> initialStateProbabilityPair = getReachabilityProbability(environmentModelPair.first, environmentModelPair.second, labeledMdp, variableInformation);

133
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -172,6 +172,7 @@ namespace storm {
// * identify labels that can directly precede a given action
// * identify labels that directly reach a target state
// * identify labels that can directly follow a given action
// * identify labels that can be found on each path to the target states.
std::set<uint_fast64_t> initialLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> precedingLabels;
@ -361,7 +362,7 @@ namespace storm {
* @param solver The solver to use for the satisfiability evaluation.
*/
static void assertSymbolicCuts(storm::ir::Program const& program, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) {
// TODO:
// FIXME:
// find synchronization cuts
// find forward/backward cuts
@ -388,9 +389,106 @@ namespace storm {
z3::expr upperBound = expressionAdapter.translateExpression(integerVariable.getUpperBound());
upperBound = solverVariables.at(integerVariable.getName()) <= upperBound;
localSolver.add(upperBound);
}
}
// Construct an expression that exactly characterizes the initial state.
std::unique_ptr<storm::utility::ir::StateType> initialState(storm::utility::ir::getInitialState(program, programVariableInformation));
z3::expr initialStateExpression = localContext.bool_val(true);
for (uint_fast64_t index = 0; index < programVariableInformation.booleanVariables.size(); ++index) {
if (std::get<0>(*initialState).at(programVariableInformation.booleanVariableToIndexMap.at(programVariableInformation.booleanVariables[index].getName()))) {
initialStateExpression = initialStateExpression && solverVariables.at(programVariableInformation.booleanVariables[index].getName());
} else {
initialStateExpression = initialStateExpression && !solverVariables.at(programVariableInformation.booleanVariables[index].getName());
}
}
for (uint_fast64_t index = 0; index < programVariableInformation.integerVariables.size(); ++index) {
storm::ir::IntegerVariable const& variable = programVariableInformation.integerVariables[index];
initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName()))));
}
std::map<uint_fast64_t, std::set<uint_fast64_t>> backwardImplications;
// First check for possible backward cuts.
for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) {
storm::ir::Module const& module = program.getModule(moduleIndex);
for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) {
storm::ir::Command const& command = module.getCommand(commandIndex);
// If the label of the command is not relevant, skip it entirely.
if (relevancyInformation.relevantLabels.find(command.getGlobalIndex()) == relevancyInformation.relevantLabels.end()) continue;
// Save the state of the solver so we can easily backtrack.
localSolver.push();
// Check if the command is enabled in the initial state.
localSolver.add(expressionAdapter.translateExpression(command.getGuard()));
localSolver.add(initialStateExpression);
z3::check_result checkResult = localSolver.check();
localSolver.pop();
localSolver.push();
// If it is not and the action is not synchronizing, we can impose backward cuts.
if (checkResult == z3::unsat && command.getActionName() == "") {
localSolver.add(!expressionAdapter.translateExpression(command.getGuard()));
localSolver.push();
// We need to check all commands of the all modules, because they could enable the current
// command via a global variable.
for (uint_fast64_t otherModuleIndex = 0; otherModuleIndex < program.getNumberOfModules(); ++otherModuleIndex) {
storm::ir::Module const& otherModule = program.getModule(otherModuleIndex);
for (uint_fast64_t otherCommandIndex = 0; otherCommandIndex < otherModule.getNumberOfCommands(); ++otherCommandIndex) {
storm::ir::Command const& otherCommand = otherModule.getCommand(otherCommandIndex);
// We don't need to consider irrelevant commands and the command itself.
if (relevancyInformation.relevantLabels.find(otherCommand.getGlobalIndex()) == relevancyInformation.relevantLabels.end()) continue;
if (moduleIndex == otherModuleIndex && commandIndex == otherCommandIndex) continue;
std::vector<z3::expr> formulae;
formulae.reserve(otherCommand.getNumberOfUpdates());
localSolver.push();
for (uint_fast64_t updateIndex = 0; updateIndex < otherCommand.getNumberOfUpdates(); ++updateIndex) {
std::unique_ptr<storm::ir::expressions::BaseExpression> weakestPrecondition = storm::utility::ir::getWeakestPrecondition(command.getGuard(), {otherCommand.getUpdate(updateIndex)});
formulae.push_back(expressionAdapter.translateExpression(weakestPrecondition));
}
assertDisjunction(localContext, localSolver, formulae);
// If the assertions were satisfiable, this means the other command could successfully
// enable the current command.
if (localSolver.check() == z3::sat) {
backwardImplications[command.getGlobalIndex()].insert(otherCommand.getGlobalIndex());
}
localSolver.pop();
}
}
// Remove the negated guard from the solver assertions.
localSolver.pop();
}
// Restore state of solver where only the variable bounds are asserted.
localSolver.pop();
}
}
std::cout << localSolver << std::endl;
std::vector<z3::expr> formulae;
for (auto const& labelImplicationsPair : backwardImplications) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelImplicationsPair.first)));
for (auto label : labelImplicationsPair.second) {
formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
assertDisjunction(context, solver, formulae);
formulae.clear();
}
}
/*!
@ -564,12 +662,16 @@ namespace storm {
}
// Check whether the assumptions are satisfiable.
LOG4CPLUS_DEBUG(logger, "Invoking satisfiability checking.");
z3::check_result result = solver.check(assumptions);
LOG4CPLUS_DEBUG(logger, "Done invoking satisfiability checking.");
if (result == z3::check_result::sat) {
if (result == z3::sat) {
return true;
} else {
LOG4CPLUS_DEBUG(logger, "Computing unsat core.");
z3::expr_vector unsatCore = solver.unsat_core();
LOG4CPLUS_DEBUG(logger, "Computed unsat core.");
std::vector<z3::expr> blockingVariables;
blockingVariables.reserve(unsatCore.size());
@ -648,6 +750,8 @@ namespace storm {
* @return The smallest set of labels such that the constraint system of the solver is still satisfiable.
*/
static std::set<uint_fast64_t> findSmallestCommandSet(z3::context& context, z3::solver& solver, VariableInformation& variableInformation, std::vector<z3::expr>& softConstraints, uint_fast64_t& nextFreeVariableIndex) {
solver.push();
for (uint_fast64_t i = 0; ; ++i) {
if (fuMalikMaxsatStep(context, solver, variableInformation, softConstraints, nextFreeVariableIndex)) {
break;
@ -661,16 +765,19 @@ namespace storm {
for (auto const& labelIndexPair : variableInformation.labelToIndexMap) {
z3::expr value = model.eval(variableInformation.labelVariables[labelIndexPair.second]);
std::stringstream resultStream;
resultStream << value;
if (resultStream.str() == "true") {
// Check whether the label variable was set or not.
if (eq(value, context.bool_val(true))) {
result.insert(labelIndexPair.first);
} else if (resultStream.str() == "false") {
} else if (eq(value, context.bool_val(false))) {
// Nothing to do in this case.
} else if (eq(value, variableInformation.labelVariables[labelIndexPair.second])) {
// If the variable is a "don't care", then we rather not take it, so nothing to do in this case
// as well.
} else {
throw storm::exceptions::InvalidStateException() << "Could not retrieve value of boolean variable.";
throw storm::exceptions::InvalidStateException() << "Could not retrieve value of boolean variable from illegal value.";
}
}
solver.pop();
return result;
}
@ -749,17 +856,9 @@ namespace storm {
} else {
done = true;
}
std::cout << "Achieved probability: " << maximalReachabilityProbability << " with " << commandSet.size() << " commands in iteration " << iterations << "." << std::endl;
++iterations;
} while (!done);
std::cout << "Achieved probability: " << maximalReachabilityProbability << " with " << commandSet.size() << " commands." << std::endl;
std::cout << "Taken commands are:" << std::endl;
for (auto label : commandSet) {
std::cout << label << ", ";
}
std::cout << std::endl;
// (8) Return the resulting command set after undefining the constants.
storm::utility::ir::undefineUndefinedConstants(program);
return commandSet;

34
src/storm.cpp
View File

@ -338,19 +338,19 @@ int main(const int argc, const char* argv[]) {
model->printModelInformationToStream(std::cout);
// Enable the following lines to test the MinimalLabelSetGenerator.
// if (model->getType() == storm::models::MDP) {
// std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
// storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
// storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
// storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
// std::unordered_set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true, true);
//
// std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
// for (uint_fast64_t label : labels) {
// std::cout << label << ", ";
// }
// std::cout << std::endl;
// }
if (model->getType() == storm::models::MDP) {
std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
for (uint_fast64_t label : labels) {
std::cout << label << ", ";
}
std::cout << std::endl;
}
// Enable the following lines to test the SMTMinimalCommandSetGenerator.
if (model->getType() == storm::models::MDP) {
@ -358,7 +358,13 @@ int main(const int argc, const char* argv[]) {
storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true);
std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
std::cout << "Found solution with " << labels.size() << " commands." << std::endl;
for (uint_fast64_t label : labels) {
std::cout << label << ", ";
}
std::cout << std::endl;
}
}

22
src/utility/IRUtility.h
View File

@ -369,6 +369,28 @@ namespace storm {
LOG4CPLUS_DEBUG(logger, "Generated initial state.");
return initialState;
}
/*!
* Sets some boolean variable in the given state object.
*
* @param state The state to modify.
* @param index The index of the boolean variable to modify.
* @param value The new value of the variable.
*/
static void setValue(StateType* state, uint_fast64_t index, bool value) {
std::get<0>(*state)[index] = value;
}
/*!
* Set some integer variable in the given state object.
*
* @param state The state to modify.
* @param index index of the integer variable to modify.
* @param value The new value of the variable.
*/
static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) {
std::get<1>(*state)[index] = value;
}
/*!
* Defines the undefined constants of the given program using the given string.

Write Preview
Loading…
Cancel
Save