From ee1c1eb9b6f3840ab297cdc5e1e4624e2f93adff Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 28 Oct 2013 01:39:20 +0100 Subject: [PATCH] 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());