From 81dd0dfadd530fda86e70aee8912945d215786bc Mon Sep 17 00:00:00 2001
From: "Arne Nordmann (CR/AEA2)" <arne.nordmann@de.bosch.com>
Date: Mon, 19 Oct 2020 13:47:09 +0200
Subject: [PATCH] Disallowusage of OCRA constraints outside OCRA

To not pollute nusmv language models with OCRA expression/constraint
concepts, additional MPS constrants are introduced. All OCRA expressions
now extend the interface IOcraExpression, which is only allowed
('can be child of') inside OCRA contracts.

https://github.com/mbeddr/mbeddr.formal/issues/54

Signed-off-by: Arne Nordmann (CR/AEA2) <arne.nordmann@de.bosch.com>
---
 .../com.mbeddr.formal.ocra.mpl                | 45 ++++++++++++
 .../com.mbeddr.formal.ocra.mpl                |  5 ++
 .../com.mbeddr.formal.ocra.behavior.mps       |  2 -
 .../com.mbeddr.formal.ocra.constraints.mps    | 34 +++++++++
 .../com.mbeddr.formal.ocra.structure.mps      | 71 ++++++++++++++++++-
 5 files changed, 153 insertions(+), 4 deletions(-)
 create mode 100644 code/languages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl

diff --git a/code/languages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl b/code/languages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
new file mode 100644
index 000000000..7abe1eb77
--- /dev/null
+++ b/code/languages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
@@ -0,0 +1,45 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<language namespace="com.mbeddr.formal.ocra" uuid="5ccce04a-9411-450d-8af4-a858c6f99d1e" languageVersion="0" moduleVersion="0">
+  <models>
+    <modelRoot contentPath="${module}" type="default">
+      <sourceRoot location="models" />
+    </modelRoot>
+  </models>
+  <facets>
+    <facet type="java">
+      <classes generated="true" path="${module}/classes_gen" />
+    </facet>
+  </facets>
+  <accessoryModels />
+  <sourcePath />
+  <languageVersions>
+    <language slang="l:ceab5195-25ea-4f22-9b92-103b95ca8c0c:jetbrains.mps.lang.core" version="2" />
+    <language slang="l:f4ad079d-bc71-4ffb-9600-9328705cf998:jetbrains.mps.lang.descriptor" version="0" />
+  </languageVersions>
+  <dependencyVersions>
+    <module reference="3f233e7f-b8a6-46d2-a57f-795d56775243(Annotations)" version="0" />
+    <module reference="6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)" version="0" />
+    <module reference="6ed54515-acc8-4d1e-a16c-9fd6cfe951ea(MPS.Core)" version="0" />
+    <module reference="1ed103c3-3aa6-49b7-9c21-6765ee11f224(MPS.Editor)" version="0" />
+    <module reference="498d89d2-c2e9-11e2-ad49-6cf049e62fe5(MPS.IDEA)" version="0" />
+    <module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
+    <module reference="742f6602-5a2f-4313-aa6e-ae1cd4ffdc61(MPS.Platform)" version="0" />
+    <module reference="83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)" version="0" />
+    <module reference="b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions)" version="0" />
+    <module reference="001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)" version="0" />
+    <module reference="5ccce04a-9411-450d-8af4-a858c6f99d1e(com.mbeddr.formal.ocra)" version="0" />
+    <module reference="f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)" version="0" />
+    <module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
+    <module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
+    <module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
+    <module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
+    <module reference="9e98f4e2-decf-4e97-bf80-9109e8b759aa(jetbrains.mps.lang.feedback.context)" version="0" />
+    <module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
+  </dependencyVersions>
+  <extendedLanguages>
+    <extendedLanguage>001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)</extendedLanguage>
+    <extendedLanguage>f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)</extendedLanguage>
+    <extendedLanguage>b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions)</extendedLanguage>
+  </extendedLanguages>
+</language>
+
diff --git a/code/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl b/code/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
index a95b0a189..f374c69e5 100644
--- a/code/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
+++ b/code/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
@@ -17,6 +17,8 @@
     <dependency reexport="false">83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)</dependency>
     <dependency reexport="false">2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)</dependency>
     <dependency reexport="false">6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)</dependency>
+    <dependency reexport="false">c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)</dependency>
+    <dependency reexport="false">001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)</dependency>
   </dependencies>
   <languageVersions>
     <language slang="l:9d69e719-78c8-4286-90db-fb19c107d049:com.mbeddr.mpsutil.grammarcells" version="1" />
