Browse Source

Fixed a few other issues. Module renaming seems to work now!

(However, there is still a segfault at some later point...)
tempestpy_adaptions
gereon 12 years ago
parent
commit
3c1cf4819c
  1. 3
      src/ir/Command.cpp
  2. 9
      src/ir/Module.cpp
  3. 1
      src/ir/Program.cpp
  4. 5
      src/ir/expressions/BinaryRelationExpression.h
  5. 6
      src/ir/expressions/VariableExpression.h
  6. 4
      src/parser/PrismParser.cpp

3
src/ir/Command.cpp

@ -27,9 +27,6 @@ Command::Command(std::string actionName, std::shared_ptr<storm::ir::expressions:
Command::Command(const Command& cmd, 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) Command::Command(const Command& cmd, 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)
: actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) { : actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) {
std::cout << "Cloning command" << std::endl;
std::cout << cmd.guardExpression->dump("\t");
std::cout << this->guardExpression->dump("\t");
if (renaming.count(this->actionName) > 0) { if (renaming.count(this->actionName) > 0) {
this->actionName = renaming.at(this->actionName); this->actionName = renaming.at(this->actionName);
} }

9
src/ir/Module.cpp

@ -23,7 +23,8 @@ Module::Module() : moduleName(), booleanVariables(), integerVariables(), boolean
} }
// Initializes all members according to the given values. // Initializes all members according to the given values.
Module::Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables,
Module::Module(std::string moduleName,
std::vector<storm::ir::BooleanVariable> booleanVariables,
std::vector<storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::IntegerVariable> integerVariables,
std::map<std::string, uint_fast64_t> booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> booleanVariableToIndexMap,
std::map<std::string, uint_fast64_t> integerVariableToIndexMap, std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
@ -41,7 +42,6 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m
for (auto it: renaming) { for (auto it: renaming) {
std::cout << "\t" << it.first << " -> " << it.second << std::endl; std::cout << "\t" << it.first << " -> " << it.second << std::endl;
} }
std::cout << "Current module " << &module << ":" << std::endl << module.toString() << std::endl;
this->booleanVariables.reserve(module.booleanVariables.size()); this->booleanVariables.reserve(module.booleanVariables.size());
for (BooleanVariable it: module.booleanVariables) { for (BooleanVariable it: module.booleanVariables) {
if (renaming.count(it.getName()) > 0) { if (renaming.count(it.getName()) > 0) {
@ -69,10 +69,9 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m
this->commands.reserve(module.commands.size()); this->commands.reserve(module.commands.size());
for (std::shared_ptr<Command> cmd: module.commands) { for (std::shared_ptr<Command> cmd: module.commands) {
std::cout << "2: Current command: " << cmd->toString() << std::endl;
this->commands.emplace_back(new Command(*cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap));
Command* c = new Command(*cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
this->commands.emplace_back(c);
} }
this->collectActions(); this->collectActions();
} }

1
src/ir/Program.cpp

@ -9,6 +9,7 @@
#include "exceptions/InvalidArgumentException.h" #include "exceptions/InvalidArgumentException.h"
#include <sstream> #include <sstream>
#include <iostream>
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"

5
src/ir/expressions/BinaryRelationExpression.h

@ -22,7 +22,6 @@ public:
enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BinaryExpression(bool_, left, right), relationType(relationType) { BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BinaryExpression(bool_, left, right), relationType(relationType) {
std::cerr << "BinaryRelationExpression: " << left.get() << " " << relationType << " " << right.get() << " ?" << std::endl;
} }
virtual ~BinaryRelationExpression() { virtual ~BinaryRelationExpression() {
@ -30,9 +29,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) { 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) {
auto res = std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType));
std::cout << "Cloning " << this->toString() << " to " << res->toString() << std::endl;
return res;
return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType));
} }
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

6
src/ir/expressions/VariableExpression.h

@ -30,17 +30,11 @@ public:
} }
virtual ~VariableExpression() { virtual ~VariableExpression() {
} }
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) { 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::cout << this << " Cloning VarExpr " << this->variableName << " (" << renaming.size() << " renamings)" << std::endl;
for (auto it: renaming) {
std::cout << "\t" << it.first << " -> " << it.second << std::endl;
}
if (renaming.count(this->variableName) > 0) { if (renaming.count(this->variableName) > 0) {
std::string newName = renaming.at(this->variableName); std::string newName = renaming.at(this->variableName);
std::cout << "index of " << newName << " are " << bools.at(newName) << " and " << ints.at(newName) << std::endl;
if (this->getType() == bool_) { 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, this->lowerBound, this->upperBound));
} else if (this->getType() == int_) { } else if (this->getType() == int_) {

4
src/parser/PrismParser.cpp

@ -173,14 +173,14 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type
// This block defines all entities that are needed for parsing a module. // This block defines all entities that are needed for parsing a module.
moduleDefinition = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&prism::VariableState::startModule, *this->state)] moduleDefinition = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&prism::VariableState::startModule, *this->state)]
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
[phoenix::bind(&PrismParser::PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
[qi::_val = phoenix::bind(&PrismParser::PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
moduleDefinition.name("module"); moduleDefinition.name("module");
moduleRenaming = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") moduleRenaming = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
> this->state->moduleNames_ > qi::lit("[") > *( > this->state->moduleNames_ > qi::lit("[") > *(
(prism::IdentifierGrammar::instance(this->state) > qi::lit("=") > prism::IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] (prism::IdentifierGrammar::instance(this->state) > qi::lit("=") > prism::IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
) > qi::lit("]") > qi::lit("endmodule")) ) > qi::lit("]") > qi::lit("endmodule"))
[phoenix::bind(&PrismParser::PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
[qi::_val = phoenix::bind(&PrismParser::PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
moduleRenaming.name("renamed module"); moduleRenaming.name("renamed module");
moduleDefinitionList %= +(moduleDefinition | moduleRenaming); moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
moduleDefinitionList.name("module list"); moduleDefinitionList.name("module list");

Loading…
Cancel
Save