Some minor cleanups, added lot of documentation in prismparser

src/adapters/ExplicitModelAdapter.cpp

@@ -26,36 +26,39 @@ namespace storm {
 
 namespace adapters {
 
-ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), 
-		booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(),
-		allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() {
-	this->initializeVariables();
-	storm::settings::Settings* s = storm::settings::instance();
-	this->precision = s->get<double>("precision");
-}
-
-ExplicitModelAdapter::~ExplicitModelAdapter() {
-	this->clearInternalState();
-}
+	ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), 
+			booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(),
+			allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() {
+		// Get variables from program.
+		this->initializeVariables();
+		storm::settings::Settings* s = storm::settings::instance();
+		this->precision = s->get<double>("precision");
+	}
 
-	std::shared_ptr<storm::models::AbstractModel<double>> ExplicitModelAdapter::getModel(std::string const & rewardModelName) {
+	ExplicitModelAdapter::~ExplicitModelAdapter() {
+		this->clearInternalState();
+	}
 
+	std::shared_ptr<storm::models::AbstractModel<double>> ExplicitModelAdapter::getModel(std::string const & rewardModelName) {
+		// Initialize rewardModel.
+		this->rewardModel = nullptr;
+		if (rewardModelName != "") {
+			this->rewardModel = std::unique_ptr<storm::ir::RewardModel>(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName)));
+		}
 		
+		// State expansion, build temporary map, compute transition rewards.
 		this->buildTransitionMap();
 		
+		// Compute labeling.
 		std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling = this->getStateLabeling(this->program.getLabels());
-		std::shared_ptr<std::vector<double>> stateRewards = nullptr;
 		
-		this->rewardModel = nullptr;
-		if (rewardModelName != "") {
-			this->rewardModel = std::unique_ptr<storm::ir::RewardModel>(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName)));;
-			if (this->rewardModel != nullptr) {
-				if (this->rewardModel->hasStateRewards()) {
-					stateRewards = this->getStateRewards(this->rewardModel->getStateRewards());
-				}
-			}
+		// Compute state rewards.
+		std::shared_ptr<std::vector<double>> stateRewards = nullptr;
+		if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) {
+			stateRewards = this->getStateRewards(this->rewardModel->getStateRewards());
 		}
 
