Browse Source

transient unbounded variables must have iniatial value

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
commit
04003de854
  1. 2
      src/storm/builder/JaniGSPNBuilder.h
  2. 3
      src/storm/parser/JaniParser.cpp
  3. 2
      src/storm/storage/jani/UnboundedIntegerVariable.cpp
  4. 2
      src/storm/storage/jani/UnboundedIntegerVariable.h

2
src/storm/builder/JaniGSPNBuilder.h

@ -39,7 +39,7 @@ namespace storm {
storm::jani::Variable* janiVar = nullptr;
if (!place.hasRestrictedCapacity()) {
// Effectively no capacity limit known
janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), false);
janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
} else {
assert(place.hasRestrictedCapacity());
janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));

3
src/storm/parser/JaniParser.cpp

@ -609,7 +609,8 @@ namespace storm {
}
return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
}
return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar);
assert(!transientVar); // Checked earlier.
return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName));
} else if(variableStructure.at("type") == "clock") {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << name << "' (scope: " << scopeDescription << ")");
} else if(variableStructure.at("type") == "continuous") {

2
src/storm/storage/jani/UnboundedIntegerVariable.cpp

@ -7,7 +7,7 @@ namespace storm {
// Intentionally left empty.
}
UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) {
UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
// Intentionally left empty.
}

2
src/storm/storage/jani/UnboundedIntegerVariable.h

@ -10,7 +10,7 @@ namespace storm {
/*!
* Creates an unbounded integer variable without initial value.
*/
UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable);
/*!
* Creates an unbounded integer variable with initial value.
*/

Loading…
Cancel
Save