diff --git a/src/counterexamples/CounterexampleOptions.cpp b/src/counterexamples/CounterexampleOptions.cpp index eb9c1c25c..b6e8a4829 100644 --- a/src/counterexamples/CounterexampleOptions.cpp +++ b/src/counterexamples/CounterexampleOptions.cpp @@ -7,5 +7,6 @@ bool CounterexampleOptionsRegistered = storm::settings::Settings::registerNewMod instance->addOption(storm::settings::OptionBuilder("Counterexample", "mincmd", "", "Computes a counterexample for the given symbolic model in terms of a minimal command set.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("propertyFile", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Must be either \"milp\" or \"sat\".").setDefaultValueString("sat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); instance->addOption(storm::settings::OptionBuilder("Counterexample", "stats", "s", "Sets whether to display statistics for certain functionalities.").build()); instance->addOption(storm::settings::OptionBuilder("Counterexample", "encreach", "", "Sets whether to encode reachability for SAT-based minimal command counterexample generation.").build()); + instance->addOption(storm::settings::OptionBuilder("Counterexample", "schedcuts", "", "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); return true; }); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 6fff846aa..9f0fb3ef0 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -97,7 +97,7 @@ namespace storm { result.problematicStates &= result.relevantStates; LOG4CPLUS_DEBUG(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states."); LOG4CPLUS_DEBUG(logger, "Found " << psiStates.getNumberOfSetBits() << " target states."); - LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states ."); + LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states."); LOG4CPLUS_DEBUG(logger, "Found " << result.problematicStates.getNumberOfSetBits() << " problematic states."); return result; } @@ -407,7 +407,9 @@ namespace storm { result.numberOfVariables += problematicTransitionVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the problematic choices."); - LOG4CPLUS_INFO(logger, "Successfully created " << result.numberOfVariables << " Gurobi variables."); + // Finally, we need to update the model to make the new variables usable. + solver.update(); + LOG4CPLUS_INFO(logger, "Successfully created " << result.numberOfVariables << " MILP variables."); // Finally, return variable information struct. return result; @@ -879,7 +881,7 @@ namespace storm { LOG4CPLUS_DEBUG(logger, "Asserted scheduler cuts."); } - LOG4CPLUS_INFO(logger, "Successfully created " << numberOfConstraints << " Gurobi constraints."); + LOG4CPLUS_INFO(logger, "Successfully created " << numberOfConstraints << " MILP constraints."); } /*! @@ -929,7 +931,7 @@ namespace storm { } /*! - * Computes the reachability probability and the selected initial state in the given optimized Gurobi model. + * Computes the reachability probability and the selected initial state in the given optimized MILP model. * * @param solver The MILP solver. * @param labeledMdp The labeled MDP. @@ -959,13 +961,16 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; - for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } - if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; + if (checkThresholdFeasible) { + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; + for (auto state : labeledMdp.getInitialStates()) { + maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); + } + if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { + throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; + } + std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl; } // (2) Identify relevant and problematic states. @@ -1044,7 +1049,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true); + boost::container::flat_set usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::Settings::getInstance()->isSet("schedcuts")); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 136045173..f95bc2806 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1428,8 +1428,11 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), subMdp.getBackwardTransitions(), phiStates, psiStates); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels); + boost::container::flat_set locallyRelevantLabels; + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); + + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantLabels); LOG4CPLUS_DEBUG(logger, "Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable @@ -1548,7 +1551,11 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), subMdp.getBackwardTransitions(), phiStates, psiStates); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels); + + boost::container::flat_set locallyRelevantLabels; + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); + + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); @@ -1565,7 +1572,6 @@ namespace storm { std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); cutLabels.insert(currentLabelSet); - } } } @@ -1635,13 +1641,16 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; - for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } - if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; + if (checkThresholdFeasible) { + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; + for (auto state : labeledMdp.getInitialStates()) { + maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); + } + if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { + throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; + } + std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. @@ -1706,7 +1715,7 @@ namespace storm { std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; - + // Now determine the maximal reachability probability by checking all initial states. maximalReachabilityProbability = 0; for (auto state : labeledMdp.getInitialStates()) { diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 213cca81f..156930b3b 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -436,6 +436,7 @@ namespace storm { stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0); } uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1); + solver->update(); // Now we encode the problem as constraints. std::vector variables; diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index f7bed4476..e343526f2 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -95,6 +95,10 @@ namespace storm { return index; } + void GlpkLpSolver::update() const { + // Intentionally left empty. + } + void GlpkLpSolver::addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) { if (variables.size() != coefficients.size()) { LOG4CPLUS_ERROR(logger, "Sizes of variable indices vector and coefficients vector do not match."); diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h index 41ddeeb8c..2bc2bf397 100644 --- a/src/solver/GlpkLpSolver.h +++ b/src/solver/GlpkLpSolver.h @@ -59,6 +59,7 @@ namespace storm { virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override; + virtual void update() const override; virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override; @@ -132,6 +133,10 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } + virtual void update() const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index 4dfa8f89c..a471781a8 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -71,7 +71,7 @@ namespace storm { error = GRBsetdblparam(env, "IntFeasTol", storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()); } - void GurobiLpSolver::updateModel() const { + void GurobiLpSolver::update() const { int error = GRBupdatemodel(model); if (error) { LOG4CPLUS_ERROR(logger, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ")."); @@ -104,7 +104,6 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ")."; } ++nextVariableIndex; - this->updateModel(); return nextVariableIndex - 1; } @@ -130,7 +129,6 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ")."; } ++nextVariableIndex; - this->updateModel(); return nextVariableIndex - 1; } @@ -141,7 +139,6 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ")."; } ++nextVariableIndex; - this->updateModel(); return nextVariableIndex - 1; } @@ -176,13 +173,11 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Unable to assert Gurobi constraint (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Unable to assert Gurobi constraint (" << GRBgeterrormsg(env) << ")."; } - - this->updateModel(); } void GurobiLpSolver::optimize() const { // First incorporate all recent changes. - this->updateModel(); + this->update(); // Set the most recently set model sense. int error = GRBsetintattr(model, "ModelSense", this->getModelSense() == MINIMIZE ? 1 : -1); @@ -318,9 +313,9 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ")."; } - if (std::abs(value - static_cast(value)) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + if (std::abs(value - static_cast(value)) <= storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()) { // Nothing to do in this case. - } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()) { LOG4CPLUS_ERROR(logger, "Illegal value for integer variable in Gurobi solution (" << value << ")."); throw storm::exceptions::InvalidStateException() << "Illegal value for integer variable in Gurobi solution (" << value << ")."; } @@ -349,9 +344,9 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ")."; } - if (std::abs(value - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + if (std::abs(value - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()) { // Nothing to do in this case. - } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble()) { LOG4CPLUS_ERROR(logger, "Illegal value for binary variable in Gurobi solution (" << value << ")."); throw storm::exceptions::InvalidStateException() << "Illegal value for binary variable in Gurobi solution (" << value << ")."; } diff --git a/src/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index 2057ffed2..18c5bbdbd 100644 --- a/src/solver/GurobiLpSolver.h +++ b/src/solver/GurobiLpSolver.h @@ -63,7 +63,8 @@ namespace storm { virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override; - + virtual void update() const override; + virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override; virtual void optimize() const override; @@ -84,11 +85,6 @@ namespace storm { */ void setGurobiEnvironmentProperties() const; - /*! - * Calls Gurobi to incorporate the latest changes to the model. - */ - void updateModel() const; - // The Gurobi environment. GRBenv* env; @@ -130,6 +126,10 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } + virtual void update() const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index f827f7462..50488cafb 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -101,6 +101,12 @@ namespace storm { */ virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) = 0; + /*! + * Updates the model to make the variables that have been declared since the last call to update + * usable. + */ + virtual void update() const = 0; + /*! * Adds a constraint of the form * a_1*x_1 + ... + a_n*x_n op c diff --git a/src/storm.cpp b/src/storm.cpp index 88ecafad4..6614172b5 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -69,8 +69,10 @@ void printUsage() { struct rusage ru; getrusage(RUSAGE_SELF, &ru); - std::cout << "Memory Usage: " << ru.ru_maxrss << "kB" << std::endl; - std::cout << "CPU Time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "===== Statistics ==============================" << std::endl; + std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; + std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "===============================================" << std::endl; #else HANDLE hProcess = GetCurrentProcess (); FILETIME ftCreation, ftExit, ftUser, ftKernel; @@ -559,6 +561,7 @@ int main(const int argc, const char* argv[]) { // Perform clean-up and terminate. cleanUp(); + printUsage(); LOG4CPLUS_INFO(logger, "StoRM terminating."); return 0; } catch (std::exception& e) { diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h index 2e1a22bdc..4c87f4d0a 100644 --- a/src/utility/ErrorHandling.h +++ b/src/utility/ErrorHandling.h @@ -80,6 +80,8 @@ std::string demangle(char const* symbol) { return symbol; } +void printUsage(); + /* * Handles the given signal. This will display the received signal and a backtrace. * @@ -87,7 +89,7 @@ std::string demangle(char const* symbol) { */ void signalHandler(int sig) { LOG4CPLUS_FATAL(logger, "The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal."); - + printUsage(); #ifndef WINDOWS # define SIZE 128 void *buffer[SIZE]; @@ -120,6 +122,9 @@ void signalHandler(int sig) { */ void installSignalHandler() { signal(SIGSEGV, signalHandler); + signal(SIGABRT, signalHandler); + signal(SIGINT, signalHandler); + signal(SIGTERM, signalHandler); } #endif /* ERRORHANDLING_H */ diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index d35828a62..23b5b372e 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -30,36 +30,94 @@ namespace storm { // Now we compute the set of labels that is present on all paths from the initial to the target states. std::vector> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels); - std::queue> worklist; +// std::queue> worklist; +// +// // Initially, put all predecessors of target states in the worklist and empty the analysis information them. +// for (auto state : psiStates) { +// analysisInformation[state] = boost::container::flat_set(); +// for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { +// if (predecessorEntry.first != state && !psiStates.get(predecessorEntry.first)) { +// worklist.push(std::make_pair(predecessorEntry.first, state)); +// } +// } +// } +// +// // Iterate as long as the worklist is non-empty. +// uint_fast64_t iters = 0; +// while (!worklist.empty()) { +// ++iters; +// std::pair const& currentStateTargetStatePair = worklist.front(); +// uint_fast64_t currentState = currentStateTargetStatePair.first; +// uint_fast64_t targetState = currentStateTargetStatePair.second; +// +// size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); +// +// // Iterate over the successor states for all choices and compute new analysis information. +// for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { +// bool choiceTargetsTargetState = false; +// +// for (auto& entry : transitionMatrix.getRow(currentChoice)) { +// if (entry.first == targetState) { +// choiceTargetsTargetState = true; +// break; +// } +// } +// +// // If we can reach the target state with this choice, we need to intersect the current +// // analysis information with the union of the new analysis information of the target state +// // and the choice labels. +// if (choiceTargetsTargetState) { +// boost::container::flat_set tmpIntersection; +// std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[targetState].begin(), analysisInformation[targetState].end(), std::inserter(tmpIntersection, tmpIntersection.end())); +// std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.end())); +// analysisInformation[currentState] = std::move(tmpIntersection); +// } +// } +// +// // If the analysis information changed, we need to update it and put all the predecessors of this +// // state in the worklist. +// if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { +// for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { +// // Only put the predecessor in the worklist if it's not already a target state. +// if (!psiStates.get(predecessorEntry.first)) { +// worklist.push(std::make_pair(predecessorEntry.first, currentState)); +// } +// } +// } +// +// worklist.pop(); +// } + + std::queue worklist; + storm::storage::BitVector statesInWorkList(labeledMdp.getNumberOfStates()); + storm::storage::BitVector markedStates(labeledMdp.getNumberOfStates()); // Initially, put all predecessors of target states in the worklist and empty the analysis information them. for (auto state : psiStates) { analysisInformation[state] = boost::container::flat_set(); - for (auto& predecessorEntry : backwardTransitions.getRow(state)) { - if (predecessorEntry.first != state) { - worklist.push(std::make_pair(predecessorEntry.first, state)); + for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + if (predecessorEntry.first != state && !statesInWorkList.get(predecessorEntry.first) && !psiStates.get(predecessorEntry.first)) { + worklist.push(predecessorEntry.first); + statesInWorkList.set(predecessorEntry.first); + markedStates.set(state); } } } - // Iterate as long as the worklist is non-empty. uint_fast64_t iters = 0; while (!worklist.empty()) { ++iters; - std::pair const& currentStateTargetStatePair = worklist.front(); - uint_fast64_t currentState = currentStateTargetStatePair.first; - uint_fast64_t targetState = currentStateTargetStatePair.second; + uint_fast64_t const& currentState = worklist.front(); size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); // Iterate over the successor states for all choices and compute new analysis information. for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { - boost::container::flat_set tmpIntersection; - bool choiceTargetsTargetState = false; + bool modifiedChoice = false; - for (auto& entry : transitionMatrix.getRow(currentChoice)) { - if (entry.first == targetState) { - choiceTargetsTargetState = true; + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.first)) { + modifiedChoice = true; break; } } @@ -67,25 +125,35 @@ namespace storm { // If we can reach the target state with this choice, we need to intersect the current // analysis information with the union of the new analysis information of the target state // and the choice labels. - if (choiceTargetsTargetState) { - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[targetState].begin(), analysisInformation[targetState].end(), std::inserter(tmpIntersection, tmpIntersection.end())); - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.end())); - analysisInformation[currentState] = std::move(tmpIntersection); + if (modifiedChoice) { + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.first)) { + boost::container::flat_set tmpIntersection; + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.first].begin(), analysisInformation[entry.first].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + analysisInformation[currentState] = std::move(tmpIntersection); + } + } } } // If the analysis information changed, we need to update it and put all the predecessors of this // state in the worklist. if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { - for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { // Only put the predecessor in the worklist if it's not already a target state. - if (!psiStates.get(predecessorEntry.first)) { - worklist.push(std::make_pair(predecessorEntry.first, currentState)); + if (!psiStates.get(predecessorEntry.first) && !statesInWorkList.get(predecessorEntry.first)) { + worklist.push(predecessorEntry.first); + statesInWorkList.set(predecessorEntry.first); } } + markedStates.set(currentState, true); + } else { + markedStates.set(currentState, false); } worklist.pop(); + statesInWorkList.set(currentState, false); } return analysisInformation;