+		// Build and return actual model.
 		switch (this->program.getModelType())
 		{
 			case storm::ir::Program::DTMC:
@@ -107,8 +110,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 	std::shared_ptr<std::vector<double>> ExplicitModelAdapter::getStateRewards(std::vector<storm::ir::StateReward> const & rewards) {
 		std::shared_ptr<std::vector<double>> results(new std::vector<double>(this->allStates.size()));
 		for (uint_fast64_t index = 0; index < this->allStates.size(); index++) {
+			(*results)[index] = 0;
 			for (auto reward: rewards) {
-				(*results)[index] = reward.getReward(this->allStates[index]);
+				// Add this reward to the state.
+				(*results)[index] += reward.getReward(this->allStates[index]);
 			}
 		}
 		return results;
@@ -116,11 +121,13 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 
 	std::shared_ptr<storm::models::AtomicPropositionsLabeling> ExplicitModelAdapter::getStateLabeling(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels) {
 		std::shared_ptr<storm::models::AtomicPropositionsLabeling> results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size()));
+		// Initialize labeling.
 		for (auto it: labels) {
 			results->addAtomicProposition(it.first);
 		}
 		for (uint_fast64_t index = 0; index < this->allStates.size(); index++) {
 			for (auto label: labels) {
+				// Add label to state, if guard is true.
 				if (label.second->getValueAsBool(this->allStates[index])) {
 					results->addAtomicPropositionToState(label.first, index);
 				}
@@ -132,6 +139,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 	void ExplicitModelAdapter::initializeVariables() {
 		uint_fast64_t numberOfIntegerVariables = 0;
 		uint_fast64_t numberOfBooleanVariables = 0;
+		// Count number of variables.
 		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
 			numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
 			numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables();
@@ -140,6 +148,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 		this->booleanVariables.resize(numberOfBooleanVariables);
 		this->integerVariables.resize(numberOfIntegerVariables);
 
+		// Create variables.
 		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
 			storm::ir::Module const& module = program.getModule(i);
 

src/adapters/ExplicitModelAdapter.h

@@ -53,17 +53,25 @@ public:
 
 class ExplicitModelAdapter {
 public:
+	/*!
+	 * Initialize adapter with given program.
+	 */
 	ExplicitModelAdapter(storm::ir::Program program);
 	~ExplicitModelAdapter();
 
+	/*!
+	 * Convert program to an AbstractModel.
+	 * The model will be of the type specified in the program.
+	 * The model will contain rewards that are specified by the given reward model.
+	 * @param rewardModelName Name of reward model to be added to the model.
+	 * @return Model resulting from the program.
+	 */
 	std::shared_ptr<storm::models::AbstractModel<double>> getModel(std::string const & rewardModelName = "");
 
 private:
 
 	double precision;
 
-	// First some generic routines to operate on states.
-
 	/*!
 	 * Set some boolean variable in the given state object.
 	 * @param state State to be changed.
@@ -78,6 +86,11 @@ private:
 	 * @param value New value.
 	 */
 	static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value);
+	/*!
+	 * Transforms a state into a somewhat readable string.
+	 * @param state State.
+	 * @return String representation of the state.
+	 */
 	static std::string toString(StateType const * const state);
 	/*!
 	 * Apply an update to the given state and return the resulting new state object.
@@ -103,7 +116,18 @@ private:
 	 */
 	void initializeVariables();
 
+	/*!
+	 * Calculate state reward for every reachable state based on given reward models.
+	 * @param rewards List of state reward models.
+	 * @return Reward for every state.
+	 */
 	std::shared_ptr<std::vector<double>> getStateRewards(std::vector<storm::ir::StateReward> const & rewards);
+	
+	/*!
+	 * Determines the labels for every reachable state, based on a list of available labels.
+	 * @param labels Mapping from label names to boolean expressions.
+	 * @returns The resulting labeling.
+	 */
 	std::shared_ptr<storm::models::AtomicPropositionsLabeling> getStateLabeling(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels);
 
 	/*!
@@ -168,29 +192,41 @@ private:
 	std::shared_ptr<storm::storage::SparseMatrix<double>> buildNondeterministicMatrix();
 
 	/*!
-	 * Build matrix from model. Starts with all initial states and explores the reachable state space.
-	 * While exploring, the transitions are stored in a temporary map.
-	 * Afterwards, we transform this map into the actual matrix.
-	 * @return result matrix.
+	 * Generate internal transition map from given model.
+	 * Starts with all initial states and explores the reachable state space.
 	 */
 	void buildTransitionMap();
 	
+	/*!
+	 * Clear all members that are initialized during the computation.
+	 */
 	void clearInternalState();
 
 	// Program that should be converted.
 	storm::ir::Program program;
+	// List of all boolean variables.
 	std::vector<storm::ir::BooleanVariable> booleanVariables;
+	// List of all integer variables.
 	std::vector<storm::ir::IntegerVariable> integerVariables;
+	// Maps boolean variable names to their index.
 	std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
+	// Maps integer variable names to their index.
 	std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
 
-	// Members that are filled during the conversion.
+	//// Members that are filled during the conversion.
+	// Selected reward model.
 	std::unique_ptr<storm::ir::RewardModel> rewardModel;
+	// List of all reachable states.
 	std::vector<StateType*> allStates;
+	// Maps states to their index (within allStates).
 	std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
+	// Number of transitions.
 	uint_fast64_t numberOfTransitions;
+	// Number of choices. (Is number of rows in matrix of nondeterministic model.)
 	uint_fast64_t numberOfChoices;
-        std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
+	// Number of choices for each state.
+	std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
+	// Rewards for transitions.
 	std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
 
 	/*!

src/parser/prismparser/BaseGrammar.h

@@ -16,11 +16,23 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+	/*!
+	 * This is the base class for all expression grammars.
+	 * It takes care of implementing a singleton, stores a VariableState and implements some common helper routines.
+	 */
 	template <typename T>
 	class BaseGrammar {
 	public:
+		/*!
+		 * Constructor.
+		 */
 		BaseGrammar(std::shared_ptr<VariableState>& state) : state(state) {}
 
+		/*!
+		 * Create and return a new instance of class T, usually the subclass.
+		 * @param state VariableState to be given to the constructor.
+		 * @returns Instance of class T.
+		 */
 		static T& instance(std::shared_ptr<VariableState> state = nullptr) {
 			if (BaseGrammar::instanceObject == nullptr) {
 				BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state));
@@ -29,26 +41,55 @@ namespace prism {
 			return *BaseGrammar::instanceObject;
 		}
 
+		/*!
+		 * Clear the cached instance.
+		 */
 		static void resetInstance() {
 			BaseGrammar::instanceObject = nullptr;
 		}
 
+		/*!
+		 * Notify the cached object, that we will begin with the second parsing run.
+		 */
 		static void secondRun() {
 			if (BaseGrammar::instanceObject != nullptr) {
 				BaseGrammar::instanceObject->prepareSecondRun();
 			}
 		}
 
+		/*!
+		 * Create a new boolean literal with the given value.
+		 * @param value Value of the literal.
+		 * @returns Boolean literal.
+		 */
 		std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) {
 			return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value));
 		}
+		/*!
+		 * Create a new double literal with the given value.
+		 * @param value Value of the literal.
+		 * @returns Double literal.
+		 */
 		std::shared_ptr<BaseExpression> createDoubleLiteral(const double value) {
 			return std::shared_ptr<DoubleLiteral>(new DoubleLiteral(value));
 		}
+		/*!
+		 * Create a new integer literal with the given value.
+		 * @param value Value of the literal.
+		 * @returns Integer literal.
+		 */
 		std::shared_ptr<BaseExpression> createIntLiteral(const int_fast64_t value) {
 			return std::shared_ptr<IntegerLiteral>(new IntegerLiteral(value));
 		}
 		
+		/*!
+		 * Create a new plus expression. If addition is true, it will be an addition, otherwise a subtraction.
+		 * @param left Left operand.
+		 * @param addition Flag for addition or subtraction.
+		 * @param right Right operand.
+		 * @param type Return type.
+		 * @returns Plus expression.
+		 */
 		std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right, BaseExpression::ReturnType type) {
 			if (addition) {
 				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS));
@@ -56,16 +97,43 @@ namespace prism {
 				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS));
 			}
 		}
