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

Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support 

Former-commit-id: f16a9b0dad [formerly 2c256c81bc]
Former-commit-id: 8360343131
tempestpy_adaptions
sjunges 8 years ago
parent
d807895298 f49a2cf5a9
commit
5a5d7ce7c8
10 changed files with 104 additions and 83 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. 8
      src/builder/DdJaniModelBuilder.cpp
  2. 14
      src/generator/JaniNextStateGenerator.cpp
  3. 3
      src/generator/JaniNextStateGenerator.h
  4. 12
      src/generator/VariableInformation.cpp
  5. 117
      src/parser/JaniParser.cpp
  6. 6
      src/storage/jani/Automaton.cpp
  7. 6
      src/storage/jani/Model.cpp
  8. 4
      src/storage/jani/Variable.h
  9. 10
      src/storage/jani/VariableSet.cpp
  10. 7
      src/storage/jani/VariableSet.h

8
src/builder/DdJaniModelBuilder.cpp
View File

@ -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() << "'.");
}

14
src/generator/JaniNextStateGenerator.cpp
View File

@ -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.

3
src/generator/JaniNextStateGenerator.h
View File

@ -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.

12
src/generator/VariableInformation.cpp
View File

@ -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()) {

117
src/parser/JaniParser.cpp
View File

@ -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));

6
src/storage/jani/Automaton.cpp
View File

@ -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()) {

6
src/storage/jani/Model.cpp
View File

@ -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());
}

4
src/storage/jani/Variable.h
View File

@ -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 {
};
}
}
}

10
src/storage/jani/VariableSet.cpp
View File

@ -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;
}
}

7
src/storage/jani/VariableSet.h
View File

@ -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.
*/
Write Preview
Loading…
Cancel
Save