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

Adapted MaxSAT-based minimal command set generator to some recent changes to make it work again. 

Former-commit-id: 8f8c33b920
main
dehnert 11 years ago
parent
40c698af90
commit
e2c2177dca
5 changed files with 158 additions and 151 deletions
Unified View
  1. 58
      src/adapters/ExplicitModelAdapter.h
  2. 185
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  3. 4
      src/models/Mdp.h
  4. 6
      src/storm.cpp
  5. 56
      src/utility/PrismUtility.h

58
src/adapters/ExplicitModelAdapter.h
View File

@ -88,62 +88,6 @@ namespace storm {
std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabeling; std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabeling;
}; };
static std::map<std::string, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<std::string, storm::expressions::Expression> constantDefinitions;
std::set<std::string> definedConstants;
if (!constantDefinitionString.empty()) {
// Parse the string that defines the undefined constants of the model and make sure that it contains exactly
// one value for each undefined constant of the model.
std::vector<std::string> definitions;
boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
for (auto& definition : definitions) {
boost::trim(definition);
// Check whether the token could be a legal constant definition.
uint_fast64_t positionOfAssignmentOperator = definition.find('=');
if (positionOfAssignmentOperator == std::string::npos) {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
}
// Now extract the variable name and the value from the string.
std::string constantName = definition.substr(0, positionOfAssignmentOperator);
boost::trim(constantName);
std::string value = definition.substr(positionOfAssignmentOperator + 1);
boost::trim(value);
// Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
if (program.hasConstant(constantName)) {
// Get the actual constant and check whether it's in fact undefined.
auto const& constant = program.getConstant(constantName);
LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(constantName);
if (constant.getType() == storm::expressions::ExpressionReturnType::Bool) {
if (value == "true") {
constantDefinitions[constantName] = storm::expressions::Expression::createTrue();
} else if (value == "false") {
constantDefinitions[constantName] = storm::expressions::Expression::createFalse();
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
}
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Int) {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[constantName] = storm::expressions::Expression::createIntegerLiteral(integerValue);
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Double) {
double doubleValue = std::stod(value);
constantDefinitions[constantName] = storm::expressions::Expression::createDoubleLiteral(doubleValue);
}
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
}
}
}
return constantDefinitions;
}
/*! /*!
* Convert the program given at construction time to an abstract model. The type of the model is the one * Convert the program given at construction time to an abstract model. The type of the model is the one
* specified in the program. The given reward model name selects the rewards that the model will contain. * specified in the program. The given reward model name selects the rewards that the model will contain.
@ -159,7 +103,7 @@ namespace storm {
static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
// Start by defining the undefined constants in the model. // Start by defining the undefined constants in the model.
// First, we need to parse the constant definition string. // First, we need to parse the constant definition string.
std::map<std::string, storm::expressions::Expression> constantDefinitions = parseConstantDefinitionString(program, constantDefinitionString); std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants."); LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");

185
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -20,6 +20,8 @@
#include "src/adapters/Z3ExpressionAdapter.h" #include "src/adapters/Z3ExpressionAdapter.h"
#endif #endif
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
#include "src/adapters/ExplicitModelAdapter.h" #include "src/adapters/ExplicitModelAdapter.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
@ -125,7 +127,7 @@ namespace storm {
for (auto const& entry : transitionMatrix.getRow(row)) { for (auto const& entry : transitionMatrix.getRow(row)) {
// If there is a relevant successor, we need to add the labels of the current choice. // If there is a relevant successor, we need to add the labels of the current choice.
if (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first)) { if (relevancyInformation.relevantStates.get(entry.getColumn()) || psiStates.get(entry.getColumn())) {
for (auto const& label : choiceLabeling[row]) { for (auto const& label : choiceLabeling[row]) {
relevancyInformation.relevantLabels.insert(label); relevancyInformation.relevantLabels.insert(label);
} }
@ -212,21 +214,21 @@ namespace storm {
for (auto const& entry : transitionMatrix.getRow(relevantChoice)) { for (auto const& entry : transitionMatrix.getRow(relevantChoice)) {
// If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition. // If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition.
if (state != entry.first && (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first))) { if (state != entry.getColumn() && (relevancyInformation.relevantStates.get(entry.getColumn()) || psiStates.get(entry.getColumn()))) {
// Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices // Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices
// targeting the same state. // targeting the same state.
if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.first)) != variableInformation.statePairToIndexMap.end()) { if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.getColumn())) != variableInformation.statePairToIndexMap.end()) {
continue; continue;
} }
// At this point we know that the state-pair does not have an associated variable. // At this point we know that the state-pair does not have an associated variable.
variableInformation.statePairToIndexMap[std::make_pair(state, entry.first)] = variableInformation.statePairVariables.size(); variableInformation.statePairToIndexMap[std::make_pair(state, entry.getColumn())] = variableInformation.statePairVariables.size();
// Clear contents of the stream to construct new expression name. // Clear contents of the stream to construct new expression name.
variableName.clear(); variableName.clear();
variableName.str(""); variableName.str("");
variableName << "t" << state << "_" << entry.first; variableName << "t" << state << "_" << entry.getColumn();
variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str())); variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str()));
} }
@ -258,7 +260,7 @@ namespace storm {
* @param solver The solver in which to assert the constraints. * @param solver The solver in which to assert the constraints.
* @param variableInformation A structure with information about the variables for the labels. * @param variableInformation A structure with information about the variables for the labels.
*/ */
static void assertFuMalikInitialConstraints(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { static void assertFuMalikInitialConstraints(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) {
// Assert that at least one of the labels must be taken. // Assert that at least one of the labels must be taken.
z3::expr formula = variableInformation.labelVariables.at(0); z3::expr formula = variableInformation.labelVariables.at(0);
for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) { for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) {
@ -316,11 +318,11 @@ namespace storm {
// Iterate over successors and add relevant choices of relevant successors to the following label set. // Iterate over successors and add relevant choices of relevant successors to the following label set.
bool canReachTargetState = false; bool canReachTargetState = false;
for (auto const& entry : transitionMatrix.getRow(currentChoice)) { for (auto const& entry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(entry.first)) { if (relevancyInformation.relevantStates.get(entry.getColumn())) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.first)) { for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.getColumn())) {
followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]); followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]);
} }
} else if (psiStates.get(entry.first)) { } else if (psiStates.get(entry.getColumn())) {
canReachTargetState = true; canReachTargetState = true;
} }
} }
@ -335,11 +337,11 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding // Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state. // label set of all labels of all relevant choices of the current state.
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.first)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) {
bool choiceTargetsCurrentState = false; bool choiceTargetsCurrentState = false;
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.first == currentState) { if (successorEntry.getColumn() == currentState) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
} }
} }
@ -554,8 +556,7 @@ namespace storm {
* @param context The Z3 context in which to build the expressions. * @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation. * @param solver The solver to use for the satisfiability evaluation.
*/ */
static void assertSymbolicCuts(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) { static void assertSymbolicCuts(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) {
// A container storing the label sets that may precede a given label set. // A container storing the label sets that may precede a given label set.
std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> precedingLabelSets; std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> precedingLabelSets;
@ -581,11 +582,11 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding // Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state. // label set of all labels of all relevant choices of the current state.
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.first)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) {
bool choiceTargetsCurrentState = false; bool choiceTargetsCurrentState = false;
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.first == currentState) { if (successorEntry.getColumn() == currentState) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
} }
} }
@ -599,45 +600,50 @@ namespace storm {
} }
} }
storm::utility::ir::VariableInformation programVariableInformation = storm::utility::ir::createVariableInformation(program);
// Create a context and register all variables of the program with their correct type. // Create a context and register all variables of the program with their correct type.
z3::context localContext; z3::context localContext;
z3::solver localSolver(localContext);
std::map<std::string, z3::expr> solverVariables; std::map<std::string, z3::expr> solverVariables;
for (auto const& booleanVariable : programVariableInformation.booleanVariables) { for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str())); solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str()));
} }
for (auto const& integerVariable : programVariableInformation.integerVariables) { for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str()));
} }
// Now create a corresponding local solver and assert all range bounds for the integer variables. for (auto const& module : program.getModules()) {
z3::solver localSolver(localContext); for (auto const& booleanVariable : module.getBooleanVariables()) {
solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str()));
}
for (auto const& integerVariable : module.getIntegerVariables()) {
solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str()));
}
}
storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, solverVariables); storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, solverVariables);
for (auto const& integerVariable : programVariableInformation.integerVariables) { // Then add the constraints for bounds of the integer variables..
z3::expr lowerBound = expressionAdapter.translateExpression(integerVariable.getLowerBound()); for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
z3::expr lowerBound = expressionAdapter.translateExpression(integerVariable.getLowerBoundExpression());
lowerBound = solverVariables.at(integerVariable.getName()) >= lowerBound; lowerBound = solverVariables.at(integerVariable.getName()) >= lowerBound;
localSolver.add(lowerBound); localSolver.add(lowerBound);
z3::expr upperBound = expressionAdapter.translateExpression(integerVariable.getUpperBoundExpression());
z3::expr upperBound = expressionAdapter.translateExpression(integerVariable.getUpperBound());
upperBound = solverVariables.at(integerVariable.getName()) <= upperBound; upperBound = solverVariables.at(integerVariable.getName()) <= upperBound;
localSolver.add(upperBound); localSolver.add(upperBound);
} }
for (auto const& module : program.getModules()) {
// Construct an expression that exactly characterizes the initial state. for (auto const& integerVariable : module.getIntegerVariables()) {
std::unique_ptr<storm::utility::ir::StateType> initialState(storm::utility::ir::getInitialState(program, programVariableInformation)); z3::expr lowerBound = expressionAdapter.translateExpression(integerVariable.getLowerBoundExpression());
z3::expr initialStateExpression = localContext.bool_val(true); lowerBound = solverVariables.at(integerVariable.getName()) >= lowerBound;
for (uint_fast64_t index = 0; index < programVariableInformation.booleanVariables.size(); ++index) { localSolver.add(lowerBound);
if (std::get<0>(*initialState).at(programVariableInformation.booleanVariableToIndexMap.at(programVariableInformation.booleanVariables[index].getName()))) { z3::expr upperBound = expressionAdapter.translateExpression(integerVariable.getUpperBoundExpression());
initialStateExpression = initialStateExpression && solverVariables.at(programVariableInformation.booleanVariables[index].getName()); upperBound = solverVariables.at(integerVariable.getName()) <= upperBound;
} else { localSolver.add(upperBound);
initialStateExpression = initialStateExpression && !solverVariables.at(programVariableInformation.booleanVariables[index].getName());
} }
} }
for (uint_fast64_t index = 0; index < programVariableInformation.integerVariables.size(); ++index) { // Construct an expression that exactly characterizes the initial state.
storm::ir::IntegerVariable const& variable = programVariableInformation.integerVariables[index]; storm::expressions::Expression initialStateExpression = program.getInitialConstruct().getInitialStatesExpression();
initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(static_cast<int>(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName())))));
}
// Store the found implications in a container similar to the preceding label sets. // Store the found implications in a container similar to the preceding label sets.
std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> backwardImplications; std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> backwardImplications;
@ -646,12 +652,12 @@ namespace storm {
for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) { for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) {
// Find out the commands for the currently considered label set. // Find out the commands for the currently considered label set.
std::vector<std::reference_wrapper<storm::ir::Command const>> currentCommandVector; std::vector<std::reference_wrapper<storm::prism::Command const>> currentCommandVector;
for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) {
storm::ir::Module const& module = program.getModule(moduleIndex); storm::prism::Module const& module = program.getModule(moduleIndex);
for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) { for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) {
storm::ir::Command const& command = module.getCommand(commandIndex); storm::prism::Command const& command = module.getCommand(commandIndex);
// If the current command is one of the commands we need to consider, store a reference to it in the container. // If the current command is one of the commands we need to consider, store a reference to it in the container.
if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) { if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) {
@ -665,9 +671,9 @@ namespace storm {
// Check if the command set is enabled in the initial state. // Check if the command set is enabled in the initial state.
for (auto const& command : currentCommandVector) { for (auto const& command : currentCommandVector) {
localSolver.add(expressionAdapter.translateExpression(command.get().getGuard())); localSolver.add(expressionAdapter.translateExpression(command.get().getGuardExpression()));
} }
localSolver.add(initialStateExpression); localSolver.add(expressionAdapter.translateExpression(initialStateExpression));
z3::check_result checkResult = localSolver.check(); z3::check_result checkResult = localSolver.check();
localSolver.pop(); localSolver.pop();
@ -676,19 +682,19 @@ namespace storm {
// If the solver reports unsat, then we know that the current selection is not enabled in the initial state. // If the solver reports unsat, then we know that the current selection is not enabled in the initial state.
if (checkResult == z3::unsat) { if (checkResult == z3::unsat) {
LOG4CPLUS_DEBUG(logger, "Selection not enabled in initial state."); LOG4CPLUS_DEBUG(logger, "Selection not enabled in initial state.");
std::unique_ptr<storm::ir::expressions::BaseExpression> guardConjunction; storm::expressions::Expression guardConjunction;
if (currentCommandVector.size() == 1) { if (currentCommandVector.size() == 1) {
guardConjunction = currentCommandVector.begin()->get().getGuard()->clone(); guardConjunction = currentCommandVector.begin()->get().getGuardExpression();
} else if (currentCommandVector.size() > 1) { } else if (currentCommandVector.size() > 1) {
std::vector<std::reference_wrapper<storm::ir::Command const>>::const_iterator setIterator = currentCommandVector.begin(); std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator setIterator = currentCommandVector.begin();
std::unique_ptr<storm::ir::expressions::BaseExpression> first = setIterator->get().getGuard()->clone(); storm::expressions::Expression first = setIterator->get().getGuardExpression();
++setIterator; ++setIterator;
std::unique_ptr<storm::ir::expressions::BaseExpression> second = setIterator->get().getGuard()->clone(); storm::expressions::Expression second = setIterator->get().getGuardExpression();
guardConjunction = std::unique_ptr<storm::ir::expressions::BaseExpression>(new storm::ir::expressions::BinaryBooleanFunctionExpression(std::move(first), std::move(second), storm::ir::expressions::BinaryBooleanFunctionExpression::AND)); guardConjunction = first && second;
++setIterator; ++setIterator;
while (setIterator != currentCommandVector.end()) { while (setIterator != currentCommandVector.end()) {
guardConjunction = std::unique_ptr<storm::ir::expressions::BaseExpression>(new storm::ir::expressions::BinaryBooleanFunctionExpression(std::move(guardConjunction), setIterator->get().getGuard()->clone(), storm::ir::expressions::BinaryBooleanFunctionExpression::AND)); guardConjunction = guardConjunction && setIterator->get().getGuardExpression();
++setIterator; ++setIterator;
} }
} else { } else {
@ -701,9 +707,9 @@ namespace storm {
bool firstAssignment = true; bool firstAssignment = true;
for (auto const& command : currentCommandVector) { for (auto const& command : currentCommandVector) {
if (firstAssignment) { if (firstAssignment) {
guardExpression = !expressionAdapter.translateExpression(command.get().getGuard()); guardExpression = !expressionAdapter.translateExpression(command.get().getGuardExpression());
} else { } else {
guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuard()); guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuardExpression());
} }
} }
localSolver.add(guardExpression); localSolver.add(guardExpression);
@ -715,12 +721,12 @@ namespace storm {
localSolver.push(); localSolver.push();
// Find out the commands for the currently considered preceding label set. // Find out the commands for the currently considered preceding label set.
std::vector<std::reference_wrapper<storm::ir::Command const>> currentPrecedingCommandVector; std::vector<std::reference_wrapper<storm::prism::Command const>> currentPrecedingCommandVector;
for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) {
storm::ir::Module const& module = program.getModule(moduleIndex); storm::prism::Module const& module = program.getModule(moduleIndex);
for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) { for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) {
storm::ir::Command const& command = module.getCommand(commandIndex); storm::prism::Command const& command = module.getCommand(commandIndex);
// If the current command is one of the commands we need to consider, store a reference to it in the container. // If the current command is one of the commands we need to consider, store a reference to it in the container.
if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) { if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) {
@ -731,10 +737,10 @@ namespace storm {
// Assert all the guards of the preceding command set. // Assert all the guards of the preceding command set.
for (auto const& command : currentPrecedingCommandVector) { for (auto const& command : currentPrecedingCommandVector) {
localSolver.add(expressionAdapter.translateExpression(command.get().getGuard())); localSolver.add(expressionAdapter.translateExpression(command.get().getGuardExpression()));
} }
std::vector<std::vector<storm::ir::Update>::const_iterator> iteratorVector; std::vector<std::vector<storm::prism::Update>::const_iterator> iteratorVector;
for (auto const& command : currentPrecedingCommandVector) { for (auto const& command : currentPrecedingCommandVector) {
iteratorVector.push_back(command.get().getUpdates().begin()); iteratorVector.push_back(command.get().getUpdates().begin());
} }
@ -743,13 +749,15 @@ namespace storm {
std::vector<z3::expr> formulae; std::vector<z3::expr> formulae;
bool done = false; bool done = false;
while (!done) { while (!done) {
std::vector<std::reference_wrapper<storm::ir::Update const>> currentUpdateCombination; std::map<std::string, storm::expressions::Expression> currentUpdateCombinationMap;
for (auto const& updateIterator : iteratorVector) { for (auto const& updateIterator : iteratorVector) {
currentUpdateCombination.push_back(*updateIterator); for (auto const& assignment : updateIterator->getAssignments()) {
currentUpdateCombinationMap.emplace(assignment.getVariableName(), assignment.getExpression());
}
} }
LOG4CPLUS_DEBUG(logger, "About to assert a weakest precondition."); LOG4CPLUS_DEBUG(logger, "About to assert a weakest precondition.");
std::unique_ptr<storm::ir::expressions::BaseExpression> wp = storm::utility::ir::getWeakestPrecondition(guardConjunction->clone(), currentUpdateCombination); storm::expressions::Expression wp = guardConjunction.substitute(currentUpdateCombinationMap);
formulae.push_back(expressionAdapter.translateExpression(wp)); formulae.push_back(expressionAdapter.translateExpression(wp));
LOG4CPLUS_DEBUG(logger, "Asserted weakest precondition."); LOG4CPLUS_DEBUG(logger, "Asserted weakest precondition.");
@ -913,16 +921,16 @@ namespace storm {
// Assert the constraints (1). // Assert the constraints (1).
boost::container::flat_set<uint_fast64_t> relevantPredecessors; boost::container::flat_set<uint_fast64_t> relevantPredecessors;
for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) {
if (relevantState != predecessorEntry.first && relevancyInformation.relevantStates.get(predecessorEntry.first)) { if (relevantState != predecessorEntry.getColumn() && relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) {
relevantPredecessors.insert(predecessorEntry.first); relevantPredecessors.insert(predecessorEntry.getColumn());
} }
} }
boost::container::flat_set<uint_fast64_t> relevantSuccessors; boost::container::flat_set<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { if (relevantState != successorEntry.getColumn() && (relevancyInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn()))) {
relevantSuccessors.insert(successorEntry.first); relevantSuccessors.insert(successorEntry.getColumn());
} }
} }
} }
@ -941,8 +949,8 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> relevantSuccessors; boost::container::flat_set<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { if (relevantState != successorEntry.getColumn() && (relevancyInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn()))) {
relevantSuccessors.insert(successorEntry.first); relevantSuccessors.insert(successorEntry.getColumn());
} }
} }
} }
@ -965,7 +973,7 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> choicesForStatePair; boost::container::flat_set<uint_fast64_t> choicesForStatePair;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (successorEntry.first == targetState) { if (successorEntry.getColumn() == targetState) {
choicesForStatePair.insert(relevantChoice); choicesForStatePair.insert(relevantChoice);
} }
} }
@ -1400,13 +1408,13 @@ namespace storm {
bool choiceTargetsRelevantState = false; bool choiceTargetsRelevantState = false;
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) { if (relevancyInformation.relevantStates.get(successorEntry.getColumn()) && currentState != successorEntry.getColumn()) {
choiceTargetsRelevantState = true; choiceTargetsRelevantState = true;
if (!reachableStates.get(successorEntry.first)) { if (!reachableStates.get(successorEntry.getColumn())) {
reachableStates.set(successorEntry.first); reachableStates.set(successorEntry.getColumn());
stack.push_back(successorEntry.first); stack.push_back(successorEntry.getColumn());
} }
} else if (psiStates.get(successorEntry.first)) { } else if (psiStates.get(successorEntry.getColumn())) {
targetStateIsReachable = true; targetStateIsReachable = true;
} }
} }
@ -1446,7 +1454,7 @@ namespace storm {
// Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states.
for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) { for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) {
if (unreachableRelevantStates.get(successorEntry.first)) { if (unreachableRelevantStates.get(successorEntry.getColumn())) {
isBorderChoice = true; isBorderChoice = true;
} }
} }
@ -1529,13 +1537,13 @@ namespace storm {
bool choiceTargetsRelevantState = false; bool choiceTargetsRelevantState = false;
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) { if (relevancyInformation.relevantStates.get(successorEntry.getColumn()) && currentState != successorEntry.getColumn()) {
choiceTargetsRelevantState = true; choiceTargetsRelevantState = true;
if (!reachableStates.get(successorEntry.first)) { if (!reachableStates.get(successorEntry.getColumn())) {
reachableStates.set(successorEntry.first, true); reachableStates.set(successorEntry.getColumn(), true);
stack.push_back(successorEntry.first); stack.push_back(successorEntry.getColumn());
} }
} else if (psiStates.get(successorEntry.first)) { } else if (psiStates.get(successorEntry.getColumn())) {
targetStateIsReachable = true; targetStateIsReachable = true;
} }
} }
@ -1613,7 +1621,7 @@ namespace storm {
* @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check
* is made and fails, an exception is thrown. * is made and fails, an exception is thrown.
*/ */
static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
// Set up all clocks used for time measurement. // Set up all clocks used for time measurement.
auto totalClock = std::chrono::high_resolution_clock::now(); auto totalClock = std::chrono::high_resolution_clock::now();
@ -1632,7 +1640,9 @@ namespace storm {
auto analysisClock = std::chrono::high_resolution_clock::now(); auto analysisClock = std::chrono::high_resolution_clock::now();
decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0); decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0);
storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString); std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
preparedProgram = preparedProgram.substituteConstants();
// (0) Check whether the MDP is indeed labeled. // (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabeling()) { if (!labeledMdp.hasChoiceLabeling()) {
@ -1676,7 +1686,7 @@ namespace storm {
LOG4CPLUS_DEBUG(logger, "Asserting cuts."); LOG4CPLUS_DEBUG(logger, "Asserting cuts.");
assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver); assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver);
LOG4CPLUS_DEBUG(logger, "Asserted explicit cuts."); LOG4CPLUS_DEBUG(logger, "Asserted explicit cuts.");
assertSymbolicCuts(program, labeledMdp, variableInformation, relevancyInformation, context, solver); assertSymbolicCuts(preparedProgram, labeledMdp, variableInformation, relevancyInformation, context, solver);
LOG4CPLUS_DEBUG(logger, "Asserted symbolic cuts."); LOG4CPLUS_DEBUG(logger, "Asserted symbolic cuts.");
if (includeReachabilityEncoding) { if (includeReachabilityEncoding) {
assertReachabilityCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver); assertReachabilityCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver);
@ -1764,8 +1774,6 @@ namespace storm {
std::cout << " * number of models that could not reach a target state: " << zeroProbabilityCount << " (" << 100 * static_cast<double>(zeroProbabilityCount)/iterations << "%)" << std::endl << std::endl; std::cout << " * number of models that could not reach a target state: " << zeroProbabilityCount << " (" << 100 * static_cast<double>(zeroProbabilityCount)/iterations << "%)" << std::endl << std::endl;
} }
// (9) Return the resulting command set after undefining the constants.
storm::utility::ir::undefineUndefinedConstants(program);
return commandSet; return commandSet;
#else #else
@ -1773,7 +1781,7 @@ namespace storm {
#endif #endif
} }
static void computeCounterexample(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) { static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl; std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
// First, we need to check whether the current formula is an Until-Formula. // First, we need to check whether the current formula is an Until-Formula.
@ -1821,9 +1829,8 @@ namespace storm {
std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl; std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
std::cout << "Resulting program:" << std::endl << std::endl; std::cout << "Resulting program:" << std::endl << std::endl;
storm::ir::Program restrictedProgram(program); storm::prism::Program restrictedProgram = program.restrictCommands(labelSet);
restrictedProgram.restrictCommands(labelSet); std::cout << restrictedProgram << std::endl;
std::cout << restrictedProgram.toString() << std::endl;
std::cout << std::endl << "-------------------------------------------" << std::endl; std::cout << std::endl << "-------------------------------------------" << std::endl;
#else #else

4
src/models/Mdp.h
View File

@ -139,7 +139,7 @@ public:
std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling(); std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder; storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, 0, 0, true);
std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling; std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling;
// Check for each choice of each state, whether the choice labels are fully contained in the given label set. // Check for each choice of each state, whether the choice labels are fully contained in the given label set.
@ -156,7 +156,7 @@ public:
} }
stateHasValidChoice = true; stateHasValidChoice = true;
for (auto const& entry : this->getTransitionMatrix().getRow(choice)) { for (auto const& entry : this->getTransitionMatrix().getRow(choice)) {
transitionMatrixBuilder.addNextValue(currentRow, entry.first, entry.second); transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue());
} }
newChoiceLabeling.emplace_back(choiceLabeling[choice]); newChoiceLabeling.emplace_back(choiceLabeling[choice]);
++currentRow; ++currentRow;

