Merge branch 'LtlParser'

Conflicts:
	src/storm.cpp

src/modelchecker/AbstractModelChecker.h

@@ -116,6 +116,20 @@ public:
 		}
 	}
 
+	/*!
+	 * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula)
+	 * for all initial states, i.e. states that carry the atomic proposition "init".
+	 *
+	 * @param formula The formula to be checked.
+	 */
+	void check(storm::property::prctl::AbstractPrctlFormula<Type> const& formula) const {
+		if (dynamic_cast<storm::property::prctl::AbstractStateFormula<Type> const*>(&formula) != nullptr) {
+			this->check(static_cast<storm::property::prctl::AbstractStateFormula<Type> const&>(formula));
+		} else if (dynamic_cast<storm::property::prctl::AbstractNoBoundOperator<Type> const*>(&formula) != nullptr) {
+			this->check(static_cast<storm::property::prctl::AbstractNoBoundOperator<Type> const&>(formula));
+		}
+	}
+
 	/*!
 	 * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e.
 	 * states that carry the atomic proposition "init".

src/parser/PrctlFileParser.cpp

@@ -16,69 +16,35 @@
 namespace storm {
 namespace parser {
 
-PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library) {
-	//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
-	storm::modelchecker::SparseDtmcPrctlModelChecker<double>* modelChecker = nullptr;
-	switch(library) {
-	//case EIGEN:
-		//Eigen Model Checker is not completely implemented at the moment, thus using Eigen is not possible...
-		//Current behaviour: Fall back to GMMXX...
-		//modelChecker = new storm::modelchecker::EigenDtmcPrctlModelChecker<double>(dtmc);
-	//	break;
-	case GMMXX:
-	default:					//Note: GMMXX is default, hence default branches here, too.
-		modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-		break;
-	}
-
-	//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
-	check(filename, modelChecker);
-	delete modelChecker;
-}
-
-PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library) {
-	//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
-	storm::modelchecker::SparseMdpPrctlModelChecker<double>* modelChecker = nullptr;
-	switch(library) {
-	//case EIGEN:
-		//Eigen MDP Model Checker is not implemented yet
-		//Current behaviour: Fall back to GMMXX...
-	//	break;
-	case GMMXX:
-	default:					//Note: GMMXX is default, hence default branches here, too.
-		modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
-		break;
-	}
-
-	//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
-	check(filename, modelChecker);
-	delete modelChecker;
+PrctlFileParser::PrctlFileParser() {
+	//Intentionally left empty
 }
 
 PrctlFileParser::~PrctlFileParser() {
 	//intentionally left empty
 }
 
-void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractModelChecker<double>* modelChecker) {
+std::list<storm::property::prctl::AbstractPrctlFormula<double>*> PrctlFileParser::parseFormulas(std::string filename) {
 	// Open file
 	std::ifstream inputFileStream(filename, std::ios::in);
 
+	if (!inputFileStream.is_open()) {
+		std::string message = "Error while opening file ";
+		throw storm::exceptions::FileIoException() << message << filename;
+	}
+
+	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> result;
+
 	while(!inputFileStream.eof()) {
 		std::string line;
 		//The while loop reads the input file line by line
 		while (std::getline(inputFileStream, line)) {
 			PrctlParser parser(line);
-			storm::property::prctl::AbstractStateFormula<double>* stateFormula = dynamic_cast<storm::property::prctl::AbstractStateFormula<double>*>(parser.getFormula());
-			if (stateFormula != nullptr) {
-				modelChecker->check(*stateFormula);
-			}
-			storm::property::prctl::AbstractNoBoundOperator<double>* noBoundFormula = dynamic_cast<storm::property::prctl::AbstractNoBoundOperator<double>*>(parser.getFormula());
-			if (noBoundFormula != nullptr) {
-				modelChecker->check(*noBoundFormula);
-			}
-			delete parser.getFormula();
+			result.push_back(parser.getFormula());
 		}
 	}
+
+	return result;
 }
 
 } /* namespace parser */

