From ad86c22249097d6c8d0ffb79b8a102dc5974d365 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Thu, 23 May 2013 13:22:44 +0200
Subject: [PATCH] Replaced positional arguments by --explicit and --symbolic.

---
 src/storm.cpp            | 56 ++++++++++++++++++++++------------------
 src/utility/Settings.cpp | 14 +++++-----
 2 files changed, 39 insertions(+), 31 deletions(-)

diff --git a/src/storm.cpp b/src/storm.cpp
index 548399d38..932f66a5d 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -283,32 +283,38 @@ int main(const int argc, const char* argv[]) {
 
 		// Now, the settings are receivd and the model is parsed.
 		storm::settings::Settings* s = storm::settings::instance();
-		storm::parser::AutoParser<double> parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
-
-		LOG4CPLUS_DEBUG(logger, s->getString("matrixlib"));
-
-
-		// Depending on the model type, the respective model checking procedure is chosen.
-		switch (parser.getType()) {
-		case storm::models::DTMC:
-			LOG4CPLUS_INFO(logger, "Model was detected as DTMC");
-			checkDtmc(parser.getModel<storm::models::Dtmc<double>>());
-			break;
-		case storm::models::MDP:
-			LOG4CPLUS_INFO(logger, "Model was detected as MDP");
-			checkMdp(parser.getModel<storm::models::Mdp<double>>());
-			break;
-		case storm::models::CTMC:
-		case storm::models::CTMDP:
-			// Continuous time model checking is not implemented yet
-			LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm.");
-			break;
-		case storm::models::Unknown:
-		default:
-			LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
-			break;
+		if (s->isSet("explicit")) {
+			std::vector<std::string> args = s->get<std::vector<std::string>>("explicit");
+			storm::parser::AutoParser<double> parser(args[0], args[1], s->getString("staterew"), s->getString("transrew"));
+
+			LOG4CPLUS_DEBUG(logger, s->getString("matrixlib"));
+
+
+			// Depending on the model type, the respective model checking procedure is chosen.
+			switch (parser.getType()) {
+			case storm::models::DTMC:
+				LOG4CPLUS_INFO(logger, "Model was detected as DTMC");
+				checkDtmc(parser.getModel<storm::models::Dtmc<double>>());
+				break;
+			case storm::models::MDP:
+				LOG4CPLUS_INFO(logger, "Model was detected as MDP");
+				checkMdp(parser.getModel<storm::models::Mdp<double>>());
+				break;
+			case storm::models::CTMC:
+			case storm::models::CTMDP:
+				// Continuous time model checking is not implemented yet
+				LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm.");
+				break;
+			case storm::models::Unknown:
+			default:
+				LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
+				break;
+			}
+		}
+		if (s->isSet("symbolic")) {
+			std::string arg = s->getString("symbolic");
+			Pr
 		}
-
 
 		cleanUp();
 
diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp
index ae0db6f4b..1a071d3c0 100644
--- a/src/utility/Settings.cpp
+++ b/src/utility/Settings.cpp
@@ -54,10 +54,6 @@ Settings::Settings(int const argc, char const * const argv[], char const * const
 		// Initially fill description objects.
 		this->initDescriptions();
 
-		// Take care of positional arguments.
-		Settings::positional.add("trafile", 1);
-		Settings::positional.add("labfile", 1);
-
 		// Check module triggers, add corresponding options.
 		std::map< std::string, std::list< std::string > > options;
 
@@ -122,6 +118,12 @@ Settings::Settings(int const argc, char const * const argv[], char const * const
 	}
 }
 
+void checkExplicit(const std::vector<std::string>& filenames) {
+	if (filenames.size() != 2) {
+		throw storm::exceptions::InvalidSettingsException() << "--explicit must be given exactly two filenames";
+	}
+}
+
 /*!
  *	Initially fill options_description objects.
  */
@@ -135,8 +137,8 @@ void Settings::initDescriptions() {
 		("trace", "be extremely verbose, expect lots of output")
 		("logfile,l", bpo::value<std::string>(), "name of the log file")
 		("configfile,c", bpo::value<std::string>(), "name of config file")
-		("trafile", bpo::value<std::string>()->required(), "name of the .tra file")
-		("labfile", bpo::value<std::string>()->required(), "name of the .lab file")
+		("explicit", bpo::value<std::vector<std::string>>()->notifier(&checkExplicit), "name of transition and labeling file")
+		("symbolic", bpo::value<std::string>(), "name of prism file")
 		("prctl", bpo::value<std::string>(), "text file containing prctl formulas")
 		("csl", bpo::value<std::string>(), "text file containing csl formulas")
 		("ltl", bpo::value<std::string>(), "text file containing ltl formulas")