Basic structure for central model checking method in storm.cpp

src/parser/PrctlFileParser.cpp

@@ -24,7 +24,7 @@ PrctlFileParser::~PrctlFileParser() {
 	//intentionally left empty
 }
 
-std::list<storm::property::prctl::AbstractPrctlFormula<double>*> parseFormulas(std::string filename) {
+std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser::parseFormulas(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> result;

src/storm.cpp

@@ -31,6 +31,8 @@
 #include "src/utility/ErrorHandling.h"
 #include "src/formula/Prctl.h"
 
+#include "src/parser/PrctlFileParser.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 #include "log4cplus/consoleappender.h"
@@ -432,6 +434,18 @@ void testCheckingConsensus(storm::models::Mdp<double>& mdp) {
 	delete mc;
 }
 
+/*!
+ * Check method for DTMCs
+ * @param dtmc Reference to the DTMC to check
+ */
+void checkDtmc(std::shared_ptr<storm::models::Dtmc<double>> dtmc) {
+	dtmc->printModelInformationToStream(std::cout);
+}
+
+void checkMdp(std::shared_ptr<storm::models::Mdp<double>> mdp) {
+	mdp->printModelInformationToStream(std::cout);
+}
+
 /*!
  * Simple testing procedure.
  */
@@ -439,22 +453,26 @@ void testChecking() {
 	storm::settings::Settings* s = storm::settings::instance();
 	storm::parser::AutoParser<double> parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
 
-	if (parser.getType() == storm::models::DTMC) {
-		std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
-		dtmc->printModelInformationToStream(std::cout);
-
-		// testCheckingDie(*dtmc);
-		// testCheckingCrowds(*dtmc);
-		// testCheckingSynchronousLeader(*dtmc, 6);
-	} else if (parser.getType() == storm::models::MDP) {
-		std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
-		mdp->printModelInformationToStream(std::cout);
-
-        // testCheckingDice(*mdp);
-		// testCheckingAsynchLeader(*mdp);
-		// testCheckingConsensus(*mdp);
-	} else {
-		std::cout << "Input is neither a DTMC nor an MDP." << std::endl;
+	if (s->isSet("prctl")) {
+		LOG4CPLUS_INFO(logger, "Parsing prctl file"+ s->getString("prctl"));
+		storm::parser::PrctlFileParser fileParser;
+		std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = fileParser.parseFormulas(s->getString("prctl"));
+
+	}
+
+
+	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;
+	default:
+		LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
+		break;
 	}
 }
 

src/utility/Settings.cpp

@@ -137,6 +137,9 @@ void Settings::initDescriptions() {
 		("test-prctl", bpo::value<std::string>(), "name of prctl file")
 		("trafile", bpo::value<std::string>()->required(), "name of the .tra file")
 		("labfile", bpo::value<std::string>()->required(), "name of the .lab file")
+		("prctl", bpo::value<std::string>()->default_value(""), "text file containing prctl formulas")
+		("csl", bpo::value<std::string>()->default_value(""), "text file containing csl formulas")
+		("ltl", bpo::value<std::string>()->default_value(""), "text file containing ltl formulas")
 		("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
 		("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
 		("fix-deadlocks", "insert self-loops for states without outgoing transitions")