Minor fixes.

Former-commit-id: f2298d312a

src/adapters/ExplicitModelAdapter.h

@@ -85,9 +85,18 @@ namespace storm {
             std::shared_ptr<storm::models::AbstractModel<double>> getModel(std::string const& constantDefinitionString = "", std::string const& rewardModelName = "");
             
         private:
-            // Copying/Moving is disabled for this class
-            ExplicitModelAdapter(ExplicitModelAdapter const& other) { }
-            ExplicitModelAdapter(ExplicitModelAdapter && other) { }
+            /*!
+             * Private copy constructor to disable copy-construction (and move-construction) of this class.
+             *
+             * @param other The object to copy-construct from.
+             */
+            ExplicitModelAdapter(ExplicitModelAdapter const& other);
+            /*!
+             * Private copy-assignment to disable copy-assignment (and move-assignment) of this class.
+             *
+             * @param other The object to copy-assign from.
+             */
+            ExplicitModelAdapter operator=(ExplicitModelAdapter const& other);
             
             /*!
              * The precision that is to be used for sanity checks internally.

src/modelchecker/prctl/AbstractModelChecker.h

@@ -153,22 +153,18 @@ public:
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
 		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
-		storm::storage::BitVector* result = nullptr;
+		storm::storage::BitVector result;
 		try {
 			result = stateFormula.check(*this);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
 			for (auto initialState : this->getInitialStates()) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
-				std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
+				std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
 			}
-			delete result;
 		} 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 (result != nullptr) {
-				delete result;
-			}
 		}
 		std::cout << std::endl << "-------------------------------------------" << std::endl;
 	}
@@ -183,21 +179,18 @@ public:
 		std::cout << std::endl;
 		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
 		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
-		std::vector<Type>* result = nullptr;
+		std::vector<Type> result;
 		try {
 			result = this->checkNoBoundOperator(noBoundFormula);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
 			for (auto initialState : this->getInitialStates()) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
+				std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
 			}
-			delete result;
 		} catch (std::exception& e) {
 			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
+            LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
 		}
 		std::cout << std::endl << "-------------------------------------------" << std::endl;
 	}

src/storage/LabeledProbabilities.h

@@ -0,0 +1,79 @@
+/*
+ * LabeledProbabilities.h
+ *
+ *  Created on: 26.09.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_STORAGE_LABELEDPROBABILITIES_H
+#define STORM_STORAGE_LABELEDPROBABILITIES_H
+
+namespace storm {
+    namespace storage {
+    
+        // This class provides the functionality to store a list of probabilities, each of which is labeled with a list
+        // of labels.
+        template<class Container, class ValueType>
+        class LabeledProbabilities {
+        public:
+            /*!
+             * Default-constructs an empty object.
+             */
+            LabeledProbabilities() : probabilityLabelList() {
+                // Intentionally left empty.
+            }
+            
+            /*!
+             * Adds a probability to the list of labeled probabilities.
+             *
+             * @return A reference to the list of labels that is associated with the given probability.
+             */
+            Container<uint_fast64_t>& addProbability(ValueType probability) {
+                probabilityLabelList.emplace_back(probability, Container<uint_fast64_t>());
+                return probabilityLabelList.back().second;
+            }
+            
+            /*!
+             * Returns an iterator pointing to the first labeled probability.
+             *
+             * @return An iterator pointing to the first labeled probability.
+             */
+            Container<std::pair<ValueType, Container<uint_fast64_t>>>::iterator begin() {
+                return probabilityLabelList.begin();
+            }
+            
+            /*!
+             * Returns an iterator pointing past the last labeled probability.
+             *
+             * @return An iterator pointing past the last labeled probability.
+             */
+            Container<std::pair<ValueType, Container<uint_fast64_t>>>::const_iterator end() {
+                return probabilityLabelList.end();
+            }
+            
+            /*!
+             * Returns a const iterator pointing to the first labeled probability.
+             *
+             * @return A const iterator pointing to the first labeled probability.
+             */
+            Container<std::pair<ValueType, Container<uint_fast64_t>>>::const_iterator begin() const {
+                return probabilityLabelList.begin();
+            }
+            
+            /*!
+             * Returns a const iterator pointing past the last labeled probability.
+             *
+             * @return A const iterator pointing past the last labeled probability.
+             */
+            Container<std::pair<ValueType, Container<uint_fast64_t>>>::const_iterator end() const {
+                return probabilityLabelList.end();
+            }
+            
+        private:
+            // The actual storage used to store the list of probabilities and the associated labels.
+            Container<std::pair<ValueType, Container<uint_fast64_t>>> probabilityLabelList;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_LABELEDPROBABILITIES_H */