added check for multiple writes to the same global variable in explicit JANI next-state generator

Former-commit-id: 5fc1bb01a9

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;

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

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

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.

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);
+            }
+        }
+
     }
 }

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;

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

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

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.
             

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.
              */

src/storage/prism/Program.cpp

@@ -1665,6 +1665,8 @@ namespace storm {
                 janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
             }
             
+            janiModel.finalize();
+            
             return janiModel;
         }
         

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

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);
+}
+

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