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> writtenGlobalVariables; for (auto const& module : this->getModules()) { std::set 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::pairvariableActionIndexPair(assignedVariable, command.getActionIndex()); + std::pair 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()));