Updated some TODOS

src/storm-dft/builder/DFTBuilder.h

@@ -106,7 +106,7 @@ namespace storm {
                 }
                 std::string trigger = children[0];
 
-                //TODO Matthias: collect constraints for SMT solving
+                //TODO: collect constraints for SMT solving
                 //0 <= probability <= 1
                 if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) {
                     // Introduce additional element for first capturing the probabilistic dependency
@@ -195,7 +195,7 @@ namespace storm {
             }
 
             bool addBasicElementExponential(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) {
-                //TODO Matthias: collect constraints for SMT solving
+                //TODO: collect constraints for SMT solving
                 //0 <= dormancyFactor <= 1
                 if (nameInUse(name)) {
                     STORM_LOG_ERROR("Element with name '" << name << "' already exists.");

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -155,7 +155,7 @@ namespace storm {
                     setMarkovian(behavior.begin()->isMarkovian());
 
                     // Now add self loop.
-                    // TODO Matthias: maybe use general method.
+                    // TODO: maybe use general method.
                     STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state.");
                     STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state.");
                     std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin());
@@ -214,7 +214,7 @@ namespace storm {
 
             // Fix the entries in the transition matrix according to the mapping of ids to row group indices
             STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
-            // TODO Matthias: do not consider all rows?
+            // TODO: do not consider all rows?
             STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
             matrixBuilder.remap();
 
@@ -238,16 +238,16 @@ namespace storm {
         void ExplicitDFTModelBuilder<ValueType, StateType>::initializeNextIteration() {
             STORM_LOG_TRACE("Refining DFT state space");
 
-            // TODO Matthias: should be easier now as skipped states all are at the end of the matrix
+            // TODO: should be easier now as skipped states all are at the end of the matrix
             // Push skipped states to explore queue
-            // TODO Matthias: remove
+            // TODO: remove
             for (auto const& skippedState : skippedStates) {
                 statesNotExplored[skippedState.second.first->getId()] = skippedState.second;
                 explorationQueue.push(skippedState.second.second);
             }
 
             // Initialize matrix builder again
-            // TODO Matthias: avoid copy
+            // TODO: avoid copy
             std::vector<uint_fast64_t> copyRemapping = matrixBuilder.stateRemapping;
             matrixBuilder = MatrixBuilder(!generator.isDeterministicModel());
             matrixBuilder.stateRemapping = copyRemapping;
@@ -309,7 +309,7 @@ namespace storm {
             modelComponents.markovianStates = markovianStatesNew;
 
             // Build submatrix for expanded states
-            // TODO Matthias: only use row groups when necessary
+            // TODO: only use row groups when necessary
             for (StateType oldRowGroup = 0; oldRowGroup < modelComponents.transitionMatrix.getRowGroupCount(); ++oldRowGroup) {
                 if (indexRemapping[oldRowGroup] < nrExpandedStates) {
                     // State is expanded -> copy to new matrix
@@ -342,7 +342,7 @@ namespace storm {
             size_t nrSkippedStates = 0;
             storm::utility::ProgressMeasurement progress("explored states");
             progress.startNewMeasurement(0);
-            // TODO Matthias: do not empty queue every time but break before
+            // TODO: do not empty queue every time but break before
             while (!explorationQueue.empty()) {
                 // Get the first state in the queue
                 ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.pop();
@@ -379,7 +379,7 @@ namespace storm {
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
                     setMarkovian(true);
                     // Add transition to target state with temporary value 0
-                    // TODO Matthias: what to do when there is no unique target state?
+                    // TODO: what to do when there is no unique target state?
                     matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>());
                     // Remember skipped state
                     skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
@@ -434,7 +434,7 @@ namespace storm {
                                         STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
 
                                         // Initialize bounds
-                                        // TODO Mathias: avoid hack
+                                        // TODO: avoid hack
                                         ValueType lowerBound = getLowerBound(state);
                                         ValueType upperBound = getUpperBound(state);
                                         heuristic->setBounds(lowerBound, upperBound);
@@ -522,12 +522,12 @@ namespace storm {
         template<typename ValueType, typename StateType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
             if (expectedTime) {
-                // TODO Matthias: handle case with no skipped states
+                // TODO: handle case with no skipped states
                 changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
                 return createModel(true);
             } else {
                 // Change model for probabilities
-                // TODO Matthias: make nicer
+                // TODO: make nicer
                 storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix;
                 storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling;
                 if (lowerBound) {
@@ -554,7 +554,7 @@ namespace storm {
                 } else {
                     // Build MA
                     // Compute exit rates
-                    // TODO Matthias: avoid computing multiple times
+                    // TODO: avoid computing multiple times
                     modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
                     std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices();
                     for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
@@ -573,7 +573,7 @@ namespace storm {
                     std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                     if (ma->hasOnlyTrivialNondeterminism()) {
                         // Markov automaton can be converted into CTMC
-                        // TODO Matthias: change components which were not moved accordingly
+                        // TODO: change components which were not moved accordingly
                         model = ma->convertToCtmc();
                     } else {
                         model = ma;
@@ -604,7 +604,7 @@ namespace storm {
             } else {
                 // Build MA
                 // Compute exit rates
-                // TODO Matthias: avoid computing multiple times
+                // TODO: avoid computing multiple times
                 modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
                 std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices();
                 for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
@@ -632,7 +632,7 @@ namespace storm {
                 }
                 if (ma->hasOnlyTrivialNondeterminism()) {
                     // Markov automaton can be converted into CTMC
-                    // TODO Matthias: change components which were not moved accordingly
+                    // TODO: change components which were not moved accordingly
                     model = ma->convertToCtmc();
                 } else {
                     model = ma;
@@ -770,7 +770,7 @@ namespace storm {
                 return result;
             }
 
-            // TODO Matthias: works only for <64 BEs!
+            // TODO: works only for <64 BEs!
             // WARNING: this code produces wrong results for more than 32 BEs
             /*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {
                 size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(i));
@@ -842,7 +842,7 @@ namespace storm {
                         STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide.");
                         state->setId(stateId);
                         // Update mapping to map to concrete state now
-                        // TODO Matthias: just change pointer?
+                        // TODO: just change pointer?
                         statesNotExplored[stateId] = std::make_pair(state, iter->second.second);
                         // We do not push the new state on the exploration queue as the pseudo state was already pushed
                         STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));

src/storm-dft/builder/ExplicitDFTModelBuilder.h

@@ -135,7 +135,7 @@ namespace storm {
                 size_t mappingOffset;
 
                 // A mapping from state ids to the row group indices in which they actually reside.
-                // TODO Matthias: avoid hack with fixed int type
+                // TODO: avoid hack with fixed int type
                 std::vector<uint_fast64_t> stateRemapping;
 
             private:
@@ -309,13 +309,13 @@ namespace storm {
             storm::storage::DFT<ValueType> const& dft;
 
             // General information for state generation
-            // TODO Matthias: use const reference
+            // TODO: use const reference
             std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
 
             // List with ids of relevant events which should be observed.
             std::set<size_t> const& relevantEvents;
 
-            //TODO Matthias: make changeable
+            //TODO: merge depending on relevant events
             const bool mergeFailedStates = true;
 
             // Heuristic used for approximation

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -33,7 +33,7 @@ namespace storm {
         template<typename ValueType, typename StateType>
         void DftNextStateGenerator<ValueType, StateType>::load(storm::storage::BitVector const& state) {
             // Load the state from bitvector
-            size_t id = 0; //TODO Matthias: set correct id
+            size_t id = 0; //TODO: set correct id
             this->state = std::make_shared<storm::storage::DFTState<ValueType>>(state, mDft, mStateGenerationInfo, id);
         }
 
@@ -144,6 +144,7 @@ namespace storm {
                     }
 
                     // Propagate dont cares
+                    // TODO: do not set DC for relevant events
                     while (relevantEvents.empty() && !queues.dontCarePropagationDone()) {
                         DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(*newState, queues);

src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@@ -24,7 +24,7 @@ namespace storm {
             // Optimizing DFT
             storm::storage::DFT<ValueType> dft = origDft.optimize();
 
-            // TODO Matthias: check that all paths reach the target state for approximation
+            // TODO: check that all paths reach the target state for approximation
 
             // Checking DFT
             if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
@@ -88,7 +88,7 @@ namespace storm {
             // Perform modularisation
             if(dfts.size() > 1) {
                 STORM_LOG_TRACE("Recursive CHECK Call");
-                // TODO Matthias: compute simultaneously
+                // TODO: compute simultaneously
                 dft_results results;
                 for (auto property : properties) {
                     if (!property->isProbabilityOperatorFormula()) {
@@ -97,7 +97,7 @@ namespace storm {
                         // Recursively call model checking
                         std::vector<ValueType> res;
                         for(auto const ft : dfts) {
-                            // TODO Matthias: allow approximation in modularisation
+                            // TODO: allow approximation in modularisation
                             dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0);
                             STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results");
                             res.push_back(boost::get<ValueType>(ftResults[0]));
@@ -143,7 +143,7 @@ namespace storm {
 
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents)  {
-            // TODO Matthias: use approximation?
+            // TODO: use approximation?
             STORM_LOG_TRACE("Build model via composition");
             std::vector<storm::storage::DFT<ValueType>> dfts;
             bool isAnd = true;
@@ -280,7 +280,7 @@ namespace storm {
                 storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
                 typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
 
-                // TODO Matthias: compute approximation for all properties simultaneously?
+                // TODO: compute approximation for all properties simultaneously?
                 std::shared_ptr<const storm::logic::Formula> property = properties[0];
                 if (properties.size() > 1) {
                     STORM_LOG_WARN("Computing approximation only for first property: " << *property);
@@ -295,12 +295,12 @@ namespace storm {
                         explorationTimer.start();
                     }
                     STORM_LOG_DEBUG("Building model...");
-                    // TODO Matthias refine model using existing model and MC results
+                    // TODO refine model using existing model and MC results
                     builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic);
                     explorationTimer.stop();
                     buildingTimer.start();
 
-                    // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one?
+                    // TODO: possible to do bisimulation on approximated model and not on concrete one?
 
                     // Build model for lower bound
                     STORM_LOG_DEBUG("Getting model for lower bound...");

src/storm-dft/storage/dft/DFTState.cpp

@@ -7,7 +7,7 @@ namespace storm {
 
         template<typename ValueType>
         DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
-            // TODO Matthias: use construct()
+            // TODO: use construct()
             
             // Initialize uses
             for(size_t spareId : mDft.getSpareIndices()) {