From 04003de85469bc3451ac11f500cba3ce3fa20a43 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 17:45:19 +0100 Subject: [PATCH] transient unbounded variables must have iniatial value --- src/storm/builder/JaniGSPNBuilder.h | 2 +- src/storm/parser/JaniParser.cpp | 3 ++- src/storm/storage/jani/UnboundedIntegerVariable.cpp | 2 +- src/storm/storage/jani/UnboundedIntegerVariable.h | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/JaniGSPNBuilder.h b/src/storm/builder/JaniGSPNBuilder.h index bab976433..46c0fb095 100644 --- a/src/storm/builder/JaniGSPNBuilder.h +++ b/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())); diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 30dd1fc70..4e1bf346d 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -609,7 +609,8 @@ namespace storm { } return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar); + assert(!transientVar); // Checked earlier. + return std::make_shared(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") { diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.cpp b/src/storm/storage/jani/UnboundedIntegerVariable.cpp index 913d54af4..8cc8ede9f 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.cpp +++ b/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. } diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.h b/src/storm/storage/jani/UnboundedIntegerVariable.h index f1b857469..16f54b723 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.h +++ b/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. */