sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Prism to Jani conversion now supports unbounded integer variables

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
8f9ff95531
commit
171ff270e0
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
3 changed files with 45 additions and 7 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      src/storm/storage/jani/UnboundedIntegerVariable.cpp
  2. 5
      src/storm/storage/jani/UnboundedIntegerVariable.h
  3. 38
      src/storm/storage/prism/ToJaniConverter.cpp

9
src/storm/storage/jani/UnboundedIntegerVariable.cpp
View File

@ -19,5 +19,14 @@ namespace storm {
return true;
}
std::shared_ptr<UnboundedIntegerVariable> makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient) {
if (initValue) {
return std::make_shared<UnboundedIntegerVariable>(name, variable, initValue.get(), transient);
} else {
assert(!transient);
return std::make_shared<UnboundedIntegerVariable>(name, variable);
}
}
}
}

5
src/storm/storage/jani/UnboundedIntegerVariable.h
View File

@ -21,5 +21,10 @@ namespace storm {
virtual bool isUnboundedIntegerVariable() const override;
};
/**
* Convenience function to call the appropriate constructor and return a shared pointer to the variable.
*/
std::shared_ptr<UnboundedIntegerVariable> makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient);
}
}

38
src/storm/storage/prism/ToJaniConverter.cpp
View File

@ -129,11 +129,21 @@ namespace storm {
// Add all global variables of the PRISM program to the JANI model.
for (auto const& variable : program.getGlobalIntegerVariables()) {
if (variable.hasInitialValue()) {
storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(),
variable.getExpressionVariable(),
variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
false,
variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none,
variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none);
storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newBoundedIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
} else {
storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(),
variable.getExpressionVariable(),
variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
false);
storm::jani::UnboundedIntegerVariable const& createdVariable = janiModel.addVariable(newUnboundedIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
}
}
@ -344,21 +354,35 @@ namespace storm {
storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix));
for (auto const& variable : module.getIntegerVariables()) {
storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
if (findRes != variablesToMakeGlobal.end()) {
bool makeVarGlobal = findRes->second;
storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newIntegerVariable) : automaton.addVariable(newIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(),
variable.getExpressionVariable(),
variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
false,
variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none,
variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none);
storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBoundedIntegerVariable) : automaton.addVariable(newBoundedIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
} else {
storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(),
variable.getExpressionVariable(),
variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none,
false);
storm::jani::UnboundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newUnboundedIntegerVariable) : automaton.addVariable(newUnboundedIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
}
} else {
STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
}
}
for (auto const& variable : module.getBooleanVariables()) {
storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
if (findRes != variablesToMakeGlobal.end()) {
bool makeVarGlobal = findRes->second;
storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
storm::jani::BooleanVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBooleanVariable) : automaton.addVariable(newBooleanVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
} else {

Write Preview
Loading…
Cancel
Save