From 12ac3549da0a05f4a3a1f7934f94a2a2a7c48f7b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 5 Sep 2016 14:56:17 +0200
Subject: [PATCH] adapted relevant parts to new way of specifying initial
values/restrictions
Former-commit-id: a55abbe3b616900f5bd721de0eb1bcd1c5f6a5a1 [formerly 6a9d8a6a5577f7f4a524542d5c5a4b201a8c456e]
Former-commit-id: 47799adaf2bd68e8e6c7356410151ab0c31b02a0
---
src/parser/JaniParser.cpp | 2 +-
src/storage/jani/Automaton.cpp | 35 +++++++++++++++++++++-----
src/storage/jani/Automaton.h | 23 ++++++++++-------
src/storage/jani/Exporter.cpp | 30 +++++++++++-----------
src/storage/jani/Model.cpp | 46 +++++++++++++++++++++-------------
src/storage/jani/Model.h | 23 ++++++++++-------
src/storage/jani/Variable.cpp | 4 +++
src/storage/jani/Variable.h | 5 ++++
src/storage/prism/Program.cpp | 30 +++++-----------------
9 files changed, 116 insertions(+), 82 deletions(-)
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index 0ebeb734d..806a26a1f 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -587,7 +587,7 @@ namespace storm {
if(automatonStructure.count("restrict-initial") > 0) {
initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial"), "Initial value restriction for automaton " + name);
}
- automaton.setInitialStatesExpression(initialValueRestriction);
+ automaton.setInitialStatesRestriction(initialValueRestriction);
uint64_t varDeclCount = automatonStructure.count("variables");
STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables");
std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> localVars;
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 29d0f838b..c6d8600e3 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -305,16 +305,39 @@ namespace storm {
return edges.size();
}
- bool Automaton::hasInitialStatesExpression() const {
- return initialStatesExpression.isInitialized();
+ bool Automaton::hasInitialStatesRestriction() const {
+ return initialStatesRestriction.isInitialized();
}
- storm::expressions::Expression const& Automaton::getInitialStatesExpression() const {
- return initialStatesExpression;
+ storm::expressions::Expression const& Automaton::getInitialStatesRestriction() const {
+ return initialStatesRestriction;
}
- void Automaton::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
- this->initialStatesExpression = initialStatesExpression;
+ void Automaton::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
+ this->initialStatesRestriction = initialStatesRestriction;
+ }
+
+ storm::expressions::Expression Automaton::getInitialStatesExpression() const {
+ storm::expressions::Expression result;
+
+ // Add initial state restriction if there is one.
+ if (this->hasInitialStatesRestriction()) {
+ result = this->getInitialStatesRestriction();
+ }
+
+ // Add the expressions for all variables that have initial expressions.
+ for (auto const& variable : this->getVariables()) {
+ if (variable.hasInitExpression()) {
+ storm::expressions::Expression newInitExpression = variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression();
+ if (result.isInitialized()) {
+ result = result && newInitExpression;
+ } else {
+ result = newInitExpression;
+ }
+ }
+ }
+
+ return result;
}
bool Automaton::hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const {
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 3ea6cea4f..1a2ad61dc 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -232,21 +232,26 @@ namespace storm {
* Retrieves the number of edges.
*/
uint64_t getNumberOfEdges() const;
-
+
/*!
- * Retrieves whether there is an expression defining the legal initial values of the automaton's variables.
+ * Retrieves whether this automaton has an initial states restriction.
*/
- bool hasInitialStatesExpression() const;
+ bool hasInitialStatesRestriction() const;
/*!
- * Retrieves the expression defining the legal initial values of the automaton's variables.
+ * Gets the expression restricting the legal initial values of the automaton's variables.
*/
- storm::expressions::Expression const& getInitialStatesExpression() const;
+ storm::expressions::Expression const& getInitialStatesRestriction() const;
/*!
- * Sets the expression defining the legal initial values of the automaton's variables.
+ * Sets the expression restricting the legal initial values of the automaton's variables.
+ */
+ void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);
+
+ /*!
+ * Retrieves the expression defining the legal initial values of the automaton's variables.
*/
- void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+ storm::expressions::Expression getInitialStatesExpression() const;
/*!
* Retrieves whether there is an edge labeled with the action with the given index in this automaton.
@@ -287,8 +292,8 @@ namespace storm {
/// The indices of the initial locations.
std::set<uint64_t> initialLocationIndices;
- /// The expression characterizing the legal initial values of the variables of the automaton.
- storm::expressions::Expression initialStatesExpression;
+ /// The expression restricting the legal initial values of the variables of the automaton.
+ storm::expressions::Expression initialStatesRestriction;
/// The set of action indices that label some action in this automaton.
std::set<uint64_t> actionIndices;
diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp
index 55b5d068f..51635f10a 100644
--- a/src/storage/jani/Exporter.cpp
+++ b/src/storage/jani/Exporter.cpp
@@ -355,7 +355,7 @@ namespace storm {
appendIndent(out, indent + 1);
out << "]";
clearLine(out);
- if (automaton.hasInitialStatesExpression()) {
+ if (automaton.hasInitialStatesRestriction()) {
appendIndent(out, indent + 1);
appendField(out, "initial-states");
clearLine(out);
@@ -413,21 +413,19 @@ namespace storm {
appendVariables(out, model.getGlobalVariables(), 1);
clearLine(out);
- if (model.hasInitialStatesExpression()) {
- appendIndent(out, 1);
- appendField(out, "initial-states");
- clearLine(out);
- appendIndent(out, 2);
- out << "{";
- clearLine(out);
- appendIndent(out, 3);
- appendField(out, "exp");
- appendValue(out, expressionToString(model.getInitialStatesExpression()));
- clearLine(out);
- appendIndent(out, 2);
- out << "}";
- clearLine(out);
- }
+ appendIndent(out, 1);
+ appendField(out, "initial-states");
+ clearLine(out);
+ appendIndent(out, 2);
+ out << "{";
+ clearLine(out);
+ appendIndent(out, 3);
+ appendField(out, "exp");
+ appendValue(out, expressionToString(model.getInitialStatesRestriction()));
+ clearLine(out);
+ appendIndent(out, 2);
+ out << "}";
+ clearLine(out);
appendAutomata(out, model, 1);
clearLine(out);
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 8af4dc560..a9fb3f25e 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -27,6 +27,9 @@ namespace storm {
this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
}
+ // Create an initial restriction.
+ initialStatesRestriction = this->expressionManager->boolean(true);
+
// Add a prefined action that represents the silent action.
silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
}
@@ -301,25 +304,23 @@ namespace storm {
// Substitute constants in all global variables.
for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
+ variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
}
// Substitute constants in initial states expression.
- if (this->hasInitialStatesExpression()) {
- result.setInitialStatesExpression(this->getInitialStatesExpression().substitute(constantSubstitution));
- }
+ result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution));
// Substitute constants in variables of automata and their edges.
for (auto& automaton : result.getAutomata()) {
for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+ variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
}
- if (automaton.hasInitialStatesExpression()) {
- automaton.setInitialStatesExpression(automaton.getInitialStatesExpression().substitute(constantSubstitution));
- }
+ automaton.setInitialStatesRestriction(automaton.getInitialStatesExpression().substitute(constantSubstitution));
for (auto& edge : automaton.getEdges()) {
edge.setGuard(edge.getGuard().substitute(constantSubstitution));
@@ -350,28 +351,39 @@ namespace storm {
return result;
}
- bool Model::hasInitialStatesExpression() const {
- return initialStatesExpression.isInitialized();
+ void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
+ this->initialStatesRestriction = initialStatesRestriction;
}
-
+
+ storm::expressions::Expression const& Model::getInitialStatesRestriction() const {
+ return initialStatesRestriction;
+ }
+
storm::expressions::Expression Model::getInitialStatesExpression(bool includeAutomataInitialStatesExpressions) const {
- STORM_LOG_THROW(globalVariables.empty() || this->hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve global initial states expression, because there is none.");
- storm::expressions::Expression result = this->hasInitialStatesExpression() ? initialStatesExpression : expressionManager->boolean(true);
+ // Start with the restriction of variables.
+ storm::expressions::Expression result = initialStatesRestriction;
+
+ // Then add initial values for those variables that have one.
+ for (auto const& variable : globalVariables) {
+ if (variable.hasInitExpression()) {
+ result = result && (variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression());
+ }
+ }
+
+ // If we are to include the expressions for the automata, do so now.
if (includeAutomataInitialStatesExpressions) {
for (auto const& automaton : automata) {
- STORM_LOG_THROW(automaton.getVariables().empty() || automaton.hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve initial states expression from automaton '" << automaton.getName() << "', because there is none.");
if (!automaton.getVariables().empty()) {
- result = result && automaton.getInitialStatesExpression();
+ storm::expressions::Expression automatonInitialStatesExpression = automaton.getInitialStatesExpression();
+ if (automatonInitialStatesExpression.isInitialized() && !automatonInitialStatesExpression.isTrue()) {
+ result = result && automatonInitialStatesExpression;
+ }
}
}
}
return result;
}
- void Model::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
- this->initialStatesExpression = initialStatesExpression;
- }
-
bool Model::isDeterministicModel() const {
return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
}
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 95163fda9..0379cd5dd 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -236,9 +236,19 @@ namespace storm {
std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
/*!
- * Retrieves whether there is an expression defining the legal initial values of the global variables.
+ * Retrieves whether there is an expression restricting the legal initial values of the global variables.
*/
- bool hasInitialStatesExpression() const;
+ bool hasInitialStatesRestriction() const;
+
+ /*!
+ * Sets the expression restricting the legal initial values of the global variables.
+ */
+ void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);
+
+ /*!
+ * Gets the expression restricting the legal initial values of the global variables.
+ */
+ storm::expressions::Expression const& getInitialStatesRestriction() const;
/*!
* Retrieves the expression defining the legal initial values of the variables.
@@ -248,11 +258,6 @@ namespace storm {
*/
storm::expressions::Expression getInitialStatesExpression(bool includeAutomataInitialStatesExpressions = false) const;
- /*!
- * Sets the expression defining the legal initial values of the global variables.
- */
- void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
-
/*!
* Determines whether this model is a deterministic one in the sense that each state only has one choice.
*/
@@ -329,8 +334,8 @@ namespace storm {
/// An expression describing how the system is composed of the automata.
std::shared_ptr<Composition> composition;
- // The expression characterizing the legal initial values of the global variables.
- storm::expressions::Expression initialStatesExpression;
+ // The expression restricting the legal initial values of the global variables.
+ storm::expressions::Expression initialStatesRestriction;
};
}
}
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index ad7a1de51..57a9289a4 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -48,6 +48,10 @@ namespace storm {
return this->init.get();
}
+ void Variable::setInitExpression(storm::expressions::Expression const& initialExpression) {
+ this->init = initialExpression;
+ }
+
BooleanVariable& Variable::asBooleanVariable() {
return dynamic_cast<BooleanVariable&>(*this);
}
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index d5ba1f20b..820014b03 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -49,6 +49,11 @@ namespace storm {
*/
storm::expressions::Expression const& getInitExpression() const;
+ /*!
+ * Sets the initial expression for this variable.
+ */
+ void setInitExpression(storm::expressions::Expression const& initialExpression);
+
// Methods to determine the type of the variable.
virtual bool isBooleanVariable() const;
virtual bool isBoundedIntegerVariable() const;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index f946fbb98..3562747e7 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1527,7 +1527,6 @@ namespace storm {
default: modelType = storm::jani::ModelType::UNDEFINED;
}
storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
- storm::expressions::Expression globalInitialStatesExpression;
// Add all constants of the PRISM program to the JANI model.
for (auto const& constant : constants) {
@@ -1540,16 +1539,12 @@ namespace storm {
// Add all global variables of the PRISM program to the JANI model.
for (auto const& variable : globalIntegerVariables) {
- storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+ storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
for (auto const& variable : globalBooleanVariables) {
- storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable()));
+ storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression()));
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
// Add all actions of the PRISM program to the JANI model.
@@ -1589,45 +1584,34 @@ namespace storm {
// previously built mapping to make variables global that are read by more than one module.
for (auto const& module : modules) {
storm::jani::Automaton automaton(module.getName());
- storm::expressions::Expression initialStatesExpression;
for (auto const& variable : module.getIntegerVariables()) {
- storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
+ storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
// If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
storm::jani::BoundedIntegerVariable const& newVariable = automaton.addBoundedIntegerVariable(newIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
} else if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global.
storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(newIntegerVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
}
for (auto const& variable : module.getBooleanVariables()) {
- storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable());
+ storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression());
std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
// If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
storm::jani::BooleanVariable const& newVariable = automaton.addBooleanVariable(newBooleanVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
} else if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global.
storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(newBooleanVariable);
variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
}
-
- // Set the proper expression characterizing the initial values of the automaton's variables.
- automaton.setInitialStatesExpression(initialStatesExpression);
+ automaton.setInitialStatesRestriction(manager->boolean(true));
// Create a single location that will have all the edges.
uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
@@ -1663,9 +1647,7 @@ namespace storm {
janiModel.addAutomaton(automaton);
}
-
- // Set the proper expression characterizing the initial values of the global variables.
- janiModel.setInitialStatesExpression(globalInitialStatesExpression);
+ janiModel.setInitialStatesRestriction(manager->boolean(true));
// Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
if (this->specifiesSystemComposition()) {