@@ -70,9 +72,12 @@
     <module reference="f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)" version="0" />
     <module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
     <module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
+    <module reference="d936855b-48da-4812-a8a0-2bfddd633ac5(jetbrains.mps.lang.behavior.api)" version="0" />
     <module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
     <module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
     <module reference="9e98f4e2-decf-4e97-bf80-9109e8b759aa(jetbrains.mps.lang.feedback.context)" version="0" />
+    <module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
+    <module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
     <module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
   </dependencyVersions>
   <extendedLanguages>
diff --git a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.behavior.mps b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.behavior.mps
index ce500b181..8f6235862 100644
--- a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.behavior.mps
+++ b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.behavior.mps
@@ -5,7 +5,6 @@
     <use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="17" />
     <use id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior" version="2" />
     <use id="d8f591ec-4d86-4af2-9f92-a9e93c803ffa" name="jetbrains.mps.lang.scopes" version="0" />
-    <use id="7a5dda62-9140-4668-ab76-d5ed1746f2b2" name="jetbrains.mps.lang.typesystem" version="5" />
     <devkit ref="fbc25dd2-5da4-483a-8b19-70928e1b62d7(jetbrains.mps.devkit.general-purpose)" />
   </languages>
   <imports>
@@ -13,7 +12,6 @@
     <import index="hqls" ref="r:9be6a7f5-8948-4321-86ee-36906d4a48b4(com.mbeddr.formal.ocra.structure)" />
     <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
     <import index="o8zo" ref="r:314576fc-3aee-4386-a0a5-a38348ac317d(jetbrains.mps.scope)" />
-    <import index="c17a" ref="8865b7a8-5271-43d3-884c-6fd1d9cfdd34/java:org.jetbrains.mps.openapi.language(MPS.OpenAPI/)" />
     <import index="w873" ref="r:0de03bcd-6ad8-423c-b85e-ae3dd18ed2b3(com.mbeddr.formal.base.behavior)" />
     <import index="ox2v" ref="r:9d0d3f45-3600-4f52-892b-d59f24c624ff(com.mbeddr.formal.base.expressions.behavior)" implicit="true" />
   </imports>
diff --git a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.constraints.mps b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.constraints.mps
index ea7e194e0..ce6dffef8 100644
--- a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.constraints.mps
+++ b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.constraints.mps
@@ -11,12 +11,14 @@
     <use id="13744753-c81f-424a-9c1b-cf8943bf4e86" name="jetbrains.mps.lang.sharedConcepts" version="0" />
     <use id="3ad5badc-1d9c-461c-b7b1-fa2fcd0a0ae7" name="jetbrains.mps.lang.context" version="0" />
     <use id="ad93155d-79b2-4759-b10c-55123e763903" name="jetbrains.mps.lang.messages" version="0" />
+    <use id="f2801650-65d5-424e-bb1b-463a8781b786" name="jetbrains.mps.baseLanguage.javadoc" version="2" />
     <devkit ref="00000000-0000-4000-0000-5604ebd4f22c(jetbrains.mps.devkit.aspect.constraints)" />
   </languages>
   <imports>
     <import index="o8zo" ref="r:314576fc-3aee-4386-a0a5-a38348ac317d(jetbrains.mps.scope)" />
     <import index="hqls" ref="r:9be6a7f5-8948-4321-86ee-36906d4a48b4(com.mbeddr.formal.ocra.structure)" />
     <import index="ehqg" ref="r:2c1724e1-8ed6-4fe4-9e44-fae13cd2a5ac(com.mbeddr.formal.base.expressions.structure)" />
+    <import index="tpcn" ref="r:00000000-0000-4000-0000-011c8959028b(jetbrains.mps.lang.structure.behavior)" />
     <import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" implicit="true" />
   </imports>
   <registry>
@@ -76,10 +78,12 @@
       </concept>
     </language>
     <language id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints">
+      <concept id="6702802731807351367" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAChild" flags="in" index="9S07l" />
       <concept id="6702802731807420587" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAParent" flags="ig" index="9SLcT" />
       <concept id="8966504967485224688" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_contextNode" flags="nn" index="2rP1CM" />
       <concept id="4303308395523343364" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_link" flags="ng" index="2DA6wF" />
       <concept id="4303308395523096213" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_childConcept" flags="ng" index="2DD5aU" />