+		/*!
+		 * Create a new double plus expression. If addition is true, it will be an addition, otherwise a subtraction.
+		 * @param left Left operand.
+		 * @param addition Flag for addition or subtraction.
+		 * @param right Right operand.
+		 * @returns Double plus expression.
+		 */
 		std::shared_ptr<BaseExpression> createDoublePlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
 			return this->createPlus(left, addition, right, BaseExpression::double_);
 		}
+		/*!
+		 * Create a new integer plus expression. If addition is true, it will be an addition, otherwise a subtraction.
+		 * @param left Left operand.
+		 * @param addition Flag for addition or subtraction.
+		 * @param right Right operand.
+		 * @returns Integer plus expression.
+		 */
 		std::shared_ptr<BaseExpression> createIntPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
 			return this->createPlus(left, addition, right, BaseExpression::int_);
 		}
 
+		/*!
+		 * Create a new integer multiplication expression.
+		 * @param left Left operand.
+		 * @param right Right operand.
+		 * @returns Integer multiplication expression.
+		 */
 		std::shared_ptr<BaseExpression> createIntMult(const std::shared_ptr<BaseExpression> left, const std::shared_ptr<BaseExpression> right) {
 			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES));
 		}
+		/*!
+		 * Create a new integer multiplication expression. If multiplication is true, it will be an multiplication, otherwise a division.
+		 * @param left Left operand.
+		 * @param addition Flag for multiplication or division.
+		 * @param right Right operand.
+		 * @returns Integer multiplication expression.
+		 */
 		std::shared_ptr<BaseExpression> createDoubleMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) {
 			if (multiplication) {
 				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES));
@@ -73,29 +141,69 @@ namespace prism {
 				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE));
 			}
 		}
-
+		/*!
+		 * Create a new binary relation expression.
+		 * @param left Left operand.
+		 * @param relationType Type of binary relation.
+		 * @param right Right operand.
+		 * @returns Binary relation expression.
+		 */
 		std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) {
 			return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType));
 		}
+		/*!
+		 * Create a new negation expression.
+		 * @param child Expression to be negated.
+		 * @returns Negation expression.
+		 */
 		std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child) {
 			return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT));
 		}
+		/*!
+		 * Create a new And expression.
+		 * @param left Left operand.
+		 * @param right Right operand.
+		 * @returns And expression.
+		 */
 		std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
 			//std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl;
 			return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND));
 		}
