diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
new file mode 100644
index 000000000..c9744d90c
--- /dev/null
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -0,0 +1,125 @@
+#include "src/builder/DdJaniModelBuilder.h"
+
+#include <sstream>
+
+#include <boost/algorithm/string/join.hpp>
+
+#include "src/logic/Formulas.h"
+
+#include "src/utility/macros.h"
+#include "src/utility/jani.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace builder {
+
+ template <storm::dd::DdType Type, typename ValueType>
+ DdJaniModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ // Intentionally left empty.
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ this->preserveFormula(formula);
+ this->setTerminalStatesFromFormula(formula);
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ if (formulas.empty()) {
+ this->buildAllRewardModels = true;
+ } else {
+ for (auto const& formula : formulas) {
+ this->preserveFormula(*formula);
+ }
+ if (formulas.size() == 1) {
+ this->setTerminalStatesFromFormula(*formulas.front());
+ }
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ void DdJaniModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) {
+ // If we already had terminal states, we need to erase them.
+ if (terminalStates) {
+ terminalStates.reset();
+ }
+ if (negatedTerminalStates) {
+ negatedTerminalStates.reset();
+ }
+
+ // If we are not required to build all reward models, we determine the reward models we need to build.
+ if (!buildAllRewardModels) {
+ std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
+ rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ void DdJaniModelBuilder<Type, ValueType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
+ if (formula.isAtomicExpressionFormula()) {
+ terminalStates = formula.asAtomicExpressionFormula().getExpression();
+ } else if (formula.isEventuallyFormula()) {
+ storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula();
+ if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) {
+ this->setTerminalStatesFromFormula(sub);
+ }
+ } else if (formula.isUntilFormula()) {
+ storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
+ if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
+ this->setTerminalStatesFromFormula(right);
+ }
+ storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+ if (left.isAtomicExpressionFormula()) {
+ negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+ }
+ } else if (formula.isProbabilityOperatorFormula()) {
+ storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
+ if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
+ this->setTerminalStatesFromFormula(sub);
+ }
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ void DdJaniModelBuilder<Type, ValueType>::Options::addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::jani::parseConstantDefinitionString(model, constantDefinitionString);
+
+ // If there is at least one constant that is defined, and the constant definition map does not yet exist,
+ // we need to create it.
+ if (!constantDefinitions && !newConstantDefinitions.empty()) {
+ constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
+ }
+
+ // Now insert all the entries that need to be defined.
+ for (auto const& entry : newConstantDefinitions) {
+ constantDefinitions.get().insert(entry);
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : options(options) {
+ if (options.constantDefinitions) {
+ this->model = model.defineUndefinedConstants(options.constantDefinitions.get());
+ } else {
+ this->model = model;
+ }
+
+ if (this->model->hasUndefinedConstants()) {
+ std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model->getUndefinedConstants();
+ std::vector<std::string> strings;
+ for (auto const& constant : undefinedConstants) {
+ std::stringstream stream;
+ stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+ strings.push_back(stream.str());
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " << boost::join(strings, ", ") << ".");
+ }
+
+ this->model = this->model->substituteConstants();
+ }
+
+ template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
+ template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
+ }
+}
\ No newline at end of file
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
new file mode 100644
index 000000000..983b7cd99
--- /dev/null
+++ b/src/builder/DdJaniModelBuilder.h
@@ -0,0 +1,121 @@
+#pragma once
+
+#include <boost/optional.hpp>
+
+#include "src/storage/dd/DdType.h"
+
+#include "src/logic/Formula.h"
+
+#include "src/storage/jani/Model.h"
+
+namespace storm {
+ namespace models {
+ namespace symbolic {
+ template <storm::dd::DdType Type, typename ValueType>
+ class Model;
+ }
+ }
+
+ namespace builder {
+
+ template <storm::dd::DdType Type, typename ValueType = double>
+ class DdJaniModelBuilder {
+ public:
+ struct Options {
+ /*!
+ * Creates an object representing the default building options.
+ */
+ Options();
+
+ /*! Creates an object representing the suggested building options assuming that the given formula is the
+ * only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
+ *
+ * @param formula The formula based on which to choose the building options.
+ */
+ Options(storm::logic::Formula const& formula);
+
+ /*! Creates an object representing the suggested building options assuming that the given formulas are
+ * the only ones to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
+ *
+ * @param formula Thes formula based on which to choose the building options.
+ */
+ Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+
+ /*!
+ * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
+ * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
+ *
+ * @param program The program managing the constants that shall be defined. Note that the program itself
+ * is not modified whatsoever.
+ * @param constantDefinitionString The string from which to parse the constants' values.
+ */
+ void addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString);
+
+ /*!
+ * Changes the options in a way that ensures that the given formula can be checked on the model once it
+ * has been built.
+ *
+ * @param formula The formula that is to be ''preserved''.
+ */
+ void preserveFormula(storm::logic::Formula const& formula);
+
+ /*!
+ * Analyzes the given formula and sets an expression for the states states of the model that can be
+ * treated as terminal states. Note that this may interfere with checking properties different than the
+ * one provided.
+ *
+ * @param formula The formula used to (possibly) derive an expression for the terminal states of the
+ * model.
+ */
+ void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
+
+ // A flag that indicates whether or not all reward models are to be build.
+ bool buildAllRewardModels;
+
+ // A list of reward models to be build in case not all reward models are to be build.
+ std::set<std::string> rewardModelsToBuild;
+
+ // An optional mapping that, if given, contains defining expressions for undefined constants.
+ boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
+
+ // An optional expression or label that (a subset of) characterizes the terminal states of the model.
+ // If this is set, the outgoing transitions of these states are replaced with a self-loop.
+ boost::optional<storm::expressions::Expression> terminalStates;
+
+ // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+ // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+ boost::optional<storm::expressions::Expression> negatedTerminalStates;
+ };
+
+ /*!
+ * Creates a builder for the given model that uses the given options.
+ */
+ DdJaniModelBuilder(storm::jani::Model const& model, Options const& options = Options());
+
+ /*!
+ * Translates the given program into a symbolic model (i.e. one that stores the transition relation as a
+ * decision diagram).
+ *
+ * @param model The model to translate.
+ * @return A pointer to the resulting model.
+ */
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> translate();
+
+ /*!
+ * Retrieves the model that was actually translated (i.e. including constant substitutions etc.). Note
+ * that this function may only be called after a succesful translation.
+ *
+ * @return The translated model.
+ */
+ storm::jani::Model const& getTranslatedModel() const;
+
+ private:
+ /// The model to translate.
+ boost::optional<storm::jani::Model> model;
+
+ /// The options to use for building the model.
+ Options options;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp
index a73c40d93..cea88f23e 100644
--- a/src/storage/jani/Assignment.cpp
+++ b/src/storage/jani/Assignment.cpp
@@ -15,6 +15,10 @@ namespace storm {
return expression;
}
+ void Assignment::setAssignedExpression(storm::expressions::Expression const& expression) {
+ this->expression = expression;
+ }
+
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
stream << assignment.getExpressionVariable().getName() << " := " << assignment.getAssignedExpression();
return stream;
diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h
index 4fc0a5330..58c078d20 100644
--- a/src/storage/jani/Assignment.h
+++ b/src/storage/jani/Assignment.h
@@ -22,6 +22,11 @@ namespace storm {
* Retrieves the expression whose value is assigned to the target variable.
*/
storm::expressions::Expression const& getAssignedExpression() const;
+
+ /*!
+ * Sets a new expression that is assigned to the target variable.
+ */
+ void setAssignedExpression(storm::expressions::Expression const& expression);
friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index f76d0fc38..79f658356 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -7,6 +7,132 @@
namespace storm {
namespace jani {
+ namespace detail {
+ EdgeIterator::EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+ // Intentionally left empty.
+ }
+
+ EdgeIterator& EdgeIterator::operator++() {
+ incrementIterator();
+ return *this;
+ }
+
+ EdgeIterator& EdgeIterator::operator++(int) {
+ incrementIterator();
+ return *this;
+ }
+
+ Edge& EdgeIterator::operator*() {
+ return *in_it;
+ }
+
+ bool EdgeIterator::operator==(EdgeIterator const& other) const {
+ return this->out_it == other.out_it && this->in_it == other.in_it;
+ }
+
+ bool EdgeIterator::operator!=(EdgeIterator const& other) const {
+ return !(*this == other);
+ }
+
+ void EdgeIterator::incrementIterator() {
+ ++in_it;
+
+ // If the inner iterator has reached its end move it to the beginning of the next outer element.
+ if (in_it == out_it->end()) {
+ ++out_it;
+ while (out_it != out_ite && out_it->empty()) {
+ ++out_it;
+ in_it = out_it->end();
+ }
+ if (out_it != out_ite) {
+ in_it = out_it->begin();
+ }
+ }
+ }
+
+ ConstEdgeIterator::ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+ // Intentionally left empty.
+ }
+
+ ConstEdgeIterator& ConstEdgeIterator::operator++() {
+ incrementIterator();
+ return *this;
+ }
+
+ ConstEdgeIterator& ConstEdgeIterator::operator++(int) {
+ incrementIterator();
+ return *this;
+ }
+
+ Edge const& ConstEdgeIterator::operator*() const {
+ return *in_it;
+ }
+
+ bool ConstEdgeIterator::operator==(ConstEdgeIterator const& other) const {
+ return this->out_it == other.out_it && this->in_it == other.in_it;
+ }
+
+ bool ConstEdgeIterator::operator!=(ConstEdgeIterator const& other) const {
+ return !(*this == other);
+ }
+
+ void ConstEdgeIterator::incrementIterator() {
+ ++in_it;
+
+ // If the inner iterator has reached its end move it to the beginning of the next outer element.
+ if (in_it == out_it->end()) {
+ ++out_it;
+ while (out_it != out_ite && out_it->empty()) {
+ ++out_it;
+ in_it = out_it->end();
+ }
+ if (out_it != out_ite) {
+ in_it = out_it->begin();
+ }
+ }
+ }
+
+ Edges::Edges(Automaton& automaton) : automaton(automaton) {
+ // Intentionally left empty.
+ }
+
+ EdgeIterator Edges::begin() {
+ auto outer = automaton.edges.begin();
+ while (outer != automaton.edges.end() && outer->empty()) {
+ ++outer;
+ }
+ if (outer == automaton.edges.end()) {
+ return end();
+ } else {
+ return EdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
+ }
+ }
+
+ EdgeIterator Edges::end() {
+ return EdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+ }
+
+ ConstEdges::ConstEdges(Automaton const& automaton) : automaton(automaton) {
+ // Intentionally left empty.
+ }
+
+ ConstEdgeIterator ConstEdges::begin() const {
+ auto outer = automaton.edges.begin();
+ while (outer != automaton.edges.end() && outer->empty()) {
+ ++outer;
+ }
+ if (outer == automaton.edges.end()) {
+ return end();
+ } else {
+ return ConstEdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
+ }
+ }
+
+ ConstEdgeIterator ConstEdges::end() const {
+ return ConstEdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+ }
+ }
+
Automaton::Automaton(std::string const& name) : name(name) {
// Intentionally left empty.
}
@@ -26,7 +152,11 @@ namespace storm {
void Automaton::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
variables.addUnboundedIntegerVariable(variable);
}
-
+
+ VariableSet& Automaton::getVariables() {
+ return variables;
+ }
+
VariableSet const& Automaton::getVariables() const {
return variables;
}
@@ -90,6 +220,14 @@ namespace storm {
edges[edge.getSourceLocationId()].addEdge(edge);
}
+ Automaton::Edges Automaton::getEdges() {
+ return Edges(*this);
+ }
+
+ Automaton::ConstEdges Automaton::getEdges() const {
+ return ConstEdges(*this);
+ }
+
uint64_t Automaton::getNumberOfLocations() const {
return edges.size();
}
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 81e231f16..36a525703 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -11,8 +11,122 @@
namespace storm {
namespace jani {
+ class Automaton;
+
+ namespace detail {
+ class EdgeIterator {
+ private:
+ typedef std::vector<EdgeSet>::iterator outer_iter;
+ typedef EdgeSet::iterator inner_iter;
+
+ public:
+ /*!
+ * Creates an iterator over all edges.
+ */
+ EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
+
+ // Methods to advance the iterator.
+ EdgeIterator& operator++();
+ EdgeIterator& operator++(int);
+
+ Edge& operator*();
+
+ bool operator==(EdgeIterator const& other) const;
+ bool operator!=(EdgeIterator const& other) const;
+
+ private:
+ // Moves the iterator to the next position.
+ void incrementIterator();
+
+ // The underlying automaton.
+ Automaton& automaton;
+
+ // The current iterator positions.
+ outer_iter out_it;
+ outer_iter out_ite;
+ inner_iter in_it;
+ };
+
+ class ConstEdgeIterator {
+ private:
+ typedef std::vector<EdgeSet>::const_iterator outer_iter;
+ typedef EdgeSet::const_iterator inner_iter;
+
+ public:
+ /*!
+ * Creates an iterator over all edges.
+ */
+ ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
+
+ // Methods to advance the iterator.
+ ConstEdgeIterator& operator++();
+ ConstEdgeIterator& operator++(int);
+
+ Edge const& operator*() const;
+
+ bool operator==(ConstEdgeIterator const& other) const;
+ bool operator!=(ConstEdgeIterator const& other) const;
+
+ private:
+ // Moves the iterator to the next position.
+ void incrementIterator();
+
+ // The underlying automaton.
+ Automaton const& automaton;
+
+ // The current iterator positions.
+ outer_iter out_it;
+ outer_iter out_ite;
+ inner_iter in_it;
+ };
+
+ class Edges {
+ public:
+ Edges(Automaton& automaton);
+
+ /*!
+ * Retrieves an iterator to all edges of the automaton.
+ */
+ EdgeIterator begin();
+
+ /*!
+ * Retrieves the end iterator to edges of the automaton.
+ */
+ EdgeIterator end();
+
+ private:
+ // The underlying automaton.
+ Automaton& automaton;
+ };
+
+ class ConstEdges {
+ public:
+ ConstEdges(Automaton const& automaton);
+
+ /*!
+ * Retrieves an iterator to all edges of the automaton.
+ */
+ ConstEdgeIterator begin() const;
+
+ /*!
+ * Retrieves the end iterator to edges of the automaton.
+ */
+ ConstEdgeIterator end() const;
+
+ private:
+ // The underlying automaton.
+ Automaton const& automaton;
+ };
+ }
+
class Automaton {
public:
+ friend class detail::Edges;
+ friend class detail::ConstEdges;
+
+ typedef detail::Edges Edges;
+ typedef detail::ConstEdges ConstEdges;
+
/*!
* Creates an empty automaton.
*/
@@ -37,7 +151,12 @@ namespace storm {
* Adds the given unbounded integer variable to this automaton.
*/
void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
-
+
+ /*!
+ * Retrieves the variables of this automaton.
+ */
+ VariableSet& getVariables();
+
/*!
* Retrieves the variables of this automaton.
*/
@@ -106,6 +225,16 @@ namespace storm {
*/
void addEdge(Edge const& edge);
+ /*!
+ * Retrieves the edges of the automaton.
+ */
+ Edges getEdges();
+
+ /*!
+ * Retrieves the edges of the automaton.
+ */
+ ConstEdges getEdges() const;
+
/*!
* Retrieves the number of locations.
*/
diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp
index 879f9a165..4ab7e5717 100644
--- a/src/storage/jani/BoundedIntegerVariable.cpp
+++ b/src/storage/jani/BoundedIntegerVariable.cpp
@@ -11,9 +11,17 @@ namespace storm {
return lowerBound;
}
+ void BoundedIntegerVariable::setLowerBound(storm::expressions::Expression const& expression) {
+ this->lowerBound = expression;
+ }
+
storm::expressions::Expression const& BoundedIntegerVariable::getUpperBound() const {
return upperBound;
}
+ void BoundedIntegerVariable::setUpperBound(storm::expressions::Expression const& expression) {
+ this->upperBound = expression;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h
index b686f4a0e..5e62c855a 100644
--- a/src/storage/jani/BoundedIntegerVariable.h
+++ b/src/storage/jani/BoundedIntegerVariable.h
@@ -18,11 +18,21 @@ namespace storm {
*/
storm::expressions::Expression const& getLowerBound() const;
+ /*!
+ * Sets a new lower bound of the variable.
+ */
+ void setLowerBound(storm::expressions::Expression const& expression);
+
/*!
* Retrieves the expression defining the upper bound of the variable.
*/
storm::expressions::Expression const& getUpperBound() const;
+ /*!
+ * Sets a new upper bound of the variable.
+ */
+ void setUpperBound(storm::expressions::Expression const& expression);
+
private:
// The expression defining the lower bound of the variable.
storm::expressions::Expression lowerBound;
diff --git a/src/storage/jani/Constant.cpp b/src/storage/jani/Constant.cpp
index a85331d40..94aa4d522 100644
--- a/src/storage/jani/Constant.cpp
+++ b/src/storage/jani/Constant.cpp
@@ -35,5 +35,13 @@ namespace storm {
return getType().isRationalType();
}
+ storm::expressions::Variable const& Constant::getExpressionVariable() const {
+ return variable;
+ }
+
+ storm::expressions::Expression const& Constant::getExpression() const {
+ return expression.get();
+ }
+
}
}
diff --git a/src/storage/jani/Constant.h b/src/storage/jani/Constant.h
index 1cfed043d..eb14f44ca 100644
--- a/src/storage/jani/Constant.h
+++ b/src/storage/jani/Constant.h
@@ -52,6 +52,16 @@ namespace storm {
*/
bool isRealConstant() const;
+ /*!
+ * Retrieves the expression variable associated with this constant.
+ */
+ storm::expressions::Variable const& getExpressionVariable() const;
+
+ /*!
+ * Retrieves the expression that defines this constant (if any).
+ */
+ storm::expressions::Expression const& getExpression() const;
+
private:
// The name of the constant.
std::string name;
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index 5b8003815..8176952a8 100644
--- a/src/storage/jani/Edge.cpp
+++ b/src/storage/jani/Edge.cpp
@@ -23,14 +23,26 @@ namespace storm {
return rate.get();
}
+ void Edge::setRate(storm::expressions::Expression const& rate) {
+ this->rate = rate;
+ }
+
storm::expressions::Expression const& Edge::getGuard() const {
return guard;
}
+ void Edge::setGuard(storm::expressions::Expression const& guard) {
+ this->guard = guard;
+ }
+
std::vector<EdgeDestination> const& Edge::getDestinations() const {
return destinations;
}
+ std::vector<EdgeDestination>& Edge::getDestinations() {
+ return destinations;
+ }
+
void Edge::addDestination(EdgeDestination const& destination) {
destinations.push_back(destination);
}
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
index ff5def7ee..1571bf9c1 100644
--- a/src/storage/jani/Edge.h
+++ b/src/storage/jani/Edge.h
@@ -30,16 +30,31 @@ namespace storm {
* Retrieves the rate of this edge. Note that calling this is only valid if the edge has an associated rate.
*/
storm::expressions::Expression const& getRate() const;
+
+ /*!
+ * Sets a new rate for this edge.
+ */
+ void setRate(storm::expressions::Expression const& rate);
/*!
* Retrieves the guard of this edge.
*/
storm::expressions::Expression const& getGuard() const;
+ /*!
+ * Sets a new guard for this edge.
+ */
+ void setGuard(storm::expressions::Expression const& guard);
+
/*!
* Retrieves the destinations of this edge.
*/
std::vector<EdgeDestination> const& getDestinations() const;
+
+ /*!
+ * Retrieves the destinations of this edge.
+ */
+ std::vector<EdgeDestination>& getDestinations();
/*!
* Adds the given destination to the destinations of this edge.
diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp
index 35554545d..bee1e0a3a 100644
--- a/src/storage/jani/EdgeDestination.cpp
+++ b/src/storage/jani/EdgeDestination.cpp
@@ -30,6 +30,14 @@ namespace storm {
return probability;
}
+ void EdgeDestination::setProbability(storm::expressions::Expression const& probability) {
+ this->probability = probability;
+ }
+
+ std::vector<Assignment>& EdgeDestination::getAssignments() {
+ return assignments;
+ }
+
std::vector<Assignment> const& EdgeDestination::getAssignments() const {
return assignments;
}
diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h
index 07efeece1..c967518eb 100644
--- a/src/storage/jani/EdgeDestination.h
+++ b/src/storage/jani/EdgeDestination.h
@@ -37,6 +37,16 @@ namespace storm {
*/
storm::expressions::Expression const& getProbability() const;
+ /*!
+ * Sets a new probability for this edge destination.
+ */
+ void setProbability(storm::expressions::Expression const& probability);
+
+ /*!
+ * Retrieves the assignments to make when choosing this destination.
+ */
+ std::vector<Assignment>& getAssignments();
+
/*!
* Retrieves the assignments to make when choosing this destination.
*/
diff --git a/src/storage/jani/EdgeSet.cpp b/src/storage/jani/EdgeSet.cpp
index 25704a864..d71b3f5be 100644
--- a/src/storage/jani/EdgeSet.cpp
+++ b/src/storage/jani/EdgeSet.cpp
@@ -27,5 +27,9 @@ namespace storm {
edges.push_back(edge);
}
+ bool EdgeSet::empty() const {
+ return edges.empty();
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeSet.h b/src/storage/jani/EdgeSet.h
index e9fe03fbf..a9e7336ad 100644
--- a/src/storage/jani/EdgeSet.h
+++ b/src/storage/jani/EdgeSet.h
@@ -21,6 +21,11 @@ namespace storm {
*/
void addEdge(Edge const& edge);
+ /*!
+ * Retrieves whether the set of edges is empty.
+ */
+ bool empty() const;
+
// Methods to get an iterator to the edges.
iterator begin();
iterator end();
diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp
index e5561b9b6..643099b78 100644
--- a/src/storage/jani/Exporter.cpp
+++ b/src/storage/jani/Exporter.cpp
@@ -227,7 +227,7 @@ namespace storm {
appendIndent(out, indent + 1);
appendField(out, "ref");
- storm::jani::Variable const& variable = model.getVariables().hasVariable(assignment.getExpressionVariable()) ? model.getVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable());
+ storm::jani::Variable const& variable = model.getGlobalVariables().hasVariable(assignment.getExpressionVariable()) ? model.getGlobalVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable());
appendValue(out, variable.getName());
out << ",";
clearLine(out);
@@ -399,7 +399,7 @@ namespace storm {
clearLine(out);
appendActions(out, model, 1);
clearLine(out);
- appendVariables(out, model.getVariables(), 1);
+ appendVariables(out, model.getGlobalVariables(), 1);
clearLine(out);
appendAutomata(out, model, 1);
clearLine(out);
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 87149f611..5ef53fe88 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -8,6 +8,7 @@
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace jani {
@@ -72,6 +73,24 @@ namespace storm {
return constants.size() - 1;
}
+ bool Model::hasConstant(std::string const& name) const {
+ return constantToIndex.find(name) != constantToIndex.end();
+ }
+
+ Constant const& Model::getConstant(std::string const& name) const {
+ auto it = constantToIndex.find(name);
+ STORM_LOG_THROW(it != constantToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve unknown constant '" << name << "'.");
+ return constants[it->second];
+ }
+
+ std::vector<Constant> const& Model::getConstants() const {
+ return constants;
+ }
+
+ std::vector<Constant>& Model::getConstants() {
+ return constants;
+ }
+
void Model::addBooleanVariable(BooleanVariable const& variable) {
globalVariables.addBooleanVariable(variable);
}
@@ -83,8 +102,12 @@ namespace storm {
void Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
globalVariables.addUnboundedIntegerVariable(variable);
}
-
- VariableSet const& Model::getVariables() const {
+
+ VariableSet& Model::getGlobalVariables() {
+ return globalVariables;
+ }
+
+ VariableSet const& Model::getGlobalVariables() const {
return globalVariables;
}
@@ -104,6 +127,14 @@ namespace storm {
return automata.size() - 1;
}
+ std::vector<Automaton>& Model::getAutomata() {
+ return automata;
+ }
+
+ std::vector<Automaton> const& Model::getAutomata() const {
+ return automata;
+ }
+
std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
@@ -129,6 +160,109 @@ namespace storm {
return result;
}
+ Model Model::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
+ Model result(*this);
+
+ std::set<storm::expressions::Variable> definedUndefinedConstants;
+ for (auto& constant : result.constants) {
+ // If the constant is already defined, we need to replace the appearances of undefined constants in its
+ // defining expression
+ if (constant.isDefined()) {
+ // Make sure we are not trying to define an already defined constant.
+ STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidOperationException, "Illegally defining already defined constant '" << constant.getName() << "'.");
+ } else {
+ auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
+
+ if (variableExpressionPair != constantDefinitions.end()) {
+ // If we need to define it, we add it to the defined constants and assign it the appropriate expression.
+ definedUndefinedConstants.insert(constant.getExpressionVariable());
+
+ // Make sure the type of the constant is correct.
+ STORM_LOG_THROW(variableExpressionPair->second.getType() == constant.getType(), storm::exceptions::InvalidOperationException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
+
+ // Now define the constant.
+ constant.define(variableExpressionPair->second);
+ }
+ }
+ }
+
+ // As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers
+ // that are not undefined constants.
+ for (auto const& constantExpressionPair : constantDefinitions) {
+ STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidOperationException, "Unable to define non-existant constant '" << constantExpressionPair.first.getName() << "'.");
+ }
+ return result;
+ }
+
+ bool Model::hasUndefinedConstants() const {
+ for (auto const& constant : constants) {
+ if (!constant.isDefined()) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ std::vector<std::reference_wrapper<Constant const>> Model::getUndefinedConstants() const {
+ std::vector<std::reference_wrapper<Constant const>> result;
+
+ for (auto const& constant : constants) {
+ if (!constant.isDefined()) {
+ result.push_back(constant);
+ }
+ }
+
+ return result;
+ }
+
+ Model Model::substituteConstants() const {
+ Model result(*this);
+
+ // Gather all defining expressions of constants.
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+ for (auto& constant : result.getConstants()) {
+ if (constant.isDefined()) {
+ constant.define(constant.getExpression().substitute(constantSubstitution));
+ constantSubstitution[constant.getExpressionVariable()] = constant.getExpression();
+ }
+ }
+
+ // Substitute constants in all global variables.
+ for (auto& variable : result.getGlobalVariables()) {
+ variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
+ }
+ for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
+ variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
+ variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+ }
+
+ // Substitute constants in variables of automata and their edges.
+ for (auto& automaton : result.getAutomata()) {
+ for (auto& variable : automaton.getVariables()) {
+ variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
+ }
+ for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+ variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
+ variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+ }
+
+ for (auto& edge : automaton.getEdges()) {
+ edge.setGuard(edge.getGuard().substitute(constantSubstitution));
+ if (edge.hasRate()) {
+ edge.setRate(edge.getRate().substitute(constantSubstitution));
+ }
+ for (auto& destination : edge.getDestinations()) {
+ destination.setProbability(destination.getProbability().substitute(constantSubstitution));
+ for (auto& assignment : destination.getAssignments()) {
+ assignment.setAssignedExpression(assignment.getAssignedExpression().substitute(constantSubstitution));
+ }
+ }
+ }
+ }
+
+ return result;
+ }
+
bool Model::checkValidity(bool logdbg) const {
// TODO switch to exception based return value.
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index a01571707..b1e5e3f9a 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -77,6 +77,26 @@ namespace storm {
*/
uint64_t addConstant(Constant const& constant);
+ /*!
+ * Retrieves whether the model has a constant with the given name.
+ */
+ bool hasConstant(std::string const& name) const;
+
+ /*!
+ * Retrieves the constants of the model.
+ */
+ std::vector<Constant> const& getConstants() const;
+
+ /*!
+ * Retrieves the constants of the model.
+ */
+ std::vector<Constant>& getConstants();
+
+ /*!
+ * Retrieves the constant with the given name (if any).
+ */
+ Constant const& getConstant(std::string const& name) const;
+
/*!
* Adds the given boolean variable to this model.
*/
@@ -91,11 +111,16 @@ namespace storm {
* Adds the given unbounded integer variable to this model.
*/
void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable);
-
+
+ /*!
+ * Retrieves the variables of this automaton.
+ */
+ VariableSet& getGlobalVariables();
+
/*!
* Retrieves the variables of this automaton.
*/
- VariableSet const& getVariables() const;
+ VariableSet const& getGlobalVariables() const;
/*!
* Retrieves the manager responsible for the expressions in the JANI model.
@@ -112,6 +137,16 @@ namespace storm {
*/
uint64_t addAutomaton(Automaton const& automaton);
+ /*!
+ * Retrieves the automata of the model.
+ */
+ std::vector<Automaton>& getAutomata();
+
+ /*!
+ * Retrieves the automata of the model.
+ */
+ std::vector<Automaton> const& getAutomata() const;
+
/*!
* Sets the system composition expression of the JANI model.
*/
@@ -137,6 +172,28 @@ namespace storm {
*/
std::string const& getSilentActionName() const;
+ /*!
+ * Defines the undefined constants of the model by the given expressions. The original model is not modified,
+ * but instead a new model is created.
+ */
+ Model defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
+
+ /*!
+ * Retrieves whether the model still has undefined constants.
+ */
+ bool hasUndefinedConstants() const;
+
+ /*!
+ * Retrieves all undefined constants of the model.
+ */
+ std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
+
+ /*!
+ * Substitutes all constants in all expressions of the model. The original model is not modified, but
+ * instead a new model is created.
+ */
+ Model substituteConstants() const;
+
/*!
* Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
*/
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index 9601d7684..84f927802 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -25,5 +25,9 @@ namespace storm {
return initialValue;
}
+ void Variable::setInitialValue(storm::expressions::Expression const& initialValue) {
+ this->initialValue = initialValue;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index b0cbf5d5a..c77e21e93 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -31,6 +31,11 @@ namespace storm {
*/
storm::expressions::Expression const& getInitialValue() const;
+ /*!
+ * Sets a new value as the initial value of the variable.
+ */
+ void setInitialValue(storm::expressions::Expression const& initialValue);
+
/*!
* Retrieves whether the variable has an initial value.
*/
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index 8afed1b1c..e4d37957d 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -9,7 +9,7 @@ namespace storm {
namespace detail {
- VariableSetIterator::VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
+ VariableSetIterator::VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
// Intentionally left empty.
}
@@ -23,7 +23,7 @@ namespace storm {
return *this;
}
- Variable const& VariableSetIterator::operator*() {
+ Variable& VariableSetIterator::operator*() {
if (it.which() == 0) {
return *boost::get<bool_iter>(it);
} else if (it.which() == 1) {
@@ -61,37 +61,117 @@ namespace storm {
}
}
- IntegerVariables::IntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+ ConstVariableSetIterator::ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
// Intentionally left empty.
}
- VariableSetIterator IntegerVariables::begin() const {
+ ConstVariableSetIterator& ConstVariableSetIterator::operator++() {
+ incrementIterator();
+ return *this;
+ }
+
+ ConstVariableSetIterator& ConstVariableSetIterator::operator++(int) {
+ incrementIterator();
+ return *this;
+ }
+
+ Variable const& ConstVariableSetIterator::operator*() {
+ if (it.which() == 0) {
+ return *boost::get<bool_iter>(it);
+ } else if (it.which() == 1) {
+ return *boost::get<bint_iter>(it);
+ } else {
+ return *boost::get<int_iter>(it);
+ }
+ }
+
+ bool ConstVariableSetIterator::operator==(ConstVariableSetIterator const& other) const {
+ return this->it == other.it;
+ }
+
+ bool ConstVariableSetIterator::operator!=(ConstVariableSetIterator const& other) const {
+ return this->it != other.it;
+ }
+
+ void ConstVariableSetIterator::incrementIterator() {
+ if (it.which() == 0) {
+ bool_iter& tmp = boost::get<bool_iter>(it);
+ if (tmp != variableSet.getBooleanVariables().end()) {
+ ++tmp;
+ } else {
+ it = variableSet.getBoundedIntegerVariables().begin();
+ }
+ } else if (it.which() == 1) {
+ bint_iter& tmp = boost::get<bint_iter>(it);
+ if (tmp != variableSet.getBoundedIntegerVariables().end()) {
+ ++tmp;
+ } else {
+ it = variableSet.getUnboundedIntegerVariables().begin();
+ }
+ } else {
+ ++boost::get<int_iter>(it);
+ }
+ }
+
+ IntegerVariables::IntegerVariables(VariableSet& variableSet) : variableSet(variableSet) {
+ // Intentionally left empty.
+ }
+
+ VariableSetIterator IntegerVariables::begin() {
return VariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
}
- VariableSetIterator IntegerVariables::end() const {
+ VariableSetIterator IntegerVariables::end() {
return VariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
}
+
+ ConstIntegerVariables::ConstIntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+ // Intentionally left empty.
+ }
+
+ ConstVariableSetIterator ConstIntegerVariables::begin() const {
+ return ConstVariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
+ }
+
+ ConstVariableSetIterator ConstIntegerVariables::end() const {
+ return ConstVariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
+ }
}
VariableSet::VariableSet() {
// Intentionally left empty.
}
- std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
+ std::vector<BooleanVariable>& VariableSet::getBooleanVariables() {
return booleanVariables;
}
+ std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
+ return booleanVariables;
+ }
+
+ std::vector<BoundedIntegerVariable>& VariableSet::getBoundedIntegerVariables() {
+ return boundedIntegerVariables;
+ }
+
std::vector<BoundedIntegerVariable> const& VariableSet::getBoundedIntegerVariables() const {
return boundedIntegerVariables;
}
-
+
+ std::vector<UnboundedIntegerVariable>& VariableSet::getUnboundedIntegerVariables() {
+ return unboundedIntegerVariables;
+ }
+
std::vector<UnboundedIntegerVariable> const& VariableSet::getUnboundedIntegerVariables() const {
return unboundedIntegerVariables;
}
-
- detail::IntegerVariables VariableSet::getIntegerVariables() const {
- return detail::IntegerVariables(*this);
+
+ VariableSet::IntegerVariables VariableSet::getIntegerVariables() {
+ return IntegerVariables(*this);
+ }
+
+ VariableSet::ConstIntegerVariables VariableSet::getIntegerVariables() const {
+ return ConstIntegerVariables(*this);
}
void VariableSet::addBooleanVariable(BooleanVariable const& variable) {
@@ -124,15 +204,23 @@ namespace storm {
STORM_LOG_THROW(it != nameToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'.");
return getVariable(it->second);
}
-
- detail::VariableSetIterator VariableSet::begin() const {
- return detail::VariableSetIterator(*this, booleanVariables.begin());
+
+ VariableSet::iterator VariableSet::begin() {
+ return iterator(*this, booleanVariables.begin());
}
-
- detail::VariableSetIterator VariableSet::end() const {
- return detail::VariableSetIterator(*this, unboundedIntegerVariables.end());
+
+ VariableSet::const_iterator VariableSet::begin() const {
+ return const_iterator(*this, booleanVariables.begin());
}
+ VariableSet::iterator VariableSet::end() {
+ return iterator(*this, unboundedIntegerVariables.end());
+ }
+
+ VariableSet::const_iterator VariableSet::end() const {
+ return const_iterator(*this, unboundedIntegerVariables.end());
+ }
+
Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const {
auto it = variableToVariable.find(variable);
STORM_LOG_THROW(it != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << variable.getName() << "'.");
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index d5a03a345..8c8ec6815 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -18,21 +18,21 @@ namespace storm {
class VariableSetIterator {
private:
- typedef std::vector<BooleanVariable>::const_iterator bool_iter;
- typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
- typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
+ typedef std::vector<BooleanVariable>::iterator bool_iter;
+ typedef std::vector<BoundedIntegerVariable>::iterator bint_iter;
+ typedef std::vector<UnboundedIntegerVariable>::iterator int_iter;
public:
/*!
* Creates an iterator over all variables.
*/
- VariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
+ VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
// Methods to advance the iterator.
VariableSetIterator& operator++();
VariableSetIterator& operator++(int);
- Variable const& operator*();
+ Variable& operator*();
bool operator==(VariableSetIterator const& other) const;
bool operator!=(VariableSetIterator const& other) const;
@@ -42,25 +42,76 @@ namespace storm {
void incrementIterator();
// The underlying variable set.
- VariableSet const& variableSet;
+ VariableSet& variableSet;
// The current iterator position.
boost::variant<bool_iter, bint_iter, int_iter> it;
};
+ class ConstVariableSetIterator {
+ private:
+ typedef std::vector<BooleanVariable>::const_iterator bool_iter;
+ typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
+ typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
+
+ public:
+ /*!
+ * Creates an iterator over all variables.
+ */
+ ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
+
+ // Methods to advance the iterator.
+ ConstVariableSetIterator& operator++();
+ ConstVariableSetIterator& operator++(int);
+
+ Variable const& operator*();
+
+ bool operator==(ConstVariableSetIterator const& other) const;
+ bool operator!=(ConstVariableSetIterator const& other) const;
+
+ private:
+ // Moves the iterator to the next position.
+ void incrementIterator();
+
+ // The underlying variable set.
+ VariableSet const& variableSet;
+
+ // The current iterator position.
+ boost::variant<bool_iter, bint_iter, int_iter> it;
+ };
+
class IntegerVariables {
public:
- IntegerVariables(VariableSet const& variableSet);
+ IntegerVariables(VariableSet& variableSet);
/*!
* Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
*/
- VariableSetIterator begin() const;
+ VariableSetIterator begin();
/*!
* Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
*/
- VariableSetIterator end() const;
+ VariableSetIterator end();
+
+ private:
+ // The underlying variable set.
+ VariableSet& variableSet;
+ };
+
+ class ConstIntegerVariables {
+ public:
+ ConstIntegerVariables(VariableSet const& variableSet);
+
+ /*!
+ * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
+ */
+ ConstVariableSetIterator begin() const;
+
+ /*!
+ * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
+ */
+ ConstVariableSetIterator end() const;
private:
// The underlying variable set.
@@ -72,30 +123,55 @@ namespace storm {
public:
friend class detail::VariableSetIterator;
+ typedef detail::VariableSetIterator iterator;
+ typedef detail::ConstVariableSetIterator const_iterator;
+ typedef detail::IntegerVariables IntegerVariables;
+ typedef detail::ConstIntegerVariables ConstIntegerVariables;
+
/*!
* Creates an empty variable set.
*/
VariableSet();
+ /*!
+ * Retrieves the boolean variables in this set.
+ */
+ std::vector<BooleanVariable>& getBooleanVariables();
+
/*!
* Retrieves the boolean variables in this set.
*/
std::vector<BooleanVariable> const& getBooleanVariables() const;
+ /*!
+ * Retrieves the bounded integer variables in this set.
+ */
+ std::vector<BoundedIntegerVariable>& getBoundedIntegerVariables();
+
/*!
* Retrieves the bounded integer variables in this set.
*/
std::vector<BoundedIntegerVariable> const& getBoundedIntegerVariables() const;
+ /*!
+ * Retrieves the unbounded integer variables in this set.
+ */
+ std::vector<UnboundedIntegerVariable>& getUnboundedIntegerVariables();
+
/*!
* Retrieves the unbounded integer variables in this set.
*/
std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
+
+ /*!
+ * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
+ */
+ IntegerVariables getIntegerVariables();
/*!
* Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
*/
- detail::IntegerVariables getIntegerVariables() const;
+ ConstIntegerVariables getIntegerVariables() const;
/*!
* Adds the given boolean variable to this set.
@@ -135,13 +211,23 @@ namespace storm {
/*!
* Retrieves an iterator to the variables in this set.
*/
- detail::VariableSetIterator begin() const;
+ iterator begin();
+
+ /*!
+ * Retrieves an iterator to the variables in this set.
+ */
+ const_iterator begin() const;
/*!
* Retrieves the end iterator to the variables in this set.
*/
- detail::VariableSetIterator end() const;
-
+ iterator end();
+
+ /*!
+ * Retrieves the end iterator to the variables in this set.
+ */
+ const_iterator end() const;
+
private:
/// The boolean variables in this set.
std::vector<BooleanVariable> booleanVariables;
diff --git a/src/utility/jani.cpp b/src/utility/jani.cpp
new file mode 100644
index 000000000..6a91f14a7
--- /dev/null
+++ b/src/utility/jani.cpp
@@ -0,0 +1,72 @@
+#include "src/utility/jani.h"
+
+#include <boost/algorithm/string.hpp>
+
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/jani/Model.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace utility {
+ namespace jani {
+
+ std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
+ std::set<storm::expressions::Variable> definedConstants;
+
+ if (!constantDefinitionString.empty()) {
+ // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
+ // one value for each undefined constant of the model.
+ std::vector<std::string> definitions;
+ boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
+ for (auto& definition : definitions) {
+ boost::trim(definition);
+
+ // Check whether the token could be a legal constant definition.
+ std::size_t positionOfAssignmentOperator = definition.find('=');
+ STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: syntax error.");
+
+ // Now extract the variable name and the value from the string.
+ std::string constantName = definition.substr(0, positionOfAssignmentOperator);
+ boost::trim(constantName);
+ std::string value = definition.substr(positionOfAssignmentOperator + 1);
+ boost::trim(value);
+
+ // Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
+ if (model.hasConstant(constantName)) {
+ // Get the actual constant and check whether it's in fact undefined.
+ auto const& constant = model.getConstant(constantName);
+ storm::expressions::Variable variable = constant.getExpressionVariable();
+ STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
+ STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
+ definedConstants.insert(variable);
+
+ if (constant.getType().isBooleanType()) {
+ if (value == "true") {
+ constantDefinitions[variable] = model.getExpressionManager().boolean(true);
+ } else if (value == "false") {
+ constantDefinitions[variable] = model.getExpressionManager().boolean(false);
+ } else {
+ throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
+ }
+ } else if (constant.getType().isIntegerType()) {
+ int_fast64_t integerValue = std::stoi(value);
+ constantDefinitions[variable] = model.getExpressionManager().integer(integerValue);
+ } else if (constant.getType().isRationalType()) {
+ double doubleValue = std::stod(value);
+ constantDefinitions[variable] = model.getExpressionManager().rational(doubleValue);
+ }
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'.");
+ }
+ }
+ }
+
+ return constantDefinitions;
+ }
+
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/utility/jani.h b/src/utility/jani.h
new file mode 100644
index 000000000..08bc75b91
--- /dev/null
+++ b/src/utility/jani.h
@@ -0,0 +1,23 @@
+#pragma once
+
+#include <map>
+
+namespace storm {
+ namespace expressions {
+ class Variable;
+ class Expression;
+ }
+
+ namespace jani {
+ class Model;
+ }
+
+ namespace utility {
+ namespace jani {
+
+ std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString);
+
+ }
+ }
+}
+