src/parser/PrctlFileParser.h

@@ -8,10 +8,9 @@
 #ifndef STORM_PARSER_PRCTLFILEPARSER_H_
 #define STORM_PARSER_PRCTLFILEPARSER_H_
 
-#include "models/Dtmc.h"
-#include "models/Mdp.h"
 #include "formula/Prctl.h"
-#include "modelchecker/AbstractModelChecker.h"
+
+#include <list>
 
 namespace storm {
 namespace parser {
@@ -25,46 +24,25 @@ namespace parser {
  */
 class PrctlFileParser {
 public:
-	enum libraries {
-		GMMXX,
-		EIGEN
-	};
-
-	/*!
-	 * Reads a given file of formulas and checks each of these against a given DTMC.
-	 *
-	 * @param filename The name of the file to parse
-	 * @param dtmc		 The DTMC model to check
-	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx)
-	 */
-	PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library=GMMXX);
-
 	/*!
-	 * Reads a given file of formulas and checks each of these against a given MDP.
-	 *
-	 * @param filename The name of the file to parse
-	 * @param mdp		 The MDP model to check
-	 * @param library  Specifies the library that should perform the algebraic operations during model checking (default is GMMxx, which at the moment also is the only implemented version...)
+	 * Constructor
 	 */
-	PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library=GMMXX);
+	PrctlFileParser();
 
-protected:
 	/*!
-	 * Does the actual checking.
-	 * This procedure is equal for all model types (only the model checker is different, so it has to be created in
-	 * different methods beforehand)
+	 * Destructor.
+	 * At this time, empty
 	 *
-	 * @param filename     The name of the file to parse
-	 * @param modelChecker The model checker that checks the formula (has to know its model!)
 	 */
-	void check(std::string filename, storm::modelchecker::AbstractModelChecker<double>* modelChecker);
+	virtual ~PrctlFileParser();
 
 	/*!
-	 * Destructor.
-	 * At this time, empty
+	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
 	 *
+	 * @param filename
+	 * @return The list of parsed formulas
 	 */
-	virtual ~PrctlFileParser();
+	std::list<storm::property::prctl::AbstractPrctlFormula<double>*> parseFormulas(std::string filename);
 };
 
 } /* namespace parser */

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"
@@ -108,10 +110,6 @@ bool parseOptions(const int argc, const char* argv[]) {
 		std::cout << storm::settings::help;
 		return false;
 	}
