diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 40d40fb2f..be2ec770f 100644
--- a/src/ir/Module.cpp
+++ b/src/ir/Module.cpp
@@ -42,18 +42,32 @@ Module::Module(std::string moduleName,
Module::Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, std::shared_ptr<VariableAdder> adder)
: moduleName(moduleName) {
LOG4CPLUS_DEBUG(logger, "Start renaming " << module.moduleName << " to " << moduleName);
- this->booleanVariables.reserve(module.booleanVariables.size());
+
+ // First step: Create new Variables via the adder.
for (BooleanVariable it: module.booleanVariables) {
if (renaming.count(it.getName()) > 0) {
- this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder->addBooleanVariable(renaming.at(it.getName()), it.getInitialValue());
+ adder->addBooleanVariable(renaming.at(it.getName()), it.getInitialValue());
} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
}
- this->integerVariables.reserve(module.integerVariables.size());
for (IntegerVariable it: module.integerVariables) {
if (renaming.count(it.getName()) > 0) {
- this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder->addIntegerVariable(renaming.at(it.getName()), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
+ adder->addIntegerVariable(renaming.at(it.getName()), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
}
+
+ // Second step: Get all indices of variables that are produced by the renaming.
+ for (auto it: renaming) {
+ std::shared_ptr<expressions::VariableExpression> var = adder->getVariable(it.second);
+ if (var != nullptr) {
+ if (var->getType() == expressions::BaseExpression::bool_) {
+ this->booleanVariablesToIndexMap[it.second] = var->getVariableIndex();
+ } else if (var->getType() == expressions::BaseExpression::int_) {
+ this->integerVariablesToIndexMap[it.second] = var->getVariableIndex();
+ }
+ }
+ }
+
+ // Third step: Create new Variable objects.
this->booleanVariables.reserve(module.booleanVariables.size());
for (BooleanVariable it: module.booleanVariables) {
if (renaming.count(it.getName()) > 0) {
@@ -66,7 +80,8 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m
this->integerVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
}
-
+
+ // Fourth step: Clone commands.
this->commands.reserve(module.commands.size());
for (Command cmd: module.commands) {
this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
diff --git a/src/ir/Module.h b/src/ir/Module.h
index 8bc465b44..6e653ce47 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -10,6 +10,7 @@
#include "BooleanVariable.h"
#include "IntegerVariable.h"
+#include "expressions/VariableExpression.h"
#include "Command.h"
#include <map>
@@ -25,6 +26,7 @@ namespace ir {
struct VariableAdder {
virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) = 0;
virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) = 0;
+ virtual std::shared_ptr<expressions::VariableExpression> getVariable(const std::string& name) = 0;
};
/*!
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
index a8d3377a9..98f8f2ee2 100644
--- a/src/ir/expressions/BaseExpression.h
+++ b/src/ir/expressions/BaseExpression.h
@@ -34,6 +34,9 @@ public:
BaseExpression(ReturnType type) : type(type) {
}
+ BaseExpression(const BaseExpression& be)
+ : type(be.type) {
+ }
virtual ~BaseExpression() {
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
index 3897c0cc6..529f6ea90 100644
--- a/src/ir/expressions/BinaryExpression.h
+++ b/src/ir/expressions/BinaryExpression.h
@@ -22,11 +22,6 @@ class BinaryExpression : public BaseExpression {
public:
BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right)
: BaseExpression(type), left(left), right(right) {
- if (left == nullptr || right == nullptr) {
- std::cerr << "BinaryExpression" << std::endl;
- if (left != nullptr) std::cerr << "\tleft: " << left->toString() << std::endl;
- if (right != nullptr) std::cerr << "\tright: " << right->toString() << std::endl;
- }
}
std::shared_ptr<BaseExpression> const& getLeft() const {
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
index 2a01a600a..2f3889b01 100644
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ b/src/ir/expressions/BooleanConstantExpression.h
@@ -24,13 +24,16 @@ public:
defined = false;
value = false;
}
+ BooleanConstantExpression(const BooleanConstantExpression& bce)
+ : ConstantExpression(bce), value(bce.value), defined(bce.defined) {
+ }
virtual ~BooleanConstantExpression() {
}
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
- return std::shared_ptr<BaseExpression>(this);
+ return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
}
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h
index b1be49e58..239dca81c 100644
--- a/src/ir/expressions/ConstantExpression.h
+++ b/src/ir/expressions/ConstantExpression.h
@@ -21,6 +21,9 @@ public:
std::string constantName;
ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) {
+ }
+ ConstantExpression(const ConstantExpression& ce)
+ : BaseExpression(ce), constantName(ce.constantName) {
}
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
index dc8cd7920..f6e26271d 100644
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ b/src/ir/expressions/DoubleConstantExpression.h
@@ -19,7 +19,10 @@ namespace expressions {
class DoubleConstantExpression : public ConstantExpression {
public:
DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) {
-
+ }
+
+ DoubleConstantExpression(const DoubleConstantExpression& dce)
+ : ConstantExpression(dce), defined(dce.defined), value(dce.value) {
}
virtual ~DoubleConstantExpression() {
@@ -27,7 +30,7 @@ public:
}
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
- return std::shared_ptr<BaseExpression>(this);
+ return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
}
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
index 8d916bf7f..c4ad56ed7 100644
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ b/src/ir/expressions/IntegerConstantExpression.h
@@ -20,13 +20,16 @@ class IntegerConstantExpression : public ConstantExpression {
public:
IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) {
}
+ IntegerConstantExpression(const IntegerConstantExpression& ice)
+ : ConstantExpression(ice), defined(ice.defined), value(ice.value) {
+ }
virtual ~IntegerConstantExpression() {
}
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
- return std::shared_ptr<BaseExpression>(this);
+ return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
}
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index e14e33d7e..54bebce72 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -13,6 +13,10 @@
#include <memory>
#include <iostream>
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+extern log4cplus::Logger logger;
+
namespace storm {
namespace ir {
@@ -26,26 +30,27 @@ public:
std::shared_ptr<BaseExpression> upperBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr))
: BaseExpression(type), index(index), variableName(variableName),
lowerBound(lowerBound), upperBound(upperBound) {
- std::cerr << "Creating " << this << std::endl;
}
virtual ~VariableExpression() {
- std::cerr << "Destroying " << this << std::endl;
}
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+ std::shared_ptr<BaseExpression> lower = this->lowerBound, upper = this->upperBound;
+ if (lower != nullptr) lower = lower->clone(renaming, bools, ints);
+ if (upper != nullptr) upper = upper->clone(renaming, bools, ints);
if (renaming.count(this->variableName) > 0) {
std::string newName = renaming.at(this->variableName);
if (this->getType() == bool_) {
- return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, this->lowerBound, this->upperBound));
+ return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, lower, upper));
} else if (this->getType() == int_) {
- return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, this->lowerBound, this->upperBound));
+ return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, lower, upper));
} else {
- std::cerr << "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int." << std::endl;
- return std::shared_ptr<BaseExpression>(this);
+ LOG4CPLUS_ERROR(logger, "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int.");
+ return std::shared_ptr<BaseExpression>(nullptr);
}
} else {
- return std::shared_ptr<BaseExpression>(this);
+ return std::shared_ptr<BaseExpression>(new VariableExpression(this->getType(), this->index, this->variableName, lower, upper));
}
}
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 08f534691..903a02d6a 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -72,13 +72,13 @@ namespace parser {
throw "Renaming module failed";
}
Module res(*old, name, mapping, this->state);
- this->state->moduleMap_.add(name, res);
+ this->state->moduleMap_.at(name) = res;
return res;
}
Module PrismParser::PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands) {
this->state->moduleNames_.add(name, name);
Module res(name, bools, ints, boolids, intids, commands);
- this->state->moduleMap_.add(name, res);
+ this->state->moduleMap_.at(name) = res;
return res;
}
diff --git a/src/parser/PrismParser/VariableState.cpp b/src/parser/PrismParser/VariableState.cpp
index 117edf954..dee14bcb3 100644
--- a/src/parser/PrismParser/VariableState.cpp
+++ b/src/parser/PrismParser/VariableState.cpp
@@ -97,6 +97,20 @@ std::shared_ptr<VariableExpression> VariableState::getIntegerVariable(const std:
}
}
}
+std::shared_ptr<VariableExpression> VariableState::getVariable(const std::string& name) {
+ std::shared_ptr<VariableExpression>* res = this->integerVariables_.find(name);
+ if (res != nullptr) {
+ return *res;
+ } else {
+ res = this->booleanVariables_.find(name);
+ if (res != nullptr) {
+ return *res;
+ } else {
+ LOG4CPLUS_ERROR(logger, "Getting variable " << name << ", but was not found. This variable does not exist.");
+ return std::shared_ptr<VariableExpression>(nullptr);
+ }
+ }
+}
void VariableState::startModule() {
this->localBooleanVariables_.clear();
diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h
index 6293da58b..c4046e658 100644
--- a/src/parser/PrismParser/VariableState.h
+++ b/src/parser/PrismParser/VariableState.h
@@ -47,12 +47,11 @@ public:
localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
public:
uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
-
uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name);
-
std::shared_ptr<VariableExpression> getIntegerVariable(const std::string& name);
+ std::shared_ptr<VariableExpression> getVariable(const std::string& name);
void startModule();