+      <concept id="1147468365020" name="jetbrains.mps.lang.constraints.structure.ConstraintsFunctionParameter_node" flags="nn" index="EsrRn" />
       <concept id="5564765827938091039" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_ReferentSearchScope_Scope" flags="ig" index="3dgokm" />
       <concept id="8401916545537438642" name="jetbrains.mps.lang.constraints.structure.InheritedNodeScopeFactory" flags="ng" index="1dDu$B">
         <reference id="8401916545537438643" name="kind" index="1dDu$A" />
@@ -90,6 +94,7 @@
       <concept id="1213093968558" name="jetbrains.mps.lang.constraints.structure.ConceptConstraints" flags="ng" index="1M2fIO">
         <reference id="1213093996982" name="concept" index="1M2myG" />
         <child id="6702802731807532712" name="canBeParent" index="9SGkU" />
+        <child id="6702802731807737306" name="canBeChild" index="9Vyp8" />
         <child id="1213100494875" name="referent" index="1Mr941" />
         <child id="1213101058038" name="defaultScope" index="1MtirG" />
       </concept>
@@ -108,6 +113,7 @@
       <concept id="4693937538533521280" name="jetbrains.mps.lang.smodel.structure.OfConceptOperation" flags="ng" index="v3k3i">
         <child id="4693937538533538124" name="requestedConcept" index="v3oSu" />
       </concept>
+      <concept id="1173122760281" name="jetbrains.mps.lang.smodel.structure.Node_GetAncestorsOperation" flags="nn" index="z$bX8" />
       <concept id="2396822768958367367" name="jetbrains.mps.lang.smodel.structure.AbstractTypeCastExpression" flags="nn" index="$5XWr">
         <child id="6733348108486823193" name="leftExpression" index="1m5AlR" />
         <child id="3906496115198199033" name="conceptArgument" index="3oSUPX" />
@@ -145,6 +151,9 @@
       </concept>
     </language>
     <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
+      <concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
+        <property id="1193676396447" name="virtualPackage" index="3GE5qa" />
+      </concept>
       <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
         <property id="1169194664001" name="name" index="TrG5h" />
       </concept>
@@ -154,6 +163,7 @@
         <child id="540871147943773366" name="argument" index="25WWJ7" />
       </concept>
       <concept id="1160666733551" name="jetbrains.mps.baseLanguage.collections.structure.AddAllElementsOperation" flags="nn" index="X8dFx" />
+      <concept id="1176501494711" name="jetbrains.mps.baseLanguage.collections.structure.IsNotEmptyOperation" flags="nn" index="3GX2aA" />
     </language>
   </registry>
   <node concept="1M2fIO" id="1QMZQ046hgc">
@@ -564,5 +574,29 @@
       </node>
     </node>
   </node>
+  <node concept="1M2fIO" id="46t5MkZs$er">
+    <property role="3GE5qa" value="constraints" />
+    <ref role="1M2myG" to="hqls:46t5MkZsy$k" resolve="IOCRAConstraint" />
+    <node concept="9S07l" id="46t5MkZs$LM" role="9Vyp8">
+      <node concept="3clFbS" id="46t5MkZs$LN" role="2VODD2">
+        <node concept="3clFbF" id="46t5MkZs_p3" role="3cqZAp">
+          <node concept="2OqwBi" id="46t5MkZsFET" role="3clFbG">
+            <node concept="2OqwBi" id="46t5MkZsBFb" role="2Oq$k0">
+              <node concept="2OqwBi" id="46t5MkZs_Ae" role="2Oq$k0">
+                <node concept="EsrRn" id="46t5MkZs_p2" role="2Oq$k0" />
+                <node concept="z$bX8" id="46t5MkZsA4e" role="2OqNvi" />
+              </node>
+              <node concept="v3k3i" id="46t5MkZsDG$" role="2OqNvi">
+                <node concept="chp4Y" id="46t5MkZsFrx" role="v3oSu">
+                  <ref role="cht4Q" to="hqls:1WjQLbKt0ti" resolve="Contract" />
+                </node>
+              </node>
+            </node>
+            <node concept="3GX2aA" id="46t5MkZsG9k" role="2OqNvi" />
+          </node>
+        </node>
+      </node>
+    </node>
+  </node>
 </model>
 
diff --git a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.structure.mps b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.structure.mps
index a1e1ab351..bb3448689 100644
--- a/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.structure.mps
+++ b/code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.structure.mps
@@ -9,8 +9,8 @@
     <import index="tpee" ref="r:00000000-0000-4000-0000-011c895902ca(jetbrains.mps.baseLanguage.structure)" />
     <import index="ehqg" ref="r:2c1724e1-8ed6-4fe4-9e44-fae13cd2a5ac(com.mbeddr.formal.base.expressions.structure)" />
     <import index="b19z" ref="r:11a68676-9d63-4e1c-b920-59aefe77def3(com.mbeddr.formal.base.structure)" />
