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

Added signal handler for SIGTERM. Introduced delayed update for LP solvers to reduce overhead. 

Former-commit-id: 1300d77ae8
main
dehnert 11 years ago
parent
a52419652d
commit
486e99d6ae
12 changed files with 165 additions and 63 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/counterexamples/CounterexampleOptions.cpp
  2. 29
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  3. 31
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  4. 1
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  5. 4
      src/solver/GlpkLpSolver.cpp
  6. 5
      src/solver/GlpkLpSolver.h
  7. 17
      src/solver/GurobiLpSolver.cpp
  8. 12
      src/solver/GurobiLpSolver.h
  9. 6
      src/solver/LpSolver.h
  10. 7
      src/storm.cpp
  11. 7
      src/utility/ErrorHandling.h
  12. 108
      src/utility/counterexamples.h

1
src/counterexamples/CounterexampleOptions.cpp
View File

@ -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;
});

29
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -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<T> modelchecker(labeledMdp);
std::vector<T> 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<T> modelchecker(labeledMdp);
std::vector<T> 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<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, true);
boost::container::flat_set<uint_fast64_t> 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<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

31
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -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<boost::container::flat_set<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
boost::container::flat_set<uint_fast64_t> locallyRelevantLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin()));
std::vector<boost::container::flat_set<uint_fast64_t>> 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<boost::container::flat_set<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels);
boost::container::flat_set<uint_fast64_t> locallyRelevantLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin()));
std::vector<boost::container::flat_set<uint_fast64_t>> 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<boost::container::flat_set<uint_fast64_t>> 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<T> modelchecker(labeledMdp);
std::vector<T> 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<T> modelchecker(labeledMdp);
std::vector<T> 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<T> 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()) {

1
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -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<uint_fast64_t> variables;

4
src/solver/GlpkLpSolver.cpp
View File

@ -95,6 +95,10 @@ namespace storm {
return index;
}
void GlpkLpSolver::update() const {
// Intentionally left empty.
}
void GlpkLpSolver::addConstraint(std::string const& name, std::vector<uint_fast64_t> const& variables, std::vector<double> 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.");

5
src/solver/GlpkLpSolver.h
View File

@ -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<uint_fast64_t> const& variables, std::vector<double> 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<uint_fast64_t> const& variables, std::vector<double> 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.";
}

17
src/solver/GurobiLpSolver.cpp
View File

@ -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<int>(value)) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
if (std::abs(value - static_cast<int>(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 << ").";
}

12
src/solver/GurobiLpSolver.h
View File

@ -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<uint_fast64_t> const& variables, std::vector<double> 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<uint_fast64_t> const& variables, std::vector<double> 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.";
}

6
src/solver/LpSolver.h
View File

@ -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 <code>update</code>
* usable.
*/
virtual void update() const = 0;
/*!
* Adds a constraint of the form
* a_1*x_1 + ... + a_n*x_n op c

7
src/storm.cpp
View File

@ -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) {

7
src/utility/ErrorHandling.h
View File

@ -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 */

108
src/utility/counterexamples.h
View File

@ -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<boost::container::flat_set<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);
std::queue<std::pair<uint_fast64_t, uint_fast64_t>> worklist;
// std::queue<std::pair<uint_fast64_t, uint_fast64_t>> 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<uint_fast64_t>();
// 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<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t> 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<uint_fast64_t> 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<uint_fast64_t>();
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<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t> 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<uint_fast64_t> 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;

Write Preview
Loading…
Cancel
Save