From 3ddf87f900e4ce696a64dc2b8fc1887b9eb37f99 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 23 Sep 2016 16:56:40 +0200
Subject: [PATCH] some more fixes for JANI model building
Former-commit-id: 5207670bfbd292ad3c9c9237d1d45b8670fd6353 [formerly 1117c095d56647ab7f6b75213d3e2273d4190fce]
Former-commit-id: f96bdcc91a58a446521a1d62e650aaeeb01776f2
---
src/builder/DdJaniModelBuilder.cpp | 4 ++--
src/parser/ExpressionParser.cpp | 2 ++
src/parser/JaniParser.cpp | 4 ++--
src/storage/jani/Variable.cpp | 6 +++++-
src/storage/jani/Variable.h | 2 +-
5 files changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index c05afd4ca..98f075bac 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -312,7 +312,7 @@ namespace storm {
void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
int_fast64_t low = variable.getLowerBound().evaluateAsInt();
int_fast64_t high = variable.getUpperBound().evaluateAsInt();
- std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getExpressionVariable().getName(), low, high);
STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
@@ -332,7 +332,7 @@ namespace storm {
}
void createVariable(storm::jani::BooleanVariable const& variable, CompositionVariables<Type, ValueType>& result) {
- std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName());
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getExpressionVariable().getName());
STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 3054f2fe0..64a0f9213 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -379,6 +379,8 @@ namespace storm {
STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
if (expression == nullptr) {
+ std::cout << "didn't find " << identifier << std::endl;
+ identifiers_->for_each([] (std::string const& name, storm::expressions::Expression const& expr) { std::cout << "name: " << name << ", " << expr << std::endl; });
pass = false;
return manager->boolean(false);
}
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index bed238255..ebcb07d4a 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -26,7 +26,7 @@ namespace storm {
const bool JaniParser::defaultBooleanInitialValue = false;
const double JaniParser::defaultRationalInitialValue = 0.0;
const int64_t JaniParser::defaultIntegerInitialValue = 0;
- const std::string VARIABLE_AUTOMATON_DELIMITER = "KUCHEN";
+ const std::string VARIABLE_AUTOMATON_DELIMITER = "_";
const std::set<std::string> JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc",
"sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"});
@@ -744,4 +744,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index 9280b7c8e..8551f14df 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -16,6 +16,10 @@ namespace storm {
// Intentionally left empty.
}
+ Variable::~Variable() {
+ // Intentionally left empty.
+ }
+
storm::expressions::Variable const& Variable::getExpressionVariable() const {
return variable;
}
@@ -95,4 +99,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index f58ddab0f..cbbe4aa69 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -27,7 +27,7 @@ namespace storm {
*/
Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false);
- virtual ~Variable() = default;
+ virtual ~Variable();
/*!
* Retrieves the associated expression variable