+    <import index="gioj" ref="r:a6dee7e9-c79f-4293-b631-7c366a8877df(com.mbeddr.formal.nusmv.structure)" />
     <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
-    <import index="gioj" ref="r:a6dee7e9-c79f-4293-b631-7c366a8877df(com.mbeddr.formal.nusmv.structure)" implicit="true" />
   </imports>
   <registry>
     <language id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure">
@@ -36,7 +36,9 @@
         <child id="1071489727083" name="linkDeclaration" index="1TKVEi" />
         <child id="1071489727084" name="propertyDeclaration" index="1TKVEl" />
       </concept>
-      <concept id="1169125989551" name="jetbrains.mps.lang.structure.structure.InterfaceConceptDeclaration" flags="ig" index="PlHQZ" />
+      <concept id="1169125989551" name="jetbrains.mps.lang.structure.structure.InterfaceConceptDeclaration" flags="ig" index="PlHQZ">
+        <child id="1169127546356" name="extends" index="PrDN$" />
+      </concept>
       <concept id="1169127622168" name="jetbrains.mps.lang.structure.structure.InterfaceConceptReference" flags="ig" index="PrWs8">
         <reference id="1169127628841" name="intfc" index="PrY4T" />
       </concept>
@@ -922,6 +924,9 @@
     <property role="34LRSv" value="and" />
     <property role="R4oN_" value="Logical &quot;and&quot; expression" />
     <ref role="1TJDcQ" to="ehqg:7mSH3WnsxDR" resolve="AndExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZuz1U" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVCPoT">
     <property role="EcuMT" value="2331162319165543993" />
@@ -930,6 +935,9 @@
     <property role="34LRSv" value="or" />
     <property role="R4oN_" value="Logical &quot;or&quot; expression" />
     <ref role="1TJDcQ" to="ehqg:7mSH3Wnte8z" resolve="OrExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZuxDn" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVCPsq">
     <property role="EcuMT" value="2331162319165544218" />
@@ -938,6 +946,9 @@
     <property role="R4oN_" value="Logical &quot;xor&quot; expression" />
     <property role="34LRSv" value="xor" />
     <ref role="1TJDcQ" to="ehqg:7mSH3WnHVWN" resolve="XorExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZux5Y" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVCPwr">
     <property role="EcuMT" value="2331162319165544475" />
@@ -946,6 +957,9 @@
     <property role="R4oN_" value="Logical &quot;if and only if&quot; expression" />
     <property role="34LRSv" value="iff" />
     <ref role="1TJDcQ" to="ehqg:57ROGn90yFJ" resolve="IffExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZuyux" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVCP$s">
     <property role="EcuMT" value="2331162319165544732" />
@@ -954,6 +968,9 @@
     <property role="R4oN_" value="Logical &quot;implies&quot; expression" />
     <property role="34LRSv" value="implies" />
     <ref role="1TJDcQ" to="ehqg:7mSH3WnsxEd" resolve="ImpliesExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZuycN" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVCX3X">
     <property role="EcuMT" value="2331162319165575421" />
@@ -962,6 +979,9 @@
     <property role="R4oN_" value="Logical &quot;not&quot; expression" />
     <property role="34LRSv" value="not" />
     <ref role="1TJDcQ" to="ehqg:7mSH3Wnsy0f" resolve="NotExpressionBase" />
+    <node concept="PrWs8" id="46t5MkZuxV5" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVD0qQ">
     <property role="EcuMT" value="2331162319165589174" />
@@ -970,6 +990,9 @@
     <property role="34LRSv" value="always" />
     <property role="R4oN_" value="LTL &quot;always / globally&quot; expression" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Um38" resolve="BoundedUnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZsNdF" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVD0C4">
     <property role="EcuMT" value="2331162319165590020" />
@@ -978,6 +1001,9 @@
     <property role="34LRSv" value="in the future" />
     <property role="R4oN_" value="LTL &quot;in the future / finally&quot; expression" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Um38" resolve="BoundedUnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZuris" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="21pWWsVD0G5">
     <property role="EcuMT" value="2331162319165590277" />
