From 71bfb4522044089db2c5c027e22713d419cab84f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 16 Jun 2016 11:26:15 +0200
Subject: [PATCH] added check for multiple writes to the same global variable
in explicit JANI next-state generator
Former-commit-id: 5fc1bb01a94d731df0e029fa5b224fbebff66d09
---
src/generator/JaniNextStateGenerator.cpp | 22 +++++++++++++
src/generator/JaniNextStateGenerator.h | 8 ++++-
src/generator/VariableInformation.cpp | 12 +++----
src/generator/VariableInformation.h | 10 ++++--
src/storage/jani/Automaton.cpp | 7 +++++
src/storage/jani/Automaton.h | 8 +++++
src/storage/jani/Edge.cpp | 15 +++++++++
src/storage/jani/Edge.h | 31 +++++++++++++++----
src/storage/jani/Model.cpp | 6 ++++
src/storage/jani/Model.h | 7 +++++
src/storage/prism/Program.cpp | 2 ++
.../builder/DdJaniModelBuilderTest.cpp | 2 +-
.../builder/ExplicitJaniModelBuilderTest.cpp | 10 +++++-
.../builder/ExplicitPrismModelBuilderTest.cpp | 2 +-
14 files changed, 124 insertions(+), 18 deletions(-)
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 7c6fe0967..10186bb98 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -327,6 +327,9 @@ namespace storm {
// Only process this action, if there is at least one feasible solution.
if (!enabledEdges.empty()) {
+ // Check whether a global variable is written multiple times in any combination.
+ checkGlobalVariableWritesValid(enabledEdges);
+
std::vector<std::vector<storm::jani::Edge const*>::const_iterator> iteratorList(enabledEdges.size());
// Initialize the list of iterators.
@@ -453,6 +456,25 @@ namespace storm {
return result;
}
+ template<typename ValueType, typename StateType>
+ void JaniNextStateGenerator<ValueType, StateType>::checkGlobalVariableWritesValid(std::vector<std::vector<storm::jani::Edge const*>> const& enabledEdges) const {
+ std::map<storm::expressions::Variable, uint64_t> writtenGlobalVariables;
+ for (auto edgeSetIt = enabledEdges.begin(), edgeSetIte = enabledEdges.end(); edgeSetIt != edgeSetIte; ++edgeSetIt) {
+ for (auto const& edge : *edgeSetIt) {
+ for (auto const& globalVariable : edge->getWrittenGlobalVariables()) {
+ auto it = writtenGlobalVariables.find(globalVariable);
+
+ auto index = std::distance(enabledEdges.begin(), edgeSetIt);
+ if (it != writtenGlobalVariables.end()) {
+ STORM_LOG_THROW(it->second == index, storm::exceptions::WrongFormatException, "Multiple writes to global variable '" << globalVariable.getName() << "' in synchronizing edges.");
+ } else {
+ writtenGlobalVariables.emplace(globalVariable, index);
+ }
+ }
+ }
+ }
+ }
+
template<typename ValueType, typename StateType>
std::size_t JaniNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
return 0;
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index 3bb4939e5..350377eec 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/src/generator/JaniNextStateGenerator.h
@@ -83,7 +83,13 @@ namespace storm {
*/
std::vector<std::vector<storm::jani::Edge const*>> getEnabledEdges(std::vector<uint64_t> const& locationIndices, uint64_t actionIndex);
- // The model used for the generation of next states.
+ /*!
+ * Checks the list of enabled edges (obtained by a call to <code>getEnabledEdges</code>) for multiple
+ * synchronized writes to the same global variable.
+ */
+ void checkGlobalVariableWritesValid(std::vector<std::vector<storm::jani::Edge const*>> const& enabledEdges) const;
+
+ /// The model used for the generation of next states.
storm::jani::Model model;
};
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index ca539432d..b009f849f 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -9,11 +9,11 @@
namespace storm {
namespace generator {
- BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset) : variable(variable), bitOffset(bitOffset) {
+ BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global) : variable(variable), bitOffset(bitOffset), global(global) {
// Intentionally left empty.
}
- IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
+ IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global) {
// Intentionally left empty.
}
@@ -23,14 +23,14 @@ namespace storm {
VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
- booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
+ booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true);
++totalBitOffset;
}
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
- integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+ integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
totalBitOffset += bitwidth;
}
for (auto const& module : program.getModules()) {
@@ -52,14 +52,14 @@ namespace storm {
VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) {
for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
- booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
+ booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
++totalBitOffset;
}
for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
- integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+ integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
totalBitOffset += bitwidth;
}
for (auto const& automaton : model.getAutomata()) {
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
index fa913f86c..1aa8ee95c 100644
--- a/src/generator/VariableInformation.h
+++ b/src/generator/VariableInformation.h
@@ -19,18 +19,21 @@ namespace storm {
// A structure storing information about the boolean variables of the model.
struct BooleanVariableInformation {
- BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset);
+ BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global = false);
// The boolean variable.
storm::expressions::Variable variable;
// Its bit offset in the compressed state.
uint_fast64_t bitOffset;
+
+ // A flag indicating whether the variable is a global one.
+ bool global;
};
// A structure storing information about the integer variables of the model.
struct IntegerVariableInformation {
- IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+ IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false);
// The integer variable.
storm::expressions::Variable variable;
@@ -46,6 +49,9 @@ namespace storm {
// Its bit width in the compressed state.
uint_fast64_t bitWidth;
+
+ // A flag indicating whether the variable is a global one.
+ bool global;
};
// A structure storing information about the location variables of the model.
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 25bb776f3..0165351be 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -315,5 +315,12 @@ namespace storm {
}
return result;
}
+
+ void Automaton::finalize(Model const& containingModel) {
+ for (auto& edge : edges) {
+ edge.finalize(containingModel);
+ }
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index c524e7d03..49b5464eb 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -80,6 +80,8 @@ namespace storm {
};
}
+ class Model;
+
class Automaton {
public:
friend class detail::Edges;
@@ -251,6 +253,12 @@ namespace storm {
*/
std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+ /*!
+ * Finalizes the building of this automaton. Subsequent changes to the automaton require another call to this
+ * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
+ */
+ void finalize(Model const& containingModel);
+
private:
/// The name of the automaton.
std::string name;
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index deaac34e5..347140b1b 100644
--- a/src/storage/jani/Edge.cpp
+++ b/src/storage/jani/Edge.cpp
@@ -1,5 +1,7 @@
#include "src/storage/jani/Edge.h"
+#include "src/storage/jani/Model.h"
+
namespace storm {
namespace jani {
@@ -47,5 +49,18 @@ namespace storm {
destinations.push_back(destination);
}
+ void Edge::finalize(Model const& containingModel) {
+ for (auto const& destination : getDestinations()) {
+ for (auto const& assignment : destination.getAssignments()) {
+ if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) {
+ writtenGlobalVariables.insert(assignment.getExpressionVariable());
+ }
+ }
+ }
+ }
+
+ boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
+ return writtenGlobalVariables;
+ }
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
index 5e835fa80..cb872ebbe 100644
--- a/src/storage/jani/Edge.h
+++ b/src/storage/jani/Edge.h
@@ -1,12 +1,15 @@
#pragma once
#include <boost/optional.hpp>
+#include <boost/container/flat_set.hpp>
#include "src/storage/jani/EdgeDestination.h"
namespace storm {
namespace jani {
+ class Model;
+
class Edge {
public:
Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
@@ -61,22 +64,38 @@ namespace storm {
*/
void addDestination(EdgeDestination const& destination);
+ /*!
+ * Finalizes the building of this edge. Subsequent changes to the edge require another call to this
+ * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
+ */
+ void finalize(Model const& containingModel);
+
+ /*!
+ * Retrieves a set of (global) variables that are written by at least one of the edge's destinations. Note
+ * that prior to calling this, the edge has to be finalized.
+ */
+ boost::container::flat_set<storm::expressions::Variable> const& getWrittenGlobalVariables() const;
+
private:
- // The index of the source location.
+ /// The index of the source location.
uint64_t sourceLocationIndex;
- // The index of the action with which this edge is labeled.
+ /// The index of the action with which this edge is labeled.
uint64_t actionIndex;
- // The rate with which this edge is taken. This only applies to continuous-time models. For discrete-time
- // models, this must be set to none.
+ /// The rate with which this edge is taken. This only applies to continuous-time models. For discrete-time
+ /// models, this must be set to none.
boost::optional<storm::expressions::Expression> rate;
- // The guard that defines when this edge is enabled.
+ /// The guard that defines when this edge is enabled.
storm::expressions::Expression guard;
- // The destinations of this edge.
+ /// The destinations of this edge.
std::vector<EdgeDestination> destinations;
+
+ /// A set of global variables that is written by at least one of the edge's destinations. This set is
+ /// initialized by the call to <code>finalize</code>.
+ boost::container::flat_set<storm::expressions::Variable> writtenGlobalVariables;
};
}
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index bef0f8d06..ed4d4aa68 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -380,6 +380,12 @@ namespace storm {
return result;
}
+ void Model::finalize() {
+ for (auto& automaton : getAutomata()) {
+ automaton.finalize(*this);
+ }
+ }
+
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 7ec380bb9..be779083c 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -269,6 +269,13 @@ namespace storm {
*/
bool hasDefaultComposition() const;
+ /*!
+ * After adding all components to the model, this method has to be called. It recursively calls
+ * <code>finalize</code> on all contained elements. All subsequent changes to the model require another call
+ * to this method.
+ */
+ void finalize();
+
/*!
* 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/prism/Program.cpp b/src/storage/prism/Program.cpp
index 24eca0256..c1a1e4cf0 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1665,6 +1665,8 @@ namespace storm {
janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
}
+ janiModel.finalize();
+
return janiModel;
}
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 46f73055a..1470e196d 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -320,7 +320,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(59ul, mdp->getNumberOfChoices());
}
-TEST(DdJaniModelBuilderTest_Cudd, IllegalFragment) {
+TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
diff --git a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
index 23e1119a7..17df2ca97 100644
--- a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
@@ -116,9 +116,17 @@ TEST(ExplicitJaniModelBuilderTest, Mdp) {
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
-TEST(ExplicitJaniModelBuilderTest, Fail) {
+TEST(ExplicitJaniModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
storm::jani::Model janiModel = program.toJani();
ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
}
+
+TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
+ storm::jani::Model janiModel = program.toJani();
+
+ ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
+}
+
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index b7e579366..ac2b1f6fb 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -99,7 +99,7 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
EXPECT_EQ(59ul, model->getNumberOfTransitions());
}
-TEST(ExplicitPrismModelBuilderTest, Fail) {
+TEST(ExplicitPrismModelBuilderTest, FailComposition) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);