From 4d161e5e8ef1e5c0f654c418b4e3fea184aff345 Mon Sep 17 00:00:00 2001 From: masawei Date: Sat, 12 Oct 2013 22:21:20 +0200 Subject: [PATCH 01/10] Began with integration of crit. subsystem generation into master. Still some compile errors to fix. Former-commit-id: 30dfdd24790194612b28c684229a51efe92b0b00 --- .../PathBasedSubsystemGenerator.h | 705 ++++++++++++++++++ src/modelchecker/prctl/AbstractModelChecker.h | 11 + src/storm.cpp | 2 +- src/utility/StormOptions.cpp | 4 +- 4 files changed, 719 insertions(+), 3 deletions(-) create mode 100644 src/counterexamples/PathBasedSubsystemGenerator.h diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h new file mode 100644 index 000000000..b29ac334a --- /dev/null +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -0,0 +1,705 @@ +/* + * PathBasedSubsystemGenerator.h + * + * Created on: 11.10.2013 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_COUNTEREXAMPLES_PATHBASEDSUBSYSTEMGENERATOR_H_ +#define STORM_COUNTEREXAMPLES_PATHBASEDSUBSYSTEMGENERATOR_H_ + +#include "src/models/Dtmc.h" +#include "src/models/AbstractModel.h" +#include "src/storage/BitVector.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + namespace counterexamples { + + template + class PathBasedSubsystemGenerator { + +private: + + template + class CompareStates { + public: + bool operator()(const std::pair& s1, const std::pair& s2) { + return s1.second < s2.second; + } + }; + +public: + + /*! + * + */ + static void computeShortestDistances(storm::storage::SparseMatrix const& transMat, storm::storage::BitVector& subSysStates, storm::storage::BitVector& terminalStates, storm::storage::BitVector& allowedStates, std::vector>& distances) { + + std::multiset, CompareStates > activeSet; + //std::priority_queue, std::vector>, CompareStates > queue; + + // resize and init distances + const std::pair initDistances(0, (T) -1); + distances.resize(transMat.getColumnCount(), initDistances); + + //since gcc 4.7.2 does not implement std::set::emplace(), insert is used. + std::pair state; + + // First store all transitions from initial states + // Also save all found initial states in array of discovered states. + for(storm::storage::BitVector::constIndexIterator init = subSysStates.begin(); init != subSysStates.end(); ++init) { + //use init state only if it is allowed + if(allowedStates.get(*init)) { + + if(terminalStates.get(*init)) { + // it's an init -> target search + // save target state as discovered and get it's outgoing transitions + + distances[*init].first = *init; + distances[*init].second = (T) 1; + } + + typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + for(; trans != transMat.end(*init); ++trans) { + //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. + if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { + //new state? + if(distances[trans.column()].second == (T) -1) { + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = trans.value(); + + activeSet.insert(std::pair(trans.column(), distances[trans.column()].second)); + } + else if(distances[trans.column()].second < trans.value()){ + //This state has already been discovered + //And the distance can be improved by using this transition. + + //find state in set, remove it, reenter it with new and correct values. + auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + for(;range.first != range.second; range.first++) { + if(trans.column() == range.first->first) { + activeSet.erase(range.first); + break; + } + } + + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = trans.value(); + + activeSet.insert(std::pair(trans.column(), trans.value())); + } + } + } + } + } + + LOG4CPLUS_DEBUG(logger, "Initialized."); + + //Now find the shortest distances to all states + while(!activeSet.empty()) { + + // copy here since using a reference leads to segfault + std::pair activeState = *(--activeSet.end()); + activeSet.erase(--activeSet.end()); + + // If this is an initial state, do not consider its outgoing transitions, since all relevant ones have already been considered + // Same goes for forbidden states since they may not be used on a path, except as last node. + if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { + // Look at all neighbors + for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + // Only consider the transition if it's not virtual + if(trans.value() != (T) 0) { + + T distance = activeState.second * trans.value(); + + //not discovered or initial terminal state + if(distances[trans.column()].second == (T)-1) { + //New state discovered -> save it + distances[trans.column()].first = activeState.first; + distances[trans.column()].second = distance; + + // push newly discovered state into activeSet + activeSet.insert(std::pair(trans.column(), distance)); + } + else if(distances[trans.column()].second < distance ){ + //This state has already been discovered + //And the distance can be improved by using this transition. + + //find state in set, remove it, reenter it with new and correct values. + + auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + for(;range.first != range.second; range.first++) { + if(trans.column() == range.first->first) { + activeSet.erase(range.first); + break; + } + } + + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = distance; + activeSet.insert(std::pair(trans.column(), distance)); + } + } + } + } + } + + LOG4CPLUS_DEBUG(logger, "Discovery done."); + } + + /*! + * + */ + static void doDijkstraSearch(storm::storage::SparseMatrix const& transMat, storm::storage::BitVector& subSysStates, storm::storage::BitVector& terminalStates, storm::storage::BitVector& allowedStates, std::vector>& itDistances, std::vector>& distances) { + std::multiset, CompareStates > activeSet; + + // resize and init distances + const std::pair initDistances(0, (T) -1); + distances.resize(transMat.getColumnCount(), initDistances); + + //since gcc 4.7.2 does not implement std::set::emplace(), insert is used. + std::pair state; + + // First store all transitions from initial states + // Also save all found initial states in array of discovered states. + for(storm::storage::BitVector::constIndexIterator init = subSysStates.begin(); init != subSysStates.end(); ++init) { + //use init state only if it is allowed + if(allowedStates.get(*init)) { + + if(terminalStates.get(*init)) { + // it's a subsys -> subsys search + // ignore terminal state completely + // (since any target state that is only reached by a path going through this state should not be reached) + continue; + } + + typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + for(; trans != transMat.end(*init); ++trans) { + //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. + if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { + //new state? + if(distances[trans.column()].second == (T) -1) { + //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = trans.value() * (itDistances[trans.row()].second == -1 ? 1 : itDistances[trans.row()].second); + + activeSet.insert(std::pair(trans.column(), distances[trans.column()].second)); + } + else if(distances[trans.column()].second < trans.value() * itDistances[trans.row()].second){ + //This state has already been discovered + //And the distance can be improved by using this transition. + + //find state in set, remove it, reenter it with new and correct values. + auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + for(;range.first != range.second; range.first++) { + if(trans.column() == range.first->first) { + activeSet.erase(range.first); + break; + } + } + + //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = trans.value() * (itDistances[trans.row()].second == -1 ? 1 : itDistances[trans.row()].second); + + activeSet.insert(std::pair(trans.column(), trans.value())); + } + } + } + } + } + + LOG4CPLUS_DEBUG(logger, "Initialized."); + + //Now find the shortest distances to all states + while(!activeSet.empty()) { + + // copy here since using a reference leads to segfault + std::pair activeState = *(--activeSet.end()); + activeSet.erase(--activeSet.end()); + + // Always stop at first target/terminal state + //if(terminalStates.get(activeState.first) || subSysStates.get(activeState.first)) break; + + // If this is an initial state, do not consider its outgoing transitions, since all relevant ones have already been considered + // Same goes for forbidden states since they may not be used on a path, except as last node. + if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { + // Look at all neighbors + for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + // Only consider the transition if it's not virtual + if(trans.value() != (T) 0) { + + T distance = activeState.second * trans.value(); + + //not discovered or initial terminal state + if(distances[trans.column()].second == (T)-1) { + //New state discovered -> save it + distances[trans.column()].first = activeState.first; + distances[trans.column()].second = distance; + + // push newly discovered state into activeSet + activeSet.insert(std::pair(trans.column(), distance)); + } + else if(distances[trans.column()].second < distance ){ + //This state has already been discovered + //And the distance can be improved by using this transition. + + //find state in set, remove it, reenter it with new and correct values. + + auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + for(;range.first != range.second; range.first++) { + if(trans.column() == range.first->first) { + activeSet.erase(range.first); + break; + } + } + + distances[trans.column()].first = trans.row(); + distances[trans.column()].second = distance; + activeSet.insert(std::pair(trans.column(), distance)); + } + } + } + } + } + + LOG4CPLUS_DEBUG(logger, "Discovery done."); + } + + /*! + * + *//* + template + static void doBackwardsSearch(storm::storage::SparseMatrix const& transMat, storm::storage::BitVector& initStates, storm::storage::BitVector& subSysStates, storm::storage::BitVector& terminalStates, storm::storage::BitVector& allowedStates, std::vector& probabilities, std::vector& shortestPath, T& probability) { + std::multiset, CompareStates > activeSet; + + // resize and init distances + const std::pair initDistances(0, (T) -1); + std::vector> distances(transMat.getColumnCount(), initDistances); + + //since the transition matrix only gives a means to iterate over successors and not over predecessors and there is no Transpose for the matrix + //GraphTransitions is used + storm::models::GraphTransitions backTrans(transMat, false); + + //First store all allowed predecessors of target states that are not in the subsystem + for(storm::storage::BitVector::constIndexIterator target = terminalStates.begin(); target != terminalStates.end(); ++target) { + + // if there is a terminal state that is an initial state then prob == 1 and return + if(initStates.get(*target)){ + distances[*target].first = *target; + distances[*target].second = (T) 1; + return; + } + + //iterate over predecessors + for(auto iter = backTrans.beginStateSuccessorsIterator(*target); iter != backTrans.endStateSuccessorsIterator(*target); iter++) { + //only use if allowed and not in subsys and not terminal + if(allowedStates.get(*iter) && !subSysStates.get(*iter) && !terminalStates.get(*iter)) { + //new state? + if(distances[*iter].second == (T) -1) { + // save as discovered and push into active set + distances[*iter].first = *target; //successor + distances[*iter].second = transMat.getValue(*iter, *target); //prob of shortest path + + activeSet.insert(std::pair(*iter, probabilities[*iter])); //prob of reaching some terminal state from pred. + } + else { + // state was already discovered + // is this the better transition? + if(distances[*iter].second > transMat.getValue(*iter, *target)) { + distances[*iter].first = *target; + distances[*iter].second = transMat.getValue(*iter, *target); + } + } + } + } + } + + //Now store all allowed predecessors of subsystem states that are not subsystem states themselves + for(storm::storage::BitVector::constIndexIterator sysState = subSysStates.begin(); sysState != subSysStates.end(); ++sysState) { + //iterate over predecessors + for(auto iter = backTrans.beginStateSuccessorsIterator(*sysState); iter != backTrans.endStateSuccessorsIterator(*sysState); iter++) { + //only use if allowed and not in subsys and not terminal + if(allowedStates.get(*iter) && !subSysStates.get(*iter) && !terminalStates.get(*iter)) { + //new state? + if(distances[*iter].second == (T) -1) { + // save as discovered and push into active set + distances[*iter].first = *sysState; //successor + distances[*iter].second = transMat.getValue(*iter, *sysState); //prob of shortest path + + activeSet.insert(std::pair(*iter, probabilities[*iter])); //prob of reaching some terminal state from pred. + } + else { + // state was already discovered + // is this the better transition? + if(distances[*iter].second > transMat.getValue(*iter, *sysState)) { + distances[*iter].first = *sysState; + distances[*iter].second = transMat.getValue(*iter, *sysState); + } + } + } + } + } + + LOG4CPLUS_DEBUG(logger, "Initialized."); + + // Do the backwards search + std::pair state; + uint_fast64_t activeState; + while(!activeSet.empty()) { + // copy here since using a reference leads to segfault + state = *(--activeSet.end()); + activeState = state.first; + activeSet.erase(--activeSet.end()); + + //stop on the first subsys/init state + if(initStates.get(activeState) || subSysStates.get(activeState)) break; + + // If this is a subSys or terminal state, do not consider its incoming transitions, since all relevant ones have already been considered + if(!terminalStates.get(activeState) && !subSysStates.get(activeState)) { + //iterate over predecessors + for(auto iter = backTrans.beginStateSuccessorsIterator(activeState); iter != backTrans.endStateSuccessorsIterator(activeState); iter++) { + //only if transition is not "virtual" and no selfloop + if(*iter != activeState && transMat.getValue(*iter, activeState) != (T) 0) { + //new state? + if(distances[*iter].second == (T) -1) { + // save as discovered and push into active set + distances[*iter].first = activeState; + distances[*iter].second = transMat.getValue(*iter, activeState) * distances[activeState].second; + + activeSet.insert(std::pair(*iter, probabilities[*iter])); + } + else { + // state was already discovered + // is this the better transition? + if(distances[*iter].second < transMat.getValue(*iter, activeState) * distances[activeState].second) { + distances[*iter].first = activeState; + distances[*iter].second = transMat.getValue(*iter, activeState) * distances[activeState].second; + } + } + } + } + } + } + + //get path probability + probability = distances[activeState].second; + if(probability == (T) -1) probability = 1; + + // iterate over the successors until reaching the end of the finite path + shortestPath.push_back(activeState); + activeState = distances[activeState].first; + while(!terminalStates.get(activeState) && !subSysStates.get(activeState)) { + shortestPath.push_back(activeState); + activeState = distances[activeState].first; + } + shortestPath.push_back(activeState); + } + + */ + + /*! + * + */ + static void findShortestPath(storm::storage::SparseMatrix const& transMat, storm::storage::BitVector& subSysStates, storm::storage::BitVector& terminalStates, storm::storage::BitVector& allowedStates, std::vector>& itDistances, std::vector& shortestPath, T& probability) { + + //Do Dijksta to find the shortest path from init states to all states + std::vector> distances; + doDijkstraSearch(transMat, subSysStates, terminalStates, allowedStates, itDistances, distances); + + // Then get the shortest of them + extractShortestPath(subSysStates, terminalStates, distances, itDistances, shortestPath, probability,false); + } + + /*! + * Only initialized distances vector! + */ + static void extractShortestPath(storm::storage::BitVector& subSysStates, storm::storage::BitVector& terminalStates, std::vector>& distances, std::vector>& itDistances, std::vector& shortestPath, T& probability, bool stopAtFirstTarget = true, bool itSearch = false) { + //Find terminal state of best distance + uint_fast64_t bestIndex = 0; + T bestValue = (T) 0; + + for(storm::storage::BitVector::constIndexIterator term = terminalStates.begin(); term != terminalStates.end(); ++term) { + + //the terminal state might not have been found if it is in a system of forbidden states + if(distances[*term].second != -1 && distances[*term].second > bestValue){ + bestIndex = *term; + bestValue = distances[*term].second; + + //if set, stop since the first target that is not null was the only one found + if(stopAtFirstTarget) break; + } + } + + if(!itSearch) { + // it's a subSys->subSys search. So target states are terminals and subsys states + for(auto term = subSysStates.begin(); term != subSysStates.end(); ++term) { + + //the terminal state might not have been found if it is in a system of forbidden states + if(distances[*term].second != -1 && distances[*term].second > bestValue){ + bestIndex = *term; + bestValue = distances[*term].second; + + //if set, stop since the first target that is not null was the only one found + if(stopAtFirstTarget) break; + } + } + } + + //safety test: is the best terminal state viable? + if(distances[bestIndex].second == (T) -1){ + shortestPath.push_back(bestIndex); + probability = (T) 0; + LOG4CPLUS_DEBUG(logger, "Terminal state not viable!"); + return; + } + + // save the probability to reach the state via the shortest path + probability = distances[bestIndex].second; + + //Reconstruct shortest path. Notice that the last state of the path might be an initState. + + //There might be a chain of terminal states with 1.0 transitions at the end of the path + while(terminalStates.get(distances[bestIndex].first)) { + bestIndex = distances[bestIndex].first; + } + + LOG4CPLUS_DEBUG(logger, "Found best state: " << bestIndex); + LOG4CPLUS_DEBUG(logger, "Value: " << bestValue); + + shortestPath.push_back(bestIndex); + bestIndex = distances[bestIndex].first; + while(!subSysStates.get(bestIndex)) { + shortestPath.push_back(bestIndex); + bestIndex = distances[bestIndex].first; + } + shortestPath.push_back(bestIndex); + + //At last compensate for the distance between init and source state + probability = itSearch ? probability : probability / itDistances[bestIndex].second; + + LOG4CPLUS_DEBUG(logger, "Found path: " << shortestPath); + } + +private: + + template + struct transition { + uint_fast64_t source; + Type prob; + uint_fast64_t target; + }; + + template + class CompareTransitions { + public: + bool operator()(transition& t1, transition& t2) { + return t1.prob < t2.prob; + } + }; + +public: + + /*! + * + */ + static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker const& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { + + //------------------------------------------------------------- + // 1. Strip and handle formulas + //------------------------------------------------------------- + +#ifdef BENCHMARK + LOG4CPLUS_INFO(logger, "Formula: " << stateFormula.toString()); +#endif + LOG4CPLUS_INFO(logger, "Start finding critical subsystem."); + + //get dtmc (model) from model checker + storm::models::Dtmc model = modelCheck.template getModel>(); + + //init bit vector to contain the subsystem + storm::storage::BitVector subSys(model.getNumberOfStates()); + + storm::property::prctl::AbstractPathFormula const* pathFormulaPtr; + T bound = 0; + + // Strip bound operator + storm::property::prctl::ProbabilisticBoundOperator const* boundOperator = dynamic_cast const*>(&stateFormula); + + if(boundOperator == nullptr){ + LOG4CPLUS_ERROR(logger, "No path bound operator at formula root."); + return; + } + bound = boundOperator->getBound(); + + storm::property::prctl::AbstractPathFormula const& abstractPathFormula = boundOperator->getPathFormula(); + pathFormulaPtr = &abstractPathFormula; + + // get "init" labeled states + const storm::storage::BitVector initStates = model.getLabeledStates("init"); + + //get real prob for formula + std::vector trueProbs = pathFormulaPtr->check(modelCheck, false); + + T trueProb = 0; + for(auto index : initStates) { + trueProb += trueProbs[index]; + } + trueProb /= initStates.getNumberOfSetBits(); + //std::cout << "True Prob: " << trueProb << std::endl; + + // get allowed and target states + storm::storage::BitVector allowedStates; + storm::storage::BitVector targetStates; + + storm::property::prctl::Eventually const* eventually = dynamic_cast const*>(pathFormulaPtr); + storm::property::prctl::Globally const* globally = dynamic_cast const*>(pathFormulaPtr); + storm::property::prctl::Until const* until = dynamic_cast const*>(pathFormulaPtr); + if(eventually != nullptr) { + targetStates = eventually->getChild().check(modelCheck); + allowedStates = storm::storage::BitVector(targetStates.getSize(), true); + } + else if(globally != nullptr){ + //eventually reaching a state without property visiting only states with property + allowedStates = globally->getChild().check(modelCheck); + targetStates = storm::storage::BitVector(allowedStates); + targetStates.complement(); + } + else if(until != nullptr) { + allowedStates = until->getLeft().check(modelCheck); + targetStates = until->getRight().check(modelCheck); + } + else { + LOG4CPLUS_ERROR(logger, "Strange path formula. Can't decipher."); + return; + } + + //------------------------------------------------------------- + // 2. Precomputations for heuristics + //------------------------------------------------------------- + + // estimate the path count using the models state count as well as the probability bound + uint_fast8_t const minPrec = 10; + uint_fast64_t const stateCount = model.getNumberOfStates(); + uint_fast64_t const stateEstimate = ((T) stateCount) * bound; + + //since this only has a good effect on big models -> use only if model has at least 10^5 states + uint_fast64_t precision = stateEstimate > 100000 ? stateEstimate/1000 : minPrec; + + + + //------------------------------------------------------------- + // 3. Subsystem generation + //------------------------------------------------------------- + + // Search from init to target states until the shortest path for each target state is reached. + std::vector shortestPath; + std::vector subSysProbs; + T pathProb = 0; + T subSysProb = 0; + uint_fast64_t pathCount = 0; + uint_fast64_t mcCount = 0; + + // First compute the shortest paths from init states to all target states + std::vector> initTargetDistances; + computeShortestDistances(model.getTransitionMatrix(), initStates, targetStates, allowedStates, initTargetDistances); + + pathProb = 0; + extractShortestPath(initStates, targetStates, initTargetDistances, initTargetDistances, shortestPath, pathProb, false, true); + + // push states of found path into subsystem + for(auto index : shortestPath) { + subSys.set(index, true); + } + pathCount++; + + // set bigger sub system + modelCheck.setSubSystem(&subSys); + + // Get estimate (upper bound) of new sub system probability + // That is: prob(target) * cost(path) * (mean(prob(inits))/prob(source)) + subSysProb += trueProbs[shortestPath[0]] * pathProb * trueProb / trueProbs[shortestPath.back()]; + + //find new nodes until the system becomes critical. + while(true) { + shortestPath.clear(); + pathProb = 0; + findShortestPath(model.getTransitionMatrix(), subSys, targetStates, allowedStates, initTargetDistances, shortestPath, pathProb); + //doBackwardsSearch(*model->getTransitionMatrix(), *initStates, subSys, targetStates, allowedStates, trueProbs, shortestPath, pathProb); + + pathCount++; + + // merge found states into subsystem + for(uint_fast32_t i = 0; i < shortestPath.size(); i++) { + subSys.set(shortestPath[i], true); + } + + // set bigger sub system + modelCheck.setSubSystem(&subSys); + + // Get estimate (upper bound) of new sub system probability + // That is: prob(target) * cost(path) * (mean(prob(inits))/prob(source)) + //subSysProb += (trueProbs[shortestPath.back()] == 0 ? 0 : trueProbs[shortestPath[0]] * pathProb * trueProb / trueProbs[shortestPath.back()]); + subSysProb += 1*(trueProbs[shortestPath.back()] == 0 ? 1 : trueProbs[shortestPath[0]] * pathProb ); + //std::cout << "Est. prob: " << subSysProb << std::endl; + // Do we want to model check? + if((pathCount % precision == 0) && subSysProb >= bound) { + + //get probabilities + subSysProbs = pathFormulaPtr->check(modelCheck, false); + + //T diff = subSysProb; + //std::cout << "Est. prob: " << diff << std::endl; + + // reset sub system prob to correct value + subSysProb = 0; + for(auto index : initStates) { + subSysProb += subSysProbs[index]; + } + subSysProb /= initStates.getNumberOfSetBits(); + + mcCount++; + //diff -= subSysProb; + //std::cout << "Real prob: " << subSysProb << std::endl; + //std::cout << "Diff: " << diff << std::endl; + //std::cout << "Path count: " << pathCount << std::endl; + + //Are we critical? + //if(!modelCheck.check(stateFormula)) break; + if(subSysProb >= bound){ + break; + } + else if (stateEstimate > 100000){ + precision = (stateEstimate/1000) - ((stateEstimate/1000) - minPrec)*(subSysProb/bound); + } + } + } + + // To be sure the model checker ignores subsystems for future calls. + modelCheck.setSubSystem(nullptr); + +#ifdef BENCHMARK + LOG4CPLUS_INFO(logger, "Critical subsystem found."); + LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount); + LOG4CPLUS_INFO(logger, "State count of critical subsystem: " << subSys.getNumberOfSetBits()); + LOG4CPLUS_INFO(logger, "Prob: " << subSysProb); + LOG4CPLUS_INFO(logger, "Model checks: " << mcCount); + //LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); +#else + LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); + std::cout << "Critical subsystem: " << subSys.toString() << std::endl; +#endif + + } + + }; + + } // namespace counterexamples +} // namespace storm + +#endif /* STORM_COUNTEREXAMPLES_PATHBASEDSUBSYSTEMGENERATOR_H_ */ diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index f9245b93d..793af403e 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -21,6 +21,8 @@ namespace prctl { #include "src/formula/Prctl.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" +#include "src/counterexamples/PathBasedSubsystemGenerator.h" +#include "src/settings/Settings.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -145,6 +147,7 @@ public: LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; storm::storage::BitVector result; + bool allSatisfied = true; try { result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); @@ -152,11 +155,19 @@ public: for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; + allSatisfied &= result.get(initialState); } } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); } + + if(!allSatisfied && storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgumentByName("subSys").getValueAsBoolean()) { + //generate critical subsystem + storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*this, stateFormula); + } + + std::cout << std::endl << "-------------------------------------------" << std::endl; } diff --git a/src/storm.cpp b/src/storm.cpp index 80573a589..aa7eef3b7 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -250,7 +250,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); for (auto formula : formulaList) { - modelchecker.check(*formula); + modelchecker.check(*formula); delete formula; } } diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index e35d09b05..4fba837f9 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -9,7 +9,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the File to read from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from Transition- and Labeling Files").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the File to read the transition system from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the File to read the labeling from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given PRISM File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prismFileName", "The path and name of the File to read the PRISM Model from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createBooleanArgument("subSys", "generate subsystem as counterexample if formula is not satisfied").setDefaultValueBoolean(false).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); @@ -21,4 +21,4 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Which matrix library is to be used in numerical solving").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "Name of a buildin Library").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build()); return true; -}); \ No newline at end of file +}); From 0cb390b186e04e5b8562e793671773eca3e31853 Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 14 Oct 2013 11:53:49 +0200 Subject: [PATCH 02/10] More integration work. Ran into problem with the AbstractModelChecker being declared const for the model check. I use it for the subsystem generation and tell it what the current subsystem is. so I have two options: 1. Carry the subsystem as argument through all checking functions of the complete checking tree 2. Store the subsystem in the checker and use it in checkAp to induce the correct result back through the tree. In the original implementation I used option 2. But that does only work if it is not constant. Former-commit-id: 8a833cc05e4c7d2eb90a5f3659ed2f9cdda05087 --- src/modelchecker/prctl/AbstractModelChecker.h | 32 ++++++++++++++++--- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 793af403e..a45a1dc50 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -68,14 +68,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model) { + explicit AbstractModelChecker(storm::models::AbstractModel const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) { // Intentionally left empty. } /*! * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) { // Intentionally left empty. } @@ -205,7 +205,11 @@ public: */ storm::storage::BitVector checkAp(storm::property::prctl::Ap const& formula) const { if (formula.getAp() == "true") { - return storm::storage::BitVector(model.getNumberOfStates(), true); + if(subSystem != nullptr) { + return *subSystem; + } else { + return storm::storage::BitVector(model.getNumberOfStates(), true); + } } else if (formula.getAp() == "false") { return storm::storage::BitVector(model.getNumberOfStates()); } @@ -215,7 +219,11 @@ public: throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; } - return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + if(subSystem != nullptr) { + return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + } else { + return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); + } } /*! @@ -305,6 +313,15 @@ public: return result; } + /*! + * Sets the subsystem. + * + * @param subSystem The subsystem the model check is to be confined to. + */ + void setSubSystem(storm::storage::BitVector* subSys) { + subSystem = subSys; + } + private: /*! @@ -314,6 +331,13 @@ private: * model checker object is unsafe after the object has been destroyed. */ storm::models::AbstractModel const& model; + + /*! + * A pointer to the subsystem of the Model to which the check of the model is to be confined. + * + * @note that this is a nullptr iff the check is not to be confined. + */ + storm::storage::BitVector* subSystem; }; } // namespace prctl From 4dca7abd3f6c7540c3dcd67796752a74b4a40659 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 16 Oct 2013 00:01:33 +0200 Subject: [PATCH 03/10] Implementaed methods for checking until formula by providing the left and right states instead of the whole formula (same with bounded Until) in the SparseDtmcPrctlModelChecker, analouge to the SparseMdpPrctlModelChecker. Reverted unnecessary changes to the AbstractModel checker. Next on the list: Adapting the subsystem generation routine to the new method of providing the subsystem to the model checker. Former-commit-id: 6c90c064a2b222101ad98f1da594cdf6ef3e153d --- .../PathBasedSubsystemGenerator.h | 10 ++-- src/modelchecker/prctl/AbstractModelChecker.h | 40 ++------------ .../prctl/SparseDtmcPrctlModelChecker.h | 52 +++++++++++++++---- 3 files changed, 50 insertions(+), 52 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index b29ac334a..ae8a997d4 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -64,7 +64,7 @@ public: distances[*init].second = (T) 1; } - typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); for(; trans != transMat.end(*init); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { @@ -111,7 +111,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -178,7 +178,7 @@ public: continue; } - typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); for(; trans != transMat.end(*init); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { @@ -230,7 +230,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -508,7 +508,7 @@ public: /*! * */ - static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker const& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index a45a1dc50..713413478 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -68,14 +68,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) { + explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model){ // Intentionally left empty. } /*! * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model) { // Intentionally left empty. } @@ -147,7 +147,6 @@ public: LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; storm::storage::BitVector result; - bool allSatisfied = true; try { result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); @@ -155,19 +154,12 @@ public: for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; - allSatisfied &= result.get(initialState); } } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); } - if(!allSatisfied && storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgumentByName("subSys").getValueAsBoolean()) { - //generate critical subsystem - storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*this, stateFormula); - } - - std::cout << std::endl << "-------------------------------------------" << std::endl; } @@ -205,11 +197,7 @@ public: */ storm::storage::BitVector checkAp(storm::property::prctl::Ap const& formula) const { if (formula.getAp() == "true") { - if(subSystem != nullptr) { - return *subSystem; - } else { - return storm::storage::BitVector(model.getNumberOfStates(), true); - } + return storm::storage::BitVector(model.getNumberOfStates(), true); } else if (formula.getAp() == "false") { return storm::storage::BitVector(model.getNumberOfStates()); } @@ -219,11 +207,7 @@ public: throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; } - if(subSystem != nullptr) { - return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp())); - } else { - return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); - } + return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); } /*! @@ -313,15 +297,6 @@ public: return result; } - /*! - * Sets the subsystem. - * - * @param subSystem The subsystem the model check is to be confined to. - */ - void setSubSystem(storm::storage::BitVector* subSys) { - subSystem = subSys; - } - private: /*! @@ -331,13 +306,6 @@ private: * model checker object is unsafe after the object has been destroyed. */ storm::models::AbstractModel const& model; - - /*! - * A pointer to the subsystem of the Model to which the check of the model is to be confined. - * - * @note that this is a nullptr iff the check is not to be confined. - */ - storm::storage::BitVector* subSystem; }; } // namespace prctl diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 03245000d..45ae525c7 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -74,6 +74,7 @@ public: return formula.check(*this, false); } + /*! * Checks the given formula that is a bounded-until formula. * @@ -86,14 +87,29 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkBoundedUntil(storm::property::prctl::BoundedUntil const& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula. - storm::storage::BitVector leftStates = formula.getLeft().check(*this); - storm::storage::BitVector rightStates = formula.getRight().check(*this); + return this->checkBoundedUntil(formula.getLeft().check(*this), formula.getRight().check(*this), formula.getBound(), qualitative); + } + + + /*! + * Computes the probability to satisfy phi until psi inside a given bound for each state in the model. + * + * @param phiStates A bit vector indicating which states satisfy phi. + * @param psiStates A bit vector indicating which states satisfy psi. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. + */ + virtual std::vector checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { + std::vector result(this->getModel().getNumberOfStates()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the // further analysis. - storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), leftStates, rightStates, true, formula.getBound()); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), phiStates, psiStates, true, stepBound); LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states."); // Check if we already know the result (i.e. probability 0) for all initial states and @@ -111,7 +127,7 @@ public: storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); // Compute the new set of target states in the reduced system. - storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % rightStates; + storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates; // Make all rows absorbing that satisfy the second sub-formula. submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); @@ -122,7 +138,7 @@ public: // Perform the matrix vector multiplication as often as required by the formula bound. if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound()); + this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound); } else { throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; } @@ -219,6 +235,7 @@ public: return result; } + /*! * Check the given formula that is an until formula. * @@ -231,13 +248,26 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkUntil(storm::property::prctl::Until const& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector leftStates = formula.getLeft().check(*this); - storm::storage::BitVector rightStates = formula.getRight().check(*this); + return this->checkUntil(formula.getLeft().check(*this), formula.getRight().check(*this), qualitative); + } + + /*! + * Computes the probability to satisfy phi until psi for each state in the model. + * + * @param phiStates A bit vector indicating which states satisfy phi. + * @param psiStates A bit vector indicating which states satisfy psi. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. + */ + virtual std::vector checkUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { - // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), leftStates, rightStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); From b55932b212d45eb10e32db76154824d37a8bde42 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 16 Oct 2013 01:28:27 +0200 Subject: [PATCH 04/10] Adapted subsystem generation to the use of the new subsystem checking method using bit vectors. Compiles now. Next up: Setting up the control flow to make it actually generate a critical subsystem. Former-commit-id: a05fd42071f461737a70e8d3a90468412506d551 --- .../PathBasedSubsystemGenerator.h | 21 +++++++------------ src/modelchecker/prctl/AbstractModelChecker.h | 1 - src/storm.cpp | 1 + 3 files changed, 8 insertions(+), 15 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index ae8a997d4..1c3777cda 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -10,6 +10,8 @@ #include "src/models/Dtmc.h" #include "src/models/AbstractModel.h" +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/storage/BitVector.h" #include "log4cplus/logger.h" @@ -508,7 +510,7 @@ public: /*! * */ - static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static void computeCriticalSubsystem(storm::models::Dtmc const model, storm::property::prctl::AbstractStateFormula const& stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas @@ -519,8 +521,9 @@ public: #endif LOG4CPLUS_INFO(logger, "Start finding critical subsystem."); - //get dtmc (model) from model checker - storm::models::Dtmc model = modelCheck.template getModel>(); + //make model checker + //TODO: Implement and use generic Model Checker factory. + storm::modelchecker::prctl::SparseDtmcPrctlModelChecker modelCheck {model, new storm::solver::GmmxxLinearEquationSolver()}; //init bit vector to contain the subsystem storm::storage::BitVector subSys(model.getNumberOfStates()); @@ -618,9 +621,6 @@ public: } pathCount++; - // set bigger sub system - modelCheck.setSubSystem(&subSys); - // Get estimate (upper bound) of new sub system probability // That is: prob(target) * cost(path) * (mean(prob(inits))/prob(source)) subSysProb += trueProbs[shortestPath[0]] * pathProb * trueProb / trueProbs[shortestPath.back()]; @@ -639,9 +639,6 @@ public: subSys.set(shortestPath[i], true); } - // set bigger sub system - modelCheck.setSubSystem(&subSys); - // Get estimate (upper bound) of new sub system probability // That is: prob(target) * cost(path) * (mean(prob(inits))/prob(source)) //subSysProb += (trueProbs[shortestPath.back()] == 0 ? 0 : trueProbs[shortestPath[0]] * pathProb * trueProb / trueProbs[shortestPath.back()]); @@ -651,7 +648,7 @@ public: if((pathCount % precision == 0) && subSysProb >= bound) { //get probabilities - subSysProbs = pathFormulaPtr->check(modelCheck, false); + subSysProbs = modelCheck.checkUntil(allowedStates & subSys, targetStates & subSys, false); //T diff = subSysProb; //std::cout << "Est. prob: " << diff << std::endl; @@ -670,7 +667,6 @@ public: //std::cout << "Path count: " << pathCount << std::endl; //Are we critical? - //if(!modelCheck.check(stateFormula)) break; if(subSysProb >= bound){ break; } @@ -680,9 +676,6 @@ public: } } - // To be sure the model checker ignores subsystems for future calls. - modelCheck.setSubSystem(nullptr); - #ifdef BENCHMARK LOG4CPLUS_INFO(logger, "Critical subsystem found."); LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount); diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 713413478..f67c719bd 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -21,7 +21,6 @@ namespace prctl { #include "src/formula/Prctl.h" #include "src/storage/BitVector.h" #include "src/models/AbstractModel.h" -#include "src/counterexamples/PathBasedSubsystemGenerator.h" #include "src/settings/Settings.h" #include "log4cplus/logger.h" diff --git a/src/storm.cpp b/src/storm.cpp index aa7eef3b7..0a00240a6 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -28,6 +28,7 @@ #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" +#include "src/counterexamples/PathBasedSubsystemGenerator.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" #include "src/utility/ErrorHandling.h" From 1b2bb9c1383c0609be2f55648f5f2be6b902ebd4 Mon Sep 17 00:00:00 2001 From: masawei Date: Sat, 19 Oct 2013 21:51:11 +0200 Subject: [PATCH 05/10] Set up command flow for subsystem generation. Results seem correct on the first look. Next up: Write the DTMC output for the subsystem generation. Also: - fixed one bug in the subsystem generation leading to an infinite loop - corrected a typo in a comment in SparseMatrix Former-commit-id: 6014bf2dd2b7911e66ed795a24236650690226dc --- .../PathBasedSubsystemGenerator.h | 54 ++++--- src/storage/SparseMatrix.h | 2 +- src/storm.cpp | 133 +++++++++++++----- src/utility/StormOptions.cpp | 3 +- 4 files changed, 138 insertions(+), 54 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 1c3777cda..06c674526 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -13,6 +13,7 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/storage/BitVector.h" +#include "src/storage/SparseMatrix.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -66,13 +67,13 @@ public: distances[*init].second = (T) 1; } - typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); - for(; trans != transMat.end(*init); ++trans) { + typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(*init); + for(auto trans = rowIt.begin() ; trans != rowIt.end(); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { //new state? if(distances[trans.column()].second == (T) -1) { - distances[trans.column()].first = trans.row(); + distances[trans.column()].first = *init; distances[trans.column()].second = trans.value(); activeSet.insert(std::pair(trans.column(), distances[trans.column()].second)); @@ -90,7 +91,7 @@ public: } } - distances[trans.column()].first = trans.row(); + distances[trans.column()].first = *init; distances[trans.column()].second = trans.value(); activeSet.insert(std::pair(trans.column(), trans.value())); @@ -113,7 +114,8 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(activeState.first); + for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -142,7 +144,7 @@ public: } } - distances[trans.column()].first = trans.row(); + distances[trans.column()].first = activeState.first; distances[trans.column()].second = distance; activeSet.insert(std::pair(trans.column(), distance)); } @@ -180,19 +182,19 @@ public: continue; } - typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); - for(; trans != transMat.end(*init); ++trans) { + typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(*init); + for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { //new state? if(distances[trans.column()].second == (T) -1) { //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) - distances[trans.column()].first = trans.row(); - distances[trans.column()].second = trans.value() * (itDistances[trans.row()].second == -1 ? 1 : itDistances[trans.row()].second); + distances[trans.column()].first = *init; + distances[trans.column()].second = trans.value() * (itDistances[*init].second == -1 ? 1 : itDistances[*init].second); activeSet.insert(std::pair(trans.column(), distances[trans.column()].second)); } - else if(distances[trans.column()].second < trans.value() * itDistances[trans.row()].second){ + else if(distances[trans.column()].second < trans.value() * itDistances[*init].second){ //This state has already been discovered //And the distance can be improved by using this transition. @@ -206,8 +208,8 @@ public: } //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) - distances[trans.column()].first = trans.row(); - distances[trans.column()].second = trans.value() * (itDistances[trans.row()].second == -1 ? 1 : itDistances[trans.row()].second); + distances[trans.column()].first = *init; + distances[trans.column()].second = trans.value() * (itDistances[*init].second == -1 ? 1 : itDistances[*init].second); activeSet.insert(std::pair(trans.column(), trans.value())); } @@ -232,7 +234,8 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(activeState.first); + for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -261,7 +264,7 @@ public: } } - distances[trans.column()].first = trans.row(); + distances[trans.column()].first = activeState.first; distances[trans.column()].second = distance; activeSet.insert(std::pair(trans.column(), distance)); } @@ -510,7 +513,7 @@ public: /*! * */ - static void computeCriticalSubsystem(storm::models::Dtmc const model, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static void computeCriticalSubsystem(storm::models::Dtmc const& model, storm::property::prctl::AbstractStateFormula const& stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas @@ -544,7 +547,7 @@ public: pathFormulaPtr = &abstractPathFormula; // get "init" labeled states - const storm::storage::BitVector initStates = model.getLabeledStates("init"); + storm::storage::BitVector initStates = model.getLabeledStates("init"); //get real prob for formula std::vector trueProbs = pathFormulaPtr->check(modelCheck, false); @@ -608,7 +611,20 @@ public: uint_fast64_t pathCount = 0; uint_fast64_t mcCount = 0; - // First compute the shortest paths from init states to all target states + // First test if there are init states that are also target states. + // If so the init state represents a subsystem with probability mass 1. + // -> return it + if((initStates & targetStates).getNumberOfSetBits() != 0) { + subSys.set((initStates & targetStates).getSetIndicesList().front(), true); + + LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); + std::cout << "Critical subsystem: " << subSys.toString() << std::endl; + + return; + } + + + // Then compute the shortest paths from init states to all target states std::vector> initTargetDistances; computeShortestDistances(model.getTransitionMatrix(), initStates, targetStates, allowedStates, initTargetDistances); @@ -642,7 +658,7 @@ public: // Get estimate (upper bound) of new sub system probability // That is: prob(target) * cost(path) * (mean(prob(inits))/prob(source)) //subSysProb += (trueProbs[shortestPath.back()] == 0 ? 0 : trueProbs[shortestPath[0]] * pathProb * trueProb / trueProbs[shortestPath.back()]); - subSysProb += 1*(trueProbs[shortestPath.back()] == 0 ? 1 : trueProbs[shortestPath[0]] * pathProb ); + subSysProb += 1*(trueProbs[shortestPath.back()] == 0 ? 1 : trueProbs[shortestPath[0]] * pathProb == 0 ? 1 : pathProb ); //std::cout << "Est. prob: " << subSysProb << std::endl; // Do we want to model check? if((pathCount % precision == 0) && subSysProb >= bound) { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 84fe0bf94..6667fd82e 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -89,7 +89,7 @@ public: typedef T const* ConstValueIterator; /*! - * A class representing an iterator over a continguous number of rows of the matrix. + * A class representing an iterator over a continuous number of rows of the matrix. */ class ConstIterator { public: diff --git a/src/storm.cpp b/src/storm.cpp index 0a00240a6..d0c4289ab 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -257,6 +257,37 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker } } +/*! + * Checks if a counterexample for the given PRCTL formula can be computed. + * + * @param formula The formula to be examined. + * @param model The model for which the formula is to be examined. + * @return true iff a counterexample can be computed + */ +bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormula &formula, storm::models::Dtmc &model) { + // First check if it is a formula type for which a counterexample can be generated. + if (dynamic_cast const*>(&formula) != nullptr) { + LOG4CPLUS_ERROR(logger, "Can not generate a counterexample without a given bound."); + return false; + } else if (dynamic_cast const*>(&formula) != nullptr) { + storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(formula); + + // Now check if the model does not satisfy the formula. + // That is if there is at least one initial state of the model that does not. + storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); + if((result & model.getInitialStates()).getNumberOfSetBits() < model.getInitialStates().getNumberOfSetBits()) { + return true; + } else { + LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample."); + return false; + } + + } else { + LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected either a No Bound or a State formula."); + return false; + } +} + /*! * Main entry point. */ @@ -297,40 +328,76 @@ int main(const int argc, const char* argv[]) { storm::parser::AutoParser parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile); - // Determine which engine is to be used to choose the right model checker. - LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); - - // Depending on the model type, the appropriate model checking procedure is chosen. - storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; - parser.getModel>()->printModelInformationToStream(std::cout); - switch (parser.getType()) { - case storm::models::DTMC: - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - modelchecker = createPrctlModelChecker(*parser.getModel>()); - checkPrctlFormulae(*modelchecker); - break; - case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model is an MDP."); - modelchecker = createPrctlModelChecker(*parser.getModel>()); - checkPrctlFormulae(*modelchecker); - break; - case storm::models::CTMC: - LOG4CPLUS_INFO(logger, "Model is a CTMC."); - LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); - break; - case storm::models::CTMDP: - LOG4CPLUS_INFO(logger, "Model is a CTMDP."); - LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); - break; - case storm::models::Unknown: - default: - LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); - break; + //Should there be a counterexample generated in case the formula is not satisfied? + if(s->isSet("subSys")) { + + //Differentiate between model types. + if(parser.getType() == storm::models::DTMC) { + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + + if (s->isSet("prctl")) { + // Get specified PRCTL formulas. + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); + std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); + + // Test for each formula if a counterexample can be generated for it. + for (auto formula : formulaList) { + if(checkForCounterExampleGeneration(*formula, *parser.getModel>())) { + //Generate counterexample + storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), static_cast const&>(*formula)); + + //Output counterexample + //TODO: Write output. + + } else { + LOG4CPLUS_INFO(logger, "No counterexample generated for PRCTL formula: " << formula->toString()); + } + + delete formula; + } + } else { + LOG4CPLUS_ERROR(logger, "No PRCTL formula specified."); + } + } else { + LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); + } + } else { + // Determine which engine is to be used to choose the right model checker. + LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); + + // Depending on the model type, the appropriate model checking procedure is chosen. + storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; + parser.getModel>()->printModelInformationToStream(std::cout); + switch (parser.getType()) { + case storm::models::DTMC: + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + modelchecker = createPrctlModelChecker(*parser.getModel>()); + checkPrctlFormulae(*modelchecker); + break; + case storm::models::MDP: + LOG4CPLUS_INFO(logger, "Model is an MDP."); + modelchecker = createPrctlModelChecker(*parser.getModel>()); + checkPrctlFormulae(*modelchecker); + break; + case storm::models::CTMC: + LOG4CPLUS_INFO(logger, "Model is a CTMC."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); + break; + case storm::models::CTMDP: + LOG4CPLUS_INFO(logger, "Model is a CTMDP."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); + break; + case storm::models::Unknown: + default: + LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); + break; + } + + if (modelchecker != nullptr) { + delete modelchecker; + } } - - if (modelchecker != nullptr) { - delete modelchecker; - } } else if (s->isSet("symbolic")) { std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index 4fba837f9..7eec103f5 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -9,9 +9,10 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the File to read from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from Transition- and Labeling Files").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the File to read the transition system from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the File to read the labeling from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given PRISM File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prismFileName", "The path and name of the File to read the PRISM Model from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createBooleanArgument("subSys", "generate subsystem as counterexample if formula is not satisfied").setDefaultValueBoolean(false).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "subSys", "", "Generate subsystem as counterexample if given formula is not satisfied").build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); From a98310a7236d6044f5443b4bb7320e6554148df4 Mon Sep 17 00:00:00 2001 From: masawei Date: Sat, 26 Oct 2013 17:02:27 +0200 Subject: [PATCH 06/10] Some code revisions. Former-commit-id: 639afbe825f778048db24cf9c7b8c3cb80d8432d --- src/storm.cpp | 93 +++++++++++++++++++++++------------- src/utility/StormOptions.cpp | 2 +- 2 files changed, 62 insertions(+), 33 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index d0c4289ab..9c2e33177 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -1,3 +1,4 @@ + /* * STORM - a C++ Rebuild of MRMC * @@ -288,6 +289,63 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu } } +/*! + * Handles the counterexample generation control. + */ + void generateCounterExample(storm::parser::AutoParser parser) { + //Differentiate between model types. + if(parser.getType() != storm::models::DTMC) { + LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); + return; + } + + storm::models::Dtmc model = *parser.getModel>(); + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + + // Test for and get PRCTL formulas. + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + + if (!s->isSet("prctl")) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + + // Get specified PRCTL formulas. + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); + std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); + + // Test for each formula if a counterexample can be generated for it. + for (auto formula : formulaList) { + + // First check if it is a formula type for which a counterexample can be generated. + if (dynamic_cast const*>(formula) == nullptr) { + LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); + delete formula; + continue; + } + + storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(*formula); + + // Now check if the model does not satisfy the formula. + // That is if there is at least one initial state of the model that does not. + storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); + if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) { + LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample."); + delete formula; + continue; + } + + //Generate counterexample + storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); + + //Output counterexample + //TODO: Write output. + + delete formula; + } + } + /*! * Main entry point. */ @@ -329,39 +387,10 @@ int main(const int argc, const char* argv[]) { storm::parser::AutoParser parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile); //Should there be a counterexample generated in case the formula is not satisfied? - if(s->isSet("subSys")) { + if(s->isSet("counterExample")) { - //Differentiate between model types. - if(parser.getType() == storm::models::DTMC) { - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - - if (s->isSet("prctl")) { - // Get specified PRCTL formulas. - std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); - LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); - - // Test for each formula if a counterexample can be generated for it. - for (auto formula : formulaList) { - if(checkForCounterExampleGeneration(*formula, *parser.getModel>())) { - //Generate counterexample - storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), static_cast const&>(*formula)); - - //Output counterexample - //TODO: Write output. - - } else { - LOG4CPLUS_INFO(logger, "No counterexample generated for PRCTL formula: " << formula->toString()); - } - - delete formula; - } - } else { - LOG4CPLUS_ERROR(logger, "No PRCTL formula specified."); - } - } else { - LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); - } + generateCounterExample(parser); + } else { // Determine which engine is to be used to choose the right model checker. LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index 7eec103f5..35d9215c2 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "subSys", "", "Generate subsystem as counterexample if given formula is not satisfied").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generate a counterexample if given formula is not satisfied").build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); From ee1c1eb9b6f3840ab297cdc5e1e4624e2f93adff Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 28 Oct 2013 01:39:20 +0100 Subject: [PATCH 07/10] First implementation of the BitVector to Dtmc subsystem converter in Dtmc.h -Had to add a addState function to AtomicPropositionLabeling to be able to throw out the unneeded states using the substates constructor while at the end adding the absorbing state and its label. An alternative for that would be to provide a constructor taking the mapping and the single labelings vector as well as a getter for the single labelings. -The --counterexample command now only uses the pctl file given as argument to it and therefore it is now superflous to give the --prctl command in that case. -Also fixed a bug in the filter constructor of the BitVector. Now it copies all bit values specified by the filter to the correct index of new instance instead of all to index 0. Next up: Handle the optionals of the Dtmc when creating the sub-Dtmc. Former-commit-id: b45ee94cb2baeb2b32cf4643ea6ca4c21fa7b8d1 --- .../PathBasedSubsystemGenerator.h | 9 +- src/models/AtomicPropositionsLabeling.h | 16 +++ src/models/Dtmc.h | 115 ++++++++++++++++++ src/storage/BitVector.h | 1 + src/storm.cpp | 50 ++------ src/utility/StormOptions.cpp | 2 +- 6 files changed, 146 insertions(+), 47 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 06c674526..24d5af991 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -513,7 +513,7 @@ public: /*! * */ - static void computeCriticalSubsystem(storm::models::Dtmc const& model, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static storm::models::Dtmc computeCriticalSubsystem(storm::models::Dtmc& model, storm::property::prctl::AbstractStateFormula const& stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas @@ -539,7 +539,7 @@ public: if(boundOperator == nullptr){ LOG4CPLUS_ERROR(logger, "No path bound operator at formula root."); - return; + return model.getSubDtmc(subSys); } bound = boundOperator->getBound(); @@ -582,7 +582,7 @@ public: } else { LOG4CPLUS_ERROR(logger, "Strange path formula. Can't decipher."); - return; + return model.getSubDtmc(subSys); } //------------------------------------------------------------- @@ -620,7 +620,7 @@ public: LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); std::cout << "Critical subsystem: " << subSys.toString() << std::endl; - return; + return model.getSubDtmc(subSys); } @@ -704,6 +704,7 @@ public: std::cout << "Critical subsystem: " << subSys.toString() << std::endl; #endif + return model.getSubDtmc(subSys); } }; diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index f4ba0de50..b7ed0de9a 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -283,6 +283,22 @@ public: return this->nameToLabelingMap; } + /*! + * Adds a state to the labeling. + * Since this operation is quite expensive (resizing of all BitVectors containing the labeling), it should + * only be used in special cases to add one or two states. + * If you want to build a new AtomicPropositionlabeling: + * - Count the number of states you need. + * - Then add the labelings using addAtomicProposition() and addAtomicPropositionToState(). + * Do NOT use this method for this purpose. + */ + void addState() { + for(uint_fast64_t i = 0; i < apsCurrent; i++) { + singleLabelings[i].resize(singleLabelings[i].getSize() + 1); + } + stateCount++; + } + /*! * Calculates a hash over all values contained in this Sparse Matrix. * @return size_t A Hash Value diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 7b012803d..93348368b 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -121,6 +121,121 @@ public: return AbstractDeterministicModel::getHash(); } + /*! + * Generates a sub-Dtmc of this Dtmc induced by the states specified by the bitvector. + * E.g. a Dtmc that is partial isomorph (on the given states) to this one. + * @param subSysStates A BitVector where all states that should be kept are indicated + * by a set bit of the corresponding index. + * Waring: If the vector does not have the correct size, it will be resized. + * @return The sub-Dtmc. + */ + storm::models::Dtmc getSubDtmc(storm::storage::BitVector& subSysStates) { + + + // Is there any state in the subsystem? + if(subSysStates.getNumberOfSetBits() == 0) { + LOG4CPLUS_ERROR(logger, "No states in subsystem!"); + return storm::models::Dtmc(storm::storage::SparseMatrix(0), + storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates), + boost::optional>(), + boost::optional>(), + boost::optional>>()); + } + + // Does the vector have the right size? + if(subSysStates.getSize() != this->getNumberOfStates()) { + LOG4CPLUS_INFO(logger, "BitVector has wrong size. Resizing it..."); + subSysStates.resize(this->getNumberOfStates()); + } + + // Test if it is a proper subsystem of this Dtmc, i.e. if there is at least one state to be left out. + if(subSysStates.getNumberOfSetBits() == subSysStates.getSize()) { + LOG4CPLUS_INFO(logger, "All states are kept. This is no proper subsystem."); + return storm::models::Dtmc(*this); + } + + // 1. Get all necessary information from the old transition matrix + storm::storage::SparseMatrix const & origMat = this->getTransitionMatrix(); + uint_fast64_t const stateCount = origMat.getColumnCount(); + + // Iterate over all rows. Count the number of all transitions from the old system to be + // transfered to the new one. Also build a mapping from the state number of the old system + // to the state number of the new system. + uint_fast64_t subSysTransitionCount = 0; + uint_fast64_t row = 0; + uint_fast64_t newRow = 0; + std::vector stateMapping; + for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) { + if(subSysStates.get(row)){ + for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { + if(subSysStates.get(colIter.column())) { + subSysTransitionCount++; + } + } + stateMapping.push_back(newRow); + newRow++; + } else { + stateMapping.push_back((uint_fast64_t) -1); + } + row++; + } + + // 2. Construct transition matrix + + // Take all states indicated by the vector as well as one additional state as target of + // all transitions that target a state that is not kept. + uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1; + storm::storage::SparseMatrix newMat(newStateCount); + + // The number of transitions of the new Dtmc is the number of transitions transfered + // from the old one plus one transition for each state to the new one. + newMat.initialize(subSysTransitionCount + newStateCount); + + // Now fill the matrix. + newRow = 0; + row = 0; + T rest = 0; + for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) { + if(subSysStates.get(row)){ + // Transfer transitions + for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { + if(subSysStates.get(colIter.column())) { + newMat.addNextValue(newRow, stateMapping[colIter.column()], colIter.value()); + } else { + rest += colIter.value(); + } + } + + // Insert the transition taking care of the remaining outgoing probability. + newMat.addNextValue(newRow, newStateCount - 1, rest); + rest = (T) 0; + + newRow++; + } + row++; + } + + // Insert last transition: self loop on added state + newMat.addNextValue(newStateCount - 1, newStateCount - 1, (T) 1); + + newMat.finalize(false); + + // 3. Take care of the labeling + storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); + newLabeling.addState(); + //newLabeling.addAtomicProposition(); + + // 4. Make Dtmc from the matrix and return it + //TODO: test the labeling, handle optionals. + return storm::models::Dtmc(newMat, + newLabeling, + boost::optional>(), + boost::optional>(), + boost::optional>>() + ); + + } + private: /*! * @brief Perform some sanity checks. diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index d8c19f523..72ad4434c 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -166,6 +166,7 @@ public: uint_fast64_t nextPosition = 0; for (auto position : filter) { this->set(nextPosition, other.get(position)); + nextPosition++; } } diff --git a/src/storm.cpp b/src/storm.cpp index 9c2e33177..5fd3d1fc2 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -258,37 +258,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker } } -/*! - * Checks if a counterexample for the given PRCTL formula can be computed. - * - * @param formula The formula to be examined. - * @param model The model for which the formula is to be examined. - * @return true iff a counterexample can be computed - */ -bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormula &formula, storm::models::Dtmc &model) { - // First check if it is a formula type for which a counterexample can be generated. - if (dynamic_cast const*>(&formula) != nullptr) { - LOG4CPLUS_ERROR(logger, "Can not generate a counterexample without a given bound."); - return false; - } else if (dynamic_cast const*>(&formula) != nullptr) { - storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(formula); - - // Now check if the model does not satisfy the formula. - // That is if there is at least one initial state of the model that does not. - storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); - if((result & model.getInitialStates()).getNumberOfSetBits() < model.getInitialStates().getNumberOfSetBits()) { - return true; - } else { - LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample."); - return false; - } - - } else { - LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected either a No Bound or a State formula."); - return false; - } -} - /*! * Handles the counterexample generation control. */ @@ -302,20 +271,17 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu storm::models::Dtmc model = *parser.getModel>(); LOG4CPLUS_INFO(logger, "Model is a DTMC."); - // Test for and get PRCTL formulas. - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - - if (!s->isSet("prctl")) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); - return; - } - // Get specified PRCTL formulas. - std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + std::string const chosenPrctlFile = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); // Test for each formula if a counterexample can be generated for it. + if(formulaList.size() == 0) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + for (auto formula : formulaList) { // First check if it is a formula type for which a counterexample can be generated. @@ -337,10 +303,10 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu } //Generate counterexample - storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); + storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); //Output counterexample - //TODO: Write output. + counterExample.printModelInformationToStream(std::cout); delete formula; } diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index 35d9215c2..79df6a567 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generate a counterexample if given formula is not satisfied").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); From 393a72d56fffb94c71cf379dcb4d1edb9a546ffd Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 28 Oct 2013 18:29:40 +0100 Subject: [PATCH 08/10] Added handling of state and transition rewards to getSubDtmc(). Remark: I don't quite get the optional choice labeling in Dtmcs. Whats its purpose? Why is it undocumented in the Dtmc constructor, not supported by the parser but needed nevertheless? Next up: Pretty up counterexample generation output. Former-commit-id: c04063b608a9a0cc598f867acaf85ea39636c717 --- src/models/Dtmc.h | 64 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 55 insertions(+), 9 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 93348368b..9e21e73f9 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -18,6 +18,7 @@ #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/Settings.h" +#include "src/utility/vector.h" namespace storm { @@ -182,13 +183,13 @@ public: // 2. Construct transition matrix - // Take all states indicated by the vector as well as one additional state as target of + // Take all states indicated by the vector as well as one additional state s_b as target of // all transitions that target a state that is not kept. uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1; storm::storage::SparseMatrix newMat(newStateCount); // The number of transitions of the new Dtmc is the number of transitions transfered - // from the old one plus one transition for each state to the new one. + // from the old one plus one transition for each state to s_b. newMat.initialize(subSysTransitionCount + newStateCount); // Now fill the matrix. @@ -215,22 +216,67 @@ public: row++; } - // Insert last transition: self loop on added state + // Insert last transition: self loop on s_b newMat.addNextValue(newStateCount - 1, newStateCount - 1, (T) 1); newMat.finalize(false); - // 3. Take care of the labeling + // 3. Take care of the labeling. storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); newLabeling.addState(); - //newLabeling.addAtomicProposition(); - // 4. Make Dtmc from the matrix and return it - //TODO: test the labeling, handle optionals. + // 4. Handle the optionals + + boost::optional> newStateRewards; + if(this->hasStateRewards()) { + + // Get the rewards and move the needed values to the front. + std::vector newRewards(this->getStateRewardVector()); + storm::utility::vector::selectVectorValues(newRewards, subSysStates, newRewards); + + // Throw away all values after the last state and set the reward for s_b to 0. + newRewards.resize(newStateCount); + newRewards[newStateCount - 1] = (T) 0; + + newStateRewards = newRewards; + } + + boost::optional> newTransitionRewards; + if(this->hasTransitionRewards()) { + + storm::storage::SparseMatrix newTransRewards(newStateCount); + newTransRewards.initialize(subSysTransitionCount + newStateCount); + + // Copy the rewards for the kept states + newRow = 0; + row = 0; + for(auto iter = this->getTransitionRewardMatrix().begin(); iter != this->getTransitionRewardMatrix().end(); ++iter) { + if(subSysStates.get(row)){ + // Transfer transition rewards + for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { + if(subSysStates.get(colIter.column())) { + newTransRewards.addNextValue(newRow, stateMapping[colIter.column()], colIter.value()); + } + } + + // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. + newTransRewards.addNextValue(newRow, newStateCount - 1, (T) 0); + + newRow++; + } + row++; + } + + newTransitionRewards = newTransRewards; + } + + //What about choice labeling?? Not documented, not parsed, not used, but there? + + // 5. Make Dtmc from its parts and return it return storm::models::Dtmc(newMat, newLabeling, - boost::optional>(), - boost::optional>(), + newStateRewards, + newTransitionRewards, boost::optional>>() ); From e3e02ecce29af533eacb19184fb804556e6c5115 Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 28 Oct 2013 23:04:14 +0100 Subject: [PATCH 09/10] Made counterexample generation output usable. -std::cout gives enough information to understand what th result of the generaton is. -Added another argument to --counterExample specifying a directory to write .dot files containing the critical subsystems (as Dtmc) to. -Cleaned up some logging output of the counterexample generationn. Next up: Merging. Former-commit-id: feb4323052a30d4ce2cbc13c4e5272b8650bc3a6 --- .../PathBasedSubsystemGenerator.h | 13 ++-- src/storm.cpp | 62 ++++++++++++++++++- src/utility/StormOptions.cpp | 2 +- 3 files changed, 65 insertions(+), 12 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 24d5af991..4d2980744 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -617,8 +617,11 @@ public: if((initStates & targetStates).getNumberOfSetBits() != 0) { subSys.set((initStates & targetStates).getSetIndicesList().front(), true); - LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); - std::cout << "Critical subsystem: " << subSys.toString() << std::endl; + LOG4CPLUS_INFO(logger, "Critical subsystem found."); + LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount); + LOG4CPLUS_INFO(logger, "State count of critical subsystem: " << subSys.getNumberOfSetBits()); + LOG4CPLUS_INFO(logger, "Prob: " << 1); + LOG4CPLUS_INFO(logger, "Model checks: " << mcCount); return model.getSubDtmc(subSys); } @@ -692,17 +695,11 @@ public: } } -#ifdef BENCHMARK LOG4CPLUS_INFO(logger, "Critical subsystem found."); LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount); LOG4CPLUS_INFO(logger, "State count of critical subsystem: " << subSys.getNumberOfSetBits()); LOG4CPLUS_INFO(logger, "Prob: " << subSysProb); LOG4CPLUS_INFO(logger, "Model checks: " << mcCount); - //LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); -#else - LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString()); - std::cout << "Critical subsystem: " << subSys.toString() << std::endl; -#endif return model.getSubDtmc(subSys); } diff --git a/src/storm.cpp b/src/storm.cpp index 5fd3d1fc2..0e30f93b8 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -262,6 +262,23 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker * Handles the counterexample generation control. */ void generateCounterExample(storm::parser::AutoParser parser) { + LOG4CPLUS_INFO(logger, "Starting counterexample generation."); + LOG4CPLUS_INFO(logger, "Testing inputs..."); + + //First test output directory. + std::string outPath = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(1).getValueAsString(); + if(outPath.back() != '/' && outPath.back() != '\\') { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + std::ofstream testFile(outPath + "test.dot"); + if(testFile.fail()) { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + testFile.close(); + std::remove((outPath + "test.dot").c_str()); + //Differentiate between model types. if(parser.getType() != storm::models::DTMC) { LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); @@ -282,6 +299,25 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker return; } + // Get prctl file name without the filetype + uint_fast64_t first = 0; + if(chosenPrctlFile.find('/') != std::string::npos) { + first = chosenPrctlFile.find_last_of('/') + 1; + } else if(chosenPrctlFile.find('\\') != std::string::npos) { + first = chosenPrctlFile.find_last_of('\\') + 1; + } + + uint_fast64_t length; + if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) { + length = chosenPrctlFile.find_last_of('.') - first; + } else { + length = chosenPrctlFile.length() - first; + } + + std::string outFileName = chosenPrctlFile.substr(first, length); + + // Test formulas and do generation + uint_fast64_t fIndex = 0; for (auto formula : formulaList) { // First check if it is a formula type for which a counterexample can be generated. @@ -293,21 +329,41 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(*formula); + // Do some output + std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; + LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": "); + std::cout << "\t" << formula->toString() << "\n" << std::endl; + LOG4CPLUS_INFO(logger, formula->toString()); + // Now check if the model does not satisfy the formula. // That is if there is at least one initial state of the model that does not. storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) { - LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample."); + std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; + LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample."); delete formula; continue; } - //Generate counterexample + // Generate counterexample storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); - //Output counterexample + LOG4CPLUS_INFO(logger, "Found counterexample."); + + // Output counterexample + // Do standard output + std::cout << "Found counterexample with following properties: " << std::endl; counterExample.printModelInformationToStream(std::cout); + std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl; + + // Write the .dot file + std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot"); + if(outFile.good()) { + counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true); + outFile.close(); + } + fIndex++; delete formula; } } diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index 79df6a567..8fea67c8f 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("outputPath", "The path to the directory to write the generated counterexample files to.").build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); From af0601c453fbef561ad26bc1eb243fbdb189c878 Mon Sep 17 00:00:00 2001 From: masawei Date: Tue, 5 Nov 2013 00:56:44 +0100 Subject: [PATCH 10/10] Made several changes. - Fixed the infinite loop bug that occured when giving a filepath pointing to a directory instead of a file. - The BitVector to Dtmc subsystem converter now supports an optional choice labeling. - The output of the modelchecker to the log file is now suppressed while doing a counterexample generation. - It is now possible to add more atomic propositions to the AtomicPropositionLabeling than previously declared (at the cost of one reserve per added ap beyond the maximum). The maximum is then increased accordingly. |-> As a result the state added for the Dtmc subsystem has now its own label. Next up: Merge.) Former-commit-id: 74c92aaea17cafa370a3b4f75afa49bdd940af52 --- .../PathBasedSubsystemGenerator.h | 10 +++++-- src/models/AbstractModel.h | 9 +++--- src/models/AtomicPropositionsLabeling.h | 20 ++++++------- src/models/Dtmc.h | 30 +++++++++++++++---- src/parser/PrctlFileParser.cpp | 21 +++++++------ src/storm.cpp | 6 ++++ 6 files changed, 62 insertions(+), 34 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 4d2980744..18355e1c4 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -524,11 +524,11 @@ public: #endif LOG4CPLUS_INFO(logger, "Start finding critical subsystem."); - //make model checker - //TODO: Implement and use generic Model Checker factory. + // make model checker + // TODO: Implement and use generic Model Checker factory. storm::modelchecker::prctl::SparseDtmcPrctlModelChecker modelCheck {model, new storm::solver::GmmxxLinearEquationSolver()}; - //init bit vector to contain the subsystem + // init bit vector to contain the subsystem storm::storage::BitVector subSys(model.getNumberOfStates()); storm::property::prctl::AbstractPathFormula const* pathFormulaPtr; @@ -550,7 +550,9 @@ public: storm::storage::BitVector initStates = model.getLabeledStates("init"); //get real prob for formula + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); std::vector trueProbs = pathFormulaPtr->check(modelCheck, false); + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); T trueProb = 0; for(auto index : initStates) { @@ -667,7 +669,9 @@ public: if((pathCount % precision == 0) && subSysProb >= bound) { //get probabilities + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); subSysProbs = modelCheck.checkUntil(allowedStates & subSys, targetStates & subSys, false); + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); //T diff = subSysProb; //std::cout << "Est. prob: " << diff << std::endl; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index deffd9999..ee50f8ee6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -65,8 +65,8 @@ class AbstractModel: public std::enable_shared_from_this> { * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalStateRewardVector The reward values associated with the states. + * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ AbstractModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, @@ -90,8 +90,9 @@ class AbstractModel: public std::enable_shared_from_this> { * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalStateRewardVector The reward values associated with the states. + * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ AbstractModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index b7ed0de9a..7c37535d8 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -27,7 +27,7 @@ namespace storm { namespace models { /*! - * This class manages the labeling of the state space with a fixed number of + * This class manages the labeling of the state space with a number of * atomic propositions. */ class AtomicPropositionsLabeling { @@ -130,8 +130,9 @@ public: /*! * Registers the name of a proposition. - * Will throw an error if more atomic propositions are added than were originally declared or if an atomic - * proposition is registered twice. + * Will throw an error if an atomic proposition is registered twice. + * If more atomic propositions are added than previously declared, the maximum number of propositions + * is increased and the capacity of the singleLabelings vector is matched with the new maximum. * * @param ap The name of the atomic proposition to add. * @return The index of the new proposition. @@ -142,9 +143,8 @@ public: throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists."); } if (apsCurrent >= apCountMax) { - LOG4CPLUS_ERROR(logger, "Added more atomic propositions than previously declared."); - throw storm::exceptions::OutOfRangeException("Added more atomic propositions than" - "previously declared."); + apCountMax++; + singleLabelings.reserve(apCountMax); } nameToLabelingMap[ap] = apsCurrent; singleLabelings.push_back(storm::storage::BitVector(stateCount)); @@ -226,9 +226,9 @@ public: } /*! - * Returns the number of atomic propositions managed by this object (set in the initialization). - * - * @return The number of atomic propositions. + * Returns the internal index of a given atomic proposition. + * + * @return The index of the atomic proposition. */ uint_fast64_t getIndexOfProposition(std::string const& ap) const { if (!this->containsAtomicProposition(ap)) { @@ -300,7 +300,7 @@ public: } /*! - * Calculates a hash over all values contained in this Sparse Matrix. + * Calculates a hash over all values contained in this Atomic Proposition Labeling. * @return size_t A Hash Value */ std::size_t getHash() const { diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 9e21e73f9..206e48c44 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -39,8 +39,9 @@ public: * @param probabilityMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalStateRewardVector The reward values associated with the states. + * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, @@ -65,8 +66,9 @@ public: * @param probabilityMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalStateRewardVector The reward values associated with the states. + * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, @@ -224,6 +226,10 @@ public: // 3. Take care of the labeling. storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); newLabeling.addState(); + if(!newLabeling.containsAtomicProposition("s_b")) { + newLabeling.addAtomicProposition("s_b"); + } + newLabeling.addAtomicPropositionToState("s_b", newStateCount - 1); // 4. Handle the optionals @@ -270,14 +276,26 @@ public: newTransitionRewards = newTransRewards; } - //What about choice labeling?? Not documented, not parsed, not used, but there? + boost::optional>> newChoiceLabels; + if(this->hasChoiceLabels()) { + + // Get the choice label sets and move the needed values to the front. + std::vector> newChoice(this->getChoiceLabeling()); + storm::utility::vector::selectVectorValues(newChoice, subSysStates, newChoice); + + // Throw away all values after the last state and set the choice label set for s_b as empty. + newChoice.resize(newStateCount); + newChoice[newStateCount - 1] = std::set(); + + newChoiceLabels = newChoice; + } // 5. Make Dtmc from its parts and return it return storm::models::Dtmc(newMat, newLabeling, newStateRewards, newTransitionRewards, - boost::optional>>() + newChoiceLabels ); } diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index a54fc3d48..ccf4c62b1 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -15,7 +15,8 @@ namespace parser { std::list*> PrctlFileParser(std::string filename) { // Open file - std::ifstream inputFileStream(filename, std::ios::in); + std::ifstream inputFileStream; + inputFileStream.open(filename, std::ios::in); if (!inputFileStream.is_open()) { std::string message = "Error while opening file "; @@ -24,16 +25,14 @@ std::list*> PrctlFileParser std::list*> result; - while(!inputFileStream.eof()) { - std::string line; - //The while loop reads the input file line by line - while (std::getline(inputFileStream, line)) { - PrctlParser parser(line); - if (!parser.parsedComment()) { - //lines containing comments will be skipped. - LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\""); - result.push_back(parser.getFormula()); - } + std::string line; + //The while loop reads the input file line by line + while (std::getline(inputFileStream, line)) { + PrctlParser parser(line); + if (!parser.parsedComment()) { + //lines containing comments will be skipped. + LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\""); + result.push_back(parser.getFormula()); } } diff --git a/src/storm.cpp b/src/storm.cpp index 0e30f93b8..37f62c41e 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -337,7 +337,13 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker // Now check if the model does not satisfy the formula. // That is if there is at least one initial state of the model that does not. + + // Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them) + // Lower it again after the model check. + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); + if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) { std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");