From f7a7ea8383b8d73c28f99eaa60e2644b21c4e2c9 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Sat, 21 Sep 2013 22:08:52 +0200
Subject: [PATCH] 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: e73e69b1cef6e2b832f9b52cc8b37c4558ff8d71
---
 src/adapters/ExplicitModelAdapter.cpp          | 16 +++++++++++++---
 src/counterexamples/MinimalLabelSetGenerator.h |  4 +++-
 src/storm.cpp                                  |  3 ++-
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp
index 417d5cf40..004a6acdb 100644
--- a/src/adapters/ExplicitModelAdapter.cpp
+++ b/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;
 					}
 				});
diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h
index de9a71b94..c182891aa 100644
--- a/src/counterexamples/MinimalLabelSetGenerator.h
+++ b/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) {}
             };
 
             /*!
diff --git a/src/storm.cpp b/src/storm.cpp
index b3442375e..48912384e 100644
--- a/src/storm.cpp
+++ b/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) {