From f49a2cf5a9a9ee515724acc1fb3b53be3165b32a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Sep 2016 14:48:06 +0200 Subject: [PATCH] added proper location handling to JANI next-state generator Former-commit-id: bd06465daa70a7a1ddff238bd9b5ae2fd3f92201 [formerly 5a5c6f7629093995830c18e23df5a68a34293b95] Former-commit-id: 05a2e55d206014eea8bb78f090547e735bb842ee --- src/builder/DdJaniModelBuilder.cpp | 8 +- src/generator/JaniNextStateGenerator.cpp | 14 ++- src/generator/JaniNextStateGenerator.h | 3 +- src/generator/VariableInformation.cpp | 12 +-- src/parser/JaniParser.cpp | 117 +++++++++++------------ src/storage/jani/Automaton.cpp | 6 +- src/storage/jani/Model.cpp | 6 +- src/storage/jani/Variable.h | 4 +- src/storage/jani/VariableSet.cpp | 10 +- src/storage/jani/VariableSet.h | 7 +- 10 files changed, 104 insertions(+), 83 deletions(-) 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 - CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) { + CompressedState JaniNextStateGenerator::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()); + 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 35f6b21f7..3986f5bec 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -153,7 +153,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(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") { @@ -210,11 +231,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(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); @@ -223,7 +243,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 + ") "); @@ -235,7 +254,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 + ") "); @@ -363,11 +381,10 @@ namespace storm { if(expressionStructure.count("op") == 1) { std::string opstring = getString(expressionStructure.at("op"), scopeDescription); std::vector 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); @@ -565,18 +582,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 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); @@ -623,8 +638,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 @@ -641,7 +655,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; @@ -679,35 +693,10 @@ namespace storm { return automaton; } - - std::vector parseSyncVectors(json const& syncvectorsStructure) { - std::vector syncVectors; - // TODO add error checks - for (auto const& syncEntry : syncvectorsStructure) { - std::vector 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 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) { @@ -720,16 +709,7 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported"); } else { - std::vector syncVectors = parseSyncVectors(compositionStructure.at("syncs")); - std::shared_ptr 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(new storm::jani::AutomatonComposition(name)); - } else { - comp = parseComposition(compositionStructure.at("elements").back().at("automaton")); - } - return std::shared_ptr(new storm::jani::ParallelComposition({comp}, syncVectors)); + // Might be rename or input-enable. } } @@ -742,7 +722,22 @@ namespace storm { } STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once"); - std::vector syncVectors = parseSyncVectors(compositionStructure.at("syncs")); + std::vector syncVectors; + if (compositionStructure.count("syncs") > 0) { + // TODO add error checks + for (auto const& syncEntry : compositionStructure.at("syncs")) { + std::vector 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(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. */