Browse Source

Fixed a few more bugs in clone() of various Expression classes and some in the module renaming.

tempestpy_adaptions
gereon 12 years ago
parent
commit
4222130524
  1. 25
      src/ir/Module.cpp
  2. 2
      src/ir/Module.h
  3. 3
      src/ir/expressions/BaseExpression.h
  4. 5
      src/ir/expressions/BinaryExpression.h
  5. 5
      src/ir/expressions/BooleanConstantExpression.h
  6. 3
      src/ir/expressions/ConstantExpression.h
  7. 7
      src/ir/expressions/DoubleConstantExpression.h
  8. 5
      src/ir/expressions/IntegerConstantExpression.h
  9. 19
      src/ir/expressions/VariableExpression.h
  10. 4
      src/parser/PrismParser.cpp
  11. 14
      src/parser/PrismParser/VariableState.cpp
  12. 3
      src/parser/PrismParser/VariableState.h

25
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);

2
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;
};
/*!

3
src/ir/expressions/BaseExpression.h

@ -34,6 +34,9 @@ public:
BaseExpression(ReturnType type) : type(type) {
}
BaseExpression(const BaseExpression& be)
: type(be.type) {
}
virtual ~BaseExpression() {

5
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 {

5
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 {

3
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) {
}

7
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 {

5
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 {

19
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));
}
}

4
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;
}

14
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();

3
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();

Loading…
Cancel
Save