Fixed the StringValidator for the constants option

Fixed a bug in the MinimalLabelSetGenerator.h where a non static variable was initialized
Added the new constants option in storm.cpp


Former-commit-id: e73e69b1ce

src/adapters/ExplicitModelAdapter.cpp

@@ -20,6 +20,7 @@
 #include <boost/algorithm/string.hpp>
 
 #include <sstream>
+#include <ostream>
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -27,7 +28,7 @@ extern log4cplus::Logger logger;
 
 bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
 	instance->addOption(storm::settings::OptionBuilder("ExplicitModelAdapter", "constants", "", "Specifies the constant replacements to use in Explicit Models").addArgument(storm::settings::ArgumentBuilder::createStringArgument("constantString", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3").addValidationFunctionString(
-		[] (std::string const& s) -> bool {
+		[] (std::string const s, std::string& errorMessageTarget) -> bool {
 			// since regex is not yet implemented in gccs C++11, we have to check by hand
 			std::vector<std::string> constants;
 			// split for single assignment expressions
@@ -36,18 +37,27 @@ bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::register
 				std::vector<std::string> constant;
 				boost::split(constant, *it, boost::is_any_of("="));
 				if (constant.size() != 2) {
+					std::ostringstream stream;
+					stream << "Expected one \"=\" in constant definition: \"" << *it << "\"" << std::endl; 
+					errorMessageTarget.append(stream.str());
 					return false;
 				}
 				// Constant Name check
 				bool error = false;
-				std::for_each(constant.at(0).cbegin(), constant.at(0).cend(), [&error] (const std::string::value_type value) -> void {
+				std::for_each(constant.at(0).cbegin(), constant.at(0).cend(), [&error, &errorMessageTarget] (const std::string::value_type value) -> void {
 					if (!(('a' <= value && value <= 'z') || ('A' <= value && value <= 'Z') || ('0' <= value && value <= '9'))) {
+						std::ostringstream stream;
+						stream << "Illegal character in constant name: \"" << value << "\"" << std::endl; 
+						errorMessageTarget.append(stream.str());
 						error = true;
 					}
 				});
 				// Value Check
-				std::for_each(constant.at(1).cbegin(), constant.at(1).cend(), [&error] (const std::string::value_type value) -> void {
+				std::for_each(constant.at(1).cbegin(), constant.at(1).cend(), [&error, &errorMessageTarget] (const std::string::value_type value) -> void {
 					if (!(('a' <= value && value <= 'z') || ('A' <= value && value <= 'Z') || ('0' <= value && value <= '9'))) {
+						std::ostringstream stream;
+						stream << "Illegal character in constant value: \"" << value << "\"" << std::endl; 
+						errorMessageTarget.append(stream.str());
 						error = true;
 					}
 				});

src/counterexamples/MinimalLabelSetGenerator.h

@@ -71,7 +71,9 @@ namespace storm {
                 std::unordered_map<uint_fast64_t, uint_fast64_t> stateToProbabilityVariableIndexMap;
                 std::unordered_map<uint_fast64_t, uint_fast64_t> problematicStateToVariableIndexMap;
                 std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, uint_fast64_t, PairHash> problematicTransitionToVariableIndexMap;
-                uint_fast64_t nextFreeVariableIndex = 0;
+                uint_fast64_t nextFreeVariableIndex;
+
+				VariableInformation() : nextFreeVariableIndex(0) {}
             };
 
             /*!

src/storm.cpp

@@ -332,7 +332,8 @@ int main(const int argc, const char* argv[]) {
 		} else if (s->isSet("symbolic")) {
 			std::string const arg = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
 			storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg));
-			std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel("K=1");
+			std::string const constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
+			std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel(constants);
 			model->printModelInformationToStream(std::cout);
             
             if (model->getType() == storm::models::MDP) {