Fixed some compile errors originating from the introductionof the new storm::storage::VectorSet.

- Also handled the case	of a missing --prctl while using the counterexample generation.
- Remark: Some documentation for the VectorSet would have been nice.


Former-commit-id: c687b67454

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -20,7 +20,7 @@ extern "C" {
 #endif
 
 #include "src/models/Mdp.h"
-#include "src/ir/program.h"
+#include "src/ir/Program.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidStateException.h"

src/models/Dtmc.h

@@ -142,7 +142,7 @@ public:
 					  	  	  	  	  	  storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates),
 					  	  	  	  	  	  boost::optional<std::vector<T>>(),
 					  	  	  	  	  	  boost::optional<storm::storage::SparseMatrix<T>>(),
-					  	  	  	  	  	  boost::optional<std::vector<std::set<uint_fast64_t>>>());
+					  	  	  	  	  	  boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
 		}
 
 		// Does the vector have the right size?
@@ -159,7 +159,6 @@ public:
 
 		// 1. Get all necessary information from the old transition matrix
 		storm::storage::SparseMatrix<T> 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 
@@ -276,16 +275,16 @@ public:
 			newTransitionRewards = newTransRewards;
 		}
 
-		boost::optional<std::vector<std::set<uint_fast64_t>>> newChoiceLabels;
+		boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> newChoiceLabels;
 		if(this->hasChoiceLabels()) {
 
 			// Get the choice label sets and move the needed values to the front.
-			std::vector<std::set<uint_fast64_t>> newChoice(this->getChoiceLabeling());
+			std::vector<storm::storage::VectorSet<uint_fast64_t>> 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<uint_fast64_t>();
+			newChoice[newStateCount - 1] = storm::storage::VectorSet<uint_fast64_t>();
 
 			newChoiceLabels = newChoice;
 		}

src/storm.cpp

@@ -260,13 +260,17 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 
 /*!
  * Handles the counterexample generation control.
+ *
+ * @param parser An AutoParser to get the model from.
  */
  void generateCounterExample(storm::parser::AutoParser<double> parser) {
 	LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
 	LOG4CPLUS_INFO(logger, "Testing inputs...");
 
+	storm::settings::Settings* s  = storm::settings::Settings::getInstance();
+
 	//First test output directory.
-	std::string outPath = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
+	std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
 	if(outPath.back() != '/' && outPath.back() != '\\') {
 		LOG4CPLUS_ERROR(logger, "The output path is not valid.");
 		return;
@@ -289,13 +293,18 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 	LOG4CPLUS_INFO(logger, "Model is a DTMC.");
 
 	// Get specified PRCTL formulas.
-	std::string const chosenPrctlFile = storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgument(0).getValueAsString();
+	if(!s->isSet("prctl")) {
+		LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
+		return;
+	}
+
+	std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
 	LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
 	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> 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.");
+		LOG4CPLUS_ERROR(logger, "No PRCTL formula found.");
 		return;
 	}