diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index da8ad0941..49bdd20c5 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -1,49 +1,35 @@
-/* * PrismParser.h
- *
- * Created on: Jan 3, 2013
- * Author: Christian Dehnert
- */
-
#ifndef STORM_PARSER_PRISMPARSER_H_
#define STORM_PARSER_PRISMPARSER_H_
// All classes of the intermediate representation are used.
-#include "src/ir/IR.h"
+#include "src/storage/prism/Program.h"
// Used for file input.
#include <istream>
-#include <memory>
namespace storm {
-
-namespace parser {
-
-using namespace storm::ir;
-using namespace storm::ir::expressions;
-
-/*
- * This functions parse the format of the PRISM model checker into an intermediate representation.
- */
-
-/*!
- * Parses the given file into the intermediate representation assuming it complies with the
- * PRISM syntax.
- * @param filename the name of the file to parse.
- * @return a shared pointer to the intermediate representation of the PRISM file.
- */
-storm::ir::Program PrismParserFromFile(std::string const& filename);
-
-/*!
- * Parses the given input stream into the intermediate representation assuming it complies with
- * the PRISM syntax.
- * @param inputStream the input stream to parse.
- * @param filename the name of the file the input stream belongs to. Used for diagnostics.
- * @return a shared pointer to the intermediate representation of the PRISM file.
- */
-storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename);
-
-} // namespace parser
-
+ namespace parser {
+ using namespace storm::prism;
+ using namespace storm::expressions;
+
+ /*!
+ * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
+ *
+ * @param filename the name of the file to parse.
+ * @return The resulting PRISM program.
+ */
+ storm::prism::Program PrismParserFromFile(std::string const& filename);
+
+ /*!
+ * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
+ *
+ * @param inputStream The input stream to parse.
+ * @param filename The name of the file the input stream belongs to.
+ * @return The resulting PRISM program.
+ */
+ storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename);
+
+ } // namespace parser
} // namespace storm
#endif /* STORM_PARSER_PRISMPARSER_H_ */
diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h
deleted file mode 100644
index 7cac493c3..000000000
--- a/src/parser/prismparser/BaseGrammar.h
+++ /dev/null
@@ -1,253 +0,0 @@
-/*
- * File: Keywords.h
- * Author: nafur
- *
- * Created on April 10, 2013, 6:03 PM
- */
-
-#ifndef BASEGRAMMAR_H
-#define BASEGRAMMAR_H
-
-#include "Includes.h"
-
-#include "VariableState.h"
-
-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> const& 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> const& state = nullptr) {
- if (BaseGrammar::instanceObject == nullptr) {
- BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state));
- if (!state->firstRun) BaseGrammar::instanceObject->secondRun();
- }
- 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(bool value) {
- return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(value));
- }
- /*!
- * Create a new double literal with the given value.
- * @param value Value of the literal.
- * @returns Double literal.
- */
- std::shared_ptr<BaseExpression> createDoubleLiteral(double value) {
- return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(value));
- }
- /*!
- * Create a new integer literal with the given value.
- * @param value Value of the literal.
- * @returns Integer literal.
- */
- std::shared_ptr<BaseExpression> createIntLiteral(int_fast64_t value) {
- return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(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(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right, BaseExpression::ReturnType type) {
- if (addition) {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::PLUS));
- } else {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), 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(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& 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(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& 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(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), 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(std::shared_ptr<BaseExpression> const& left, bool multiplication, std::shared_ptr<BaseExpression> const& right) {
- if (multiplication) {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES));
- } else {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::DIVIDE));
- }
- }
-
- /*!
- * Creates an integer min/max expression.
- *
- * @param min Indicates whether the expression is min or max.
- * @param left The left operand.
- * @param right The right operand.
- * @return An integer min/max expression.
- */
- std::shared_ptr<BaseExpression> createIntMinMax(bool min, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
- if (min) {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MIN));
- } else {
- return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MAX));
- }
- }
-
- /*!
- * Creates an integer floor/ceil expression.
- *
- * @param floor Indicates whether the expression is a floor expression.
- * @param operand The argument of the floor/ceil operation.
- * @return An integer floor/ceil expression.
- */
- std::shared_ptr<BaseExpression> createIntFloorCeil(bool floor, std::shared_ptr<BaseExpression> const& operand) {
- if (floor) {
- return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::FLOOR));
- } else {
- return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::CEIL));
- }
- }
-
- /*!
- * 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> const& left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> const& right) {
- return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(left->clone(), right->clone(), relationType));
- }
- /*!
- * Create a new negation expression.
- * @param child Expression to be negated.
- * @returns Negation expression.
- */
- std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> const& child) {
- return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child->clone(), 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> const& left, std::shared_ptr<BaseExpression> const& right) {
- return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), 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> const& left, std::shared_ptr<BaseExpression> const& right) {
- return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::OR));
- }
- /*!
- * Retrieve boolean variable by name.
- * @param name Variable name.
- * @returns Boolean variable.
- */
- std::shared_ptr<BaseExpression> getBoolVariable(std::string const& name) {
- return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getBooleanVariableExpression(name)));
- }
- /*!
- * Retrieve integer variable by name.
- * @param name Variable name.
- * @returns Integer variable.
- */
- std::shared_ptr<BaseExpression> getIntVariable(std::string const& name) {
- return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getIntegerVariableExpression(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:
- static std::shared_ptr<T> instanceObject;
- static bool inSecondRun;
- };
-
- template <typename T>
- std::shared_ptr<T> BaseGrammar<T>::instanceObject;
-}
-}
-}
-#endif /* BASEGRAMMAR_H */
-
diff --git a/src/parser/prismparser/BooleanExpressionGrammar.cpp b/src/parser/prismparser/BooleanExpressionGrammar.cpp
deleted file mode 100644
index a7d9366f8..000000000
--- a/src/parser/prismparser/BooleanExpressionGrammar.cpp
+++ /dev/null
@@ -1,42 +0,0 @@
-#include "BooleanExpressionGrammar.h"
-
-#include "IntegerExpressionGrammar.h"
-#include "ConstBooleanExpressionGrammar.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
- BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState> const& state)
- : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
-
- booleanExpression %= orExpression;
- booleanExpression.name("boolean expression");
-
- orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
- orExpression.name("boolean expression");
-
- andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
- andExpression.name("boolean expression");
-
- notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
- notExpression.name("boolean expression");
-
- atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | this->state->constantBooleanFormulas_ | this->state->booleanFormulas_ | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
- atomicBooleanExpression.name("boolean expression");
-
- relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
- relativeExpression.name("relative expression");
-
- booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)];
- booleanVariableExpression.name("boolean variable");
- }
-
- void BooleanExpressionGrammar::prepareSecondRun() {
- booleanVariableExpression %= this->state->booleanVariables_;
- booleanVariableExpression.name("boolean variable");
- }
-
- } // namespace prism
- } // namespace parser
-} // namespace storm
diff --git a/src/parser/prismparser/BooleanExpressionGrammar.h b/src/parser/prismparser/BooleanExpressionGrammar.h
deleted file mode 100644
index 909219fa3..000000000
--- a/src/parser/prismparser/BooleanExpressionGrammar.h
+++ /dev/null
@@ -1,54 +0,0 @@
-/*
- * File: BooleanExpressionGrammar.h
- * Author: nafur
- *
- * Created on April 10, 2013, 6:27 PM
- */
-
-#ifndef BOOLEANEXPRESSIONGRAMMAR_H
-#define BOOLEANEXPRESSIONGRAMMAR_H
-
-#include "Includes.h"
-#include "VariableState.h"
-#include "IdentifierGrammars.h"
-#include "Tokens.h"
-
-#include <iostream>
-
-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> const& 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:
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> booleanExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> orExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> andExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> notExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicBooleanExpression;
- 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_;
-};
-
-
-}
-}
-}
-
-#endif /* BOOLEANEXPRESSIONGRAMMAR_H */
diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
deleted file mode 100644
index a5ce0567d..000000000
--- a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-#include "ConstBooleanExpressionGrammar.h"
-
-#include "ConstIntegerExpressionGrammar.h"
-
-namespace storm {
-namespace parser {
-namespace prism {
-
- ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState> const& 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(&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(&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(&BaseGrammar::createNot, this, qi::_1)];
- constantNotExpression.name("constant boolean expression");
-
- constantAtomicBooleanExpression %= (constantRelativeExpression | this->state->constantBooleanFormulas_ | 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(&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(&BaseGrammar::createBoolLiteral, this, qi::_1)];
- booleanLiteralExpression.name("boolean literal");
- }
-}
-}
-}
diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.h b/src/parser/prismparser/ConstBooleanExpressionGrammar.h
deleted file mode 100644
index 8fea3ce95..000000000
--- a/src/parser/prismparser/ConstBooleanExpressionGrammar.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
- * File: ConstBooleanExpressionGrammar.h
- * Author: nafur
- *
- * Created on April 10, 2013, 6:34 PM
- */
-
-#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H
-#define CONSTBOOLEANEXPRESSIONGRAMMAR_H
-
-#include "Includes.h"
-#include "VariableState.h"
-#include "IdentifierGrammars.h"
-#include "Tokens.h"
-
-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> const& state);
-
-
-private:
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantBooleanExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantOrExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAndExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantNotExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicBooleanExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantRelativeExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
-
- storm::parser::prism::relationalOperatorStruct relations_;
-};
-
-
-}
-}
-}
-
-#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */
-
diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
deleted file mode 100644
index 18cd5ae31..000000000
--- a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
+++ /dev/null
@@ -1,34 +0,0 @@
-#include "ConstDoubleExpressionGrammar.h"
-
-namespace storm {
-namespace parser {
-namespace prism {
-
-ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState> const& state)
- : ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) {
-
- constantDoubleExpression %= constantDoublePlusExpression;
- 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(&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(&BaseGrammar::createDoubleMult, this, qi::_val, qi::_a, qi::_1)];
- constantDoubleMultExpression.name("constant double expression");
-
- constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | this->state->constantDoubleFormulas_ | this->state->constantIntegerFormulas_ | doubleConstantExpression);
- constantAtomicDoubleExpression.name("constant double expression");
-
- doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression);
- doubleConstantExpression.name("double constant or literal");
-
- doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&BaseGrammar::createDoubleLiteral, this, qi::_1)];
- doubleLiteralExpression.name("double literal");
-}
-
-
-}
-}
-}
diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.h b/src/parser/prismparser/ConstDoubleExpressionGrammar.h
deleted file mode 100644
index 41c503731..000000000
--- a/src/parser/prismparser/ConstDoubleExpressionGrammar.h
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
- * File: ConstDoubleExpressionGrammar.h
- * Author: nafur
- *
- * Created on April 10, 2013, 7:04 PM
- */
-
-#ifndef CONSTDOUBLEEXPRESSIONGRAMMAR_H
-#define CONSTDOUBLEEXPRESSIONGRAMMAR_H
-
-#include "Includes.h"
-#include "VariableState.h"
-#include "IdentifierGrammars.h"
-
-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> const& state);
-
- private:
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
- 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;
- };
-
-
- }
- }
-}
-
-#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */
-
diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
deleted file mode 100644
index 9ebebebc7..000000000
--- a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-#include "ConstIntegerExpressionGrammar.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
-
- ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
- : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) {
-
- constantIntegerExpression %= constantIntegerPlusExpression;
- constantIntegerExpression.name("constant integer expression");
-
- constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)
- [qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
- constantIntegerPlusExpression.name("constant integer expression");
-
- constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)
- [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
- constantIntegerMultExpression.name("constant integer expression");
-
- constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | this->state->constantIntegerFormulas_ | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
- constantAtomicIntegerExpression.name("constant integer expression");
-
- constantIntegerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(",") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)];
- constantIntegerMinMaxExpression.name("integer min/max expression");
-
- constantIntegerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)];
- constantIntegerFloorCeilExpression.name("integer floor/ceil expression");
-
- integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
- integerConstantExpression.name("integer constant or literal");
-
- integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)];
- integerLiteralExpression.name("integer literal");
-
- }
-
- } // namespace prism
- } // namespace parser
-} // namespace storm
diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.h b/src/parser/prismparser/ConstIntegerExpressionGrammar.h
deleted file mode 100644
index 2b6a08cae..000000000
--- a/src/parser/prismparser/ConstIntegerExpressionGrammar.h
+++ /dev/null
@@ -1,42 +0,0 @@
-/*
- * File: ConstIntegerExpressionGrammar.h
- * Author: nafur
- *
- * Created on April 10, 2013, 6:02 PM
- */
-
-#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H
-#define CONSTINTEGEREXPRESSIONGRAMMAR_H
-
-#include "Includes.h"
-#include "VariableState.h"
-#include "IdentifierGrammars.h"
-
-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> const& state);
-
- private:
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerMinMaxExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerFloorCeilExpression;
- };
-
-
- }
- }
-}
-
-#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */
diff --git a/src/parser/prismparser/IdentifierGrammars.cpp b/src/parser/prismparser/IdentifierGrammars.cpp
deleted file mode 100644
index ec6f14931..000000000
--- a/src/parser/prismparser/IdentifierGrammars.cpp
+++ /dev/null
@@ -1,23 +0,0 @@
-#include "IdentifierGrammars.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
- IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState> const& state)
- : IdentifierGrammar::base_type(identifierName), BaseGrammar(state) {
-
- identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
- identifierName.name("identifier");
- }
-
- FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState> const& state)
- : FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) {
-
- freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
- freeIdentifierName.name("identifier");
- }
-
- }
- }
-}
\ No newline at end of file
diff --git a/src/parser/prismparser/IdentifierGrammars.h b/src/parser/prismparser/IdentifierGrammars.h
deleted file mode 100644
index ccb14bbc1..000000000
--- a/src/parser/prismparser/IdentifierGrammars.h
+++ /dev/null
@@ -1,42 +0,0 @@
-/*
- * File: Keywords.h
- * Author: nafur
- *
- * Created on April 10, 2013, 6:03 PM
- */
-
-#ifndef IDENTIFIERGRAMMARS_H
-#define IDENTIFIERGRAMMARS_H
-
-#include "Includes.h"
-#include "BaseGrammar.h"
-#include "VariableState.h"
-
-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> const& state);
- private:
- 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> const& state);
- private:
- qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
- };
- }
- }
-}
-#endif /* IDENTIFIERGRAMMARS_H */
-
diff --git a/src/parser/prismparser/Includes.h b/src/parser/prismparser/Includes.h
deleted file mode 100644
index 49a720dad..000000000
--- a/src/parser/prismparser/Includes.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
- * File: Includes
- * Author: Gereon Kremer
- *
- * Created on April 10, 2013, 4:46 PM
- */
-
-#ifndef BOOSTINCLUDES_H
-#define BOOSTINCLUDES_H
-
-// Used for Boost spirit.
-#include <boost/typeof/typeof.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/phoenix.hpp>
-
-// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
-#include <boost/spirit/include/classic_position_iterator.hpp>
-#include <boost/spirit/include/support_multi_pass.hpp>
-
-namespace qi = boost::spirit::qi;
-namespace phoenix = boost::phoenix;
-
-typedef std::string::const_iterator BaseIteratorType;
-typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
-typedef PositionIteratorType Iterator;
-typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
-typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
-typedef boost::spirit::unused_type Unused;
-
-#include "src/ir/IR.h"
-using namespace storm::ir;
-using namespace storm::ir::expressions;
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-extern log4cplus::Logger logger;
-
-#endif /* BOOSTINCLUDES_H */
-
diff --git a/src/parser/prismparser/IntegerExpressionGrammar.cpp b/src/parser/prismparser/IntegerExpressionGrammar.cpp
deleted file mode 100644
index 3bcfd4d4f..000000000
--- a/src/parser/prismparser/IntegerExpressionGrammar.cpp
+++ /dev/null
@@ -1,42 +0,0 @@
-#include "IntegerExpressionGrammar.h"
-
-#include "IdentifierGrammars.h"
-#include "ConstIntegerExpressionGrammar.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
- IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
- : IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) {
-
- integerExpression %= integerPlusExpression;
- integerExpression.name("integer expression");
-
- integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
- integerPlusExpression.name("integer expression");
-
- integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
- integerMultExpression.name("integer expression");
-
- atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | this->state->constantIntegerFormulas_ | this->state->integerFormulas_ | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state));
- atomicIntegerExpression.name("integer expression");
-
- integerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(",") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)];
- integerMinMaxExpression.name("integer min/max expression");
-
- integerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)];
- integerFloorCeilExpression.name("integer floor/ceil expression");
-
- integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)];
- integerVariableExpression.name("integer variable");
- }
-
- void IntegerExpressionGrammar::prepareSecondRun() {
- integerVariableExpression %= this->state->integerVariables_;
- integerVariableExpression.name("integer variable");
- }
-
- }
- }
-}
diff --git a/src/parser/prismparser/IntegerExpressionGrammar.h b/src/parser/prismparser/IntegerExpressionGrammar.h
deleted file mode 100644
index 7531ef36e..000000000
--- a/src/parser/prismparser/IntegerExpressionGrammar.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
- * File: IntegerExpressionGrammar.h
- * Author: nafur
- *
- * Created on April 10, 2013, 4:39 PM
- */
-
-#ifndef INTEGEREXPRESSIONGRAMMAR_H
-#define INTEGEREXPRESSIONGRAMMAR_H
-
-#include "src/ir/IR.h"
-#include "VariableState.h"
-#include "Includes.h"
-#include "IdentifierGrammars.h"
-
-#include <memory>
-
-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> const& 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:
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerMinMaxExpression;
- qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerFloorCeilExpression;
- };
-
- }
- }
-}
-
-#endif /* INTEGEREXPRESSIONGRAMMAR_H */
-
diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h
index 57ba55c5b..c73420057 100644
--- a/src/parser/prismparser/PrismGrammar.h
+++ b/src/parser/prismparser/PrismGrammar.h
@@ -1,103 +1,61 @@
-/*
- * File: PrismGrammar.h
- * Author: nafur
- *
- * Created on April 30, 2013, 5:20 PM
- */
+#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_
+#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_
-#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H
-#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H
+// Include files for file input.
+#include <istream>
+#include <memory>
+
+// Include boost spirit.
+#include <boost/typeof/typeof.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/phoenix.hpp>
+
+// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
+#include <boost/spirit/include/classic_position_iterator.hpp>
+#include <boost/spirit/include/support_multi_pass.hpp>
+
+namespace qi = boost::spirit::qi;
+namespace phoenix = boost::phoenix;
+
+typedef std::string::const_iterator BaseIteratorType;
+typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
+typedef PositionIteratorType Iterator;
+typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
+typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
+typedef boost::spirit::unused_type Unused;
-// 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"
-// Used for file input.
-#include <istream>
-#include <memory>
+#include "src/storage/prism/Program.h"
+#include "src/storage/expressions/Expression.h"
+using namespace storm::prism;
+using namespace storm::expressions;
namespace storm {
namespace parser {
namespace prism {
-
- using namespace storm::ir;
- using namespace storm::ir::expressions;
-
- struct GlobalVariableInformation {
- std::vector<BooleanVariable> booleanVariables;
- std::vector<IntegerVariable> integerVariables;
- std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
- std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
- };
-
- /*!
- * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of
- * the input that complies with the PRISM syntax.
- */
- class PrismGrammar : public qi::grammar<
- Iterator,
- Program(),
- qi::locals<
- std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
- std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
- std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
- GlobalVariableInformation,
- std::map<std::string, RewardModel>,
- std::map<std::string, std::unique_ptr<BaseExpression>>
- >,
- Skipper> {
+ class PrismGrammar : public qi::grammar<Iterator, Program(), Skipper> {
public:
/*!
* Default constructor that creates an empty and functional grammar.
*/
PrismGrammar();
- /*!
- * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen
- * because modules can involve variables that are only declared afterwards, so the first run
- * creates all variables and the second one tries to parse the full model.
- */
- void prepareForSecondRun();
-
- /*!
- * Resets all sub-grammars, i.e. puts them into an initial state.
- */
- void resetGrammars();
-
private:
-
- std::shared_ptr<storm::parser::prism::VariableState> state;
- struct qi::symbols<char, Module> moduleMap_;
-
// The starting point of the grammar.
- qi::rule<
- Iterator,
- Program(),
- qi::locals<
- std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
- std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
- std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
- GlobalVariableInformation,
- std::map<std::string, RewardModel>,
- std::map<std::string, std::unique_ptr<BaseExpression>>
- >,
- Skipper> start;
+ qi::rule<Iterator, Program(), Skipper> start;
+
+ // Rules for model type.
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
- qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
+
+ // Rules for global constant definitions.
+ qi::rule<Iterator, qi::unused_type(std::set<std::string>&, std::set<std::string>&, std::set<std::string>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&), Skipper> constantDefinitionList;
// Rules for global variable definitions
- qi::rule<Iterator, qi::unused_type(GlobalVariableInformation&), Skipper> globalVariableDefinitionList;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&, std::map<std::string, IntegerVariable>), Skipper> globalVariableDefinitionList;
- // Rules for module definition.
+ // Rules for modules definition.
+ qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
@@ -156,6 +114,9 @@ namespace storm {
storm::parser::prism::modelTypeStruct modelType_;
storm::parser::prism::relationalOperatorStruct relations_;
+ // A mapping from module names to the modules themselves so they can be looked up for renaming later.
+ struct qi::symbols<char, Module> moduleMap_;
+
/*!
* Adds a label with the given name and expression to the given label-to-expression map.
*
@@ -263,5 +224,5 @@ namespace storm {
} // namespace storm
-#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H */
+#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ */
diff --git a/src/parser/prismparser/Tokens.h b/src/parser/prismparser/Tokens.h
index bbf7e8418..bcaefce7b 100644
--- a/src/parser/prismparser/Tokens.h
+++ b/src/parser/prismparser/Tokens.h
@@ -1,75 +1,66 @@
-/*
- * File: Tokens.h
- * Author: nafur
- *
- * Created on April 19, 2013, 11:17 PM
- */
+#ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_
+#define STORM_PARSER_PRISMPARSER_TOKENS_H_
-#ifndef TOKENS_H
-#define TOKENS_H
+#include "src/storage/expressions/Expression.h"
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.
- */
- struct modelTypeStruct : qi::symbols<char, Program::ModelType> {
- modelTypeStruct() {
- add
- ("dtmc", Program::ModelType::DTMC)
- ("ctmc", Program::ModelType::CTMC)
- ("mdp", Program::ModelType::MDP)
- ("ctmdp", Program::ModelType::CTMDP)
- ;
- }
- };
-
-
- /*!
- * A structure defining the keywords that are not allowed to be chosen as identifiers.
- */
- struct keywordsStruct : qi::symbols<char, unsigned> {
- keywordsStruct() {
- add
- ("dtmc", 1)
- ("ctmc", 2)
- ("mdp", 3)
- ("ctmdp", 4)
- ("const", 5)
- ("int", 6)
- ("bool", 7)
- ("module", 8)
- ("endmodule", 9)
- ("rewards", 10)
- ("endrewards", 11)
- ("true", 12)
- ("false", 13)
- ;
- }
- };
-
- /*!
- * 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
- ("=", BinaryRelationExpression::EQUAL)
- ("!=", BinaryRelationExpression::NOT_EQUAL)
- ("<", BinaryRelationExpression::LESS)
- ("<=", BinaryRelationExpression::LESS_OR_EQUAL)
- (">", BinaryRelationExpression::GREATER)
- (">=", BinaryRelationExpression::GREATER_OR_EQUAL)
- ;
- }
- };
-}
-}
+ namespace parser {
+ namespace prism {
+ /*!
+ * 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
+ ("dtmc", Program::ModelType::DTMC)
+ ("ctmc", Program::ModelType::CTMC)
+ ("mdp", Program::ModelType::MDP)
+ ("ctmdp", Program::ModelType::CTMDP)
+ ("ma", Program::ModelType::MA);
+ }
+ };
+
+ /*!
+ * A structure defining the keywords that are not allowed to be chosen as identifiers.
+ */
+ struct keywordsStruct : qi::symbols<char, unsigned> {
+ keywordsStruct() {
+ add
+ ("dtmc", 1)
+ ("ctmc", 2)
+ ("mdp", 3)
+ ("ctmdp", 4)
+ ("ma", 5)
+ ("const", 6)
+ ("int", 7)
+ ("bool", 8)
+ ("module", 9)
+ ("endmodule", 10)
+ ("rewards", 11)
+ ("endrewards", 12)
+ ("true", 13)
+ ("false", 14);
+ }
+ };
+
+ /*!
+ * A structure mapping the textual representation of a binary relation.
+ */
+ struct relationalOperatorStruct : qi::symbols<char, BinaryRelationExpression::RelationType> {
+ relationalOperatorStruct() {
+ add
+ ("=", BinaryRelationExpression::RelationType::EQUAL)
+ ("!=", BinaryRelationExpression::RelationType::NOT_EQUAL)
+ ("<", BinaryRelationExpression::RelationType::LESS)
+ ("<=", BinaryRelationExpression::RelationType::LESS_OR_EQUAL)
+ (">", BinaryRelationExpression::RelationType::GREATER)
+ (">=", BinaryRelationExpression::RelationType::GREATER_OR_EQUAL);
+ }
+ };
+ }
+ }
}
-#endif /* TOKENS_H */
+#endif /* STORM_PARSER_PRISMPARSER_TOKENS_H_ */
diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp
deleted file mode 100644
index 244a3f17e..000000000
--- a/src/parser/prismparser/VariableState.cpp
+++ /dev/null
@@ -1,191 +0,0 @@
-#include "VariableState.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
- using namespace storm::ir;
- using namespace storm::ir::expressions;
-
- template<typename T>
- struct SymbolDump {
- SymbolDump(std::ostream& out) : out(out) {}
- void operator() (std::basic_string<char> s, T elem) {
- this->out << "\t" << s << " -> " << elem << std::endl;
- }
- private:
- std::ostream& out;
- };
- template<typename T>
- std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols) {
- out << "Dumping symbol table" << std::endl;
- SymbolDump<T> dump(out);
- symbols.for_each(dump);
- return out;
- }
- std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) {
- SymbolDump<std::string> dump(out);
- symbols.for_each(dump);
- return out;
- }
-
-
- VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0), nextGlobalCommandIndex(0), nextGlobalUpdateIndex(0) {
- // Nothing to do here.
- }
-
- uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const {
- return this->nextLocalBooleanVariableIndex;
- }
-
- uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const {
- return this->nextLocalIntegerVariableIndex;
- }
-
- uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const {
- return this->nextGlobalBooleanVariableIndex;
- }
-
- uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const {
- return this->nextGlobalIntegerVariableIndex;
- }
-
- uint_fast64_t VariableState::getNextGlobalCommandIndex() const {
- return this->nextGlobalCommandIndex;
- }
-
- uint_fast64_t VariableState::getNextGlobalUpdateIndex() const {
- return this->nextGlobalUpdateIndex;
- }
-
- uint_fast64_t VariableState::addBooleanVariable(std::string const& name) {
- if (firstRun) {
- LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << ".");
- this->booleanVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name)));
- this->booleanVariableNames_.add(name, name);
- ++this->nextGlobalBooleanVariableIndex;
- ++this->nextLocalBooleanVariableIndex;
- return this->nextGlobalBooleanVariableIndex - 1;
- } else {
- std::shared_ptr<VariableExpression> variableExpression = this->booleanVariables_.at(name);
- if (variableExpression != nullptr) {
- return variableExpression->getGlobalVariableIndex();
- } else {
- LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist.");
- throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist.";
- }
- }
- }
-
- uint_fast64_t VariableState::addIntegerVariable(std::string const& name) {
- if (firstRun) {
- LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << ".");
- this->integerVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name)));
- this->integerVariableNames_.add(name, name);
- ++this->nextGlobalIntegerVariableIndex;
- ++this->nextLocalIntegerVariableIndex;
- return this->nextGlobalIntegerVariableIndex - 1;
- } else {
- std::shared_ptr<VariableExpression> variableExpression = this->integerVariables_.at(name);
- if (variableExpression != nullptr) {
- return variableExpression->getGlobalVariableIndex();
- } else {
- LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist.");
- throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist.";
- }
- }
- }
-
- std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(std::string const& name) const {
- std::shared_ptr<VariableExpression> const* variableExpression = this->booleanVariables_.find(name);
- if (variableExpression != nullptr) {
- return *variableExpression;
- } else {
- if (firstRun) {
- LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead.");
- return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::bool_, name));
- } else {
- LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist.");
- throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist.";
- }
- }
- }
-
- std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(std::string const& name) const {
- std::shared_ptr<VariableExpression> const* variableExpression = this->integerVariables_.find(name);
- if (variableExpression != nullptr) {
- return *variableExpression;
- } else {
- if (firstRun) {
- LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead.");
- return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::int_, name));
- } else {
- LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist.");
- throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist.";
- }
- }
- }
-
- std::shared_ptr<VariableExpression> VariableState::getVariableExpression(std::string const& name) const {
- std::shared_ptr<VariableExpression> const* variableExpression = this->integerVariables_.find(name);
- if (variableExpression != nullptr) {
- return *variableExpression;
- }
-
- variableExpression = this->booleanVariables_.find(name);
- if (variableExpression != nullptr) {
- return *variableExpression;
- }
- LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist.");
- throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist.";
- }
-
- void VariableState::clearLocalVariables() {
- this->localBooleanVariables_.clear();
- this->localIntegerVariables_.clear();
- this->nextLocalBooleanVariableIndex = 0;
- this->nextLocalIntegerVariableIndex = 0;
- }
-
- bool VariableState::isFreeIdentifier(std::string const& identifier) const {
- if (this->booleanVariableNames_.find(identifier) != nullptr) return false;
- if (this->integerVariableNames_.find(identifier) != nullptr) return false;
- if (this->allConstantNames_.find(identifier) != nullptr) return false;
- if (this->labelNames_.find(identifier) != nullptr) return false;
- if (this->moduleNames_.find(identifier) != nullptr) return false;
- if (this->keywords.find(identifier) != nullptr) return false;
- if (this->booleanFormulas_.find(identifier) != nullptr) return false;
- if (this->integerFormulas_.find(identifier) != nullptr) return false;
- if (this->doubleFormulas_.find(identifier) != nullptr) return false;
- if (this->constantBooleanFormulas_.find(identifier) != nullptr) return false;
- if (this->constantIntegerFormulas_.find(identifier) != nullptr) return false;
- if (this->constantDoubleFormulas_.find(identifier) != nullptr) return false;
- return true;
- }
-
- bool VariableState::isIdentifier(std::string const& identifier) const {
- if (this->allConstantNames_.find(identifier) != nullptr) return false;
- if (this->keywords.find(identifier) != nullptr) return false;
- return true;
- }
-
- void VariableState::prepareForSecondRun() {
- integerConstants_.clear();
- booleanConstants_.clear();
- doubleConstants_.clear();
- allConstantNames_.clear();
- constantBooleanFormulas_.clear();
- booleanFormulas_.clear();
- constantIntegerFormulas_.clear();
- integerFormulas_.clear();
- constantDoubleFormulas_.clear();
- doubleFormulas_.clear();
- this->firstRun = false;
- nextGlobalCommandIndex = 0;
- nextGlobalUpdateIndex = 0;
- }
-
- } // namespace prism
- } // namespace parser
-} // namespace storm
diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h
deleted file mode 100644
index 6dc7170a4..000000000
--- a/src/parser/prismparser/VariableState.h
+++ /dev/null
@@ -1,207 +0,0 @@
-/*
- * File: VariableState.h
- * Author: nafur
- *
- * Created on April 10, 2013, 4:43 PM
- */
-
-#ifndef STORM_PARSER_PRISMPARSER_VARIABLESTATE_H
-#define STORM_PARSER_PRISMPARSER_VARIABLESTATE_H
-
-#include <iostream>
-
-#include "src/ir/IR.h"
-#include "Includes.h"
-#include "Tokens.h"
-
-namespace storm {
- namespace parser {
- namespace prism {
-
- using namespace storm::ir;
- using namespace storm::ir::expressions;
-
- template<typename T>
- std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols);
-
- /*!
- * This class contains the internal state that is needed for parsing a PRISM model.
- */
- class VariableState {
- public:
- /*!
- * Creates a new variable state object. By default, this object will be set to a state in which
- * it is ready for performing a first run on some input. The first run creates all variables
- * while the second one checks for the correct usage of variables in expressions.
- *
- * @param firstRun If set, this object will be in a state ready for performing the first run. If
- * set to false, this object will assume that it has all variable data already.
- */
- VariableState(bool firstRun = true);
-
- /*!
- * Indicator, if we are still in the first run.
- */
- bool firstRun;
-
- /*!
- * A parser for all reserved keywords.
- */
- keywordsStruct keywords;
-
- /*!
- * Internal counter for the local index of the next new boolean variable.
- */
- uint_fast64_t nextLocalBooleanVariableIndex;
-
- /*!
- * Retrieves the next free local index for a boolean variable.
- *
- * @return The next free local index for a boolean variable.
- */
- uint_fast64_t getNextLocalBooleanVariableIndex() const;
-
- /*!
- * Internal counter for the local index of the next new integer variable.
- */
- uint_fast64_t nextLocalIntegerVariableIndex;
-
- /*!
- * Retrieves the next free global index for a integer variable.
- *
- * @return The next free global index for a integer variable.
- */
- uint_fast64_t getNextLocalIntegerVariableIndex() const;
-
- /*!
- * Internal counter for the index of the next new boolean variable.
- */
- uint_fast64_t nextGlobalBooleanVariableIndex;
-
- /*!
- * Retrieves the next free global index for a boolean variable.
- *
- * @return The next free global index for a boolean variable.
- */
- uint_fast64_t getNextGlobalBooleanVariableIndex() const;
-
- /*!
- * Internal counter for the index of the next new integer variable.
- */
- uint_fast64_t nextGlobalIntegerVariableIndex;
-
- /*!
- * Retrieves the next free global index for a integer variable.
- *
- * @return The next free global index for a integer variable.
- */
- uint_fast64_t getNextGlobalIntegerVariableIndex() const;
-
- /*!
- * Internal counter for the index of the next command.
- */
- uint_fast64_t nextGlobalCommandIndex;
-
- /*!
- * Retrieves the next free global index for a command.
- *
- * @return The next free global index for a command.
- */
- uint_fast64_t getNextGlobalCommandIndex() const;
-
- /*!
- * Internal counter for the index of the next update.
- */
- uint_fast64_t nextGlobalUpdateIndex;
-
- /*!
- * Retrieves the next free global index for an update.
- *
- * @return The next free global index for an update.
- */
- uint_fast64_t getNextGlobalUpdateIndex() const;
-
- // 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_, booleanFormulas_, constantBooleanFormulas_, integerFormulas_, constantIntegerFormulas_, doubleFormulas_, constantDoubleFormulas_;
-
- // A structure representing the identity function over identifier names.
- struct variableNamesStruct : qi::symbols<char, std::string> { }
- integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
- localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_,
- globalBooleanVariables_, globalIntegerVariables_;
-
- /*!
- * Adds a new boolean variable with the given name.
- *
- * @param name The name of the variable.
- * @return The global index of the variable.
- */
- uint_fast64_t addBooleanVariable(std::string const& name);
-
- /*!
- * Adds a new integer variable with the given name.
- *
- * @param name The name of the variable.
- * @return The global index of the variable.
- */
- uint_fast64_t addIntegerVariable(std::string const& name);
-
- /*!
- * Retrieves the variable expression for the boolean variable with the given name.
- *
- * @param name The name of the boolean variable for which to retrieve the variable expression.
- * @return The variable expression for the boolean variable with the given name.
- */
- std::shared_ptr<VariableExpression> getBooleanVariableExpression(std::string const& name) const;
-
- /*!
- * Retrieves the variable expression for the integer variable with the given name.
- *
- * @param name The name of the integer variable for which to retrieve the variable expression.
- * @return The variable expression for the integer variable with the given name.
- */
- std::shared_ptr<VariableExpression> getIntegerVariableExpression(std::string const& name) const;
-
- /*!
- * Retrieve the variable expression for the variable with the given name.
- *
- * @param name The name of the variable for which to retrieve the variable expression.
- * @return The variable expression for the variable with the given name.
- */
- std::shared_ptr<VariableExpression> getVariableExpression(std::string const& name) const;
-
- /*!
- * Clears all local variables.
- */
- void clearLocalVariables();
-
- /*!
- * Check if the given string is a free identifier.
- *
- * @param identifier A string to be checked.
- * @return True iff the given string is a free identifier.
- */
- bool isFreeIdentifier(std::string const& identifier) const;
-
- /*!
- * Check if given string is a valid identifier.
- *
- * @param identifier A string to be checked.
- * @return True iff the given string is an identifier.
- */
- bool isIdentifier(std::string const& identifier) const;
-
- /*!
- * Prepare state to proceed to second parser run. Currently, this clears the constants.
- */
- void prepareForSecondRun();
- };
-
- } // namespace prism
- } // namespace parser
-} // namespace storm
-
-#endif /* STORM_PARSER_PRISMPARSER_VARIABLESTATE_H */
-
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
index 4455ec65d..2c639a535 100644
--- a/src/storage/prism/Assignment.cpp
+++ b/src/storage/prism/Assignment.cpp
@@ -2,11 +2,11 @@
namespace storm {
namespace prism {
- Assignment::Assignment(std::string const& variableName, storm::expressions::Expression const& expression) : variableName(variableName), expression(expression) {
+ Assignment::Assignment(std::string const& variableName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(variableName), expression(expression) {
// Intentionally left empty.
}
- Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming) : variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute<std::map>(renaming)) {
+ Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute<std::map>(renaming)) {
auto renamingPair = renaming.find(oldAssignment.variableName);
if (renamingPair != renaming.end()) {
this->variableName = renamingPair->second;
diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h
index 48a235c8a..955c8417e 100644
--- a/src/storage/prism/Assignment.h
+++ b/src/storage/prism/Assignment.h
@@ -3,34 +3,39 @@
#include <map>
+#include "src/storage/prism/LocatedInformation.h"
#include "src/storage/expressions/Expression.h"
namespace storm {
namespace prism {
- class Assignment {
+ class Assignment : public LocatedInformation {
public:
/*!
* Constructs an assignment using the given variable name and expression.
*
* @param variableName The variable that this assignment targets.
* @param expression The expression to assign to the variable.
+ * @param filename The filename in which the assignment is defined.
+ * @param lineNumber The line number in which the assignment is defined.
*/
- Assignment(std::string const& variableName, storm::expressions::Expression const& expression);
+ Assignment(std::string const& variableName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given assignment and performs the provided renaming.
*
* @param oldAssignment The assignment to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+ * @param filename The filename in which the assignment is defined.
+ * @param lineNumber The line number in which the assignment is defined.
*/
- Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming);
+ Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Assignment() = default;
- Assignment(Assignment const& otherVariable) = default;
- Assignment& operator=(Assignment const& otherVariable)= default;
- Assignment(Assignment&& otherVariable) = default;
- Assignment& operator=(Assignment&& otherVariable) = default;
+ Assignment(Assignment const& other) = default;
+ Assignment& operator=(Assignment const& other)= default;
+ Assignment(Assignment&& other) = default;
+ Assignment& operator=(Assignment&& other) = default;
/*!
* Retrieves the name of the variable that this assignment targets.
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
index 39ea86304..0ce68d34d 100644
--- a/src/storage/prism/BooleanVariable.cpp
+++ b/src/storage/prism/BooleanVariable.cpp
@@ -2,15 +2,15 @@
namespace storm {
namespace prism {
- BooleanVariable::BooleanVariable(std::string const& variableName) : Variable(variableName, storm::expressions::Expression::createFalse(), true) {
+ BooleanVariable::BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, storm::expressions::Expression::createFalse(), true, filename, lineNumber) {
// Nothing to do here.
}
- BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false) {
+ BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, initialValueExpression, false, filename, lineNumber) {
// Nothing to do here.
}
- BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : Variable(oldVariable, newName, renaming) {
+ BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber) {
// Nothing to do here.
}
diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h
index 74c046e00..580a6c33a 100644
--- a/src/storage/prism/BooleanVariable.h
+++ b/src/storage/prism/BooleanVariable.h
@@ -11,26 +11,30 @@ namespace storm {
public:
// Create default implementations of constructors/assignment.
BooleanVariable() = default;
- BooleanVariable(BooleanVariable const& otherVariable) = default;
- BooleanVariable& operator=(BooleanVariable const& otherVariable)= default;
- BooleanVariable(BooleanVariable&& otherVariable) = default;
- BooleanVariable& operator=(BooleanVariable&& otherVariable) = default;
-
+ BooleanVariable(BooleanVariable const& other) = default;
+ BooleanVariable& operator=(BooleanVariable const& other)= default;
+ BooleanVariable(BooleanVariable&& other) = default;
+ BooleanVariable& operator=(BooleanVariable&& other) = default;
+
/*!
- * Creates a boolean variable with the given name and default initial value.
+ * Creates a boolean variable with the given name and the default initial value expression.
*
* @param variableName The name of the variable.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- BooleanVariable(std::string const& variableName);
+ BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber);
/*!
* Creates a boolean variable with the given name and the given constant initial value expression.
*
* @param variableName The name of the variable.
* @param initialValueExpression The constant expression that defines the initial value of the variable.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression);
-
+ BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber);
+
/*!
* Creates a copy of the given boolean variable and performs the provided renaming.
*
@@ -38,8 +42,10 @@ namespace storm {
* @param newName New name of this variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+ BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber);
friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);
};
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index 5624eafdb..038884593 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -2,18 +2,18 @@
namespace storm {
namespace prism {
- Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates) : actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) {
+ Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) {
// Nothing to do here.
}
- Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming) : actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute<std::map>(renaming)), globalIndex(newGlobalIndex) {
+ Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute<std::map>(renaming)), globalIndex(newGlobalIndex) {
auto const& namePair = renaming.find(this->actionName);
if (namePair != renaming.end()) {
this->actionName = namePair->second;
}
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.getUpdates()) {
- this->updates.emplace_back(update, update.getGlobalIndex(), renaming);
+ this->updates.emplace_back(update, update.getGlobalIndex(), renaming, filename, lineNumber);
}
}
diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h
index 8cb905346..5780c3dce 100644
--- a/src/storage/prism/Command.h
+++ b/src/storage/prism/Command.h
@@ -10,7 +10,7 @@
namespace storm {
namespace prism {
- class Command {
+ class Command : public LocatedInformation {
public:
/*!
* Creates a command with the given action name, guard and updates.
@@ -19,8 +19,10 @@ namespace storm {
* @param actionName The action name of the command.
* @param guardExpression the expression that defines the guard of the command.
* @param updates A list of updates that is associated with this command.
+ * @param filename The filename in which the command is defined.
+ * @param lineNumber The line number in which the command is defined.
*/
- Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates);
+ Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given command and performs the provided renaming.
@@ -28,15 +30,17 @@ namespace storm {
* @param oldCommand The command to copy.
* @param newGlobalIndex The global index of the copy of the command.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+ * @param filename The filename in which the command is defined.
+ * @param lineNumber The line number in which the command is defined.
*/
- Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming);
+ Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Command() = default;
- Command(Command const& otherVariable) = default;
- Command& operator=(Command const& otherVariable)= default;
- Command(Command&& otherVariable) = default;
- Command& operator=(Command&& otherVariable) = default;
+ Command(Command const& other) = default;
+ Command& operator=(Command const& other)= default;
+ Command(Command&& other) = default;
+ Command& operator=(Command&& other) = default;
/*!
* Retrieves the action name of this command.
diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp
index 10a3f3e88..47005e6cd 100644
--- a/src/storage/prism/IntegerVariable.cpp
+++ b/src/storage/prism/IntegerVariable.cpp
@@ -2,15 +2,15 @@
namespace storm {
namespace prism {
- IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression) : Variable(variableName, lowerBoundExpression, true), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
+ IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, lowerBoundExpression, true, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
// Intentionally left empty.
}
- IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
+ IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, initialValueExpression, false, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
// Intentionally left empty.
}
- IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : Variable(oldVariable, newName, renaming), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute<std::map>(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute<std::map>(renaming)) {
+ IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute<std::map>(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute<std::map>(renaming)) {
// Intentionally left empty.
}
diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h
index b2dbb4cb5..919bab480 100644
--- a/src/storage/prism/IntegerVariable.h
+++ b/src/storage/prism/IntegerVariable.h
@@ -11,10 +11,10 @@ namespace storm {
public:
// Create default implementations of constructors/assignment.
IntegerVariable() = default;
- IntegerVariable(IntegerVariable const& otherVariable) = default;
- IntegerVariable& operator=(IntegerVariable const& otherVariable)= default;
- IntegerVariable(IntegerVariable&& otherVariable) = default;
- IntegerVariable& operator=(IntegerVariable&& otherVariable) = default;
+ IntegerVariable(IntegerVariable const& other) = default;
+ IntegerVariable& operator=(IntegerVariable const& other)= default;
+ IntegerVariable(IntegerVariable&& other) = default;
+ IntegerVariable& operator=(IntegerVariable&& other) = default;
/*!
* Creates an integer variable with the given name and a default initial value.
@@ -22,8 +22,10 @@ namespace storm {
* @param variableName The name of the variable.
* @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
* @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression);
+ IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates an integer variable with the given name and the given initial value expression.
@@ -32,8 +34,10 @@ namespace storm {
* @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
* @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
* @param initialValueExpression A constant expression that defines the initial value of the variable.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression);
+ IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given integer variable and performs the provided renaming.
@@ -41,8 +45,10 @@ namespace storm {
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+ IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Retrieves an expression defining the lower bound for this integer variable.
diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp
new file mode 100644
index 000000000..94d965e94
--- /dev/null
+++ b/src/storage/prism/LocatedInformation.cpp
@@ -0,0 +1,17 @@
+#include "src/storage/prism/LocatedInformation.h"
+
+namespace storm {
+ namespace prism {
+ LocatedInformation::LocatedInformation(std::string const& filename, uint_fast64_t lineNumber) : filename(filename), lineNumber(lineNumber) {
+ // Intentionally left empty.
+ }
+
+ std::string const& LocatedInformation::getFilename() const {
+ return this->filename;
+ }
+
+ uint_fast64_t LocatedInformation::getLineNumber() const {
+ return this->lineNumber;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h
new file mode 100644
index 000000000..f86060958
--- /dev/null
+++ b/src/storage/prism/LocatedInformation.h
@@ -0,0 +1,48 @@
+#ifndef STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_
+#define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_
+
+#include <string>
+
+namespace storm {
+ namespace prism {
+ class LocatedInformation {
+ public:
+ /*!
+ * Constructs a located information with the given filename and line number.
+ *
+ * @param filename The file in which the information was found.
+ * @param lineNumber The line number in which the information was found.
+ */
+ LocatedInformation(std::string const& filename, uint_fast64_t lineNumber);
+
+ // Create default implementations of constructors/assignment.
+ LocatedInformation(LocatedInformation const& other) = default;
+ LocatedInformation& operator=(LocatedInformation const& other)= default;
+ LocatedInformation(LocatedInformation&& other) = default;
+ LocatedInformation& operator=(LocatedInformation&& other) = default;
+
+ /*!
+ * Retrieves the name of the file in which the information was found.
+ *
+ * @return The name of the file in which the information was found.
+ */
+ std::string const& getFilename() const;
+
+ /*!
+ * Retrieves the line number in which the information was found.
+ *
+ * @return The line number in which the information was found.
+ */
+ uint_fast64_t getLineNumber() const;
+
+ private:
+ // The file in which the piece of information was found.
+ std::string filename;
+
+ // The line in the file in which the piece of information was found.
+ uint_fast64_t lineNumber;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ */
\ No newline at end of file
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 5a90c4bda..78f561734 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -5,24 +5,24 @@
namespace storm {
namespace prism {
- Module::Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() {
+ Module::Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() {
// Initialize the internal mappings for fast information retrieval.
this->collectActions();
}
- Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming) : moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
+ Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown.
for (auto const& nameVariablePair : oldModule.getBooleanVariables()) {
auto renamingPair = renaming.find(nameVariablePair.first);
LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
- this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming));
+ this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber));
}
// Now do the same for the integer variables.
for (auto const& nameVariablePair : oldModule.getIntegerVariables()) {
auto renamingPair = renaming.find(nameVariablePair.first);
LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
- this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming));
+ this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber));
}
// Now we are ready to clone all commands and rename them if requested.
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 789cd0e09..d8f75d13b 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -14,7 +14,7 @@
namespace storm {
namespace prism {
- class Module {
+ class Module : public LocatedInformation {
public:
/*!
* Creates a module with the given name, variables and commands.
@@ -23,10 +23,10 @@ namespace storm {
* @param booleanVariables The boolean variables defined by the module.
* @param integerVariables The integer variables defined by the module.
* @param commands The commands of the module.
+ * @param filename The filename in which the module is defined.
+ * @param lineNumber The line number in which the module is defined.
*/
- Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables,
- std::map<std::string, storm::prism::IntegerVariable> const& integerVariables,
- std::vector<storm::prism::Command> const& commands);
+ Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Special copy constructor, implementing the module renaming functionality. This will create a new module
@@ -35,15 +35,17 @@ namespace storm {
* @param oldModule The module to be copied.
* @param newModuleName The name of the new module.
* @param renaming A mapping of identifiers to the new identifiers they are to be replaced with.
+ * @param filename The filename in which the module is defined.
+ * @param lineNumber The line number in which the module is defined.
*/
- Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming);
+ Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Module() = default;
- Module(Module const& otherVariable) = default;
- Module& operator=(Module const& otherVariable)= default;
- Module(Module&& otherVariable) = default;
- Module& operator=(Module&& otherVariable) = default;
+ Module(Module const& other) = default;
+ Module& operator=(Module const& other)= default;
+ Module(Module&& other) = default;
+ Module& operator=(Module&& other) = default;
/*!
* Retrieves the number of boolean variables in the module.
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index a688a63dd..c01e24c0d 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -5,7 +5,7 @@
namespace storm {
namespace prism {
- Program::Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels) : modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+ Program::Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
Module const& module = this->getModule(moduleIndex);
@@ -52,15 +52,27 @@ namespace storm {
std::set<std::string> const& Program::getUndefinedBooleanConstants() const {
return this->undefinedBooleanConstants;
}
+
+ std::map<std::string, storm::expressions::Expression> const& Program::getDefinedBooleanConstants() const {
+ return this->definedBooleanConstants;
+ }
std::set<std::string> const& Program::getUndefinedIntegerConstants() const {
return this->undefinedIntegerConstants;
}
+ std::map<std::string, storm::expressions::Expression> const& Program::getDefinedIntegerConstants() const {
+ return this->definedIntegerConstants;
+ }
+
std::set<std::string> const& Program::getUndefinedDoubleConstants() const {
return this->undefinedDoubleConstants;
}
-
+
+ std::map<std::string, storm::expressions::Expression> const& Program::getDefinedDoubleConstants() const {
+ return this->definedDoubleConstants;
+ }
+
std::map<std::string, storm::prism::BooleanVariable> const& Program::getGlobalBooleanVariables() const {
return this->globalBooleanVariables;
}
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 3f1b54e0d..36326b12b 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -12,7 +12,7 @@
namespace storm {
namespace prism {
- class Program {
+ class Program : public LocatedInformation {
public:
/*!
* An enum for the different model types.
@@ -25,8 +25,11 @@ namespace storm {
*
* @param modelType The type of the program.
* @param undefinedBooleanConstants The undefined boolean constants of the program.
+ * @param definedBooleanConstants The defined boolean constants of the program.
* @param undefinedIntegerConstants The undefined integer constants of the program.
+ * @param definedIntegerConstants The defined integer constants of the program.
* @param undefinedDoubleConstants The undefined double constants of the program.
+ * @param definedDoubleConstants The defined double constants of the program.
* @param globalBooleanVariables The global boolean variables of the program.
* @param globalIntegerVariables The global integer variables of the program.
* @param modules The modules of the program.
@@ -37,15 +40,17 @@ namespace storm {
* valid) expression, e.g. false.
* @param rewardModels The reward models of the program.
* @param labels The labels defined for this program.
+ * @param filename The filename in which the program is defined.
+ * @param lineNumber The line number in which the program is defined.
*/
- Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels);
+ Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Provide default implementations for constructors and assignments.
Program() = default;
- Program(Program const& otherProgram) = default;
- Program& operator=(Program const& otherProgram) = default;
- Program(Program&& otherProgram) = default;
- Program& operator=(Program&& otherProgram) = default;
+ Program(Program const& other) = default;
+ Program& operator=(Program const& other) = default;
+ Program(Program&& other) = default;
+ Program& operator=(Program&& other) = default;
/*!
* Retrieves the model type of the model.
@@ -89,6 +94,13 @@ namespace storm {
*/
std::set<std::string> const& getUndefinedBooleanConstants() const;
+ /*!
+ * Retrieves the defined boolean constants of the program.
+ *
+ * @return The defined boolean constants of the program.
+ */
+ std::map<std::string, storm::expressions::Expression> const& getDefinedBooleanConstants() const;
+
/*!
* Retrieves the undefined integer constants of the program.
*
@@ -96,6 +108,13 @@ namespace storm {
*/
std::set<std::string> const& getUndefinedIntegerConstants() const;
+ /*!
+ * Retrieves the defined integer constants of the program.
+ *
+ * @return The defined integer constants of the program.
+ */
+ std::map<std::string, storm::expressions::Expression> const& getDefinedIntegerConstants() const;
+
/*!
* Retrieves the undefined double constants of the program.
*
@@ -103,6 +122,13 @@ namespace storm {
*/
std::set<std::string> const& getUndefinedDoubleConstants() const;
+ /*!
+ * Retrieves the defined double constants of the program.
+ *
+ * @return The defined double constants of the program.
+ */
+ std::map<std::string, storm::expressions::Expression> const& getDefinedDoubleConstants() const;
+
/*!
* Retrieves the global boolean variables of the program.
*
@@ -242,15 +268,24 @@ namespace storm {
// The type of the model.
ModelType modelType;
- // A list of undefined boolean constants of the model.
+ // The undefined boolean constants of the program.
std::set<std::string> undefinedBooleanConstants;
- // A list of undefined integer constants of the model.
+ // A mapping of (defined) boolean constants to their values (given as expressions).
+ std::map<std::string, storm::expressions::Expression> definedBooleanConstants;
+
+ // The undefined integer constants of the program.
std::set<std::string> undefinedIntegerConstants;
- // A list of undefined double constants of the model.
+ // A mapping of (defined) integer constants to their values (given as expressions).
+ std::map<std::string, storm::expressions::Expression> definedIntegerConstants;
+
+ // The undefined double constants of the program.
std::set<std::string> undefinedDoubleConstants;
+ // A mapping of (defined) double constants to their values (given as expressions).
+ std::map<std::string, storm::expressions::Expression> definedDoubleConstants;
+
// A list of global boolean variables.
std::map<std::string, BooleanVariable> globalBooleanVariables;
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 006ee1054..a25d58fc9 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -2,7 +2,7 @@
namespace storm {
namespace prism {
- RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
+ RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
// Nothing to do here.
}
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index 6c172c744..9e9498843 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -9,7 +9,7 @@
namespace storm {
namespace prism {
- class RewardModel {
+ class RewardModel : public LocatedInformation {
public:
/*!
* Creates a reward model with the given name, state and transition rewards.
@@ -17,15 +17,17 @@ namespace storm {
* @param rewardModelName The name of the reward model.
* @param stateRewards A vector of state-based rewards.
* @param transitionRewards A vector of transition-based rewards.
+ * @param filename The filename in which the reward model is defined.
+ * @param lineNumber The line number in which the reward model is defined.
*/
- RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards);
+ RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
RewardModel() = default;
- RewardModel(RewardModel const& otherVariable) = default;
- RewardModel& operator=(RewardModel const& otherVariable)= default;
- RewardModel(RewardModel&& otherVariable) = default;
- RewardModel& operator=(RewardModel&& otherVariable) = default;
+ RewardModel(RewardModel const& other) = default;
+ RewardModel& operator=(RewardModel const& other)= default;
+ RewardModel(RewardModel&& other) = default;
+ RewardModel& operator=(RewardModel&& other) = default;
/*!
* Retrieves the name of the reward model.
diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp
index c4bcbd428..7e36406c5 100644
--- a/src/storage/prism/StateReward.cpp
+++ b/src/storage/prism/StateReward.cpp
@@ -2,7 +2,7 @@
namespace storm {
namespace prism {
- StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
+ StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
// Nothing to do here.
}
diff --git a/src/storage/prism/StateReward.h b/src/storage/prism/StateReward.h
index bdd08d446..5eb98886f 100644
--- a/src/storage/prism/StateReward.h
+++ b/src/storage/prism/StateReward.h
@@ -1,11 +1,12 @@
#ifndef STORM_STORAGE_PRISM_STATEREWARD_H_
#define STORM_STORAGE_PRISM_STATEREWARD_H_
+#include "src/storage/prism/LocatedInformation.h"
#include "src/storage/expressions/Expression.h"
namespace storm {
namespace prism {
- class StateReward {
+ class StateReward : public LocatedInformation {
public:
/*!
* Creates a state reward for the states satisfying the given expression with the value given by a second
@@ -13,15 +14,17 @@ namespace storm {
*
* @param statePredicateExpression The predicate that states earning this state-based reward need to satisfy.
* @param rewardValueExpression An expression specifying the values of the rewards to attach to the states.
+ * @param filename The filename in which the state reward is defined.
+ * @param lineNumber The line number in which the state reward is defined.
*/
- StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression);
+ StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
StateReward() = default;
- StateReward(StateReward const& otherVariable) = default;
- StateReward& operator=(StateReward const& otherVariable)= default;
- StateReward(StateReward&& otherVariable) = default;
- StateReward& operator=(StateReward&& otherVariable) = default;
+ StateReward(StateReward const& other) = default;
+ StateReward& operator=(StateReward const& other)= default;
+ StateReward(StateReward&& other) = default;
+ StateReward& operator=(StateReward&& other) = default;
/*!
* Retrieves the state predicate that is associated with this state reward.
diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp
index f972f1270..a5b81e55f 100644
--- a/src/storage/prism/TransitionReward.cpp
+++ b/src/storage/prism/TransitionReward.cpp
@@ -2,7 +2,7 @@
namespace storm {
namespace prism {
- TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
+ TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
// Nothing to do here.
}
diff --git a/src/storage/prism/TransitionReward.h b/src/storage/prism/TransitionReward.h
index 1fb783101..1232e5b51 100644
--- a/src/storage/prism/TransitionReward.h
+++ b/src/storage/prism/TransitionReward.h
@@ -1,11 +1,12 @@
#ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
#define STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
+#include "src/storage/prism/LocatedInformation.h"
#include "src/storage/expressions/Expression.h"
namespace storm {
namespace prism {
- class TransitionReward {
+ class TransitionReward : public LocatedInformation {
public:
/*!
* Creates a transition reward for the transitions with the given name emanating from states satisfying the
@@ -15,15 +16,17 @@ namespace storm {
* @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously
* specified name in order to obtain the reward.
* @param rewardValueExpression An expression specifying the values of the rewards to attach to the transitions.
+ * @param filename The filename in which the transition reward is defined.
+ * @param lineNumber The line number in which the transition reward is defined.
*/
- TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression);
+ TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
TransitionReward() = default;
- TransitionReward(TransitionReward const& otherVariable) = default;
- TransitionReward& operator=(TransitionReward const& otherVariable)= default;
- TransitionReward(TransitionReward&& otherVariable) = default;
- TransitionReward& operator=(TransitionReward&& otherVariable) = default;
+ TransitionReward(TransitionReward const& other) = default;
+ TransitionReward& operator=(TransitionReward const& other)= default;
+ TransitionReward(TransitionReward&& other) = default;
+ TransitionReward& operator=(TransitionReward&& other) = default;
/*!
* Retrieves the action name that is associated with this transition reward.
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index f08627479..da92823bb 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -3,25 +3,25 @@
namespace storm {
namespace prism {
- Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments) : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
+ Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
// Nothing to do here.
}
- Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming) : likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) {
+ Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) {
for (auto const& variableAssignmentPair : update.getBooleanAssignments()) {
auto const& namePair = renaming.find(variableAssignmentPair.first);
if (namePair != renaming.end()) {
- this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming));
+ this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
} else {
- this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming));
+ this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
}
}
for (auto const& variableAssignmentPair : update.getIntegerAssignments()) {
auto const& namePair = renaming.find(variableAssignmentPair.first);
if (renaming.count(variableAssignmentPair.first) > 0) {
- this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming));
+ this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
} else {
- this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming));
+ this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
}
}
this->likelihoodExpression = update.getLikelihoodExpression().substitute<std::map>(renaming);
diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h
index 878e394c3..4999c04bd 100644
--- a/src/storage/prism/Update.h
+++ b/src/storage/prism/Update.h
@@ -3,11 +3,12 @@
#include <map>
-#include "Assignment.h"
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/storage/prism/Assignment.h"
namespace storm {
namespace prism {
- class Update {
+ class Update : public LocatedInformation {
public:
/*!
* Creates an update with the given expression specifying the likelihood and the mapping of variable to
@@ -16,8 +17,10 @@ namespace storm {
* @param globalIndex The global index of the update.
* @param likelihoodExpression An expression specifying the likelihood of this update.
* @param assignments A map of variable names to their assignments.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments);
+ Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given update and performs the provided renaming.
@@ -25,15 +28,17 @@ namespace storm {
* @param update The update that is to be copied.
* @param newGlobalIndex The global index of the resulting update.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming);
+ Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Update() = default;
- Update(Update const& otherVariable) = default;
- Update& operator=(Update const& otherVariable)= default;
- Update(Update&& otherVariable) = default;
- Update& operator=(Update&& otherVariable) = default;
+ Update(Update const& other) = default;
+ Update& operator=(Update const& other)= default;
+ Update(Update&& other) = default;
+ Update& operator=(Update&& other) = default;
/*!
* Retrieves the expression for the likelihood of this update.
diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp
index a6f6f57ae..8ec4f2a98 100644
--- a/src/storage/prism/Variable.cpp
+++ b/src/storage/prism/Variable.cpp
@@ -4,11 +4,11 @@
namespace storm {
namespace prism {
- Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue) : variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) {
+ Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) {
// Nothing to do here.
}
- Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
+ Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
// Intentionally left empty.
}
diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h
index ef77a2c2d..51516bc24 100644
--- a/src/storage/prism/Variable.h
+++ b/src/storage/prism/Variable.h
@@ -3,11 +3,12 @@
#include <map>
+#include "src/storage/prism/LocatedInformation.h"
#include "src/storage/expressions/Expression.h"
namespace storm {
namespace prism {
- class Variable {
+ class Variable : public LocatedInformation {
public:
// Create default implementations of constructors/assignment.
Variable(Variable const& otherVariable) = default;
@@ -47,8 +48,10 @@ namespace storm {
* @param initialValueExpression The constant expression that defines the initial value of the variable.
* @param hasDefaultInitialValue A flag indicating whether the initial value of the variable is its default
* value.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue);
+ Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given variable and performs the provided renaming.
@@ -56,8 +59,10 @@ namespace storm {
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+ * @param filename The filename in which the variable is defined.
+ * @param lineNumber The line number in which the variable is defined.
*/
- Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+ Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
private:
// The name of the variable.