+		/*!
+		 * Create a new Or expression.
+		 * @param left Left operand.
+		 * @param right Right operand.
+		 * @returns Or expression.
+		 */
 		std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
 			return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR));
 		}
+		/*!
+		 * Retrieve boolean variable by name.
+		 * @param name Variable name.
+		 * @returns Boolean variable.
+		 */
 		std::shared_ptr<BaseExpression> getBoolVariable(const std::string name) {
 			return state->getBooleanVariable(name);
 		}
+		/*!
+		 * Retrieve integer variable by name.
+		 * @param name Variable name.
+		 * @returns Integer variable.
+		 */
 		std::shared_ptr<BaseExpression> getIntVariable(const std::string name) {
 			return state->getIntegerVariable(name);
 		}
 
+		/*!
+		 * Base method to switch to second run. This does nothing.
+		 * Any subclass that needs to do something in order to proceed to the second run should override this method.
+		 */
 		virtual void prepareSecondRun() {}
 	protected:
+		/*!
+		 * Pointer to variable state.
+		 */
 		std::shared_ptr<VariableState> state;
 
 	private:

src/parser/prismparser/BooleanExpressionGrammar.h

@@ -19,9 +19,16 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+/*!
+ * This grammar parses (non constant) boolean expressions as used in prism models.
+ */
 class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<BooleanExpressionGrammar> {
 public:
 	BooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
+	/*!
+	 * Switch to second run.
+	 * Variable names may be any valid identifier in the first run, but only defined variables in the second run.
+	 */
 	virtual void prepareSecondRun();
 	
 private:
@@ -33,6 +40,9 @@ private:
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> relativeExpression;
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableExpression;
 
+	/*!
+	 * Parser relation operators.
+	 */
 	storm::parser::prism::relationalOperatorStruct relations_;
 };
 

src/parser/prismparser/ConstBooleanExpressionGrammar.cpp

@@ -6,47 +6,31 @@ namespace storm {
 namespace parser {
 namespace prism {
 
-	std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) {
-		return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType));
-	}
-	std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createNot(std::shared_ptr<BaseExpression> child) {
-		return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT));
-	}
-	std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
-		return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND));
-	}
-	std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
-		return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR));
-	}
-	std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createLiteral(const bool value) {
-		return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value));
-	}
-
 	ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
 		: ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) {
 
 		constantBooleanExpression %= constantOrExpression;
 		constantBooleanExpression.name("constant boolean expression");
 		
-		constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createOr, this, qi::_val, qi::_1)];
+		constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
 		constantOrExpression.name("constant boolean expression");
 
-		constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createAnd, this, qi::_val, qi::_1)];
+		constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
 		constantAndExpression.name("constant boolean expression");
 
-		constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createNot, this, qi::_1)];
+		constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
 		constantNotExpression.name("constant boolean expression");
 
 		constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
 		constantAtomicBooleanExpression.name("constant boolean expression");
 
-		constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
+		constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
 		constantRelativeExpression.name("constant boolean expression");
 		
 		booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression);
 		booleanConstantExpression.name("boolean constant or literal");
 
-		booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createLiteral, this, qi::_1)];
+		booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&BaseGrammar::createBoolLiteral, this, qi::_1)];
 		booleanLiteralExpression.name("boolean literal");
 	}
 }

src/parser/prismparser/ConstBooleanExpressionGrammar.h

@@ -17,6 +17,9 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+/*!
+ * This grammar parses constant boolean expression as used in prism models.
+ */
 class ConstBooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstBooleanExpressionGrammar> {
 public:
 	ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
@@ -33,12 +36,6 @@ private:
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
 
 	storm::parser::prism::relationalOperatorStruct relations_;
-
-	std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right);
-	std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child);
-	std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right);
-	std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right);
-	std::shared_ptr<BaseExpression> createLiteral(const bool value);
 };
 
 

src/parser/prismparser/ConstDoubleExpressionGrammar.cpp

@@ -4,25 +4,6 @@ namespace storm {
 namespace parser {
 namespace prism {
 
-
-	std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createLiteral(double value) {
-		return std::shared_ptr<DoubleLiteral>(new DoubleLiteral(value));
-	}
-	std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
-		if (addition) {
-			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::PLUS));
-		} else {
-			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::MINUS));
-		}
-	}
-	std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) {
-		if (multiplication) {
-			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES));
-		} else {
-			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE));
-		}
-	}
-
 ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state)
 	: ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) {
 
@@ -30,11 +11,11 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<Varia
 	constantDoubleExpression.name("constant double expression");
 
 	constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression)
