Browse Source

some more fixes for JANI model building

Former-commit-id: 5207670bfb [formerly 1117c095d5]
Former-commit-id: f96bdcc91a
main
dehnert 9 years ago
parent
commit
3ddf87f900
  1. 4
      src/builder/DdJaniModelBuilder.cpp
  2. 2
      src/parser/ExpressionParser.cpp
  3. 4
      src/parser/JaniParser.cpp
  4. 6
      src/storage/jani/Variable.cpp
  5. 2
      src/storage/jani/Variable.h

4
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() << ".");

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

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

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

2
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

Loading…
Cancel
Save