-	if (s->isSet("test-prctl")) {
-		storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
-		return false;
-	}
 
 	if (s->isSet("verbose")) {
 		logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
@@ -139,322 +137,100 @@ void cleanUp() {
 	// nothing here
 }
 
-void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-
-	storm::property::prctl::Ap<double>* oneFormula = new storm::property::prctl::Ap<double>("one");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(oneFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	oneFormula = new storm::property::prctl::Ap<double>("two");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(oneFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	oneFormula = new storm::property::prctl::Ap<double>("three");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(oneFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	storm::property::prctl::Ap<double>* done = new storm::property::prctl::Ap<double>("done");
-	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(done);
-	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-	delete mc;
+/*!
+ * Factory style creation of new DTMC model checker
+ * @param dtmc The Dtmc that the model checker will check
+ * @return
+ */
+storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double>& dtmc) {
+	storm::settings::Settings* s = storm::settings::instance();
+	if (s->getString("matrixlib") == "gmm++") {
+		return new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	}
-
-void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
-	storm::property::prctl::Ap<double>* observe0Greater1Formula = new storm::property::prctl::Ap<double>("observe0Greater1");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(observe0Greater1Formula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-	mc->check(*probFormula);
-	delete probFormula;
-
-	storm::property::prctl::Ap<double>* observeIGreater1Formula = new storm::property::prctl::Ap<double>("observeIGreater1");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(observeIGreater1Formula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	storm::property::prctl::Ap<double>* observeOnlyTrueSenderFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(observeOnlyTrueSenderFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	delete mc;
+	// The control flow should never reach this point, as there is a default setting for matrixlib (gmm++)
+	std::string message = "No matrix library suitable for DTMC model checking has been set";
+	throw storm::exceptions::InvalidSettingsException() << message;
+	return nullptr;
 }
 
-void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast64_t n) {
-	storm::property::prctl::Ap<double>* electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(electedFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
-
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-	mc->check(*probFormula);
-	delete probFormula;
-
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), electedFormula, n * 4);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(electedFormula);
-	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-
-	delete mc;
+/*!
+ * Factory style creation of new MDP model checker
+ * @param mdp The Dtmc that the model checker will check
+ * @return
+ */
+storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double>& mdp) {
+	storm::settings::Settings* s = storm::settings::instance();
+	if (s->getString("matrixlib") == "gmm++") {
+		return new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
 	}
-
-void testCheckingDice(storm::models::Mdp<double>& mdp) {
-	storm::property::prctl::Ap<double>* twoFormula = new storm::property::prctl::Ap<double>("two");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-
-	twoFormula = new storm::property::prctl::Ap<double>("two");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("three");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("three");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("four");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("four");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("five");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("five");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("six");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	twoFormula = new storm::property::prctl::Ap<double>("six");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(twoFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	storm::property::prctl::Ap<double>* doneFormula = new storm::property::prctl::Ap<double>("done");
-	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(doneFormula);
-	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-
-	doneFormula = new storm::property::prctl::Ap<double>("done");
-	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(doneFormula);
-	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-
-	delete mc;
+	// The control flow should never reach this point, as there is a default setting for matrixlib (gmm++)
+	std::string message = "No matrix library suitable for MDP model checking has been set";
+	throw storm::exceptions::InvalidSettingsException() << message;
+	return nullptr;
 }
 
-void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
-	storm::property::prctl::Ap<double>* electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(electedFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
-
-	mc->check(*probMinFormula);
-	delete probMinFormula;
-
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(electedFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probMaxFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probMaxFormula);
-	delete probMaxFormula;
-
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(electedFormula, 25);
-	probMinFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
-
-	mc->check(*probMinFormula);
-	delete probMinFormula;
-
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(electedFormula, 25);
-	probMaxFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
-
-	mc->check(*probMaxFormula);
-	delete probMaxFormula;
+/*!
+ * Calls the check method of a model checker for all PRCTL formulas in a given list.
+ *
+ * @param formulaList The list of PRCTL formulas
+ * @param mc the model checker
+ */
+void checkPrctlFormulasAgainstModel(std::list<storm::property::prctl::AbstractPrctlFormula<double>*>& formulaList,
+									storm::modelchecker::AbstractModelChecker<double> const& mc) {
+	for ( auto formula : formulaList ) {
+		mc.check(*formula);
 
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(electedFormula);
-	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+		//TODO: Should that be done here or in a second iteration through the list?
+		delete formula;
+	}
+	formulaList.clear();
+}
 
-	mc->check(*rewardFormula);
-	delete rewardFormula;
+/*!
+ * Check method for DTMCs
+ * @param dtmc Reference to the DTMC to check
+ */
+void checkMdp(std::shared_ptr<storm::models::Mdp<double>> mdp) {
+	mdp->printModelInformationToStream(std::cout);
+	storm::settings::Settings* s = storm::settings::instance();
+	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"));
 
-	electedFormula = new storm::property::prctl::Ap<double>("elected");
-	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(electedFormula);
-	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+		storm::modelchecker::AbstractModelChecker<double>* mc = createPrctlModelChecker(*mdp);
 
-	mc->check(*rewardFormula);
-	delete rewardFormula;
+		checkPrctlFormulasAgainstModel(formulaList, *mc);
 
 		delete mc;
 	}
 
-void testCheckingConsensus(storm::models::Mdp<double>& mdp) {
-	storm::property::prctl::Ap<double>* finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(finishedFormula);
-	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::Ap<double>* allCoinsEqual0Formula = new storm::property::prctl::Ap<double>("all_coins_equal_0");
-	storm::property::prctl::And<double>* conjunctionFormula = new storm::property::prctl::And<double>(finishedFormula, allCoinsEqual0Formula);
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::Ap<double>* allCoinsEqual1Formula = new storm::property::prctl::Ap<double>("all_coins_equal_1");
-	conjunctionFormula = new storm::property::prctl::And<double>(finishedFormula, allCoinsEqual1Formula);
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::Ap<double>* agree = new storm::property::prctl::Ap<double>("agree");
-	storm::property::prctl::Not<double>* notAgree = new storm::property::prctl::Not<double>(agree);
-	conjunctionFormula = new storm::property::prctl::And<double>(finishedFormula, notAgree);
-	eventuallyFormula = new storm::property::prctl::Eventually<double>(conjunctionFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(finishedFormula, 50);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(finishedFormula, 50);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
-
-	mc->check(*probFormula);
-	delete probFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(finishedFormula);
-	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-
-	finishedFormula = new storm::property::prctl::Ap<double>("finished");
-	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(finishedFormula);
-	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
-
-	mc->check(*rewardFormula);
-	delete rewardFormula;
-
-	delete mc;
+	if(s->isSet("csl")) {
+		LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on MDPs.");
+	}
 }
 
 /*!
- * Simple testing procedure.
+ * Check method for DTMCs
+ * @param dtmc Reference to the DTMC to check
  */
-void testChecking() {
+void checkDtmc(std::shared_ptr<storm::models::Dtmc<double>> dtmc) {
+	dtmc->printModelInformationToStream(std::cout);
 	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 (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"));
 
-	if (parser.getType() == storm::models::DTMC) {
-		std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
-		dtmc->printModelInformationToStream(std::cout);
+		storm::modelchecker::AbstractModelChecker<double>* mc = createPrctlModelChecker(*dtmc);
 
-		// 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);
+		checkPrctlFormulasAgainstModel(formulaList, *mc);
 
-        // testCheckingDice(*mdp);
-		// testCheckingAsynchLeader(*mdp);
-		// testCheckingConsensus(*mdp);
-	} else {
-		std::cout << "Input is neither a DTMC nor an MDP." << std::endl;
+		delete mc;
+	}
+
+	if(s->isSet("csl")) {
+		LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs.");
 	}
 }
 
@@ -468,16 +244,46 @@ int main(const int argc, const char* argv[]) {
 	printHeader(argc, argv);
 
 	initializeLogger();
-	if (!parseOptions(argc, argv)) {
-		return 0;
-	}
-	setUp();
 
+	setUp();
 
 	try {
 		LOG4CPLUS_INFO(logger, "StoRM was invoked.");
 
-		testChecking();
+		// Parse options
+		if (!parseOptions(argc, argv)) {
+			// If false is returned, the program execution is stopped here
+			// E.g. if the user asked to see the help text
+			return 0;
+		}
+
+		// 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;
+		}
 
 
 		cleanUp();

src/utility/Settings.cpp

@@ -134,9 +134,11 @@ void Settings::initDescriptions() {
 		("debug", "be very verbose, intended for debugging")
 		("logfile,l", bpo::value<std::string>(), "name of the log file")
 		("configfile,c", bpo::value<std::string>(), "name of config file")
-		("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>(), "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")
 		("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")

test/functional/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -81,8 +81,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
 
-	ASSERT_EQ(dtmc->getNumberOfStates(), 8607);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460);
+	ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
@@ -135,8 +135,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
 
-	ASSERT_EQ(dtmc->getNumberOfStates(), 12400);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894);
+	ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 

test/functional/die/testFormulas.prctl

@@ -0,0 +1,4 @@
+P=? [ F one ]
+P=? [ F two ]
+P=? [ F three ]
+R=? [ F done ]