From 63e0d772a49f689a1688e5e60b58d60a34ccd6bf Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sun, 8 Mar 2020 20:02:49 -0700
Subject: [PATCH] do not use the 'goal' label for internal purposes, but rather
 __goal__. TODO: Consider if we can do without a fresh label

---
 .../modelchecker/ApproximatePOMDPModelchecker.cpp          | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
index 91947e075..0a910d64f 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
@@ -37,18 +37,19 @@ namespace storm {
                 storm::utility::Stopwatch underlyingWatch(true);
                 // Compute the results on the underlying MDP as a basic overapproximation
                 storm::models::sparse::StateLabeling underlyingMdpLabeling(pomdp.getStateLabeling());
-                underlyingMdpLabeling.addLabel("goal");
+                // TODO: Is the following really necessary
+                underlyingMdpLabeling.addLabel("__goal__");
                 std::vector<uint64_t> goalStates;
                 for (auto const &targetObs : targetObservations) {
                     for (auto const &goalState : pomdp.getStatesWithObservation(targetObs)) {
-                        underlyingMdpLabeling.addLabelToState("goal", goalState);
+                        underlyingMdpLabeling.addLabelToState("__goal__", goalState);
                     }
                 }
                 storm::models::sparse::Mdp<ValueType, RewardModelType> underlyingMdp(pomdp.getTransitionMatrix(), underlyingMdpLabeling, pomdp.getRewardModels());
                 auto underlyingModel = std::static_pointer_cast<storm::models::sparse::Model<ValueType, RewardModelType>>(
                         std::make_shared<storm::models::sparse::Mdp<ValueType, RewardModelType>>(underlyingMdp));
                 std::string initPropString = min ? "Pmin" : "Pmax";
-                initPropString += "=? [F \"goal\"]";
+                initPropString += "=? [F \"__goal__\"]";
                 std::vector<storm::jani::Property> propVector = storm::api::parseProperties(initPropString);
                 std::shared_ptr<storm::logic::Formula const> underlyingProperty = storm::api::extractFormulasFromProperties(propVector).front();
                 STORM_PRINT("Underlying MDP" << std::endl)