@@ -986,6 +1012,9 @@
     <property role="34LRSv" value="then" />
     <property role="R4oN_" value="LTL &quot;then / next state&quot; expression" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgr" resolve="UnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZus7z" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Uq4L">
     <property role="EcuMT" value="9133754867501343025" />
@@ -994,6 +1023,9 @@
     <property role="R4oN_" value="LTL &quot;until&quot; expression" />
     <property role="34LRSv" value="until" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgs" resolve="BinaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZusWE" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utri">
     <property role="EcuMT" value="9133754867501356754" />
@@ -1002,6 +1034,9 @@
     <property role="R4oN_" value="LTL &quot;releases&quot; expression" />
     <property role="34LRSv" value="releases" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgs" resolve="BinaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZuqtl" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utro">
     <property role="EcuMT" value="9133754867501356760" />
@@ -1010,6 +1045,9 @@
     <property role="R4oN_" value="LTL &quot;triggered&quot; expression" />
     <property role="34LRSv" value="triggered" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgs" resolve="BinaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZusph" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utrn">
     <property role="EcuMT" value="9133754867501356759" />
@@ -1018,6 +1056,9 @@
     <property role="R4oN_" value="LTL &quot;since&quot; expression" />
     <property role="34LRSv" value="since" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgs" resolve="BinaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZur$a" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utrl">
     <property role="EcuMT" value="9133754867501356757" />
@@ -1026,6 +1067,9 @@
     <property role="R4oN_" value="LTL &quot;historically&quot; expression" />
     <property role="34LRSv" value="historically" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Um38" resolve="BoundedUnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZuofR" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utrm">
     <property role="EcuMT" value="9133754867501356758" />
@@ -1034,6 +1078,9 @@
     <property role="34LRSv" value="in the past" />
     <property role="R4oN_" value="LTL &quot;in the past&quot; expression" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Um38" resolve="BoundedUnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZur0I" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7V1Bqz6Utrj">
     <property role="EcuMT" value="9133754867501356755" />
@@ -1042,6 +1089,9 @@
     <property role="R4oN_" value="LTL &quot;previously&quot; expression" />
     <property role="34LRSv" value="previously" />
     <ref role="1TJDcQ" to="gioj:7V1Bqz6Uhgr" resolve="UnaryLTLExpression" />
+    <node concept="PrWs8" id="46t5MkZupCh" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="7mSH3WnwK$u">
     <property role="EcuMT" value="8482728081222732062" />
@@ -1057,6 +1107,9 @@
       <property role="20lbJX" value="fLJekj4/_1" />
       <ref role="20lvS9" to="ehqg:6NmtaR1V301" resolve="Expression" />
     </node>
+    <node concept="PrWs8" id="46t5MkZuul7" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="404$BAz1Qz6">
     <property role="EcuMT" value="4612972969458100422" />
@@ -1072,6 +1125,9 @@
       <property role="20lbJX" value="fLJekj4/_1" />
       <ref role="20lvS9" to="ehqg:6NmtaR1V301" resolve="Expression" />
     </node>
+    <node concept="PrWs8" id="46t5MkZutLI" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="404$BAz2uz_">
     <property role="EcuMT" value="4612972969458264293" />
@@ -1098,6 +1154,9 @@
       <property role="20kJfa" value="timeExpr" />
       <ref role="20lvS9" to="ehqg:6NmtaR1V301" resolve="Expression" />
     </node>
+    <node concept="PrWs8" id="46t5MkZuvab" role="PzmwI">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="404$BAz78Ye">
     <property role="EcuMT" value="4612972969459486606" />
@@ -1169,6 +1228,9 @@
     <property role="EcuMT" value="4612972969459487050" />
     <property role="3GE5qa" value="constraints.relational" />
     <property role="TrG5h" value="RelationalOperator" />
+    <node concept="PrWs8" id="46t5MkZuwy_" role="PrDN$">
+      <ref role="PrY4T" node="46t5MkZsy$k" resolve="IOCRAConstraint" />
+    </node>
   </node>
   <node concept="1TIwiD" id="5MFfD6faVUc">
     <property role="EcuMT" value="6677499667400081036" />
@@ -1198,5 +1260,10 @@
       <ref role="PrY4T" to="tpck:3fifI_xCcJN" resolve="ScopeProvider" />
     </node>
   </node>
+  <node concept="PlHQZ" id="46t5MkZsy$k">
+    <property role="EcuMT" value="4727960632554563860" />
+    <property role="3GE5qa" value="constraints" />
+    <property role="TrG5h" value="IOCRAConstraint" />
+  </node>
 </model>