-			[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createPlus, this, qi::_val, qi::_a, qi::_1)];
+			[qi::_val = phoenix::bind(&BaseGrammar::createDoublePlus, this, qi::_val, qi::_a, qi::_1)];
 	constantDoublePlusExpression.name("constant double expression");
 
 	constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression)
-			[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createMult, this, qi::_val, qi::_a, qi::_1)];
+			[qi::_val = phoenix::bind(&BaseGrammar::createDoubleMult, this, qi::_val, qi::_a, qi::_1)];
 	constantDoubleMultExpression.name("constant double expression");
 
 	constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
@@ -43,7 +24,7 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<Varia
 	doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression);
 	doubleConstantExpression.name("double constant or literal");
 
-	doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createLiteral, this, qi::_1)];
+	doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&BaseGrammar::createDoubleLiteral, this, qi::_1)];
 	doubleLiteralExpression.name("double literal");
 }
 

src/parser/prismparser/ConstDoubleExpressionGrammar.h

@@ -16,11 +16,13 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+/*!
+ * This grammar parses constant double expressions as used in prism models.
+ */
 class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> {
 public:
 	ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state);
 
-
 private:
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
@@ -28,10 +30,6 @@ private:
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
 	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
-
-	std::shared_ptr<BaseExpression> createLiteral(double value);
-	std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right);
-	std::shared_ptr<BaseExpression> createMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right);
 };
 
 

src/parser/prismparser/ConstIntegerExpressionGrammar.h

@@ -16,6 +16,9 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+/*!
+ * This grammar parses constant integer expressions as used in prism models.
+ */
 class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> {
 public:
 	ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state);

src/parser/prismparser/IdentifierGrammars.h

@@ -16,6 +16,9 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+	/*!
+	 * This grammar parses a (possibly used) identifier as used in a prism models.
+	 */
 	class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
 	public:
 		IdentifierGrammar(std::shared_ptr<VariableState>& state);
@@ -23,6 +26,9 @@ namespace prism {
 		qi::rule<Iterator, std::string(), Skipper> identifierName;
 	};
 	
