diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 966113a02..c05afd4ca 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -188,13 +188,11 @@ namespace storm {
this->model.getSystemComposition().accept(*this, boost::none);
STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
- // Then, check that the model does not contain unbounded integer or non-transient real variables.
- STORM_LOG_THROW(!this->model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
- for (auto const& automaton : this->model.getAutomata()) {
- STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
- }
+ // Then, check that the model does not contain non-transient unbounded integer or non-transient real variables.
+ STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient global unbounded integer variables.");
STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");
for (auto const& automaton : this->model.getAutomata()) {
+ STORM_LOG_THROW(!automaton.getVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient unbounded integer variables in automaton '" << automaton.getName() << "'.");
STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
}
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 9a675dbfd..49efb76d1 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -204,9 +204,13 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
+ CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable) {
CompressedState newState(state);
+ // Update the location of the state.
+ setLocation(newState, locationVariable, destination.getLocationIndex());
+
+ // Then perform the assignments.
auto assignmentIt = destination.getOrderedAssignments().getNonTransientAssignments().begin();
auto assignmentIte = destination.getOrderedAssignments().getNonTransientAssignments().end();
@@ -233,7 +237,7 @@ namespace storm {
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
-
+
return newState;
}
@@ -339,6 +343,7 @@ namespace storm {
// Iterate over all automata.
uint64_t automatonIndex = 0;
+
for (auto const& automaton : model.getAutomata()) {
uint64_t location = locations[automatonIndex];
@@ -368,7 +373,7 @@ namespace storm {
for (auto const& destination : edge.getDestinations()) {
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
- StateType stateIndex = stateToIdCallback(applyUpdate(state, destination));
+ StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
// Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator.asRational(destination.getProbability());
@@ -418,13 +423,14 @@ namespace storm {
currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+ auto locationVariableIt = this->variableInformation.locationVariables.cbegin();
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::jani::Edge const& edge = **iteratorList[i];
for (auto const& destination : edge.getDestinations()) {
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
- CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination);
+ CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, *locationVariableIt);
// If the new state was already found as a successor state, update the probability
// and otherwise insert it.
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index edd345b9d..7855bc5cf 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/src/generator/JaniNextStateGenerator.h
@@ -54,9 +54,10 @@ namespace storm {
* the given compressed state.
* @params state The state to which to apply the new values.
* @params update The update to apply.
+ * @params locationVariable The location variable that is being updated.
* @return The resulting state.
*/
- CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update);
+ CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable);
/*!
* Retrieves all choices labeled with the silent action possible from the given state.
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index 1e83b2812..125e6089d 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -53,14 +53,12 @@ namespace storm {
}
VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) {
- // Check that the model does not contain unbounded integer or non-real transient variables.
- STORM_LOG_THROW(!model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
+ // Check that the model does not contain non-transient unbounded integer or non-transient real variables.
+ STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains global non-transient real variables.");
+ STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables.");
for (auto const& automaton : model.getAutomata()) {
- STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
- }
- STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");
- for (auto const& automaton : model.getAutomata()) {
- STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
+ STORM_LOG_THROW(!automaton.getVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables in automaton '" << automaton.getName() << "'.");
+ STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
}
for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index be574a421..bed238255 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -154,7 +154,28 @@ namespace storm {
}
if (constantStructure.at("type").is_object()) {
-
+// STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given");
+// std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") ");
+// if(kind == "bounded") {
+// // First do the bounds, that makes the code a bit more streamlined
+// STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
+// storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scopeDescription + ")");
+// assert(lowerboundExpr.isInitialized());
+// STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
+// storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")");
+// assert(upperboundExpr.isInitialized());
+// STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given");
+// std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") ");
+// if(basictype == "int") {
+// STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
+// STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
+// return std::make_shared<storm::jani::BoundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr);
+// } else {
+// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") ");
+// }
+// } else {
+// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") ");
+// }
}
else if(constantStructure.at("type").is_string()) {
if(constantStructure.at("type") == "real") {
@@ -211,11 +232,10 @@ namespace storm {
expressionManager->declareRationalVariable(name);
if(initvalcount == 1) {
if(variableStructure.at("initial-value").is_null()) {
- STORM_LOG_WARN("Deprecated null value in initial value");
initVal = expressionManager->rational(defaultRationalInitialValue);
} else {
initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
- STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational");
+ STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational");
}
return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
@@ -224,7 +244,6 @@ namespace storm {
} else if(variableStructure.at("type") == "bool") {
if(initvalcount == 1) {
if(variableStructure.at("initial-value").is_null()) {
- STORM_LOG_WARN("Deprecated null value in initial value");
initVal = expressionManager->boolean(defaultBooleanInitialValue);
} else {
initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
@@ -236,7 +255,6 @@ namespace storm {
} else if(variableStructure.at("type") == "int") {
if(initvalcount == 1) {
if(variableStructure.at("initial-value").is_null()) {
- STORM_LOG_WARN("Deprecated null value in initial value");
initVal = expressionManager->integer(defaultIntegerInitialValue);
} else {
initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
@@ -364,11 +382,10 @@ namespace storm {
if(expressionStructure.count("op") == 1) {
std::string opstring = getString(expressionStructure.at("op"), scopeDescription);
std::vector<storm::expressions::Expression> arguments = {};
- if(opstring == "ite") {
- storm::expressions::Expression ifexpr = parseExpression(expressionStructure.at("if"), "If argument of operator ite in " + scopeDescription, localVars);
- storm::expressions::Expression thenexpr = parseExpression(expressionStructure.at("then"), "Then argument of operator ite in " + scopeDescription, localVars);
- storm::expressions::Expression elseexpr = parseExpression(expressionStructure.at("else"), "Else argument of operator ite in " + scopeDescription, localVars);
- return storm::expressions::ite(ifexpr, thenexpr, elseexpr);
+ if(opstring == "?:") {
+ ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription);
+ assert(arguments.size() == 3);
+ return storm::expressions::ite(arguments[0], arguments[1], arguments[2]);
} else if (opstring == "∨") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
assert(arguments.size() == 2);
@@ -566,18 +583,16 @@ namespace storm {
STORM_LOG_THROW(locEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name");
std::string locName = getString(locEntry.at("name"), "location of automaton " + name);
STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'");
- STORM_LOG_THROW(locEntry.count("time-progress") == 0, storm::exceptions::InvalidJaniException, "Time progress conditions in locations as in '" + locName + "' in automaton '" + name + "' are not supported");
+ STORM_LOG_THROW(locEntry.count("invariant") == 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' in automaton '" + name + "' are not supported");
//STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType()));
std::vector<storm::jani::Assignment> transientAssignments;
- if (locEntry.count("transient-values") > 0) {
- for(auto const& transientValueEntry : locEntry.at("transient-values")) {
- STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
- STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
- storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
- STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
- storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
- transientAssignments.emplace_back(lhs, rhs);
- }
+ for(auto const& transientValueEntry : locEntry.at("transient-values")) {
+ STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
+ STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
+ storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
+ STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
+ storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
+ transientAssignments.emplace_back(lhs, rhs);
}
uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments));
locIds.emplace(locName, id);
@@ -624,8 +639,7 @@ namespace storm {
STORM_LOG_THROW(edgeEntry.count("rate") < 2, storm::exceptions::InvalidJaniException, "Edge from '" << sourceLoc << "' in automaton '" << name << "' has multiple rates");
storm::expressions::Expression rateExpr;
if(edgeEntry.count("rate") > 0) {
- STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' has no expression");
- rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), "Rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'");
+ rateExpr = parseExpression(edgeEntry.at("rate"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'");
STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type");
}
// guard
@@ -642,7 +656,7 @@ namespace storm {
for(auto const& destEntry : edgeEntry.at("destinations")) {
// target location
STORM_LOG_THROW(edgeEntry.count("location") == 1, storm::exceptions::InvalidJaniException, "Each destination in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a target location");
- std::string targetLoc = getString(edgeEntry.at("location"), "target location for edge from '" + sourceLoc + "' in automaton '" + name + "'");
+ std::string targetLoc = getString(destEntry.at("location"), "target location for edge from '" + sourceLoc + "' in automaton '" + name + "'");
STORM_LOG_THROW(locIds.count(targetLoc) == 1, storm::exceptions::InvalidJaniException, "Target of edge has unknown location '" << targetLoc << "' in automaton '" << name << "'.");
// probability
storm::expressions::Expression probExpr;
@@ -680,35 +694,10 @@ namespace storm {
return automaton;
}
-
- std::vector<storm::jani::SynchronizationVector> parseSyncVectors(json const& syncvectorsStructure) {
- std::vector<storm::jani::SynchronizationVector> syncVectors;
- // TODO add error checks
- for (auto const& syncEntry : syncvectorsStructure) {
- std::vector<std::string> inputs;
- for (auto const& syncInput : syncEntry.at("synchronise")) {
- if(syncInput.is_null()) {
- inputs.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
- } else {
- inputs.push_back(syncInput);
- }
- }
- if (syncEntry.count("result") > 0) {
- std::string syncResult = syncEntry.at("result");
- syncVectors.emplace_back(inputs, syncResult);
- } else {
- syncVectors.emplace_back(inputs);
- }
-
- }
- return syncVectors;
-
- }
-
std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
- STORM_LOG_THROW(compositionStructure.count("elements") > 0, storm::exceptions::InvalidJaniException, "Elements of a composition must be given.");
- STORM_LOG_THROW(compositionStructure.count("elements") < 2, storm::exceptions::InvalidJaniException, "Elements of a composition must be given at most once.");
+
+ STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given");
if (compositionStructure.at("elements").size() == 1) {
if (compositionStructure.count("syncs") == 0) {
@@ -721,16 +710,7 @@ namespace storm {
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported");
} else {
- std::vector<storm::jani::SynchronizationVector> syncVectors = parseSyncVectors(compositionStructure.at("syncs"));
- std::shared_ptr<storm::jani::Composition> comp;
- if (compositionStructure.at("elements").back().at("automaton").is_string()) {
- std::string name = compositionStructure.at("elements").back().at("automaton");
- // TODO check whether name exist?
- comp = std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
- } else {
- comp = parseComposition(compositionStructure.at("elements").back().at("automaton"));
- }
- return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition({comp}, syncVectors));
+ // Might be rename or input-enable.
}
}
@@ -743,7 +723,22 @@ namespace storm {
}
STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
- std::vector<storm::jani::SynchronizationVector> syncVectors = parseSyncVectors(compositionStructure.at("syncs"));
+ std::vector<storm::jani::SynchronizationVector> syncVectors;
+ if (compositionStructure.count("syncs") > 0) {
+ // TODO add error checks
+ for (auto const& syncEntry : compositionStructure.at("syncs")) {
+ std::vector<std::string> inputs;
+ for (auto const& syncInput : syncEntry.at("synchronise")) {
+ if(syncInput.is_null()) {
+ // TODO handle null;
+ } else {
+ inputs.push_back(syncInput);
+ }
+ }
+ std::string syncResult = syncEntry.at("result");
+ syncVectors.emplace_back(inputs, syncResult);
+ }
+ }
return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 8341cbc6e..fcb843112 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -358,8 +358,12 @@ namespace storm {
result = this->getInitialStatesRestriction();
}
- // Add the expressions for all variables that have initial expressions.
+ // Add the expressions for all non-transient variables that have initial expressions.
for (auto const& variable : this->getVariables()) {
+ if (variable.isTransient()) {
+ continue;
+ }
+
if (variable.hasInitExpression()) {
storm::expressions::Expression newInitExpression = variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression();
if (result.isInitialized()) {
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 51f80e01b..5c6dbf273 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -399,8 +399,12 @@ namespace storm {
// Start with the restriction of variables.
storm::expressions::Expression result = initialStatesRestriction;
- // Then add initial values for those variables that have one.
+ // Then add initial values for those non-transient variables that have one.
for (auto const& variable : globalVariables) {
+ if (variable.isTransient()) {
+ continue;
+ }
+
if (variable.hasInitExpression()) {
result = result && (variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression());
}
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index 1add2768b..f58ddab0f 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -27,6 +27,8 @@ namespace storm {
*/
Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false);
+ virtual ~Variable() = default;
+
/*!
* Retrieves the associated expression variable
*/
@@ -93,4 +95,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index 137c3603d..a5468f63a 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -147,7 +147,15 @@ namespace storm {
bool VariableSet::containsNonTransientRealVariables() const {
for (auto const& variable : realVariables) {
if (!variable->isTransient()) {
- std::cout << "var " << variable->getName() << "is non-transient " << std::endl;
+ return true;
+ }
+ }
+ return false;
+ }
+
+ bool VariableSet::containsNonTransientUnboundedIntegerVariables() const {
+ for (auto const& variable : unboundedIntegerVariables) {
+ if (!variable->isTransient()) {
return true;
}
}
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index db8d0de6a..1c947669e 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -157,7 +157,12 @@ namespace storm {
* Retrieves whether the set of variables contains a non-transient real variable.
*/
bool containsNonTransientRealVariables() const;
-
+
+ /*!
+ * Retrieves whether the set of variables contains a non-transient unbounded integer variable.
+ */
+ bool containsNonTransientUnboundedIntegerVariables() const;
+
/*!
* Retrieves whether this variable set is empty.
*/