diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index e5b61020e7798f7e879c68d3724f4a62c5285da0..b38ec5fb382b676f522043d296d77854902c1c07 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1645,6 +1645,7 @@ public class TML2Avatar {
     private String processName(String name, int id) {
         name = reworkStringName(name).replaceAll("-", "_");
         if (allStates.contains(name)) {
+            allStates.add(name + id);
             return name + id;
 
         } else {
@@ -1895,6 +1896,7 @@ public class TML2Avatar {
             //AvatarTransition last;
             AvatarStateMachine asm = block.getStateMachine();
             //TODO: Create a fork with many requests. This looks terrible
+            allStates.clear();
             if (tmlmodel.getRequestToMe(task) != null) {
                 //Create iteration attribute
                 AvatarAttribute req_loop_index = new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 4420489e555e9a8bd6a36dc222a78feda559a60a..bdc902064fe08c2271408e38222cf4c4941f27f4 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -59,7 +59,7 @@ public class DiplodocusSecurityTest extends AbstractTest {
                 {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce",  "KeyExchange", "Mac", "SampleAutoSec"))},
                 {"ITA01_v6", new ArrayList<>(Arrays.asList("mapAtt", "mapNoProtection"))},
                 {"Rovers_SPARTA_DIPLO", new ArrayList<>(Arrays.asList("NoCountermeasureMapping", "MACMapping", "SymmetricEncryptionNonceMapping"))},
-                {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_hsm", "Architecture_enc_or"))}
+                {"ITSDemo", new ArrayList<>(Arrays.asList("Architecture", "Architecture_enc_or"))}
         });
     }
 
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
index 53b182021d69604a62e5b83ed4d819495d0fc091..9f56e4cf71f8f057e6f6d70afcddd909e3506814 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/KeyExchange/golden
@@ -1,5 +1,5 @@
 RESULT not attacker(Alice___encryptedKey_symKey0[!1 = v]) is true.
 RESULT not attacker(Alice___symKey_encrypted0[!1 = v]) is true.
 RESULT not attacker(Alice___symKey[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___symKey___decrypt_symKey_dummy(dummyM)) ==> inj-event(authenticity___Alice___symKey____encrypt_symKey(dummyM)) is false.
-RESULT (even event(authenticity___Bob___symKey___decrypt_symKey_dummy(dummyM)) ==> event(authenticity___Alice___symKey____encrypt_symKey(dummyM)) is false.)
+RESULT inj-event(authenticity___Bob___symKey___symKey_dummy(dummyM)) ==> inj-event(authenticity___Alice___symKey____symKey(dummyM)) is false.
+RESULT (even event(authenticity___Bob___symKey___symKey_dummy(dummyM)) ==> event(authenticity___Alice___symKey____symKey(dummyM)) is false.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
index 31f48beb63a359405ae50962a4421fb9cd404c27..cd1256e2d8d8156f82fb8e5bd31bf04fa78fccd5 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Mac/golden
@@ -1,4 +1,4 @@
 RESULT not attacker(Alice___mac[!1 = v]) is false.
 RESULT not attacker(Alice___mac_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___mac___decrypt_mac_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____encrypt_mac(dummyM)) is false.
-RESULT (but event(authenticity___Bob___mac___decrypt_mac_dummy(dummyM)) ==> event(authenticity___Alice___mac____encrypt_mac(dummyM)) is true.)
+RESULT inj-event(authenticity___Bob___mac___mac_dummy(dummyM)) ==> inj-event(authenticity___Alice___mac____mac(dummyM)) is false.
+RESULT (but event(authenticity___Bob___mac___mac_dummy(dummyM)) ==> event(authenticity___Alice___mac____mac(dummyM)) is true.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
index 920b9d782b0c5af446290475849883f178fa7edc..629b5f9a641abcc252c5f6c5bb379e112b4b5ac1 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/Nonce/golden
@@ -1,3 +1,3 @@
 RESULT not attacker(Alice___symN[!1 = v]) is true.
 RESULT not attacker(Alice___symN_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___symN___decrypt_symN_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____encrypt_symN(dummyM)) is true.
+RESULT inj-event(authenticity___Bob___symN___symN_dummy(dummyM)) ==> inj-event(authenticity___Alice___symN____symN(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
index 18dbf797352da865779b0c76dbeb1fe01661c26b..972a5ea44c99849686050b6f0add237820e16518 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/AliceAndBobHW/SymmetricExchange/golden
@@ -1,4 +1,4 @@
 RESULT not attacker(Alice___sym_encrypted0[!1 = v]) is true.
 RESULT not attacker(Alice___sym[!1 = v]) is true.
-RESULT inj-event(authenticity___Bob___sym___decrypt_sym_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____encrypt_sym(dummyM)) is false.
-RESULT (but event(authenticity___Bob___sym___decrypt_sym_dummy(dummyM)) ==> event(authenticity___Alice___sym____encrypt_sym(dummyM)) is true.)
+RESULT inj-event(authenticity___Bob___sym___sym_dummy(dummyM)) ==> inj-event(authenticity___Alice___sym____sym(dummyM)) is false.
+RESULT (but event(authenticity___Bob___sym___sym_dummy(dummyM)) ==> event(authenticity___Alice___sym____sym(dummyM)) is true.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
index c3dbb650434eb7c8b41859f1595fa10b97b36070..f7d41308df00552c7e20c8b9520a0857aea36104 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapAtt/golden
@@ -3,7 +3,7 @@ RESULT not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v])
 RESULT not attacker(BatterySensor___battery_chData0[!1 = v]) is true.
 RESULT not attacker(PumpController___AES_CTRL_encrypted0[!1 = v]) is true.
 RESULT not attacker(PumpController___AES_CTRL[!1 = v]) is true.
-RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
-RESULT (but event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is true.)
-RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
-RESULT (but event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is true.)
+RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is false.
+RESULT (but event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is true.)
+RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.
+RESULT (but event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is true.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
index 07e2bafe38ea32b7bf65d2d51c316332c22bcf0f..01dc1daea69a0ed29a8721e5ead863d2ec76827a 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v6/mapNoProtection/golden
@@ -3,7 +3,7 @@ RESULT not attacker(PumpController___AES_CTRL[!1 = v]) is false.
 RESULT not attacker(SmartphoneAppController___AES_Emergency_encrypted0[!1 = v]) is true.
 RESULT not attacker(SmartphoneAppController___AES_Emergency[!1 = v]) is false.
 RESULT not attacker(BatterySensor___battery_chData0[!1 = v]) is false.
-RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.
-RESULT (even event(authenticity___SmartphoneAppController___AES_CTRL___decrypt_AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____encrypt_AES_CTRL(dummyM)) is false.)
-RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.
-RESULT (even event(authenticity___MedicalInformationSystem___AES_Emergency___decrypt_AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____encrypt_AES_Emergency(dummyM)) is false.)
+RESULT inj-event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> inj-event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.
+RESULT (even event(authenticity___SmartphoneAppController___AES_CTRL___AES_CTRL_dummy(dummyM)) ==> event(authenticity___PumpController___AES_CTRL____AES_CTRL(dummyM)) is false.)
+RESULT inj-event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is false.
+RESULT (even event(authenticity___MedicalInformationSystem___AES_Emergency___AES_Emergency_dummy(dummyM)) ==> event(authenticity___SmartphoneAppController___AES_Emergency____AES_Emergency(dummyM)) is false.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
index 279f135f2087620efbd9057d6f357db496d7d97f..f993c8d3804bfaec3adb6e6a3aa1299c43e9ee57 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture/golden
@@ -3,5 +3,5 @@ RESULT inj-event(authenticity___vehicleControlGateway___vehData_chData0___afters
 RESULT (even event(authenticity___vehicleControlGateway___vehData_chData0___aftersignalstate_App_vehData_App_vehData(dummyM)) ==> event(authenticity___NavigationControl___vehData_chData0___signalstate_App_vehData_App_vehData(dummyM)) is false.)
 RESULT inj-event(authenticity___NavigationControl___GPSdata_chData0___aftersignalstate_App_GPSdata_App_GPSdata(dummyM)) ==> inj-event(authenticity___GPSGateway___GPSdata_chData0___signalstate_App_GPSdata_App_GPSdata(dummyM)) is false.
 RESULT (even event(authenticity___NavigationControl___GPSdata_chData0___aftersignalstate_App_GPSdata_App_GPSdata(dummyM)) ==> event(authenticity___GPSGateway___GPSdata_chData0___signalstate_App_GPSdata_App_GPSdata(dummyM)) is false.)
-RESULT inj-event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData316(dummyM)) is false.
-RESULT (even event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData316(dummyM)) is false.)
+RESULT inj-event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> inj-event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData(dummyM)) is false.
+RESULT (even event(authenticity___NavigationControl___sensorData_chData0___aftersignalstate_App_sensorData_App_sensorData(dummyM)) ==> event(authenticity___SensorUnit___sensorData_chData0___signalstate_App_sensorData_App_sensorData(dummyM)) is false.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
index f8bc28605a46484bd3dec5e3cee93db02136f64c..833cc3343249bbb471cd878c86597e727bd73012 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_enc_or/golden
@@ -4,6 +4,6 @@ RESULT not attacker(SensorUnit___autoEncrypt_sensorData[!1 = v]) is false.
 RESULT not attacker(SensorUnit___autoEncrypt_sensorData_encrypted0[!1 = v]) is true.
 RESULT not attacker(GPSGateway___autoEncrypt_GPSdata_encrypted0[!1 = v]) is true.
 RESULT not attacker(GPSGateway___autoEncrypt_GPSdata[!1 = v]) is true.
-RESULT inj-event(authenticity___vehicleControlGateway___autoEncrypt_vehData___decrypt_autoEncrypt_vehData_dummy(dummyM)) ==> inj-event(authenticity___NavigationControl___autoEncrypt_vehData____encrypt_autoEncrypt_vehData(dummyM)) is true.
-RESULT inj-event(authenticity___NavigationControl___autoEncrypt_sensorData___decrypt_autoEncrypt_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___autoEncrypt_sensorData____encrypt_autoEncrypt_sensorData(dummyM)) is true.
-RESULT inj-event(authenticity___NavigationControl___autoEncrypt_GPSdata___decrypt_autoEncrypt_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___autoEncrypt_GPSdata____encrypt_autoEncrypt_GPSdata(dummyM)) is true.
+RESULT inj-event(authenticity___vehicleControlGateway___autoEncrypt_vehData___autoEncrypt_vehData_dummy(dummyM)) ==> inj-event(authenticity___NavigationControl___autoEncrypt_vehData____autoEncrypt_vehData(dummyM)) is true.
+RESULT inj-event(authenticity___NavigationControl___autoEncrypt_sensorData___autoEncrypt_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___autoEncrypt_sensorData____autoEncrypt_sensorData(dummyM)) is true.
+RESULT inj-event(authenticity___NavigationControl___autoEncrypt_GPSdata___autoEncrypt_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___autoEncrypt_GPSdata____autoEncrypt_GPSdata(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
index 289a324f9b404aea74f7e0e492fcc96ef2ae5f09..7afd5edbdcba7573606ba6c0a34967392cf2d940 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITSDemo/Architecture_hsm/golden
@@ -1,5 +1,5 @@
 RESULT not attacker(GPSGateway___hsmSec_GPSdata_encrypted0[!1 = v]) is true.
 RESULT not attacker(GPSGateway___hsmSec_GPSdata[!1 = v]) is true.
-RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_sensorData___decrypt_hsmSec_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___hsmSec_sensorData____encrypt_hsmSec_sensorData(dummyM)) is true.
-RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_GPSdata___decrypt_hsmSec_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___hsmSec_GPSdata____encrypt_hsmSec_GPSdata(dummyM)) is true.
-RESULT inj-event(authenticity___vehicleControlGateway___hsmSec_vehData___decrypt_hsmSec_vehData_dummy(dummyM)) ==> inj-event(authenticity___HSM_CPU_Navigation___hsmSec_vehData____encrypt_hsmSec_vehData(dummyM)) is true.
+RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_sensorData___hsmSec_sensorData_dummy(dummyM)) ==> inj-event(authenticity___SensorUnit___hsmSec_sensorData____hsmSec_sensorData(dummyM)) is true.
+RESULT inj-event(authenticity___HSM_CPU_Navigation___hsmSec_GPSdata___hsmSec_GPSdata_dummy(dummyM)) ==> inj-event(authenticity___GPSGateway___hsmSec_GPSdata____hsmSec_GPSdata(dummyM)) is true.
+RESULT inj-event(authenticity___vehicleControlGateway___hsmSec_vehData___hsmSec_vehData_dummy(dummyM)) ==> inj-event(authenticity___HSM_CPU_Navigation___hsmSec_vehData____hsmSec_vehData(dummyM)) is true.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
index bc0ac5afaed63a7fd43f2a89ef7a59da80e8627a..e295e8d3136c45fd9a5ca68da027b6cf45fe583c 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/MACMapping/golden
@@ -1,4 +1,4 @@
 RESULT not attacker(Leader_Socket___PlatoonMAC_encrypted0[!1 = v]) is true.
 RESULT not attacker(Leader_Socket___PlatoonMAC[!1 = v]) is false.
-RESULT inj-event(authenticity___Socket___PlatoonMAC___decrypt_PlatoonMAC_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___PlatoonMAC____encrypt_PlatoonMAC(dummyM)) is false.
-RESULT (but event(authenticity___Socket___PlatoonMAC___decrypt_PlatoonMAC_dummy(dummyM)) ==> event(authenticity___Leader_Socket___PlatoonMAC____encrypt_PlatoonMAC(dummyM)) is true.)
+RESULT inj-event(authenticity___Socket___PlatoonMAC___PlatoonMAC_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___PlatoonMAC____PlatoonMAC(dummyM)) is false.
+RESULT (but event(authenticity___Socket___PlatoonMAC___PlatoonMAC_dummy(dummyM)) ==> event(authenticity___Leader_Socket___PlatoonMAC____PlatoonMAC(dummyM)) is true.)
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
index 84a71fb96a809f1dec891074a443ec9ecd58b6b8..a92bd324e64d885c72b4605eb610818f7ddc189a 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/NoCountermeasureMapping/golden
@@ -1,4 +1,4 @@
 RESULT not attacker(Leader_Socket___fromLSocToSoc_chData0[!1 = v]) is false.
-RESULT inj-event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc718(dummyM)) is false.
-RESULT (even event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc718(dummyM)) is false.)
+RESULT inj-event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> inj-event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) is false.
+RESULT (even event(authenticity___Socket___fromLSocToSoc_chData0___aftersignalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) ==> event(authenticity___Leader_Socket___fromLSocToSoc_chData0___signalstate_NoCountermeasure_fromLSocToSoc_NoCountermeasure_fromLSocToSoc(dummyM)) is false.)
 
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
index 0b313e80e6e674309ebae8e68cf6f8f7df0a9345..4be6877af7a4c0c7ba2e40cfa8b28c80fea3c4c9 100644
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/Rovers_SPARTA_DIPLO/SymmetricEncryptionNonceMapping/golden
@@ -4,6 +4,6 @@ RESULT not attacker(Socket___encrR[!1 = v]) is true.
 RESULT not attacker(Leader_Socket___nonceL[!1 = v]) is false.
 RESULT not attacker(Leader_Socket___encrL[!1 = v]) is true.
 RESULT not attacker(Leader_Socket___encrL_encrypted0[!1 = v]) is true.
-RESULT inj-event(authenticity___Leader_Socket___encrR___decrypt_encrR_dummy(dummyM)) ==> inj-event(authenticity___Socket___encrR____encrypt_encrR(dummyM)) is true.
-RESULT inj-event(authenticity___Socket___encrL___decrypt_encrL_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___encrL____encrypt_encrL(dummyM)) is true.
+RESULT inj-event(authenticity___Leader_Socket___encrR___encrR_dummy(dummyM)) ==> inj-event(authenticity___Socket___encrR____encrR(dummyM)) is true.
+RESULT inj-event(authenticity___Socket___encrL___encrL_dummy(dummyM)) ==> inj-event(authenticity___Leader_Socket___encrL____encrL(dummyM)) is true.