+	/*!
+	 * This grammar parses an used identifier as used in a prism models.
+	 */
 	class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar>  {
 	public:
 		FreeIdentifierGrammar(std::shared_ptr<VariableState>& state);

src/parser/prismparser/IntegerExpressionGrammar.h

@@ -19,9 +19,17 @@ namespace storm {
 namespace parser {
 namespace prism {
 
+/*!
+ * This grammar parses a (non constant) integer expressions as used in prism models.
+ */
 class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
 public:
 	IntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
+	
+	/*!
+	 * Switch to second run.
+	 * Variable names may be any valid identifier in the first run, but only defined variables in the second run.
+	 */
 	virtual void prepareSecondRun();
 
 private:

src/parser/prismparser/PrismGrammar.cpp

@@ -63,19 +63,19 @@ void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_pt
 }
 Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping) {
 	this->state->moduleNames_.add(name, name);
-	Module* old = this->state->moduleMap_.find(oldname);
+	Module* old = this->moduleMap_.find(oldname);
 	if (old == nullptr) {
 		LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!");
 		throw "Renaming module failed";
 	}
 	Module res(*old, name, mapping, this->state);
-	this->state->moduleMap_.at(name) = res;
+	this->moduleMap_.at(name) = res;
 	return res;
 }
 Module PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands) {
 	this->state->moduleNames_.add(name, name);
 	Module res(name, bools, ints, boolids, intids, commands);
-	this->state->moduleMap_.at(name) = res;
+	this->moduleMap_.at(name) = res;
 	return res;
 }
 

src/parser/prismparser/PrismGrammar.h

@@ -54,6 +54,7 @@ public:
 private:
 
 	std::shared_ptr<storm::parser::prism::VariableState> state;
+	struct qi::symbols<char, Module> moduleMap_;
 
 	// The starting point of the grammar.
 	qi::rule<

src/parser/prismparser/Tokens.h

@@ -12,9 +12,10 @@ namespace storm {
 namespace parser {
 namespace prism {
 
-
-	// A structure mapping the textual representation of a model type to the model type
-	// representation of the intermediate representation.
+	/*!
+	 * A structure mapping the textual representation of a model type to the model type
+	 * representation of the intermediate representation.
+	 */
 	struct modelTypeStruct : qi::symbols<char, Program::ModelType> {
 		modelTypeStruct() {
 			add
@@ -27,7 +28,9 @@ namespace prism {
 	};
 
 
-	// A structure defining the keywords that are not allowed to be chosen as identifiers.
+	/*!
+	 * A structure defining the keywords that are not allowed to be chosen as identifiers.
+	 */
 	struct keywordsStruct : qi::symbols<char, unsigned> {
 		keywordsStruct() {
 			add
@@ -48,8 +51,10 @@ namespace prism {
 		}
 	};
 	
-	// A structure mapping the textual representation of a binary relation to the representation
-	// of the intermediate representation.
+	/*!
+	 * A structure mapping the textual representation of a binary relation to the representation
+	 * of the intermediate representation.
+	 */
 	struct relationalOperatorStruct : qi::symbols<char, BinaryRelationExpression::RelationType> {
 		relationalOperatorStruct() {
 			add

src/parser/prismparser/VariableState.h

@@ -23,43 +23,104 @@ using namespace storm::ir::expressions;
 template<typename T>
 std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols);
 
+/*!
+ * This class contains the state that is needed during the parsing of a prism model.
+ */
 struct VariableState : public storm::ir::VariableAdder {
 
-public:
 	VariableState(bool firstRun = true);
 	
-public:
+	/*!
+	 * Indicator, if we are still in the first run.
+	 */
 	bool firstRun;
+	/*!
+	 * A parser for all reserved keywords.
+	 */
 	keywordsStruct keywords;
 
-	// Used for indexing the variables.
+	/*!
+	 * Internal counter for the index of the next new boolean variable.
+	 */
 	uint_fast64_t nextBooleanVariableIndex;
+	/*!
+	 * Internal counter for the index of the next new integer variable.
+	 */
 	uint_fast64_t nextIntegerVariableIndex;
 
 	// Structures mapping variable and constant names to the corresponding expression nodes of
 	// the intermediate representation.
 	struct qi::symbols<char, std::shared_ptr<VariableExpression>> integerVariables_, booleanVariables_;
 	struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
-	struct qi::symbols<char, Module> moduleMap_;
 
 	// A structure representing the identity function over identifier names.
 	struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
 			localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
-public:
+	
+	/*!
+	 * Add a new boolean variable with the given name.
+	 * @param name Name of the variable.
+	 * @return Index of the variable.
+	 */
 	uint_fast64_t addBooleanVariable(const std::string& name);
+	/*!
+	 * Add a new integer variable with the given name and constraints.
+	 * @param name Name of the variable.
+	 * @param lower Lower bound for the variable value.
+	 * @param upper Upper bound for the variable value.
+	 * @return Index of the variable.
+	 */
 	uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper);
 
+	/*!
+	 * Retrieve boolean Variable with given name.
+	 * @param name Variable name.
+	 * @returns Variable.
+	 */
 	std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name);
+	/*!
+	 * Retrieve integer Variable with given name.
+	 * @param name Variable name.
+	 * @returns Variable.
+	 */
 	std::shared_ptr<VariableExpression> getIntegerVariable(const std::string& name);
+	/*!
+	 * Retrieve any Variable with given name.
+	 * @param name Variable name.
+	 * @returns Variable.
+	 */
 	std::shared_ptr<VariableExpression> getVariable(const std::string& name);
 
+	/*!
+	 * Perform operations necessary for a module renaming.
+	 * This includes creating new variables and constants.
+	 * @param renaming String mapping for renaming operation.
+	 */
 	void performRenaming(const std::map<std::string, std::string>& renaming);
 
+	/*!
+	 * Start with a new module.
+	 * Clears sets of local variables.
+	 */
 	void startModule();
 
+	/*!
+	 * Check if given string is a free identifier.
+	 * @param s String.
+	 * @returns If s is a free identifier.
+	 */
 	bool isFreeIdentifier(std::string& s) const;
+	/*!
+	 * Check if given string is a valid identifier.
+	 * @param s String.
+	 * @returns If s is a valid identifier.
+	 */
 	bool isIdentifier(std::string& s) const;
 
+	/*!
+	 * Prepare state to proceed to second parser run.
+	 * Clears constants.
+	 */
 	void prepareForSecondRun();
 };