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.");