diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 211baa2f1..fa89f12a8 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -58,7 +58,7 @@ namespace storm { stack.push(leftResult || rightResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; + << "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; } } @@ -85,8 +85,14 @@ namespace storm { case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE: stack.push(leftResult / rightResult); break; + case storm::ir::expressions::BinaryNumericalFunctionExpression::MIN: + stack.push(ite(leftResult <= rightResult, leftResult, rightResult)); + break; + case storm::ir::expressions::BinaryNumericalFunctionExpression::MAX: + stack.push(ite(leftResult >= rightResult, leftResult, rightResult)); + break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; + << "Unknown numerical binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; } } @@ -119,7 +125,7 @@ namespace storm { stack.push(leftResult >= rightResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getRelationType() << "'."; + << "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression->toString() << "."; } } @@ -177,7 +183,7 @@ namespace storm { stack.push(!childResult); break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean unary operator: '" << expression->getFunctionType() << "'."; + << "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << "."; } } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index b9ccb04c0..7b83b53a4 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -49,7 +49,7 @@ namespace storm { std::set knownLabels; // A list of relevant choices for each relevant state. - std::unordered_map> relevantChoicesForRelevantStates; + std::map> relevantChoicesForRelevantStates; }; struct VariableInformation { @@ -253,10 +253,12 @@ namespace storm { targetLabels.insert(label); } } - - // 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. - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + } + + // 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. + for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + if (relevancyInformation.relevantStates.get(*predecessorIt)) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) { bool choiceTargetsCurrentState = false; for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) { @@ -266,9 +268,11 @@ namespace storm { } if (choiceTargetsCurrentState) { - for (auto labelToAdd : choiceLabeling[predecessorChoice]) { - for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { - precedingLabels[labelForWhichToAdd].insert(labelToAdd); + for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { + for (auto labelToAdd : choiceLabeling[predecessorChoice]) { + for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { + precedingLabels[labelForWhichToAdd].insert(labelToAdd); + } } } } @@ -277,8 +281,11 @@ namespace storm { } } + LOG4CPLUS_DEBUG(logger, "Successfully gathered data for explicit cuts."); + std::vector formulae; + LOG4CPLUS_DEBUG(logger, "Asserting initial label is taken."); // Start by asserting that we take at least one initial label. We may do so only if there is no initial // label that is already known. Otherwise this condition would be too strong. std::set intersection; @@ -294,6 +301,7 @@ namespace storm { intersection.clear(); } + LOG4CPLUS_DEBUG(logger, "Asserting target label is taken."); // Likewise, if no target label is known, we may assert that there is at least one. std::set_intersection(targetLabels.begin(), targetLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(intersection, intersection.begin())); if (intersection.empty()) { @@ -306,6 +314,7 @@ namespace storm { intersection.clear(); } + LOG4CPLUS_DEBUG(logger, "Asserting taken labels are followed by another label if they are not a target label."); // Now assert that for each non-target label, we take a following label. for (auto const& labelSetPair : followingLabels) { formulae.clear(); @@ -330,21 +339,38 @@ namespace storm { } } + LOG4CPLUS_DEBUG(logger, "Asserting synchronization cuts."); // Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations // the label appears in. for (auto const& labelSynchronizingSetsPair : synchronizingLabels) { formulae.clear(); - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first))); + if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first))); + } + // We need to be careful, because there may be one synchronisation set out of which all labels are + // known, which means we must not assert anything. + bool allImplicantsKnownForOneSet = false; for (auto const& synchronizingSet : labelSynchronizingSetsPair.second) { z3::expr currentCombination = context.bool_val(true); + bool allImplicantsKnownForCurrentSet = true; for (auto label : synchronizingSet) { - currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { + currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + } } formulae.push_back(currentCombination); + + // If all implicants of the current set are known, we do not need to further build the constraint. + if (allImplicantsKnownForCurrentSet) { + allImplicantsKnownForOneSet = true; + break; + } } - assertDisjunction(context, solver, formulae); + if (!allImplicantsKnownForOneSet) { + assertDisjunction(context, solver, formulae); + } } } @@ -371,23 +397,25 @@ namespace storm { // 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. for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) { - bool choiceTargetsCurrentState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) { - if (*successorIt == currentState) { - choiceTargetsCurrentState = true; - } - } - - if (choiceTargetsCurrentState) { - if (choiceLabeling.at(predecessorChoice).size() > 1) { - for (auto label : choiceLabeling.at(currentChoice)) { - hasSynchronizingPredecessor.insert(label); + if (relevancyInformation.relevantStates.get(*predecessorIt)) { + for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) { + bool choiceTargetsCurrentState = false; + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) { + if (*successorIt == currentState) { + choiceTargetsCurrentState = true; } } - for (auto labelToAdd : choiceLabeling[predecessorChoice]) { - for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { - precedingLabels[labelForWhichToAdd].insert(labelToAdd); + + if (choiceTargetsCurrentState) { + if (choiceLabeling.at(predecessorChoice).size() > 1) { + for (auto label : choiceLabeling.at(currentChoice)) { + hasSynchronizingPredecessor.insert(label); + } + } + for (auto labelToAdd : choiceLabeling[predecessorChoice]) { + for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { + precedingLabels[labelForWhichToAdd].insert(labelToAdd); + } } } } @@ -396,9 +424,6 @@ namespace storm { } } - // FIXME: The following procedure to assert backward cuts is not correct in the presence of synchronizing - // actions, because it may be the case that several synchronizing commands are necessary to enable another - // command and not just one. storm::utility::ir::VariableInformation programVariableInformation = storm::utility::ir::createVariableInformation(program); // Create a context and register all variables of the program with their correct type. @@ -451,6 +476,10 @@ namespace storm { // If the label of the command is not relevant, skip it entirely. if (relevancyInformation.relevantLabels.find(command.getGlobalIndex()) == relevancyInformation.relevantLabels.end()) continue; + // If the label has a synchronizing predecessor, we also need to skip it, because the following + // procedure can only consider predecessors in isolation. + if(hasSynchronizingPredecessor.find(command.getGlobalIndex()) != hasSynchronizingPredecessor.end()) continue; + // Save the state of the solver so we can easily backtrack. localSolver.push(); @@ -926,6 +955,7 @@ namespace storm { static std::set getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false) { #ifdef STORM_HAVE_Z3 auto startTime = std::chrono::high_resolution_clock::now(); + auto endTime = std::chrono::high_resolution_clock::now(); storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString); @@ -965,6 +995,7 @@ namespace storm { variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(context, solver, variableInformation.adderVariables, 0)); // (7) Add constraints that cut off a lot of suboptimal solutions. + LOG4CPLUS_DEBUG(logger, "Asserting cuts."); assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver); LOG4CPLUS_DEBUG(logger, "Asserted explicit cuts."); assertSymbolicCuts(program, labeledMdp, variableInformation, relevancyInformation, context, solver); @@ -981,10 +1012,11 @@ namespace storm { uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; maximalReachabilityProbability = 0; + auto iterationTimer = std::chrono::high_resolution_clock::now(); do { LOG4CPLUS_DEBUG(logger, "Computing minimal command set."); commandSet = findSmallestCommandSet(context, solver, variableInformation, currentBound); - LOG4CPLUS_DEBUG(logger, "Computed minimal command set of size " << commandSet.size() << "."); + LOG4CPLUS_DEBUG(logger, "Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); // Restrict the given MDP to the current set of labels and compute the reachability probability. commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); @@ -1006,14 +1038,20 @@ namespace storm { done = true; } ++iterations; + + endTime = std::chrono::high_resolution_clock::now(); + if (std::chrono::duration_cast(endTime - iterationTimer).count() > 5) { + std::cout << "Performed " << iterations << " iterations in " << std::chrono::duration_cast(endTime - startTime).count() << "s. Current command set size is " << commandSet.size() << "." << std::endl; + iterationTimer = std::chrono::high_resolution_clock::now(); + } } while (!done); LOG4CPLUS_INFO(logger, "Found minimal label set after " << iterations << " iterations."); // (9) Return the resulting command set after undefining the constants. storm::utility::ir::undefineUndefinedConstants(program); - auto endTime = std::chrono::high_resolution_clock::now(); - LOG4CPLUS_WARN(logger, "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms."); + endTime = std::chrono::high_resolution_clock::now(); + std::cout << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms (" << iterations << " iterations)." << std::endl; return commandSet; diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 9898c5187..8437e6ad3 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -27,7 +27,7 @@ namespace storm { : actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)), globalIndex(newGlobalIndex) { auto renamingPair = renaming.find(this->actionName); if (renamingPair != renaming.end()) { - this->actionName = renamingPair->first; + this->actionName = renamingPair->second; } this->updates.reserve(oldCommand.getNumberOfUpdates()); for (Update const& update : oldCommand.updates) { diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp index d49e7f9ee..c7340a891 100644 --- a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp +++ b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp @@ -19,9 +19,15 @@ namespace storm { [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]; constantIntegerMultExpression.name("constant integer expression"); - constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); constantAtomicIntegerExpression.name("constant integer expression"); + constantIntegerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(",") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; + constantIntegerMinMaxExpression.name("integer min/max expression"); + + constantIntegerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)]; + constantIntegerFloorCeilExpression.name("integer floor/ceil expression"); + integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); integerConstantExpression.name("integer constant or literal"); diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.h b/src/parser/prismparser/ConstIntegerExpressionGrammar.h index a75654391..2b6a08cae 100644 --- a/src/parser/prismparser/ConstIntegerExpressionGrammar.h +++ b/src/parser/prismparser/ConstIntegerExpressionGrammar.h @@ -30,6 +30,8 @@ namespace storm { qi::rule(), Skipper> constantAtomicIntegerExpression; qi::rule(), Skipper> integerConstantExpression; qi::rule(), Skipper> integerLiteralExpression; + qi::rule(), qi::locals, Skipper> constantIntegerMinMaxExpression; + qi::rule(), qi::locals, Skipper> constantIntegerFloorCeilExpression; }; diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 4ab8fae58..220663a99 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -245,7 +245,7 @@ namespace storm { // This block defines all entities that are needed for parsing a program. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); - start = ( + start = (qi::eps > modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > globalVariableDefinitionList(qi::_d) > diff --git a/src/storm.cpp b/src/storm.cpp index 6005961f1..79e0d4d11 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -355,14 +355,26 @@ int main(const int argc, const char* argv[]) { // Enable the following lines to test the SMTMinimalCommandSetGenerator. if (model->getType() == storm::models::MDP) { std::shared_ptr> labeledMdp = model->as>(); - 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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true); -// storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff"); -// storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered"); -// std::set labels = storm::counterexamples::MILPMinimalLabelSetGenerator::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, true); + // Build stuff for coin example. +// 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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true); + + // Build stuff for csma example. + storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff"); + storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered"); + std::set labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, ~collisionStates, deliveredStates, 0.5, true); + + // Build stuff for firewire example. +// storm::storage::BitVector const& electedStates = labeledMdp->getLabeledStates("elected"); +// std::set labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), electedStates, 0.01, true); + + // Build stuff for wlan example. +// storm::storage::BitVector const& oneCollisionStates = labeledMdp->getLabeledStates("oneCollision"); +// storm::storage::BitVector const& twoCollisionStates = labeledMdp->getLabeledStates("twoCollisions"); +// std::set labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), twoCollisionStates, 0.1, true); } }