From bd367f89c75977d162a97cf161b51d9303360844 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 26 Nov 2013 21:34:46 +0100
Subject: [PATCH] Enabled model checking of PCTL properties for symbolic
 models.

Former-commit-id: a8e2fc6a9251cb680240b6adb5bbd5adcea22b2d
---
 src/storm.cpp | 40 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/storm.cpp b/src/storm.cpp
index a0d8006c9..b6dd20bc6 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -486,7 +486,7 @@ int main(const int argc, const char* argv[]) {
             storm::ir::Program program = storm::parser::PrismParserFromFile(programFile);
             std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
             model->printModelInformationToStream(std::cout);
-
+            
             if (s->isSet("mincmd")) {
                 if (model->getType() != storm::models::MDP) {
                     LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP.");
@@ -513,6 +513,44 @@ int main(const int argc, const char* argv[]) {
                     // Once we are done with the formula, delete it.
                     delete formulaPtr;
                 }
+            } else if (s->isSet("prctl")) {
+                // Determine which engine is to be used to choose the right model checker.
+				LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString());
+                
+				// Depending on the model type, the appropriate model checking procedure is chosen.
+				storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
+                
+				switch (model->getType()) {
+                    case storm::models::DTMC:
+                        LOG4CPLUS_INFO(logger, "Model is a DTMC.");
+                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
+                        checkPrctlFormulae(*modelchecker);
+                        break;
+                    case storm::models::MDP:
+                        LOG4CPLUS_INFO(logger, "Model is an MDP.");
+                        modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
+                        checkPrctlFormulae(*modelchecker);
+                        break;
+                    case storm::models::CTMC:
+                        LOG4CPLUS_INFO(logger, "Model is a CTMC.");
+                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
+                        break;
+                    case storm::models::CTMDP:
+                        LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
+                        LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
+                        break;
+                    case storm::models::MA:
+                        LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
+                        break;
+                    case storm::models::Unknown:
+                    default:
+                        LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
+                        break;
+				}
+                
+				if (modelchecker != nullptr) {
+					delete modelchecker;
+				}
             }
         }