From 6dd6c502e7c991b582cab2e62598572fb0686c6f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 4 Nov 2019 13:06:14 +0100
Subject: [PATCH] Prism: Error upon synchronized write to global variable.

---
 src/storm/storage/prism/Program.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index bb4132205..907ddf097 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -1134,6 +1134,7 @@ namespace storm {
             bool hasProbabilisticCommand = false;
             bool hasMarkovianCommand = false;
             bool hasLabeledMarkovianCommand = false;
+            std::map<std::pair<storm::expressions::Variable,uint64_t>,std::pair<uint64_t,std::string>> writtenGlobalVariables;
             for (auto const& module : this->getModules()) {
                 std::set<storm::expressions::Variable> legalVariables = globalVariables;
                 for (auto const& variable : module.getBooleanVariables()) {
@@ -1218,6 +1219,13 @@ namespace storm {
                             STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
                             STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() || (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
                             
+                            if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
+                                std::pair<storm::expressions::Variable, uint64_t>variableActionIndexPair(assignedVariable, command.getActionIndex());
+                                std::pair<uint64_t,std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
+                                auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
+                                STORM_LOG_THROW(insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": Syncronizing command with action label '" << command.getActionName() << "' illegally assigns a value to global variable '" << assignedVariable.getName() << "'. Previous assignment to the variable at line " << insertionResult.first->second.first << " in module '" << insertionResult.first->second.second << "'.");
+                            }
+                            
                             containedVariables = assignment.getExpression().getVariables();
                             illegalVariables.clear();
                             std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin()));