6
src/storm.cpp
View File

@ -35,7 +35,7 @@
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/solver/GurobiLpSolver.h" #include "src/solver/GurobiLpSolver.h"
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
// #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
#include "src/counterexamples/PathBasedSubsystemGenerator.h" #include "src/counterexamples/PathBasedSubsystemGenerator.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/parser/MarkovAutomatonParser.h" #include "src/parser/MarkovAutomatonParser.h"
@ -587,7 +587,7 @@ int main(const int argc, const char* argv[]) {
if (useMILP) { if (useMILP) {
storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr); storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr);
} else { } else {
// storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr); storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
} }
// Once we are done with the formula, delete it. // Once we are done with the formula, delete it.
@ -596,7 +596,7 @@ int main(const int argc, const char* argv[]) {
// MinCMD Time Measurement, End // MinCMD Time Measurement, End
std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point minCmdEnd = std::chrono::high_resolution_clock::now();
std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast<std::chrono::milliseconds>(minCmdStart - minCmdEnd).count() << " milliseconds." << std::endl; std::cout << "Minimal command Counterexample generation took " << std::chrono::duration_cast<std::chrono::milliseconds>(minCmdEnd - minCmdStart).count() << " milliseconds." << std::endl;
} else if (s->isSet("prctl")) { } else if (s->isSet("prctl")) {
// Depending on the model type, the appropriate model checking procedure is chosen. // Depending on the model type, the appropriate model checking procedure is chosen.
storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr; storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;

56
src/utility/PrismUtility.h
View File

@ -188,6 +188,62 @@ namespace storm {
auto& labeledEntry = choice.getOrAddEntry(state); auto& labeledEntry = choice.getOrAddEntry(state);
labeledEntry.addValue(probability, labels); labeledEntry.addValue(probability, labels);
} }
static std::map<std::string, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<std::string, storm::expressions::Expression> constantDefinitions;
std::set<std::string> definedConstants;
if (!constantDefinitionString.empty()) {
// Parse the string that defines the undefined constants of the model and make sure that it contains exactly
// one value for each undefined constant of the model.
std::vector<std::string> definitions;
boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
for (auto& definition : definitions) {
boost::trim(definition);
// Check whether the token could be a legal constant definition.
uint_fast64_t positionOfAssignmentOperator = definition.find('=');
if (positionOfAssignmentOperator == std::string::npos) {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
}
// Now extract the variable name and the value from the string.
std::string constantName = definition.substr(0, positionOfAssignmentOperator);
boost::trim(constantName);
std::string value = definition.substr(positionOfAssignmentOperator + 1);
boost::trim(value);
// Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
if (program.hasConstant(constantName)) {
// Get the actual constant and check whether it's in fact undefined.
auto const& constant = program.getConstant(constantName);
LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(constantName);
if (constant.getType() == storm::expressions::ExpressionReturnType::Bool) {
if (value == "true") {
constantDefinitions[constantName] = storm::expressions::Expression::createTrue();
} else if (value == "false") {
constantDefinitions[constantName] = storm::expressions::Expression::createFalse();
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
}
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Int) {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[constantName] = storm::expressions::Expression::createIntegerLiteral(integerValue);
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Double) {
double doubleValue = std::stod(value);
constantDefinitions[constantName] = storm::expressions::Expression::createDoubleLiteral(doubleValue);
}
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
}
}
}
return constantDefinitions;
}
} // namespace prism } // namespace prism
} // namespace utility } // namespace utility
} // namespace storm } // namespace storm

Write Preview
|||||||
100:0
Loading…
Cancel
Save