diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp
index 244eaa0b5..4e5c975b0 100644
--- a/src/storm/storage/jani/ArrayEliminator.cpp
+++ b/src/storm/storage/jani/ArrayEliminator.cpp
@@ -404,6 +404,7 @@ namespace storm {
public:
typedef ArrayEliminatorData ResultType;
+ using JaniTraverser::traverse;
ArrayVariableReplacer(storm::expressions::ExpressionManager& expressionManager, bool keepNonTrivialArrayAccess, std::unordered_map<storm::expressions::Variable, std::size_t> const& arrayVarToSizesMap) : expressionManager(expressionManager) , keepNonTrivialArrayAccess(keepNonTrivialArrayAccess), arraySizes(arrayVarToSizesMap) {}
@@ -470,19 +471,27 @@ namespace storm {
arrayExprEliminator = std::make_unique<ArrayExpressionEliminationVisitor>(replacements, arraySizes);
for (auto& loc : automaton.getLocations()) {
- JaniTraverser::traverse(loc, data);
+ traverse(loc, data);
}
- JaniTraverser::traverse(automaton.getEdgeContainer(), data);
+ traverse(automaton.getEdgeContainer(), data);
if (automaton.hasInitialStatesRestriction()) {
automaton.setInitialStatesRestriction(arrayExprEliminator->eliminate(automaton.getInitialStatesRestriction()));
}
}
-
+
+ virtual void traverse(Location& location, boost::any const& data) override {
+ traverse(location.getAssignments(), data);
+ if (location.hasTimeProgressInvariant()) {
+ location.setTimeProgressInvariant(arrayExprEliminator->eliminate(location.getTimeProgressInvariant()));
+ traverse(location.getTimeProgressInvariant(), data);
+ }
+ }
+
void traverse(TemplateEdge& templateEdge, boost::any const& data) override {
templateEdge.setGuard(arrayExprEliminator->eliminate(templateEdge.getGuard()));
for (auto& dest : templateEdge.getDestinations()) {
- JaniTraverser::traverse(dest, data);
+ traverse(dest, data);
}
traverse(templateEdge.getAssignments(), data);
}
@@ -493,7 +502,7 @@ namespace storm {
edge.setRate(arrayExprEliminator->eliminate(edge.getRate()));
}
for (auto& dest : edge.getDestinations()) {
- JaniTraverser::traverse(dest, data);
+ traverse(dest, data);
}
}
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index 37924c221..beba4b92e 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -36,6 +36,8 @@ namespace storm {
return addVariable(variable.asRealVariable());
} else if (variable.isArrayVariable()) {
return addVariable(variable.asArrayVariable());
+ } else if (variable.isClockVariable()) {
+ return addVariable(variable.asClockVariable());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
}
@@ -60,6 +62,10 @@ namespace storm {
ArrayVariable const& Automaton::addVariable(ArrayVariable const& variable) {
return variables.addVariable(variable);
}
+
+ ClockVariable const& Automaton::addVariable(ClockVariable const& variable) {
+ return variables.addVariable(variable);
+ }
bool Automaton::hasVariable(std::string const& name) const {
return variables.hasVariable(name);
@@ -440,6 +446,9 @@ namespace storm {
for (auto& variable : this->getVariables().getArrayVariables()) {
variable.substitute(substitution);
}
+ for (auto& variable : this->getVariables().getClockVariables()) {
+ variable.substitute(substitution);
+ }
for (auto& location : this->getLocations()) {
location.substitute(substitution);
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index 0dd74eeb9..809ddb1cc 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -75,6 +75,11 @@ namespace storm {
*/
ArrayVariable const& addVariable(ArrayVariable const& variable);
+ /*!
+ * Adds the given array variable to this automaton.
+ */
+ ClockVariable const& addVariable(ClockVariable const& variable);
+
/*!
* Retrieves the variables of this automaton.
*/
diff --git a/src/storm/storage/jani/ClockVariable.cpp b/src/storm/storage/jani/ClockVariable.cpp
new file mode 100644
index 000000000..17340892a
--- /dev/null
+++ b/src/storm/storage/jani/ClockVariable.cpp
@@ -0,0 +1,32 @@
+#include "storm/storage/jani/ClockVariable.h"
+
+namespace storm {
+ namespace jani {
+
+ ClockVariable::ClockVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
+ // Intentionally left empty.
+ }
+
+ ClockVariable::ClockVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+ // Intentionally left empty.
+ }
+
+ std::unique_ptr<Variable> ClockVariable::clone() const {
+ return std::make_unique<ClockVariable>(*this);
+ }
+
+ bool ClockVariable::isClockVariable() const {
+ return true;
+ }
+
+ std::shared_ptr<ClockVariable> makeClockVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient) {
+ if (initValue) {
+ return std::make_shared<ClockVariable>(name, variable, initValue.get(), transient);
+ } else {
+ assert(!transient);
+ return std::make_shared<ClockVariable>(name, variable);
+ }
+ }
+
+ }
+}
diff --git a/src/storm/storage/jani/ClockVariable.h b/src/storm/storage/jani/ClockVariable.h
new file mode 100644
index 000000000..cf32a6b24
--- /dev/null
+++ b/src/storm/storage/jani/ClockVariable.h
@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm/storage/jani/Variable.h"
+
+namespace storm {
+ namespace jani {
+
+ class ClockVariable : public Variable {
+ public:
+
+ /*!
+ * Creates a clock variable
+ */
+ ClockVariable(std::string const& name, storm::expressions::Variable const& variable);
+
+ /*!
+ * Creates a clock variable with initial value
+ */
+ ClockVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue, bool transient=false);
+
+ virtual std::unique_ptr<Variable> clone() const override;
+
+ virtual bool isClockVariable() const override;
+ };
+
+ /**
+ * Convenience function to call the appropriate constructor and return a shared pointer to the variable.
+ */
+ std::shared_ptr<ClockVariable> makeClockVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient);
+
+ }
+}
diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp
index 32a9895de..c81ffbeae 100644
--- a/src/storm/storage/jani/FunctionEliminator.cpp
+++ b/src/storm/storage/jani/FunctionEliminator.cpp
@@ -200,6 +200,8 @@ namespace storm {
class FunctionEliminatorTraverser : public JaniTraverser {
public:
+
+ using JaniTraverser::traverse;
FunctionEliminatorTraverser() = default;
@@ -277,7 +279,7 @@ namespace storm {
for (auto& c : model.getConstants()) {
traverse(c, &globalFunctionEliminationVisitor);
}
- JaniTraverser::traverse(model.getGlobalVariables(), &globalFunctionEliminationVisitor);
+ traverse(model.getGlobalVariables(), &globalFunctionEliminationVisitor);
for (auto& aut : model.getAutomata()) {
traverse(aut, &globalFunctionEliminationVisitor);
}
@@ -295,16 +297,24 @@ namespace storm {
eliminateFunctionsInFunctionBodies(functionEliminationVisitor, automaton.getFunctionDefinitions());
// Now run through the remaining components
- JaniTraverser::traverse(automaton.getVariables(), &functionEliminationVisitor);
+ traverse(automaton.getVariables(), &functionEliminationVisitor);
for (auto& loc : automaton.getLocations()) {
- JaniTraverser::traverse(loc, &functionEliminationVisitor);
+ traverse(loc, &functionEliminationVisitor);
}
- JaniTraverser::traverse(automaton.getEdgeContainer(), &functionEliminationVisitor);
+ traverse(automaton.getEdgeContainer(), &functionEliminationVisitor);
if (automaton.hasInitialStatesRestriction()) {
automaton.setInitialStatesRestriction(functionEliminationVisitor.eliminate(automaton.getInitialStatesRestriction()));
}
}
+ void traverse(Location& location, boost::any const& data) override {
+ traverse(location.getAssignments(), data);
+ if (location.hasTimeProgressInvariant()) {
+ FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
+ location.setTimeProgressInvariant(functionEliminationVisitor->eliminate(location.getTimeProgressInvariant()));
+ }
+ }
+
void traverse(Constant& constant, boost::any const& data) override {
if (constant.isDefined()) {
FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
@@ -355,13 +365,20 @@ namespace storm {
}
}
+ void traverse(ClockVariable& variable, boost::any const& data) override {
+ FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
+ if (variable.hasInitExpression()) {
+ variable.setInitExpression(functionEliminationVisitor->eliminate(variable.getInitExpression()));
+ }
+ }
+
void traverse(TemplateEdge& templateEdge, boost::any const& data) override {
FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
templateEdge.setGuard(functionEliminationVisitor->eliminate(templateEdge.getGuard()));
for (auto& dest : templateEdge.getDestinations()) {
- JaniTraverser::traverse(dest, data);
+ traverse(dest, data);
}
- JaniTraverser::traverse(templateEdge.getAssignments(), data);
+ traverse(templateEdge.getAssignments(), data);
}
void traverse(Edge& edge, boost::any const& data) override {
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index d5e43af93..27797c4bd 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -811,7 +811,7 @@ namespace storm {
modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
- modernjson::json variableDeclarations;
+ modernjson::json variableDeclarations = std::vector<modernjson::json>();
for(auto const& variable : varSet) {
modernjson::json varEntry;
varEntry["name"] = variable.getName();
@@ -830,8 +830,7 @@ namespace storm {
typeDesc["base"] = "int";
typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound(), constants, globalVariables, localVariables);
typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound(), constants, globalVariables, localVariables);
- } else {
- assert(variable.isArrayVariable());
+ } else if (variable.isArrayVariable()) {
typeDesc["kind"] = "array";
switch (variable.asArrayVariable().getElementType()) {
case storm::jani::ArrayVariable::ElementType::Bool:
@@ -857,6 +856,9 @@ namespace storm {
}
break;
}
+ } else {
+ assert(variable.isClockVariable());
+ typeDesc = "clock";
}
varEntry["type"] = typeDesc;
if (variable.hasInitExpression()) {
@@ -885,7 +887,7 @@ namespace storm {
}
modernjson::json buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
- modernjson::json functionDeclarations;
+ modernjson::json functionDeclarations = std::vector<modernjson::json>();
for (auto const& nameFunDef : functionDefinitions) {
storm::jani::FunctionDefinition const& funDef = nameFunDef.second;
modernjson::json funDefJson;
@@ -908,7 +910,7 @@ namespace storm {
}
modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
- modernjson::json assignmentDeclarations;
+ modernjson::json assignmentDeclarations = std::vector<modernjson::json>();
bool addIndex = orderedAssignments.hasMultipleLevels();
for(auto const& assignment : orderedAssignments) {
modernjson::json assignmentEntry;
@@ -935,11 +937,18 @@ namespace storm {
}
modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
- modernjson::json locationDeclarations;
+ modernjson::json locationDeclarations = std::vector<modernjson::json>();
for(auto const& location : locations) {
modernjson::json locEntry;
locEntry["name"] = location.getName();
- // TODO support invariants?
+ if (location.hasTimeProgressInvariant()) {
+ modernjson::json timeProg;
+ timeProg["exp"] = buildExpression(location.getTimeProgressInvariant(), constants, globalVariables, localVariables);
+ if (commentExpressions) {
+ timeProg["comment"] = location.getTimeProgressInvariant().toString();
+ }
+ locEntry["time-progress"] = std::move(timeProg);
+ }
if (!location.getAssignments().empty()) {
locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables, commentExpressions);
}
diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp
index 7831436a7..89c8dc846 100644
--- a/src/storm/storage/jani/Location.cpp
+++ b/src/storm/storage/jani/Location.cpp
@@ -1,5 +1,6 @@
#include "storm/storage/jani/Location.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidJaniException.h"
#include "storm/exceptions/InvalidArgumentException.h"
@@ -32,10 +33,25 @@ namespace storm {
assignments.add(assignment);
}
+ bool Location::hasTimeProgressInvariant() const {
+ return timeProgressInvariant.isInitialized();
+ }
+
+ storm::expressions::Expression const& Location::getTimeProgressInvariant() const {
+ return timeProgressInvariant;
+ }
+
+ void Location::setTimeProgressInvariant(storm::expressions::Expression const& expression) {
+ timeProgressInvariant = expression;
+ }
+
void Location::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
for (auto& assignment : assignments) {
assignment.substitute(substitution);
}
+ if (hasTimeProgressInvariant()) {
+ setTimeProgressInvariant(substituteJaniExpression(getTimeProgressInvariant(), substitution));
+ }
}
void Location::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h
index 1fc3cd65d..a18f9c0b6 100644
--- a/src/storm/storage/jani/Location.h
+++ b/src/storm/storage/jani/Location.h
@@ -40,6 +40,22 @@ namespace storm {
*/
void addTransientAssignment(storm::jani::Assignment const& assignment);
+ /*!
+ * Retrieves whether a time progress invariant is attached to this location
+ */
+ bool hasTimeProgressInvariant() const;
+
+ /*!
+ * Retrieves the time progress invariant
+ */
+ storm::expressions::Expression const& getTimeProgressInvariant() const;
+
+ /*!
+ * Sets the time progress invariant of this location
+ * @param expression the location invariant (type bool)
+ */
+ void setTimeProgressInvariant(storm::expressions::Expression const& expression);
+
/*!
* Substitutes all variables in all expressions according to the given substitution.
*/
@@ -66,6 +82,9 @@ namespace storm {
/// The transient assignments made in this location.
OrderedAssignments assignments;
+
+ // The location's time progress condition
+ storm::expressions::Expression timeProgressInvariant;
};
}
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index bc8c687c7..7e690d059 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -687,6 +687,8 @@ namespace storm {
return addVariable(variable.asRealVariable());
} else if (variable.isArrayVariable()) {
return addVariable(variable.asArrayVariable());
+ } else if (variable.isClockVariable()) {
+ return addVariable(variable.asClockVariable());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
}
@@ -711,6 +713,10 @@ namespace storm {
ArrayVariable const& Model::addVariable(ArrayVariable const& variable) {
return globalVariables.addVariable(variable);
}
+
+ ClockVariable const& Model::addVariable(ClockVariable const& variable) {
+ return globalVariables.addVariable(variable);
+ }
VariableSet& Model::getGlobalVariables() {
return globalVariables;
@@ -1033,6 +1039,9 @@ namespace storm {
for (auto& variable : result.getGlobalVariables().getArrayVariables()) {
variable.substitute(constantSubstitution);
}
+ for (auto& variable : result.getGlobalVariables().getClockVariables()) {
+ variable.substitute(constantSubstitution);
+ }
// Substitute constants in initial states expression.
result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
@@ -1086,6 +1095,9 @@ namespace storm {
for (auto& variable : this->getGlobalVariables().getArrayVariables()) {
variable.substitute(substitution);
}
+ for (auto& variable : this->getGlobalVariables().getClockVariables()) {
+ variable.substitute(substitution);
+ }
// Substitute in initial states expression.
this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution));
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 656003853..5db1551d5 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -221,6 +221,11 @@ namespace storm {
*/
ArrayVariable const& addVariable(ArrayVariable const& variable);
+ /*!
+ * Adds the given array variable to this model.
+ */
+ ClockVariable const& addVariable(ClockVariable const& variable);
+
/*!
* Retrieves the variables of this automaton.
*/
diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp
index 50fae165b..6d4c611c3 100644
--- a/src/storm/storage/jani/Variable.cpp
+++ b/src/storm/storage/jani/Variable.cpp
@@ -5,6 +5,7 @@
#include "storm/storage/jani/UnboundedIntegerVariable.h"
#include "storm/storage/jani/RealVariable.h"
#include "storm/storage/jani/ArrayVariable.h"
+#include "storm/storage/jani/ClockVariable.h"
#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
namespace storm {
@@ -54,6 +55,10 @@ namespace storm {
return false;
}
+ bool Variable::isClockVariable() const {
+ return false;
+ }
+
bool Variable::isTransient() const {
return transient;
}
@@ -110,6 +115,14 @@ namespace storm {
return static_cast<ArrayVariable const&>(*this);
}
+ ClockVariable& Variable::asClockVariable() {
+ return static_cast<ClockVariable&>(*this);
+ }
+
+ ClockVariable const& Variable::asClockVariable() const {
+ return static_cast<ClockVariable const&>(*this);
+ }
+
void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
if (this->hasInitExpression()) {
this->setInitExpression(substituteJaniExpression(this->getInitExpression(), substitution));
diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h
index ab4bf80c1..d7e3a4b9a 100644
--- a/src/storm/storage/jani/Variable.h
+++ b/src/storm/storage/jani/Variable.h
@@ -15,6 +15,7 @@ namespace storm {
class UnboundedIntegerVariable;
class RealVariable;
class ArrayVariable;
+ class ClockVariable;
class Variable {
public:
@@ -74,6 +75,7 @@ namespace storm {
virtual bool isUnboundedIntegerVariable() const;
virtual bool isRealVariable() const;
virtual bool isArrayVariable() const;
+ virtual bool isClockVariable() const;
virtual bool isTransient() const;
@@ -88,6 +90,8 @@ namespace storm {
RealVariable const& asRealVariable() const;
ArrayVariable& asArrayVariable();
ArrayVariable const& asArrayVariable() const;
+ ClockVariable& asClockVariable();
+ ClockVariable const& asClockVariable() const;
/*!
* Substitutes all variables in all expressions according to the given substitution.
diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp
index a3af625d5..83ef34bdb 100644
--- a/src/storm/storage/jani/VariableSet.cpp
+++ b/src/storm/storage/jani/VariableSet.cpp
@@ -52,6 +52,14 @@ namespace storm {
return detail::ConstVariables<ArrayVariable>(arrayVariables.begin(), arrayVariables.end());
}
+ detail::Variables<ClockVariable> VariableSet::getClockVariables() {
+ return detail::Variables<ClockVariable>(clockVariables.begin(), clockVariables.end());
+ }
+
+ detail::ConstVariables<ClockVariable> VariableSet::getClockVariables() const {
+ return detail::ConstVariables<ClockVariable>(clockVariables.begin(), clockVariables.end());
+ }
+
Variable const& VariableSet::addVariable(Variable const& variable) {
if (variable.isBooleanVariable()) {
return addVariable(variable.asBooleanVariable());
@@ -63,6 +71,8 @@ namespace storm {
return addVariable(variable.asRealVariable());
} else if (variable.isArrayVariable()) {
return addVariable(variable.asArrayVariable());
+ } else if (variable.isClockVariable()) {
+ return addVariable(variable.asClockVariable());
}
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type.");
}
@@ -132,6 +142,19 @@ namespace storm {
return *newVariable;
}
+ ClockVariable const& VariableSet::addVariable(ClockVariable const& variable) {
+ STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+ std::shared_ptr<ClockVariable> newVariable = std::make_shared<ClockVariable>(variable);
+ variables.push_back(newVariable);
+ clockVariables.push_back(newVariable);
+ if (variable.isTransient()) {
+ transientVariables.push_back(newVariable);
+ }
+ nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+ variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
+ return *newVariable;
+ }
+
std::vector<std::shared_ptr<ArrayVariable>> VariableSet::dropAllArrayVariables() {
if (!arrayVariables.empty()) {
for (auto const& arrVar : arrayVariables) {
@@ -228,6 +251,10 @@ namespace storm {
return !arrayVariables.empty();
}
+ bool VariableSet::containsClockVariables() const {
+ return !clockVariables.empty();
+ }
+
bool VariableSet::containsNonTransientRealVariables() const {
for (auto const& variable : realVariables) {
if (!variable->isTransient()) {
@@ -247,7 +274,7 @@ namespace storm {
}
bool VariableSet::empty() const {
- return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables());
+ return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables() || containsClockVariables());
}
uint_fast64_t VariableSet::getNumberOfTransientVariables() const {
@@ -332,6 +359,13 @@ namespace storm {
}
}
}
+ for (auto const& clockVariable : this->getClockVariables()) {
+ if (clockVariable.hasInitExpression()) {
+ if (clockVariable.getInitExpression().containsVariable(variables)) {
+ return true;
+ }
+ }
+ }
return false;
}
diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h
index 4e4d2d511..af63c949d 100644
--- a/src/storm/storage/jani/VariableSet.h
+++ b/src/storm/storage/jani/VariableSet.h
@@ -10,6 +10,7 @@
#include "storm/storage/jani/BoundedIntegerVariable.h"
#include "storm/storage/jani/RealVariable.h"
#include "storm/storage/jani/ArrayVariable.h"
+#include "storm/storage/jani/ClockVariable.h"
namespace storm {
namespace jani {
@@ -78,6 +79,16 @@ namespace storm {
* Retrieves the Array variables in this set.
*/
detail::ConstVariables<ArrayVariable> getArrayVariables() const;
+
+ /*!
+ * Retrieves the clock variables in this set.
+ */
+ detail::Variables<ClockVariable> getClockVariables();
+
+ /*!
+ * Retrieves the clock variables in this set.
+ */
+ detail::ConstVariables<ClockVariable> getClockVariables() const;
/*!
* Adds the given variable to this set.
@@ -105,7 +116,7 @@ namespace storm {
RealVariable const& addVariable(RealVariable const& variable);
/*!
- * Adds the given real variable to this set.
+ * Adds the given array variable to this set.
*/
ArrayVariable const& addVariable(ArrayVariable const& variable);
@@ -113,6 +124,11 @@ namespace storm {
* Removes all array variables in this set
*/
std::vector<std::shared_ptr<ArrayVariable>> dropAllArrayVariables();
+
+ /*!
+ * Adds the given clock variable to this set.
+ */
+ ClockVariable const& addVariable(ClockVariable const& variable);
/*!
* Retrieves whether this variable set contains a variable with the given name.
@@ -188,6 +204,11 @@ namespace storm {
*/
bool containsArrayVariables() const;
+ /*!
+ * Retrieves whether the set of variables contains a clock variable.
+ */
+ bool containsClockVariables() const;
+
/*!
* Retrieves whether the set of variables contains a non-transient real variable.
*/
@@ -258,6 +279,9 @@ namespace storm {
/// The array variables in this set.
std::vector<std::shared_ptr<ArrayVariable>> arrayVariables;
+ /// The clock variables in this set.
+ std::vector<std::shared_ptr<ClockVariable>> clockVariables;
+
/// The transient variables in this set.
std::vector<std::shared_ptr<Variable>> transientVariables;
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
index e77377a15..dc403479a 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.cpp
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -70,10 +70,16 @@ namespace storm {
for (auto& v : variableSet.getArrayVariables()) {
traverse(v, data);
}
+ for (auto& v : variableSet.getClockVariables()) {
+ traverse(v, data);
+ }
}
void JaniTraverser::traverse(Location& location, boost::any const& data) {
traverse(location.getAssignments(), data);
+ if (location.hasTimeProgressInvariant()) {
+ traverse(location.getTimeProgressInvariant(), data);
+ }
}
void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) {
@@ -114,6 +120,12 @@ namespace storm {
}
}
+ void JaniTraverser::traverse(ClockVariable& variable, boost::any const& data) {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ }
+
void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) {
for (auto& templateEdge : edgeContainer.getTemplateEdges()) {
traverse(*templateEdge, data);
@@ -236,10 +248,16 @@ namespace storm {
for (auto const& v : variableSet.getArrayVariables()) {
traverse(v, data);
}
+ for (auto const& v : variableSet.getClockVariables()) {
+ traverse(v, data);
+ }
}
void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) {
traverse(location.getAssignments(), data);
+ if (location.hasTimeProgressInvariant()) {
+ traverse(location.getTimeProgressInvariant(), data);
+ }
}
void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) {
@@ -280,6 +298,12 @@ namespace storm {
}
}
+ void ConstJaniTraverser::traverse(ClockVariable const& variable, boost::any const& data) {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ }
+
void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) {
for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
traverse(*templateEdge, data);
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h
index a7da8bc6f..3d2310458 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.h
+++ b/src/storm/storage/jani/traverser/JaniTraverser.h
@@ -24,6 +24,7 @@ namespace storm {
virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data);
virtual void traverse(RealVariable& variable, boost::any const& data);
virtual void traverse(ArrayVariable& variable, boost::any const& data);
+ virtual void traverse(ClockVariable& variable, boost::any const& data);
virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data);
virtual void traverse(TemplateEdge& templateEdge, boost::any const& data);
virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data);
@@ -52,6 +53,7 @@ namespace storm {
virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data);
virtual void traverse(RealVariable const& variable, boost::any const& data);
virtual void traverse(ArrayVariable const& variable, boost::any const& data);
+ virtual void traverse(ClockVariable const& variable, boost::any const& data);
virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data);
virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data);
virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data);