Made choiceIndices work in ExplicitModelAdapter, added code to somehow use --symbolic (parse model, show model information)

src/adapters/ExplicitModelAdapter.cpp

@@ -73,8 +73,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 			case storm::ir::Program::MDP:
 			{
 				std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildNondeterministicMatrix();
-				std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
-				return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Mdp<double>(matrix, stateLabeling, choiceIndices, stateRewards, this->transitionRewards));
+				return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Mdp<double>(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards));
 				break;
 			}
 			case storm::ir::Program::CTMDP:
@@ -493,9 +492,12 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 			this->transitionRewards = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(this->numberOfChoices, allStates.size()));
 			this->transitionRewards->initialize(this->numberOfTransitions);
 		}
+		this->choiceIndices = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>());
+		this->choiceIndices->reserve(allStates.size());
 		// Build matrix.
 		uint_fast64_t nextRow = 0;
 		for (uint_fast64_t state = 0; state < this->allStates.size(); state++) {
+			this->choiceIndices->push_back(transitionMap[state].size());
 			for (auto choice : transitionMap[state]) {
 				for (auto it : choice.second) {
 					result->addNextValue(nextRow, it.first, it.second);

src/adapters/ExplicitModelAdapter.h

@@ -190,6 +190,7 @@ private:
 	std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
 	uint_fast64_t numberOfTransitions;
 	uint_fast64_t numberOfChoices;
+        std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
 	std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
 
 	/*!

src/parser/PrismParser.cpp

@@ -9,7 +9,7 @@
 
 #include "src/utility/OsDetection.h"
 
-#include "src/parser/PrismParser/PrismGrammar.h"
+#include "src/parser/prismparser/PrismGrammar.h"
 
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"

src/parser/prismparser/PrismGrammar.cpp

@@ -9,14 +9,14 @@
 
 #include "src/utility/OsDetection.h"
 
-#include "src/parser/PrismParser/Includes.h"
-#include "src/parser/PrismParser/BooleanExpressionGrammar.h"
-#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h"
-#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h"
-#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h"
-#include "src/parser/PrismParser/IntegerExpressionGrammar.h"
-#include "src/parser/PrismParser/IdentifierGrammars.h"
-#include "src/parser/PrismParser/VariableState.h"
+#include "src/parser/prismparser/Includes.h"
+#include "src/parser/prismparser/BooleanExpressionGrammar.h"
+#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h"
+#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h"
+#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h"
+#include "src/parser/prismparser/IntegerExpressionGrammar.h"
+#include "src/parser/prismparser/IdentifierGrammars.h"
+#include "src/parser/prismparser/VariableState.h"
 
 // Needed for file IO.
 #include <fstream>

src/parser/prismparser/PrismGrammar.h

@@ -10,15 +10,15 @@
 
 // All classes of the intermediate representation are used.
 #include "src/ir/IR.h"
-#include "src/parser/PrismParser/Includes.h"
-#include "src/parser/PrismParser/Tokens.h"
-#include "src/parser/PrismParser/IdentifierGrammars.h"
-#include "src/parser/PrismParser/VariableState.h"
-#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h"
-#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h"
-#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h"
-#include "src/parser/PrismParser/BooleanExpressionGrammar.h"
-#include "src/parser/PrismParser/IntegerExpressionGrammar.h"
+#include "src/parser/prismparser/Includes.h"
+#include "src/parser/prismparser/Tokens.h"
+#include "src/parser/prismparser/IdentifierGrammars.h"
+#include "src/parser/prismparser/VariableState.h"
+#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h"
+#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h"
+#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h"
+#include "src/parser/prismparser/BooleanExpressionGrammar.h"
+#include "src/parser/prismparser/IntegerExpressionGrammar.h"
 
 // Used for file input.
 #include <istream>

src/storm.cpp

@@ -343,7 +343,10 @@ int main(const int argc, const char* argv[]) {
 		}
 		if (s->isSet("symbolic")) {
 			std::string arg = s->getString("symbolic");
-			Pr
+			storm::parser::PrismParser parser;
+			storm::adapters::ExplicitModelAdapter adapter(parser.parseFile(arg));
+			std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel();
+			model->printModelInformationToStream(std::cout);
 		}
 
 		cleanUp();