diff --git a/build.gradle.kts b/build.gradle.kts
index d26acc1d6..69044a37e 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -421,6 +421,7 @@ tasks {
         maxHeapSize = "4G"
 
         excludeModuleMigration("de.itemis.mps.editor.diagram", 0)
+	excludeModuleMigration("jetbrains.mps.baseLanguage.javadoc", 0)
     }
 }
 
diff --git a/code/languages/com.fasten.symo/solutions/com.fasten.symo.hw.sandbox/models/com.fasten.symo.hw.sandbox._010_simple_hw_architecture.mps b/code/languages/com.fasten.symo/solutions/com.fasten.symo.hw.sandbox/models/com.fasten.symo.hw.sandbox._010_simple_hw_architecture.mps
index 4fc115cf2..a806177e2 100644
--- a/code/languages/com.fasten.symo/solutions/com.fasten.symo.hw.sandbox/models/com.fasten.symo.hw.sandbox._010_simple_hw_architecture.mps
+++ b/code/languages/com.fasten.symo/solutions/com.fasten.symo.hw.sandbox/models/com.fasten.symo.hw.sandbox._010_simple_hw_architecture.mps
@@ -89,12 +89,12 @@
       <property role="TrG5h" value="ecu2" />
     </node>
     <node concept="2jnq7J" id="2gpUZARhwa8" role="2jnmDS">
-      <ref role="2jnmXU" node="2gpUZARh4BO" />
-      <ref role="2jnmXW" node="2gpUZARh4BT" />
+      <ref role="2jnmXU" node="2gpUZARh4BO" resolve="ecu1" />
+      <ref role="2jnmXW" node="2gpUZARh4BT" resolve="bus" />
     </node>
     <node concept="2jnq7J" id="2gpUZARhwaa" role="2jnmDS">
-      <ref role="2jnmXU" node="2gpUZARh4C9" />
-      <ref role="2jnmXW" node="2gpUZARh4BT" />
+      <ref role="2jnmXU" node="2gpUZARh4C9" resolve="ecu2" />
+      <ref role="2jnmXW" node="2gpUZARh4BT" resolve="bus" />
     </node>
   </node>
 </model>
diff --git a/code/languages/com.fasten.symo/solutions/com.symo.sysml.ibd.sandbox/models/com.symo.sysml.ibd.sandbox._010_smoke.mps b/code/languages/com.fasten.symo/solutions/com.symo.sysml.ibd.sandbox/models/com.symo.sysml.ibd.sandbox._010_smoke.mps
index 65fbb51e7..73f275a44 100644
--- a/code/languages/com.fasten.symo/solutions/com.symo.sysml.ibd.sandbox/models/com.symo.sysml.ibd.sandbox._010_smoke.mps
+++ b/code/languages/com.fasten.symo/solutions/com.symo.sysml.ibd.sandbox/models/com.symo.sysml.ibd.sandbox._010_smoke.mps
@@ -76,7 +76,7 @@
       <property role="TrG5h" value="Sender" />
       <node concept="3USqFc" id="pk5lVrZWqi" role="3UVs02">
         <property role="TrG5h" value="data" />
-        <ref role="3US7yy" node="pk5lVrZWqd" />
+        <ref role="3US7yy" node="pk5lVrZWqd" resolve="Data" />
       </node>
     </node>
     <node concept="3UUxL_" id="pk5lVrZWqq" role="3UUxLy" />
@@ -84,7 +84,7 @@
       <property role="TrG5h" value="Receiver" />
       <node concept="3USqFc" id="pk5lVrZWqL" role="3UVs00">
         <property role="TrG5h" value="data" />
-        <ref role="3US7yy" node="pk5lVrZWqd" />
+        <ref role="3US7yy" node="pk5lVrZWqd" resolve="Data" />
       </node>
     </node>
     <node concept="3UUxL_" id="pk5lVrZWr9" role="3UUxLy" />
@@ -93,20 +93,20 @@
       <node concept="3UVpuM" id="pk5lVrZWrH" role="3UVWDc">
         <node concept="3UVpuK" id="pk5lVrZWrJ" role="3UVKbZ">
           <property role="TrG5h" value="s" />
-          <ref role="3UVpu6" node="6TLpWSY0gIt" />
+          <ref role="3UVpu6" node="6TLpWSY0gIt" resolve="Sender" />
         </node>
         <node concept="3UVpuK" id="pk5lVrZWrO" role="3UVKbZ">
           <property role="TrG5h" value="r" />
-          <ref role="3UVpu6" node="pk5lVrZWqB" />
+          <ref role="3UVpu6" node="pk5lVrZWqB" resolve="Receiver" />
         </node>
         <node concept="3UVptf" id="pk5lVrZWrW" role="3UVKbZ">
           <node concept="3UVgTP" id="pk5lVrZWs1" role="3UVptc">
-            <ref role="3UVgTb" node="pk5lVrZWrJ" />
-            <ref role="3UVgT4" node="pk5lVrZWqi" />
+            <ref role="3UVgTb" node="pk5lVrZWrJ" resolve="s" />
+            <ref role="3UVgT4" node="pk5lVrZWqi" resolve="data" />
           </node>
           <node concept="3UVgTP" id="pk5lVrZWs3" role="3UVpta">
-            <ref role="3UVgTb" node="pk5lVrZWrO" />
-            <ref role="3UVgT4" node="pk5lVrZWqL" />
+            <ref role="3UVgTb" node="pk5lVrZWrO" resolve="r" />
+            <ref role="3UVgT4" node="pk5lVrZWqL" resolve="data" />
           </node>
         </node>
         <node concept="37mRI7" id="pk5lVrZWs6" role="lGtFl">
diff --git a/code/languages/com.mbeddr.formal.cprover/solutions/test.com.mbeddr.formal.cbmc/test.com.mbeddr.formal.cbmc.msd b/code/languages/com.mbeddr.formal.cprover/solutions/test.com.mbeddr.formal.cbmc/test.com.mbeddr.formal.cbmc.msd
index a22745688..6be245449 100644
--- a/code/languages/com.mbeddr.formal.cprover/solutions/test.com.mbeddr.formal.cbmc/test.com.mbeddr.formal.cbmc.msd
+++ b/code/languages/com.mbeddr.formal.cprover/solutions/test.com.mbeddr.formal.cbmc/test.com.mbeddr.formal.cbmc.msd
@@ -9,6 +9,7 @@
     <facet type="java" compile="mps" classes="mps" ext="no">
       <classes generated="true" path="${module}/classes_gen" />
     </facet>
+    <facet type="tests" />
   </facets>
   <sourcePath />
   <dependencies>
diff --git a/code/languages/com.mbeddr.formal.prism/tests/test.com.mbeddr.formal.prism/models/test.com.mbeddr.formal.prism._010_smoke.mps b/code/languages/com.mbeddr.formal.prism/tests/test.com.mbeddr.formal.prism/models/test.com.mbeddr.formal.prism._010_smoke.mps
index b27723d94..c17f9a295 100644
--- a/code/languages/com.mbeddr.formal.prism/tests/test.com.mbeddr.formal.prism/models/test.com.mbeddr.formal.prism._010_smoke.mps
+++ b/code/languages/com.mbeddr.formal.prism/tests/test.com.mbeddr.formal.prism/models/test.com.mbeddr.formal.prism._010_smoke.mps
@@ -155,7 +155,7 @@
         <node concept="112hEE" id="ZaBFheNc6A" role="112hEJ">
           <node concept="113wzp" id="ZaBFheNc6B" role="113wzu">
             <node concept="112hFX" id="ZaBFheNc72" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="ZaBFheNc78" role="113wz4">
               <property role="2IPVms" value="1" />
@@ -168,7 +168,7 @@
         <node concept="112hEE" id="1rXrB7iRZXF" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iRZXG" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShfw" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShfA" role="113wz4">
               <property role="2IPVms" value="2" />
@@ -183,7 +183,7 @@
             <property role="2IPVms" value="0" />
           </node>
           <node concept="112hFX" id="ZaBFheNc7c" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -191,7 +191,7 @@
         <node concept="112hEE" id="1rXrB7iShgJ" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShgK" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShgL" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShgM" role="113wz4">
               <property role="2IPVms" value="3" />
@@ -204,7 +204,7 @@
         <node concept="112hEE" id="1rXrB7iShgO" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShgP" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShgQ" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShgR" role="113wz4">
               <property role="2IPVms" value="4" />
@@ -219,7 +219,7 @@
             <property role="2IPVms" value="1" />
           </node>
           <node concept="112hFX" id="1rXrB7iShgV" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -227,7 +227,7 @@
         <node concept="112hEE" id="1rXrB7iShhS" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShhT" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShhU" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShhV" role="113wz4">
               <property role="2IPVms" value="5" />
@@ -240,7 +240,7 @@
         <node concept="112hEE" id="1rXrB7iShhX" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShhY" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShhZ" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShi0" role="113wz4">
               <property role="2IPVms" value="6" />
@@ -255,7 +255,7 @@
             <property role="2IPVms" value="2" />
           </node>
           <node concept="112hFX" id="1rXrB7iShi4" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -263,7 +263,7 @@
         <node concept="112hEE" id="1rXrB7iShj3" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShj4" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShj5" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShj6" role="113wz4">
               <property role="2IPVms" value="1" />
@@ -276,7 +276,7 @@
         <node concept="112hEE" id="1rXrB7iShj8" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShj9" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShja" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShjb" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -284,7 +284,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShkr" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShk$" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShkF" role="113wz4">
               <property role="2IPVms" value="1" />
@@ -299,7 +299,7 @@
             <property role="2IPVms" value="3" />
           </node>
           <node concept="112hFX" id="1rXrB7iShjf" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -307,7 +307,7 @@
         <node concept="112hEE" id="1rXrB7iShkI" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShkJ" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShkK" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShkL" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -315,7 +315,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShmt" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShmA" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShmH" role="113wz4">
               <property role="2IPVms" value="2" />
@@ -328,7 +328,7 @@
         <node concept="112hEE" id="1rXrB7iShkN" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShkO" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShkP" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShkQ" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -336,7 +336,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShkR" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShkS" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShkT" role="113wz4">
               <property role="2IPVms" value="3" />
@@ -351,7 +351,7 @@
             <property role="2IPVms" value="4" />
           </node>
           <node concept="112hFX" id="1rXrB7iShkX" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -359,7 +359,7 @@
         <node concept="112hEE" id="1rXrB7iShnk" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShnl" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShnm" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShnn" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -367,7 +367,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShno" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShnp" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShnq" role="113wz4">
               <property role="2IPVms" value="4" />
@@ -380,7 +380,7 @@
         <node concept="112hEE" id="1rXrB7iShns" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShnt" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShnu" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShnv" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -388,7 +388,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShnw" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShnx" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShny" role="113wz4">
               <property role="2IPVms" value="5" />
@@ -403,7 +403,7 @@
             <property role="2IPVms" value="5" />
           </node>
           <node concept="112hFX" id="1rXrB7iShnA" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -411,7 +411,7 @@
         <node concept="112hEE" id="1rXrB7iShpu" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShpv" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShpw" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShpx" role="113wz4">
               <property role="2IPVms" value="2" />
@@ -424,7 +424,7 @@
         <node concept="112hEE" id="1rXrB7iShpA" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iShpB" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShpC" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShpD" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -432,7 +432,7 @@
           </node>
           <node concept="113wzp" id="1rXrB7iShpE" role="113wzu">
             <node concept="112hFX" id="1rXrB7iShpF" role="113wzq">
-              <ref role="112hCK" node="ZaBFheMfar" />
+              <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iShpG" role="113wz4">
               <property role="2IPVms" value="6" />
@@ -447,7 +447,7 @@
             <property role="2IPVms" value="6" />
           </node>
           <node concept="112hFX" id="1rXrB7iShpK" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -455,7 +455,7 @@
         <node concept="112hEE" id="1rXrB7iSySp" role="112hEJ">
           <node concept="113wzp" id="1rXrB7iSySq" role="113wzu">
             <node concept="112hFX" id="1rXrB7iSyUS" role="113wzq">
-              <ref role="112hCK" node="ZaBFheM00U" />
+              <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
             </node>
             <node concept="2IPVmt" id="1rXrB7iSyUY" role="113wz4">
               <property role="2IPVms" value="7" />
@@ -467,7 +467,7 @@
             <property role="2IPVms" value="7" />
           </node>
           <node concept="112hFX" id="1rXrB7iSyUB" role="2H9Iav">
-            <ref role="112hCK" node="ZaBFheM00U" />
+            <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
           </node>
         </node>
       </node>
@@ -476,7 +476,7 @@
   </node>
   <node concept="2oyOwK" id="1xpXAu0Q0D5">
     <property role="TrG5h" value="_010_die_spec" />
-    <ref role="2oGCQt" node="ZaBFheK9QZ" />
+    <ref role="2oGCQt" node="ZaBFheK9QZ" resolve="_010_die" />
     <node concept="2ozijr" id="1xpXAu0Q0D6" role="2oyNpA">
       <property role="TrG5h" value="x" />
       <node concept="2owvKH" id="1xpXAu0QqIZ" role="112KhV" />
@@ -491,7 +491,7 @@
           <node concept="2oJwby" id="1xpXAu0X$cy" role="32OYtT">
             <node concept="110AQS" id="1xpXAu0X$cz" role="2H9Iav">
               <node concept="112hFX" id="1xpXAu0X$c$" role="2H9Iav">
-                <ref role="112hCK" node="ZaBFheM00U" />
+                <ref role="112hCK" node="ZaBFheM00U" resolve="s" />
               </node>
               <node concept="2IPVmt" id="1xpXAu0X$c_" role="2H9Ial">
                 <property role="2IPVms" value="7" />
@@ -499,10 +499,10 @@
             </node>
             <node concept="110AQS" id="1xpXAu0X$cA" role="2H9Ial">
               <node concept="112hFX" id="1xpXAu0X$cB" role="2H9Ial">
-                <ref role="112hCK" node="1xpXAu0Q0D6" />
+                <ref role="112hCK" node="1xpXAu0Q0D6" resolve="x" />
               </node>
               <node concept="112hFX" id="1xpXAu0X$cC" role="2H9Iav">
-                <ref role="112hCK" node="ZaBFheMfar" />
+                <ref role="112hCK" node="ZaBFheMfar" resolve="d" />
               </node>
             </node>
           </node>
diff --git a/code/languages/com.mbeddr.formal.repo_admin/solutions/com.fasten.meta.all/models/com.fasten.meta.all.scripts.mps b/code/languages/com.mbeddr.formal.repo_admin/solutions/com.fasten.meta.all/models/com.fasten.meta.all.scripts.mps
index a256e1f87..4db261ce6 100644
--- a/code/languages/com.mbeddr.formal.repo_admin/solutions/com.fasten.meta.all/models/com.fasten.meta.all.scripts.mps
+++ b/code/languages/com.mbeddr.formal.repo_admin/solutions/com.fasten.meta.all/models/com.fasten.meta.all.scripts.mps
@@ -125,7 +125,9 @@
     </language>
     <language id="760a0a8c-eabb-4521-8bfd-65db761a9ba3" name="jetbrains.mps.baseLanguage.logging">
       <concept id="6332851714983831325" name="jetbrains.mps.baseLanguage.logging.structure.MsgStatement" flags="ng" index="2xdQw9">
+        <property id="6332851714983843871" name="severity" index="2xdLsb" />
         <child id="5721587534047265374" name="message" index="9lYJi" />
+        <child id="5721587534047265375" name="throwable" index="9lYJj" />
       </concept>
     </language>
     <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
@@ -158,6 +160,7 @@
       <concept id="1203518072036" name="jetbrains.mps.baseLanguage.collections.structure.SmartClosureParameterDeclaration" flags="ig" index="Rh6nW" />
       <concept id="1160600644654" name="jetbrains.mps.baseLanguage.collections.structure.ListCreatorWithInit" flags="nn" index="Tc6Ow" />
       <concept id="1160612413312" name="jetbrains.mps.baseLanguage.collections.structure.AddElementOperation" flags="nn" index="TSZUe" />
+      <concept id="1162935959151" name="jetbrains.mps.baseLanguage.collections.structure.GetSizeOperation" flags="nn" index="34oBXx" />
     </language>
     <language id="de1ad86d-6e50-4a02-b306-d4d17f64c375" name="jetbrains.mps.console.base">
       <concept id="752693057587755272" name="jetbrains.mps.console.base.structure.ProjectExpression" flags="ng" index="o6qdh" />
@@ -303,6 +306,15 @@
               </node>
             </node>
             <node concept="3clFbS" id="6r0uA12M7jh" role="1zc67A">
+              <node concept="2xdQw9" id="1k6eCQni1xz" role="3cqZAp">
+                <property role="2xdLsb" value="gZ5fh_4/error" />
+                <node concept="Xl_RD" id="1k6eCQni1x_" role="9lYJi">
+                  <property role="Xl_RC" value="Exception occurred while building fasten.all super-project" />
+                </node>
+                <node concept="37vLTw" id="1k6eCQni1zu" role="9lYJj">
+                  <ref role="3cqZAo" node="6r0uA12M7je" resolve="e" />
+                </node>
+              </node>
               <node concept="3clFbF" id="6r0uA12M7ji" role="3cqZAp">
                 <node concept="2OqwBi" id="6r0uA12M7jj" role="3clFbG">
                   <node concept="37vLTw" id="6r0uA12M7jk" role="2Oq$k0">
@@ -402,6 +414,21 @@
                     </node>
                   </node>
                 </node>
+                <node concept="2xdQw9" id="1k6eCQnhQNV" role="3cqZAp">
+                  <node concept="3cpWs3" id="1k6eCQnhREC" role="9lYJi">
+                    <node concept="2OqwBi" id="1k6eCQnhRRh" role="3uHU7w">
+                      <node concept="37vLTw" id="1k6eCQnhRFq" role="2Oq$k0">
+                        <ref role="3cqZAo" node="yuql$cyaeH" resolve="moduleFile" />
+                      </node>
+                      <node concept="liA8E" id="1k6eCQnhSoq" role="2OqNvi">
+                        <ref role="37wK5l" to="guwi:~File.getAbsolutePath()" resolve="getAbsolutePath" />
+                      </node>
+                    </node>
+                    <node concept="Xl_RD" id="1k6eCQnhQNX" role="3uHU7B">
+                      <property role="Xl_RC" value="reading module file: " />
+                    </node>
+                  </node>
+                </node>
                 <node concept="3clFbJ" id="yuql$cyadn" role="3cqZAp">
                   <node concept="2OqwBi" id="yuql$cydO6" role="3clFbw">
                     <node concept="37vLTw" id="yuql$cyd$S" role="2Oq$k0">
@@ -666,8 +693,21 @@
                     <ref role="37wK5l" to="guwi:~File.getAbsolutePath()" resolve="getAbsolutePath" />
                   </node>
                 </node>
-                <node concept="Xl_RD" id="1y75PbziWYc" role="3uHU7B">
-                  <property role="Xl_RC" value="wrote lines in " />
+                <node concept="3cpWs3" id="1k6eCQnhZm1" role="3uHU7B">
+                  <node concept="Xl_RD" id="1k6eCQnhZo$" role="3uHU7w">
+                    <property role="Xl_RC" value=" lines in " />
+                  </node>
+                  <node concept="3cpWs3" id="1k6eCQnhWoT" role="3uHU7B">
+                    <node concept="Xl_RD" id="1y75PbziWYc" role="3uHU7B">
+                      <property role="Xl_RC" value="wrote " />
+                    </node>
+                    <node concept="2OqwBi" id="1k6eCQnhX1p" role="3uHU7w">
+                      <node concept="37vLTw" id="1k6eCQnhWpG" role="2Oq$k0">
+                        <ref role="3cqZAo" node="yuql$cxEkm" resolve="lines" />
+                      </node>
+                      <node concept="34oBXx" id="1k6eCQnhYzI" role="2OqNvi" />
+                    </node>
+                  </node>
                 </node>
               </node>
             </node>
diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.fasten.safety.ft/models/com.fasten.safety.ft.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.fasten.safety.ft/models/com.fasten.safety.ft.editor.mps
index b7749ee7c..cd2953845 100644
--- a/code/languages/com.mbeddr.formal.safety/languages/com.fasten.safety.ft/models/com.fasten.safety.ft.editor.mps
+++ b/code/languages/com.mbeddr.formal.safety/languages/com.fasten.safety.ft/models/com.fasten.safety.ft.editor.mps
@@ -408,9 +408,6 @@
         <child id="5855146979801445196" name="width" index="2JxpDF" />
         <child id="5855146979801445211" name="height" index="2JxpDW" />
       </concept>
-      <concept id="8433227566816385664" name="de.itemis.mps.editor.diagram.structure.ILayoutAlgorithm" flags="ng" index="35SPa">
-        <child id="2064429317493348220" name="config" index="3pGojU" />
-      </concept>
       <concept id="6554619383003875357" name="de.itemis.mps.editor.diagram.structure.InlineEditorComponent" flags="ig" index="238au4" />
       <concept id="8433227566817223068" name="de.itemis.mps.editor.diagram.structure.LayeredLayoutAlgorithm" flags="ng" index="39fpm">
         <property id="7623784619795245948" name="direction" index="1NdBj4" />
@@ -462,15 +459,6 @@
       <concept id="5383048119156619323" name="de.itemis.mps.editor.diagram.structure.IDiagramElementsProvider" flags="ng" index="HB_m5">
         <child id="3155126767688717334" name="contentList" index="aCds2" />
       </concept>
-      <concept id="5878290447138467534" name="de.itemis.mps.editor.diagram.structure.Padding" flags="ng" index="POkNa">
-        <property id="5878290447138468454" name="top" index="POl1y" />
-        <property id="5878290447138468820" name="right" index="POl7g" />
-        <property id="5878290447138469609" name="bottom" index="POljH" />
-        <property id="5878290447138469821" name="left" index="POlmT" />
-      </concept>
-      <concept id="5878290447138443303" name="de.itemis.mps.editor.diagram.structure.ContentAlignment" flags="ng" index="POr8z">
-        <property id="5878290447138443694" name="alignment" index="POreE" />
-      </concept>
       <concept id="5112292084089908370" name="de.itemis.mps.editor.diagram.structure.EditorContextExpression" flags="ng" index="UMIS2" />
       <concept id="6237710625713195816" name="de.itemis.mps.editor.diagram.structure.CellModel_DiagramNode" flags="ng" index="2ZK4vF">
         <child id="7464726264117682823" name="shape" index="2xQQDV" />
@@ -483,18 +471,6 @@
       <concept id="6237710625713942002" name="de.itemis.mps.editor.diagram.structure.Content_BLQuery" flags="ig" index="2ZMM4L" />
       <concept id="6237710625713964946" name="de.itemis.mps.editor.diagram.structure.Parameter_Node" flags="ng" index="2ZN8Hh" />
       <concept id="5468226901223973329" name="de.itemis.mps.editor.diagram.structure.PortObject" flags="ng" index="15kUEO" />
-      <concept id="3662141892379115490" name="de.itemis.mps.editor.diagram.structure.Margin" flags="ng" index="36xZl7">
-        <property id="3662141892379115493" name="bottom" index="36xZl0" />
-        <property id="3662141892379115492" name="right" index="36xZl1" />
-        <property id="3662141892379115494" name="left" index="36xZl3" />
-        <property id="3662141892379115491" name="top" index="36xZl6" />
-      </concept>
-      <concept id="3662141892377043655" name="de.itemis.mps.editor.diagram.structure.ISupportTopdownPacking" flags="ng" index="36TQxy">
-        <property id="3662141892371757000" name="topdownHierarchicalNodeAspectRatio" index="31dVPH" />
-        <property id="3662141892371761113" name="topdownScaleFactor" index="31dWPW" />
-        <property id="3662141892374571168" name="topdownNodeType" index="36KE85" />
-        <property id="3662141892374569619" name="topdownHierarchicalNodeWidth" index="36KEwQ" />
-      </concept>
       <concept id="5051221038171022699" name="de.itemis.mps.editor.diagram.structure.ShadeColor" flags="lg" index="38c6YI" />
       <concept id="4277219764978107440" name="de.itemis.mps.editor.diagram.structure.SNodeConncetionType_toNode" flags="ng" index="3m_Ry6" />
       <concept id="4277219764978107398" name="de.itemis.mps.editor.diagram.structure.SNodeConncetionType_fromNode" flags="ng" index="3m_RyK" />
@@ -526,59 +502,6 @@
       </concept>
       <concept id="8637411062062623445" name="de.itemis.mps.editor.diagram.structure.Parameter_PaletteFolder_Concept" flags="ng" index="1yATlc" />
       <concept id="6987730699889040828" name="de.itemis.mps.editor.diagram.structure.LineColor" flags="lg" index="3C0NmK" />
-      <concept id="3333801137936756207" name="de.itemis.mps.editor.diagram.structure.LayeredLayoutConfig" flags="ng" index="3GLQun">
-        <property id="3662141892379183286" name="highDegreeNodeMaximumTreeHeight" index="36x08j" />
-        <property id="3662141892379184421" name="highDegreeNodeThreshold" index="36x0u0" />
-        <property id="3662141892379181918" name="hierarchicalSweepiness" index="36x0BV" />
-        <property id="3662141892379181279" name="greedySwitchCrossingminimizationHierarchical" index="36x0DU" />
-        <property id="3662141892379187702" name="improveCuts" index="36x1dj" />
-        <property id="3662141892379188269" name="improveWrappedEdges" index="36x1q8" />
-        <property id="3662141892379186382" name="horizontalSpacingBetweenLabelAndPort" index="36x1TF" />
-        <property id="3662141892379191931" name="labelSpacing" index="36x23u" />
-        <property id="3662141892379192633" name="layerBound" index="36x2us" />
-        <property id="3662141892379191100" name="labelNodeSpacing" index="36x2Qp" />
-        <property id="3662141892379194849" name="linearSegmentDeflectionDampening" index="36x3X4" />
-        <property id="3662141892379204315" name="maxNodePromotionIterations" index="36x51Y" />
-        <property id="3662141892379206070" name="mergeHierarchyCrossingEdges" index="36x6Gj" />
-        <property id="3662141892379207456" name="msdFreedom" index="36x6Q5" />
-        <property id="3662141892379211526" name="nodeNodeBetweenLayersSpacing" index="36x7Qz" />
-        <property id="3662141892379155187" name="crossingCounterPortInfluence" index="36x91m" />
-        <property id="3662141892379153202" name="correctionFactorForWrapping" index="36x9An" />
-        <property id="3662141892379154155" name="crossingCounterNodeInfluence" index="36x9Le" />
-        <property id="3662141892379160447" name="direction" index="36xanq" />
-        <property id="3662141892379162028" name="multiEdgeDistancePenalty" index="36xbW9" />
-        <property id="3662141892379167712" name="edgeNodeBetweenLayersSpacing" index="36xc55" />
-        <property id="3662141892379166982" name="edgeLabelSpacing" index="36xcez" />
-        <property id="3662141892379164867" name="edgeEdgeBetweenLayersSpacing" index="36xcDA" />
-        <property id="3662141892379171281" name="edgeSpacing" index="36xddO" />
-        <property id="3662141892379171857" name="edgeThickness" index="36xdqO" />
-        <property id="3662141892379168833" name="edgeNodeSpacing" index="36xdF$" />
-        <property id="3662141892379180082" name="greedySwitchCrossingminimization" index="36xfqn" />
-        <property id="3662141892379178639" name="greedySwitchActivationThreshold" index="36xfKE" />
-        <property id="3662141892379216113" name="nodeSelfLoopSpacing" index="36xo9k" />
-        <property id="3662141892379216986" name="nodeSpacing" index="36xorZ" />
-        <property id="3662141892379221784" name="randomizationSeed" index="36xpmX" />
-        <property id="3662141892379218932" name="portSpacing" index="36xp_h" />
-        <property id="3662141892379224606" name="slopedEdgeZoneWidth" index="36xq2V" />
-        <property id="3662141892379225514" name="sloppySplineLayerSpacingFactor" index="36xqsf" />
-        <property id="3662141892379223673" name="separateConnectedComponents" index="36xqNs" />
-        <property id="3662141892379228412" name="thoroughness" index="36xr9p" />
-        <property id="3662141892379226684" name="spacingBaseValue" index="36xryp" />
-        <property id="3662141892379230763" name="upperBoundOnWidthMinWidthLayerer" index="36xsye" />
-        <property id="3662141892379231963" name="upperLayerEstimationScalingFactorMinWidthLayerer" index="36xsLY" />
-        <property id="3662141892379238267" name="verticalSpacingBetweenLabelAndPort" index="36xtnu" />
-        <property id="3662141892379139136" name="additionalWrappedEdgesSpacing" index="36xPr_" />
-        <property id="3662141892379140237" name="aspectRatio" index="36xQCC" />
-        <property id="3662141892379147547" name="considerModelOrderStrategy" index="36xRuY" />
-        <property id="3662141892379145171" name="commentNodeSpacing" index="36xR_Q" />
-        <property id="3662141892379144303" name="commentCommentSpacing" index="36xRFa" />
-        <property id="3662141892379145832" name="componentsSpacing" index="36xRNd" />
-        <property id="2064429317495021368" name="subdiagramDirection" index="3p_KMY" />
-        <child id="3662141892379210077" name="nodeLabelPadding" index="36x7JS" />
-        <child id="3662141892379152132" name="contentAlignment" index="36x8mx" />
-        <child id="3662141892379217652" name="padding" index="36xohh" />
-        <child id="3662141892379113988" name="additionalPortSpace" index="36xZ2x" />
-      </concept>
       <concept id="8587703283519920118" name="de.itemis.mps.editor.diagram.structure.ThisNodeExpression" flags="ng" index="1Pxb5l" />
       <concept id="8587703283523590697" name="de.itemis.mps.editor.diagram.structure.ConnectionEndpoint" flags="ng" index="1PNbMa">
         <child id="9064581101900868073" name="target" index="ljJml" />
@@ -7237,83 +7160,6 @@
       </node>
       <node concept="39fpm" id="5rwT_JnuRbZ" role="35U2g">
         <property role="1NdBj4" value="6Bd7VwqYQBY/DOWN" />
-        <node concept="3GLQun" id="3M596RFvBLe" role="3pGojU">
-          <property role="36xPr_" value="10.0" />
-          <property role="36xQCC" value="1.6" />
-          <property role="36xRFa" value="10.0" />
-          <property role="36xR_Q" value="10.0" />
-          <property role="36xRNd" value="20.0" />
-          <property role="36xRuY" value="3biyEnOlw4F/PREFER_NODES" />
-          <property role="36x9An" value="1.0" />
-          <property role="36x9Le" value="0.0" />
-          <property role="36x91m" value="0.0" />
-          <property role="36xbW9" value="2.0" />
-          <property role="36xcDA" value="10.0" />
-          <property role="36xcez" value="2.0" />
-          <property role="36xc55" value="20.0" />
-          <property role="36xdF$" value="10.0" />
-          <property role="36xddO" value="10.0" />
-          <property role="36xdqO" value="1.0" />
-          <property role="36xfKE" value="40" />
-          <property role="36xfqn" value="3biyEnOlBXf/TWO_SIDED" />
-          <property role="36x0DU" value="3biyEnOlBXk/OFF" />
-          <property role="36x0BV" value="0.1" />
-          <property role="36x08j" value="5" />
-          <property role="36x0u0" value="16" />
-          <property role="36x1TF" value="1.0" />
-          <property role="36x1dj" value="true" />
-          <property role="36x1q8" value="true" />
-          <property role="36x2Qp" value="5.0" />
-          <property role="36x23u" value="0.0" />
-          <property role="36x2us" value="2147483647" />
-          <property role="36x3X4" value="0.3" />
-          <property role="36x51Y" value="0" />
-          <property role="36x6Gj" value="true" />
-          <property role="36x6Q5" value="1" />
-          <property role="36x7Qz" value="40.0" />
-          <property role="36xo9k" value="10.0" />
-          <property role="36xorZ" value="40.0" />
-          <property role="36xp_h" value="5.0" />
-          <property role="36xpmX" value="1" />
-          <property role="36xqNs" value="true" />
-          <property role="36xq2V" value="2.0" />
-          <property role="36xqsf" value="0.2" />
-          <property role="36xr9p" value="7" />
-          <property role="31dVPH" value="1.414" />
-          <property role="36KEwQ" value="15.0" />
-          <property role="36KE85" value="qwNnoEIHRM/HIERARCHICAL_NODE" />
-          <property role="31dWPW" value="1.0" />
-          <property role="36xsye" value="4" />
-          <property role="36xsLY" value="2" />
-          <property role="36xtnu" value="1.0" />
-          <property role="3p_KMY" value="6Bd7VwqYQBY/DOWN" />
-          <property role="36xanq" value="6Bd7VwqYQBY/DOWN" />
-          <property role="36xryp" value="40.0" />
-          <node concept="36xZl7" id="3M596RFvBLf" role="36xZ2x">
-            <property role="36xZl6" value="0.0" />
-            <property role="36xZl1" value="0.0" />
-            <property role="36xZl0" value="0.0" />
-            <property role="36xZl3" value="0.0" />
-          </node>
-          <node concept="POr8z" id="3M596RFvBLg" role="36x8mx">
-            <property role="POreE" value="56jSwh$g$O2/V_TOP" />
-          </node>
-          <node concept="POr8z" id="3M596RFvBLh" role="36x8mx">
-            <property role="POreE" value="56jSwh$g_03/H_LEFT" />
-          </node>
-          <node concept="POkNa" id="3M596RFvBLi" role="36x7JS">
-            <property role="POl1y" value="5.0" />
-            <property role="POl7g" value="5.0" />
-            <property role="POljH" value="5.0" />
-            <property role="POlmT" value="5.0" />
-          </node>
-          <node concept="POkNa" id="3M596RFvBLj" role="36xohh">
-            <property role="POl1y" value="12.0" />
-            <property role="POl7g" value="12.0" />
-            <property role="POljH" value="12.0" />
-            <property role="POlmT" value="12.0" />
-          </node>
-        </node>
       </node>
       <node concept="3mAFYk" id="5rwT_JnwhXM" role="1xLlFP">
         <property role="3m_KjL" value="Edge" />
diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps
index 92ee37935..b3573fede 100644
--- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps
+++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps
@@ -540,9 +540,6 @@
       </concept>
     </language>
     <language id="fa13cc63-c476-4d46-9c96-d53670abe7bc" name="de.itemis.mps.editor.diagram">
-      <concept id="8433227566816385664" name="de.itemis.mps.editor.diagram.structure.ILayoutAlgorithm" flags="ng" index="35SPa">
-        <child id="2064429317493348220" name="config" index="3pGojU" />
-      </concept>
       <concept id="6554619383003875357" name="de.itemis.mps.editor.diagram.structure.InlineEditorComponent" flags="ig" index="238au4" />
       <concept id="8433227566817223068" name="de.itemis.mps.editor.diagram.structure.LayeredLayoutAlgorithm" flags="ng" index="39fpm">
         <property id="7623784619795245948" name="direction" index="1NdBj4" />
@@ -587,15 +584,6 @@
         <child id="3155126767688717334" name="contentList" index="aCds2" />
       </concept>
       <concept id="621570459751009499" name="de.itemis.mps.editor.diagram.structure.EdgeEditor_CanSplit" flags="ig" index="KXoZh" />
-      <concept id="5878290447138467534" name="de.itemis.mps.editor.diagram.structure.Padding" flags="ng" index="POkNa">
-        <property id="5878290447138468454" name="top" index="POl1y" />
-        <property id="5878290447138468820" name="right" index="POl7g" />
-        <property id="5878290447138469609" name="bottom" index="POljH" />
-        <property id="5878290447138469821" name="left" index="POlmT" />
-      </concept>
-      <concept id="5878290447138443303" name="de.itemis.mps.editor.diagram.structure.ContentAlignment" flags="ng" index="POr8z">
-        <property id="5878290447138443694" name="alignment" index="POreE" />
-      </concept>
       <concept id="5112292084089908370" name="de.itemis.mps.editor.diagram.structure.EditorContextExpression" flags="ng" index="UMIS2" />
       <concept id="6237710625713195816" name="de.itemis.mps.editor.diagram.structure.CellModel_DiagramNode" flags="ng" index="2ZK4vF">
         <child id="7464726264117682823" name="shape" index="2xQQDV" />
@@ -606,18 +594,6 @@
       <concept id="6237710625713831199" name="de.itemis.mps.editor.diagram.structure.CellModel_DiagramConnector" flags="ng" index="2ZMJ7s" />
       <concept id="6237710625713942002" name="de.itemis.mps.editor.diagram.structure.Content_BLQuery" flags="ig" index="2ZMM4L" />
       <concept id="6237710625713964946" name="de.itemis.mps.editor.diagram.structure.Parameter_Node" flags="ng" index="2ZN8Hh" />
-      <concept id="3662141892379115490" name="de.itemis.mps.editor.diagram.structure.Margin" flags="ng" index="36xZl7">
-        <property id="3662141892379115493" name="bottom" index="36xZl0" />
-        <property id="3662141892379115492" name="right" index="36xZl1" />
-        <property id="3662141892379115494" name="left" index="36xZl3" />
-        <property id="3662141892379115491" name="top" index="36xZl6" />
-      </concept>
-      <concept id="3662141892377043655" name="de.itemis.mps.editor.diagram.structure.ISupportTopdownPacking" flags="ng" index="36TQxy">
-        <property id="3662141892371757000" name="topdownHierarchicalNodeAspectRatio" index="31dVPH" />
-        <property id="3662141892371761113" name="topdownScaleFactor" index="31dWPW" />
-        <property id="3662141892374571168" name="topdownNodeType" index="36KE85" />
-        <property id="3662141892374569619" name="topdownHierarchicalNodeWidth" index="36KEwQ" />
-      </concept>
       <concept id="5051221038171022699" name="de.itemis.mps.editor.diagram.structure.ShadeColor" flags="lg" index="38c6YI" />
       <concept id="3454709602156468860" name="de.itemis.mps.editor.diagram.structure.ShapeParameterDeclaration" flags="ng" index="1xmO9C">
         <child id="3454709602156468949" name="type" index="1xmOb1" />
@@ -628,60 +604,6 @@
       <concept id="8637411062076624999" name="de.itemis.mps.editor.diagram.structure.Function_ConnectionTypes" flags="ig" index="1xLmZY" />
       <concept id="8637411062062623445" name="de.itemis.mps.editor.diagram.structure.Parameter_PaletteFolder_Concept" flags="ng" index="1yATlc" />
       <concept id="8637411062062430894" name="de.itemis.mps.editor.diagram.structure.Function_PaletteFolder" flags="ig" index="1yB8kR" />
-      <concept id="3333801137936756207" name="de.itemis.mps.editor.diagram.structure.LayeredLayoutConfig" flags="ng" index="3GLQun">
-        <property id="3662141892379183286" name="highDegreeNodeMaximumTreeHeight" index="36x08j" />
-        <property id="3662141892379184421" name="highDegreeNodeThreshold" index="36x0u0" />
-        <property id="3662141892379181918" name="hierarchicalSweepiness" index="36x0BV" />
-        <property id="3662141892379181279" name="greedySwitchCrossingminimizationHierarchical" index="36x0DU" />
-        <property id="3662141892379187702" name="improveCuts" index="36x1dj" />
-        <property id="3662141892379188269" name="improveWrappedEdges" index="36x1q8" />
-        <property id="3662141892379186382" name="horizontalSpacingBetweenLabelAndPort" index="36x1TF" />
-        <property id="3662141892379191931" name="labelSpacing" index="36x23u" />
-        <property id="3662141892379192633" name="layerBound" index="36x2us" />
-        <property id="3662141892379191100" name="labelNodeSpacing" index="36x2Qp" />
-        <property id="3662141892379194849" name="linearSegmentDeflectionDampening" index="36x3X4" />
-        <property id="3662141892379204315" name="maxNodePromotionIterations" index="36x51Y" />
-        <property id="3662141892379206070" name="mergeHierarchyCrossingEdges" index="36x6Gj" />
-        <property id="3662141892379207456" name="msdFreedom" index="36x6Q5" />
-        <property id="3662141892379213488" name="nodePlacementStrategy" index="36x7gl" />
-        <property id="3662141892379211526" name="nodeNodeBetweenLayersSpacing" index="36x7Qz" />
-        <property id="3662141892379155187" name="crossingCounterPortInfluence" index="36x91m" />
-        <property id="3662141892379153202" name="correctionFactorForWrapping" index="36x9An" />
-        <property id="3662141892379154155" name="crossingCounterNodeInfluence" index="36x9Le" />
-        <property id="3662141892379160447" name="direction" index="36xanq" />
-        <property id="3662141892379162028" name="multiEdgeDistancePenalty" index="36xbW9" />
-        <property id="3662141892379167712" name="edgeNodeBetweenLayersSpacing" index="36xc55" />
-        <property id="3662141892379166982" name="edgeLabelSpacing" index="36xcez" />
-        <property id="3662141892379164867" name="edgeEdgeBetweenLayersSpacing" index="36xcDA" />
-        <property id="3662141892379171281" name="edgeSpacing" index="36xddO" />
-        <property id="3662141892379171857" name="edgeThickness" index="36xdqO" />
-        <property id="3662141892379168833" name="edgeNodeSpacing" index="36xdF$" />
-        <property id="3662141892379180082" name="greedySwitchCrossingminimization" index="36xfqn" />
-        <property id="3662141892379178639" name="greedySwitchActivationThreshold" index="36xfKE" />
-        <property id="3662141892379216113" name="nodeSelfLoopSpacing" index="36xo9k" />
-        <property id="3662141892379216986" name="nodeSpacing" index="36xorZ" />
-        <property id="3662141892379221784" name="randomizationSeed" index="36xpmX" />
-        <property id="3662141892379218932" name="portSpacing" index="36xp_h" />
-        <property id="3662141892379224606" name="slopedEdgeZoneWidth" index="36xq2V" />
-        <property id="3662141892379225514" name="sloppySplineLayerSpacingFactor" index="36xqsf" />
-        <property id="3662141892379223673" name="separateConnectedComponents" index="36xqNs" />
-        <property id="3662141892379228412" name="thoroughness" index="36xr9p" />
-        <property id="3662141892379226684" name="spacingBaseValue" index="36xryp" />
-        <property id="3662141892379230763" name="upperBoundOnWidthMinWidthLayerer" index="36xsye" />
-        <property id="3662141892379231963" name="upperLayerEstimationScalingFactorMinWidthLayerer" index="36xsLY" />
-        <property id="3662141892379238267" name="verticalSpacingBetweenLabelAndPort" index="36xtnu" />
-        <property id="3662141892379139136" name="additionalWrappedEdgesSpacing" index="36xPr_" />
-        <property id="3662141892379140237" name="aspectRatio" index="36xQCC" />
-        <property id="3662141892379147547" name="considerModelOrderStrategy" index="36xRuY" />
-        <property id="3662141892379145171" name="commentNodeSpacing" index="36xR_Q" />
-        <property id="3662141892379144303" name="commentCommentSpacing" index="36xRFa" />
-        <property id="3662141892379145832" name="componentsSpacing" index="36xRNd" />
-        <property id="2064429317495021368" name="subdiagramDirection" index="3p_KMY" />
-        <child id="3662141892379210077" name="nodeLabelPadding" index="36x7JS" />
-        <child id="3662141892379152132" name="contentAlignment" index="36x8mx" />
-        <child id="3662141892379217652" name="padding" index="36xohh" />
-        <child id="3662141892379113988" name="additionalPortSpace" index="36xZ2x" />
-      </concept>
       <concept id="3457085882768508785" name="de.itemis.mps.editor.diagram.structure.CustomDiagramButtonConfig" flags="ng" index="1J_kSU">
         <child id="8146470885692384072" name="vertex" index="2zNVtj" />
         <child id="8146470885735904427" name="edge" index="2$lU2K" />
@@ -2951,84 +2873,6 @@
       </node>
       <node concept="39fpm" id="42InK5baDIm" role="35U2g">
         <property role="1NdBj4" value="6Bd7VwqYQBY/DOWN" />
-        <node concept="3GLQun" id="5RDzpIVUtj1" role="3pGojU">
-          <property role="36xPr_" value="10.0" />
-          <property role="36xQCC" value="1.6" />
-          <property role="36xRFa" value="10.0" />
-          <property role="36xR_Q" value="10.0" />
-          <property role="36xRNd" value="40.0" />
-          <property role="36xRuY" value="3biyEnOlw4v/NONE" />
-          <property role="36x9An" value="1.0" />
-          <property role="36x9Le" value="0.0" />
-          <property role="36x91m" value="0.0" />
-          <property role="36xbW9" value="2.0" />
-          <property role="36xcDA" value="40.0" />
-          <property role="36xcez" value="2.0" />
-          <property role="36xc55" value="20.0" />
-          <property role="36xdF$" value="30.0" />
-          <property role="36xddO" value="20.0" />
-          <property role="36xdqO" value="1.0" />
-          <property role="36xfKE" value="40" />
-          <property role="36xfqn" value="3biyEnOlBXf/TWO_SIDED" />
-          <property role="36x0DU" value="3biyEnOlBXk/OFF" />
-          <property role="36x0BV" value="0.1" />
-          <property role="36x08j" value="5" />
-          <property role="36x0u0" value="16" />
-          <property role="36x1TF" value="1.0" />
-          <property role="36x1dj" value="true" />
-          <property role="36x1q8" value="true" />
-          <property role="36x2Qp" value="5.0" />
-          <property role="36x23u" value="0.0" />
-          <property role="36x2us" value="2147483647" />
-          <property role="36x3X4" value="0.3" />
-          <property role="36x51Y" value="0" />
-          <property role="36x6Gj" value="true" />
-          <property role="36x6Q5" value="1" />
-          <property role="36x7Qz" value="40.0" />
-          <property role="36xo9k" value="10.0" />
-          <property role="36xorZ" value="40.0" />
-          <property role="36xp_h" value="10.0" />
-          <property role="36xpmX" value="1" />
-          <property role="36xqNs" value="true" />
-          <property role="36xq2V" value="2.0" />
-          <property role="36xqsf" value="0.2" />
-          <property role="36xr9p" value="7" />
-          <property role="31dVPH" value="1.414" />
-          <property role="36KEwQ" value="150.0" />
-          <property role="36KE85" value="qwNnoEIHRQ/ROOT_NODE" />
-          <property role="31dWPW" value="1.0" />
-          <property role="36xsye" value="4" />
-          <property role="36xsLY" value="2" />
-          <property role="36xtnu" value="1.0" />
-          <property role="36xryp" value="40.0" />
-          <property role="36x7gl" value="3biyEnOlKd8/NETWORK_SIMPLEX" />
-          <property role="3p_KMY" value="6Bd7VwqYQBY/DOWN" />
-          <property role="36xanq" value="6Bd7VwqYQBY/DOWN" />
-          <node concept="36xZl7" id="5RDzpIVUtj2" role="36xZ2x">
-            <property role="36xZl6" value="0.0" />
-            <property role="36xZl1" value="0.0" />
-            <property role="36xZl0" value="0.0" />
-            <property role="36xZl3" value="0.0" />
-          </node>
-          <node concept="POr8z" id="5RDzpIVUtj3" role="36x8mx">
-            <property role="POreE" value="56jSwh$g$O2/V_TOP" />
-          </node>
-          <node concept="POr8z" id="5RDzpIVUtj4" role="36x8mx">
-            <property role="POreE" value="56jSwh$g_03/H_LEFT" />
-          </node>
-          <node concept="POkNa" id="5RDzpIVUtj5" role="36x7JS">
-            <property role="POl1y" value="5.0" />
-            <property role="POl7g" value="5.0" />
-            <property role="POljH" value="5.0" />
-            <property role="POlmT" value="5.0" />
-          </node>
-          <node concept="POkNa" id="5RDzpIVUtj6" role="36xohh">
-            <property role="POl1y" value="12.0" />
-            <property role="POl7g" value="12.0" />
-            <property role="POljH" value="12.0" />
-            <property role="POlmT" value="12.0" />
-          </node>
-        </node>
       </node>
       <node concept="1J_kSU" id="5Imyhiim4le" role="3sAl1G">
         <node concept="pkWqu" id="5Imyhiim4lf" role="1J_oW_">
diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
index 4cc04d75a..89a54fc9b 100644
--- a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
+++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
@@ -368,6 +368,21 @@
         </node>
       </node>
     </node>
+    <node concept="398rNT" id="1k6eCQnEQWe" role="1l3spd">
+      <property role="TrG5h" value="fasten.symo.code" />
+      <node concept="398BVA" id="1k6eCQnEQWf" role="398pKh">
+        <ref role="398BVh" node="42jqVeFkUG2" resolve="mbeddr.formal.home" />
+        <node concept="2Ry0Ak" id="1k6eCQnEQWg" role="iGT6I">
+          <property role="2Ry0Am" value="code" />
+          <node concept="2Ry0Ak" id="1k6eCQnEQWh" role="2Ry0An">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnERlb" role="2Ry0An">
+              <property role="2Ry0Am" value="com.fasten.symo" />
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
     <node concept="398rNT" id="6mm$FLYQyYs" role="1l3spd">
       <property role="TrG5h" value="mbeddr.formal.nusmv.code" />
       <node concept="398BVA" id="4MDOjos4ufk" role="398pKh">
@@ -413,6 +428,36 @@
         </node>
       </node>
     </node>
+    <node concept="398rNT" id="1k6eCQnp9eV" role="1l3spd">
+      <property role="TrG5h" value="mbeddr.formal.prism.code" />
+      <node concept="398BVA" id="1k6eCQnp9eW" role="398pKh">
+        <ref role="398BVh" node="42jqVeFkUG2" resolve="mbeddr.formal.home" />
+        <node concept="2Ry0Ak" id="1k6eCQnp9eX" role="iGT6I">
+          <property role="2Ry0Am" value="code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp9eY" role="2Ry0An">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnp9OG" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.prism" />
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="398rNT" id="1k6eCQnoUp$" role="1l3spd">
+      <property role="TrG5h" value="mbeddr.formal.smt.code" />
+      <node concept="398BVA" id="1k6eCQnoUp_" role="398pKh">
+        <ref role="398BVh" node="42jqVeFkUG2" resolve="mbeddr.formal.home" />
+        <node concept="2Ry0Ak" id="1k6eCQnoUpA" role="iGT6I">
+          <property role="2Ry0Am" value="code" />
+          <node concept="2Ry0Ak" id="1k6eCQnoUpB" role="2Ry0An">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnoVah" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.smt" />
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
     <node concept="398rNT" id="7he_lUurqtF" role="1l3spd">
       <property role="TrG5h" value="mbeddr.formal.safety.code" />
       <node concept="398BVA" id="7he_lUurqtG" role="398pKh">
@@ -598,6 +643,10 @@
           </node>
         </node>
       </node>
+      <node concept="m$_wl" id="1k6eCQnF1G0" role="39821P">
+        <ref role="m_rDy" node="1k6eCQnEZzO" resolve="fasten.symo" />
+        <node concept="pUk6x" id="1k6eCQnF24M" role="pUk7w" />
+      </node>
       <node concept="m$_wl" id="7he_lUumQum" role="39821P">
         <ref role="m_rDy" node="7he_lUumO49" resolve="com.mbeddr.formal.req" />
         <node concept="pUk6x" id="7Jv9b4B9k9w" role="pUk7w" />
@@ -606,6 +655,35 @@
         <ref role="m_rDy" node="7he_lUuoSVd" resolve="com.mbeddr.formal.spin" />
         <node concept="pUk6x" id="7Jv9b4B9k9x" role="pUk7w" />
       </node>
+      <node concept="m$_wl" id="1k6eCQnp820" role="39821P">
+        <ref role="m_rDy" node="1k6eCQnoSvI" resolve="com.mbeddr.formal.smt" />
+        <node concept="pUk6x" id="1k6eCQnp8qM" role="pUk7w" />
+        <node concept="398223" id="1k6eCQnpKcF" role="39821P">
+          <node concept="3_J27D" id="1k6eCQnpKcG" role="Nbhlr">
+            <node concept="3Mxwew" id="1k6eCQnpKp4" role="3MwsjC">
+              <property role="3MwjfP" value="lib" />
+            </node>
+          </node>
+          <node concept="2HvfSZ" id="1k6eCQnpKp5" role="39821P">
+            <node concept="398BVA" id="1k6eCQnpK_u" role="2HvfZ0">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnpKLT" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="1k6eCQnpKLW" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib" />
+                  <node concept="2Ry0Ak" id="1k6eCQnpKLZ" role="2Ry0An">
+                    <property role="2Ry0Am" value="lib" />
+                  </node>
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="m$_wl" id="1k6eCQnpiXs" role="39821P">
+        <ref role="m_rDy" node="1k6eCQnphZt" resolve="com.mbeddr.formal.prism" />
+        <node concept="pUk6x" id="1k6eCQnpiXt" role="pUk7w" />
+      </node>
       <node concept="m$_wl" id="wUJmWCyrgV" role="39821P">
         <ref role="m_rDy" node="42jqVeFkUv3" resolve="com.mbeddr.formal.nusmv" />
         <node concept="398223" id="wUJmWCzUGy" role="39821P">
@@ -708,6 +786,33 @@
         <ref role="m$_y1" node="7he_lUumEw2" resolve="com.mpsbasics" />
       </node>
     </node>
+    <node concept="m$_wf" id="1k6eCQnEZzO" role="3989C9">
+      <property role="m$_wk" value="fasten.symo" />
+      <node concept="3_J27D" id="1k6eCQnEZzQ" role="m$_yQ">
+        <node concept="3Mxwew" id="1k6eCQnF0lo" role="3MwsjC">
+          <property role="3MwjfP" value="fasten.symo" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnEZzS" role="m_cZH">
+        <node concept="3Mxwew" id="1k6eCQnF0lp" role="3MwsjC">
+          <property role="3MwjfP" value="fasten.symo" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnEZzU" role="m$_w8">
+        <node concept="3Mxwey" id="1k6eCQnF0xL" role="3MwsjC">
+          <ref role="3Mxwex" node="4aeOpjlAy7f" resolve="version" />
+        </node>
+      </node>
+      <node concept="m$f5U" id="1k6eCQnF0I9" role="m$_yh">
+        <ref role="m$f5T" node="1k6eCQnESS5" resolve="fasten.symo" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnF0Ux" role="m$_yJ">
+        <ref role="m$_y1" node="7he_lUumEw2" resolve="com.mpsbasics" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnF16T" role="m$_yJ">
+        <ref role="m$_y1" node="1uyUeTt3ODd" resolve="com.mbeddr.formal.base" />
+      </node>
+    </node>
     <node concept="m$_wf" id="1uyUeTt3ODd" role="3989C9">
       <property role="m$_wk" value="com.mbeddr.formal.base" />
       <node concept="m$_yC" id="1uyUeTt3RyR" role="m$_yJ">
@@ -834,6 +939,72 @@
         <ref role="m$_y1" node="42jqVeFkUv3" resolve="com.mbeddr.formal.nusmv" />
       </node>
     </node>
+    <node concept="m$_wf" id="1k6eCQnoSvI" role="3989C9">
+      <property role="m$_wk" value="com.mbeddr.formal.smt" />
+      <node concept="3_J27D" id="1k6eCQnoSvJ" role="m$_yQ">
+        <node concept="3Mxwew" id="1k6eCQnoSvK" role="3MwsjC">
+          <property role="3MwjfP" value="com.mbeddr.formal.smt" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnoSvL" role="m_cZH">
+        <node concept="3Mxwew" id="1k6eCQnoSvM" role="3MwsjC">
+          <property role="3MwjfP" value="com.mbeddr.formal.smt" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnoSvN" role="m$_w8">
+        <node concept="3Mxwey" id="1k6eCQnoSvO" role="3MwsjC">
+          <ref role="3Mxwex" node="4aeOpjlAy7f" resolve="version" />
+        </node>
+      </node>
+      <node concept="m$f5U" id="1k6eCQnoSvP" role="m$_yh">
+        <ref role="m$f5T" node="1k6eCQnp8Bb" resolve="com.mbeddr.formal.smt" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnoSvR" role="m$_yJ">
+        <ref role="m$_y1" to="ffeo:4k71ibbKLe8" resolve="jetbrains.mps.core" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnoSvS" role="m$_yJ">
+        <ref role="m$_y1" to="90a9:3$A0JaN5ezp" resolve="MPS.ThirdParty" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnoSvT" role="m$_yJ">
+        <ref role="m$_y1" to="al5i:$bJ0jguQdg" resolve="com.mbeddr.platform" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnoSvU" role="m$_yJ">
+        <ref role="m$_y1" node="42jqVeFkUv3" resolve="com.mbeddr.formal.nusmv" />
+      </node>
+    </node>
+    <node concept="m$_wf" id="1k6eCQnphZt" role="3989C9">
+      <property role="m$_wk" value="com.mbeddr.formal.prism" />
+      <node concept="3_J27D" id="1k6eCQnphZu" role="m$_yQ">
+        <node concept="3Mxwew" id="1k6eCQnphZv" role="3MwsjC">
+          <property role="3MwjfP" value="com.mbeddr.formal.prism" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnphZw" role="m_cZH">
+        <node concept="3Mxwew" id="1k6eCQnphZx" role="3MwsjC">
+          <property role="3MwjfP" value="com.mbeddr.formal.prism" />
+        </node>
+      </node>
+      <node concept="3_J27D" id="1k6eCQnphZy" role="m$_w8">
+        <node concept="3Mxwey" id="1k6eCQnphZz" role="3MwsjC">
+          <ref role="3Mxwex" node="4aeOpjlAy7f" resolve="version" />
+        </node>
+      </node>
+      <node concept="m$f5U" id="1k6eCQnphZ$" role="m$_yh">
+        <ref role="m$f5T" node="1k6eCQnoTg$" resolve="com.mbeddr.formal.prism" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnphZ_" role="m$_yJ">
+        <ref role="m$_y1" to="ffeo:4k71ibbKLe8" resolve="jetbrains.mps.core" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnphZA" role="m$_yJ">
+        <ref role="m$_y1" to="90a9:3$A0JaN5ezp" resolve="MPS.ThirdParty" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnphZB" role="m$_yJ">
+        <ref role="m$_y1" to="al5i:$bJ0jguQdg" resolve="com.mbeddr.platform" />
+      </node>
+      <node concept="m$_yC" id="1k6eCQnphZC" role="m$_yJ">
+        <ref role="m$_y1" node="42jqVeFkUv3" resolve="com.mbeddr.formal.nusmv" />
+      </node>
+    </node>
     <node concept="m$_wf" id="42jqVeFkUv3" role="3989C9">
       <property role="m$_wk" value="com.mbeddr.formal.nusmv" />
       <node concept="m$_yC" id="1uZbIJyquh_" role="m$_yJ">
@@ -2809,6 +2980,155 @@
         </node>
       </node>
     </node>
+    <node concept="2G$12M" id="1k6eCQnESS5" role="3989C9">
+      <property role="TrG5h" value="fasten.symo" />
+      <node concept="1E1JtD" id="1k6eCQnETgP" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.fasten.symo.hw" />
+        <property role="3LESm3" value="c2f3ae03-6a71-4e2a-88c9-c9e6eb4e20fa" />
+        <node concept="398BVA" id="1k6eCQnETte" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnETQ0" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnEUeL" role="2Ry0An">
+              <property role="2Ry0Am" value="com.fasten.symo.hw" />
+              <node concept="2Ry0Ak" id="1k6eCQnEUBy" role="2Ry0An">
+                <property role="2Ry0Am" value="com.fasten.symo.hw.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEUZZ" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEV00" role="1SiIV1">
+            <property role="3bR36h" value="true" />
+            <ref role="3bR37D" to="90a9:4be$WTb1AQa" resolve="de.itemis.mps.editor.diagram.runtime" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEV01" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEV02" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnEV0e" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnEV0f" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnEV03" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnEV04" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnEV05" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.fasten.symo.hw" />
+                  <node concept="2Ry0Ak" id="1k6eCQnEV06" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnEV0g" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="3rtmxn" id="1k6eCQnEZaY" role="3bR31x">
+          <node concept="3LXTmp" id="1k6eCQnEZaZ" role="3rtmxm">
+            <node concept="398BVA" id="1k6eCQnEZb0" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnEZb1" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnEZb2" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.fasten.symo.hw" />
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnEZb4" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="1E1JtD" id="1k6eCQnEVCy" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.symo.sysml.ibd" />
+        <property role="3LESm3" value="d7ce0776-e180-44b6-8b3f-a274ad438311" />
+        <node concept="398BVA" id="1k6eCQnEVOX" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnEW1o" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnEWq9" role="2Ry0An">
+              <property role="2Ry0Am" value="com.symo.sysml.ibd" />
+              <node concept="2Ry0Ak" id="1k6eCQnEWMU" role="2Ry0An">
+                <property role="2Ry0Am" value="com.symo.sysml.ibd.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEXby" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEXbz" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEXb$" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEXb_" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:6wEeo$QJAsB" resolve="de.itemis.mps.editor.diagram.shapes" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEXbA" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEXbB" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6LfQ" resolve="jetbrains.mps.kernel" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEXbC" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEXbD" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:6fQhGuklQWU" resolve="de.q60.mps.collections.libs" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnEXbE" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnEXbF" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnEXbR" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnEXbS" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnEXbG" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnEXbH" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnEXbI" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.symo.sysml.ibd" />
+                  <node concept="2Ry0Ak" id="1k6eCQnEXbJ" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnEXbT" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="3rtmxn" id="1k6eCQnEYYw" role="3bR31x">
+          <node concept="3LXTmp" id="1k6eCQnEYYx" role="3rtmxm">
+            <node concept="398BVA" id="1k6eCQnEYYy" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnEQWe" resolve="fasten.symo.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnEYYz" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnEYY$" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.symo.sysml.ibd" />
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnEYYA" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
     <node concept="2G$12M" id="7he_lUumCVe" role="3989C9">
       <property role="TrG5h" value="com.mbeddr.formal.req" />
       <node concept="1E1JtA" id="7he_lUumHB4" role="2G$12L">
@@ -4855,225 +5175,800 @@
             <node concept="3bR9La" id="7he_lUup0yz" role="1SiIV1">
               <ref role="3bR37D" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
             </node>
-          </node>
-          <node concept="1SiIV0" id="7he_lUup1h0" role="3bR37C">
-            <node concept="3bR9La" id="7he_lUup1h1" role="1SiIV1">
-              <ref role="3bR37D" node="7he_lUuoYjX" resolve="com.mbeddr.formal.spin.ext#3050019586772960524" />
+          </node>
+          <node concept="1SiIV0" id="7he_lUup1h0" role="3bR37C">
+            <node concept="3bR9La" id="7he_lUup1h1" role="1SiIV1">
+              <ref role="3bR37D" node="7he_lUuoYjX" resolve="com.mbeddr.formal.spin.ext#3050019586772960524" />
+            </node>
+          </node>
+          <node concept="1BupzO" id="5TezZ1Vej9n" role="3bR31x">
+            <property role="3ZfqAx" value="generator/template" />
+            <property role="1Hdu6h" value="true" />
+            <property role="1HemKv" value="true" />
+            <node concept="3LXTmp" id="5TezZ1Vej9o" role="1HemKq">
+              <node concept="398BVA" id="5TezZ1Vej9a" role="3LXTmr">
+                <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
+                <node concept="2Ry0Ak" id="5TezZ1Vej9b" role="iGT6I">
+                  <property role="2Ry0Am" value="languages" />
+                  <node concept="2Ry0Ak" id="5TezZ1Vej9c" role="2Ry0An">
+                    <property role="2Ry0Am" value="com.mbeddr.formal.spin.hdl" />
+                    <node concept="2Ry0Ak" id="5TezZ1Vej9d" role="2Ry0An">
+                      <property role="2Ry0Am" value="generator" />
+                      <node concept="2Ry0Ak" id="5TezZ1Vej9e" role="2Ry0An">
+                        <property role="2Ry0Am" value="template" />
+                      </node>
+                    </node>
+                  </node>
+                </node>
+              </node>
+              <node concept="3qWCbU" id="5TezZ1Vej9p" role="3LXTna">
+                <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+              </node>
+            </node>
+          </node>
+          <node concept="1SiIV0" id="8xY_IhvyGY" role="3bR37C">
+            <node concept="3bR9La" id="8xY_IhvyGZ" role="1SiIV1">
+              <ref role="3bR37D" to="al5i:Vtr7jyAKU4" resolve="com.mbeddr.mpsutil.filepicker" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUuoZZW" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUuoZZX" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUuoZZY" role="3bR37C">
+          <node concept="1Busua" id="7he_lUuoZZZ" role="1SiIV1">
+            <ref role="1Busuk" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0y8" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0y9" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1ZViq9oppal" resolve="jetbrains.mps.make.facets" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0ya" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yb" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yc" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yd" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0ye" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yf" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6Lg2" resolve="jetbrains.mps.smodel.resources" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yg" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yh" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yi" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yj" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yk" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yl" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yo" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yp" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6LfQ" resolve="jetbrains.mps.kernel" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yq" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0yr" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1TaHNgiIbIQ" resolve="MPS.Core" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0yu" role="3bR37C">
+          <node concept="1Busua" id="7he_lUup0yv" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1gY" role="3bR37C">
+          <node concept="1Busua" id="7he_lUup1gZ" role="1SiIV1">
+            <ref role="1Busuk" node="7he_lUuoYjo" resolve="com.mbeddr.formal.spin.ext" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1yO" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup1yP" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUuoZZG" resolve="com.mbeddr.formal.spin.hdl" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="5TezZ1Vej97" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="5TezZ1Vej98" role="1HemKq">
+            <node concept="398BVA" id="5TezZ1Vej8W" role="3LXTmr">
+              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
+              <node concept="2Ry0Ak" id="5TezZ1Vej8X" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="5TezZ1Vej8Y" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.hdl" />
+                  <node concept="2Ry0Ak" id="5TezZ1Vej8Z" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="5TezZ1Vej99" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="5OSKzlGxLL_" role="3bR37C">
+          <node concept="3bR9La" id="5OSKzlGxLLA" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUuoWYb" resolve="com.mbeddr.formal.spin.c.core" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="8xY_IhvyGL" role="3bR37C">
+          <node concept="3bR9La" id="8xY_IhvyGM" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:PE3B26QCrP" resolve="org.apache.commons" />
+          </node>
+        </node>
+      </node>
+      <node concept="1E1JtD" id="7he_lUup0GQ" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.spin.analyses" />
+        <property role="3LESm3" value="80ea7e60-3c36-4583-be96-3e7d3ad3504e" />
+        <node concept="398BVA" id="7he_lUup0GR" role="3LF7KH">
+          <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
+          <node concept="2Ry0Ak" id="7he_lUup0GS" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="7he_lUup0GT" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
+              <node concept="2Ry0Ak" id="7he_lUup11q" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0H8" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup0H9" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup0Hy" role="3bR37C">
+          <node concept="1Busua" id="7he_lUup0Hz" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1h2" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup1h3" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuP" resolve="com.mbeddr.formal.base.tooling" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1h4" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup1h5" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUuoVxm" resolve="com.mbeddr.formal.spin.pluginSolution" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1h6" role="3bR37C">
+          <node concept="3bR9La" id="7he_lUup1h7" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUub" resolve="com.mbeddr.formal.base.analyses" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="7he_lUup1h8" role="3bR37C">
+          <node concept="1Busua" id="7he_lUup1h9" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUub" resolve="com.mbeddr.formal.base.analyses" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="5TezZ1Vej9_" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="5TezZ1Vej9A" role="1HemKq">
+            <node concept="398BVA" id="5TezZ1Vej9q" role="3LXTmr">
+              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
+              <node concept="2Ry0Ak" id="5TezZ1Vej9r" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="5TezZ1Vej9s" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
+                  <node concept="2Ry0Ak" id="5TezZ1Vej9t" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="5TezZ1Vej9B" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="3rtmxn" id="7Jv9b4B5bY3" role="3bR31x">
+          <node concept="3LXTmp" id="7Jv9b4B5bY4" role="3rtmxm">
+            <node concept="3qWCbU" id="7Jv9b4B5bY5" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+            <node concept="398BVA" id="7Jv9b4B5bY6" role="3LXTmr">
+              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
+              <node concept="2Ry0Ak" id="7Jv9b4B5bY7" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="7Jv9b4B5bY8" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2G$12M" id="1k6eCQnoTg$" role="3989C9">
+      <property role="TrG5h" value="com.mbeddr.formal.prism" />
+      <node concept="1E1JtD" id="1k6eCQnoUdo" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.prism" />
+        <property role="3LESm3" value="3c34ac43-22de-4ba4-9539-377c90eb9be6" />
+        <node concept="398BVA" id="1k6eCQnoVUU" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnoWji" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnoWFD" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.prism" />
+              <node concept="2Ry0Ak" id="1k6eCQnpfKS" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.prism.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnoXxK" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnoXxL" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnoXxZ" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnpgf4" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnpgeT" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnpgeU" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnpgeV" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.prism" />
+                  <node concept="2Ry0Ak" id="1k6eCQnpgeW" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnpgf5" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnoXy2" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnoXy3" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnoXy4" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnoXy5" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpgeN" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpgeO" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpgeP" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpgeQ" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpgeR" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpgeS" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:1sO539bGQvB" resolve="de.slisson.mps.richtext" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpgf6" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnpgf7" role="1SiIV1">
+            <ref role="1Busuk" to="ffeo:7Kfy9QB6LbO" resolve="jetbrains.mps.lang.traceable" />
+          </node>
+        </node>
+        <node concept="3rtmxn" id="1k6eCQnpgYi" role="3bR31x">
+          <node concept="3LXTmp" id="1k6eCQnpgYj" role="3rtmxm">
+            <node concept="398BVA" id="1k6eCQnpgYk" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnpgYl" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnpgYm" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.prism" />
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnpgYo" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnphsj" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnphsk" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnoUdo" resolve="com.mbeddr.formal.prism" />
+          </node>
+        </node>
+      </node>
+      <node concept="1E1JtA" id="1k6eCQnp0L6" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.prism.pluginSolution" />
+        <property role="3LESm3" value="4e6c1b7e-ca4e-4172-8e14-215a5bd55c18" />
+        <node concept="398BVA" id="1k6eCQnp0Xk" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp1lG" role="iGT6I">
+            <property role="2Ry0Am" value="solutions" />
+            <node concept="2Ry0Ak" id="1k6eCQnp1I3" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.prism.pluginSolution" />
+              <node concept="2Ry0Ak" id="1k6eCQnpcEC" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.prism.pluginSolution.msd" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp2$U" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp2$V" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnp2_m" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnpd8Q" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnpd8F" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnpd8G" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="1k6eCQnpd8H" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.prism.pluginSolution" />
+                  <node concept="2Ry0Ak" id="1k6eCQnpd8I" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnpd8R" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpd8z" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpd8$" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuP" resolve="com.mbeddr.formal.base.tooling" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpd8_" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpd8A" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1ia2VB5guYy" resolve="MPS.IDEA" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpd8B" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpd8C" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpd8D" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpd8E" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:PE3B26QCrP" resolve="org.apache.commons" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnphsw" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnphsx" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnoUdo" resolve="com.mbeddr.formal.prism" />
+          </node>
+        </node>
+        <node concept="3rtmxn" id="8wvJyaWlTF" role="3bR31x">
+          <node concept="3LXTmp" id="8wvJyaWlTG" role="3rtmxm">
+            <node concept="3qWCbU" id="8wvJyaWlTH" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+            <node concept="398BVA" id="8wvJyaWlTI" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnp9eV" resolve="mbeddr.formal.prism.code" />
+              <node concept="2Ry0Ak" id="8wvJyaWlTJ" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="8wvJyaWlTK" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.prism.pluginSolution" />
+                </node>
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2G$12M" id="1k6eCQnp8Bb" role="3989C9">
+      <property role="TrG5h" value="com.mbeddr.formal.smt" />
+      <node concept="1E1JtD" id="1k6eCQnp8Bc" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.smtlib" />
+        <property role="3LESm3" value="9e54e509-552a-4f20-9b96-12a273367cff" />
+        <node concept="398BVA" id="1k6eCQnp8Bd" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp8Be" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnp8Bf" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.smtlib" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8Bg" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8Bh" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8Bi" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8Bj" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8Bk" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8Bl" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8Bm" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6LfQ" resolve="jetbrains.mps.kernel" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnp8Bn" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnp8Bo" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnp8Bp" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8Bq" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8Br" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib" />
+                  <node concept="2Ry0Ak" id="1k6eCQnp8Bs" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnp8Bt" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8Bu" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnp8Bv" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8Bw" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnp8Bx" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+          </node>
+        </node>
+        <node concept="3rtmxn" id="1k6eCQnp8BH" role="3bR31x">
+          <node concept="3LXTmp" id="1k6eCQnp8BI" role="3rtmxm">
+            <node concept="398BVA" id="1k6eCQnp8BJ" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8BK" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8BL" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib" />
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnp8BM" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnpepO" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpepP" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8CR" resolve="com.mbeddr.formal.smtlib.z3.rt" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnBL7i" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnBL7j" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8Cy" resolve="com.mbeddr.formal.smtlib.z3.lib" />
+          </node>
+        </node>
+      </node>
+      <node concept="1E1JtD" id="1k6eCQnp8BN" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.smtlib.synthesis" />
+        <property role="3LESm3" value="bf6758cd-1d80-487a-8750-bda80ddbed16" />
+        <node concept="398BVA" id="1k6eCQnp8BO" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp8BP" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="1k6eCQnp8BQ" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.synthesis" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8BR" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.synthesis.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8BS" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8BT" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8BW" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8BX" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8BY" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8BZ" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="1k6eCQnp8C0" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="1k6eCQnp8C1" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnp8C2" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8C3" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8C4" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.synthesis" />
+                  <node concept="2Ry0Ak" id="1k6eCQnp8C5" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnp8C6" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
             </node>
           </node>
-          <node concept="1BupzO" id="5TezZ1Vej9n" role="3bR31x">
+        </node>
+        <node concept="1SiIV0" id="1k6eCQnp8C7" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnp8C8" role="1SiIV1">
+            <ref role="1Busuk" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+          </node>
+        </node>
+        <node concept="1yeLz9" id="1k6eCQnp8Cb" role="1TViLv">
+          <property role="TrG5h" value="com.mbeddr.formal.smtlib.synthesis#01" />
+          <property role="3LESm3" value="352dbb2d-f836-4cb8-b2d2-d25f120ce99a" />
+          <node concept="1BupzO" id="1k6eCQnp8Ce" role="3bR31x">
             <property role="3ZfqAx" value="generator/template" />
             <property role="1Hdu6h" value="true" />
             <property role="1HemKv" value="true" />
-            <node concept="3LXTmp" id="5TezZ1Vej9o" role="1HemKq">
-              <node concept="398BVA" id="5TezZ1Vej9a" role="3LXTmr">
-                <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
-                <node concept="2Ry0Ak" id="5TezZ1Vej9b" role="iGT6I">
+            <node concept="3LXTmp" id="1k6eCQnp8Cf" role="1HemKq">
+              <node concept="398BVA" id="1k6eCQnp8Cg" role="3LXTmr">
+                <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8Ch" role="iGT6I">
                   <property role="2Ry0Am" value="languages" />
-                  <node concept="2Ry0Ak" id="5TezZ1Vej9c" role="2Ry0An">
-                    <property role="2Ry0Am" value="com.mbeddr.formal.spin.hdl" />
-                    <node concept="2Ry0Ak" id="5TezZ1Vej9d" role="2Ry0An">
+                  <node concept="2Ry0Ak" id="1k6eCQnp8Ci" role="2Ry0An">
+                    <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.synthesis" />
+                    <node concept="2Ry0Ak" id="1k6eCQnp8Cj" role="2Ry0An">
                       <property role="2Ry0Am" value="generator" />
-                      <node concept="2Ry0Ak" id="5TezZ1Vej9e" role="2Ry0An">
+                      <node concept="2Ry0Ak" id="1k6eCQnp8Ck" role="2Ry0An">
                         <property role="2Ry0Am" value="template" />
                       </node>
                     </node>
                   </node>
                 </node>
               </node>
-              <node concept="3qWCbU" id="5TezZ1Vej9p" role="3LXTna">
+              <node concept="3qWCbU" id="1k6eCQnp8Cl" role="3LXTna">
                 <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
               </node>
             </node>
           </node>
-          <node concept="1SiIV0" id="8xY_IhvyGY" role="3bR37C">
-            <node concept="3bR9La" id="8xY_IhvyGZ" role="1SiIV1">
-              <ref role="3bR37D" to="al5i:Vtr7jyAKU4" resolve="com.mbeddr.mpsutil.filepicker" />
+          <node concept="1SiIV0" id="1k6eCQnphtk" role="3bR37C">
+            <node concept="3bR9La" id="1k6eCQnphtl" role="1SiIV1">
+              <ref role="3bR37D" node="1k6eCQnp8Bc" resolve="com.mbeddr.formal.smtlib" />
             </node>
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUuoZZW" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUuoZZX" role="1SiIV1">
-            <ref role="3bR37D" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
+        <node concept="1SiIV0" id="1k6eCQnp8Cm" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8Cn" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8BN" resolve="com.mbeddr.formal.smtlib.synthesis" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUuoZZY" role="3bR37C">
-          <node concept="1Busua" id="7he_lUuoZZZ" role="1SiIV1">
-            <ref role="1Busuk" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
+        <node concept="3rtmxn" id="1k6eCQnp8Cq" role="3bR31x">
+          <node concept="3LXTmp" id="1k6eCQnp8Cr" role="3rtmxm">
+            <node concept="398BVA" id="1k6eCQnp8Cs" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8Ct" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8Cu" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.synthesis" />
+                </node>
+              </node>
+            </node>
+            <node concept="3qWCbU" id="1k6eCQnp8Cv" role="3LXTna">
+              <property role="3qWCbO" value="icons/**" />
+            </node>
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0y8" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0y9" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:1ZViq9oppal" resolve="jetbrains.mps.make.facets" />
+        <node concept="1SiIV0" id="1k6eCQnpeqe" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpeqf" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8CR" resolve="com.mbeddr.formal.smtlib.z3.rt" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0ya" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yb" role="1SiIV1">
-            <ref role="3bR37D" node="42jqVeFkUun" resolve="com.mbeddr.formal.base.expressions" />
+        <node concept="1SiIV0" id="1k6eCQnpeqg" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpeqh" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8Cy" resolve="com.mbeddr.formal.smtlib.z3.lib" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0yc" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yd" role="1SiIV1">
-            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+        <node concept="1SiIV0" id="1k6eCQnpht5" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnpht6" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8Bc" resolve="com.mbeddr.formal.smtlib" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0ye" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yf" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:7Kfy9QB6Lg2" resolve="jetbrains.mps.smodel.resources" />
+        <node concept="1SiIV0" id="1k6eCQnphti" role="3bR37C">
+          <node concept="1Busua" id="1k6eCQnphtj" role="1SiIV1">
+            <ref role="1Busuk" node="1k6eCQnp8Bc" resolve="com.mbeddr.formal.smtlib" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0yg" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yh" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
+      </node>
+      <node concept="1E1JtA" id="1k6eCQnp8Cy" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.smtlib.z3.lib" />
+        <property role="3LESm3" value="f7821750-33bf-489c-8f64-0850d86d540d" />
+        <node concept="398BVA" id="1k6eCQnp8Cz" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp8C$" role="iGT6I">
+            <property role="2Ry0Am" value="solutions" />
+            <node concept="2Ry0Ak" id="1k6eCQnp8C_" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8CA" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib.msd" />
+              </node>
+            </node>
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0yi" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yj" role="1SiIV1">
+        <node concept="1SiIV0" id="1k6eCQnp8CB" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8CC" role="1SiIV1">
+            <property role="3bR36h" value="true" />
             <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0yk" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yl" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup0yo" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yp" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:7Kfy9QB6LfQ" resolve="jetbrains.mps.kernel" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup0yq" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0yr" role="1SiIV1">
-            <ref role="3bR37D" to="ffeo:1TaHNgiIbIQ" resolve="MPS.Core" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup0yu" role="3bR37C">
-          <node concept="1Busua" id="7he_lUup0yv" role="1SiIV1">
-            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup1gY" role="3bR37C">
-          <node concept="1Busua" id="7he_lUup1gZ" role="1SiIV1">
-            <ref role="1Busuk" node="7he_lUuoYjo" resolve="com.mbeddr.formal.spin.ext" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup1yO" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup1yP" role="1SiIV1">
-            <ref role="3bR37D" node="7he_lUuoZZG" resolve="com.mbeddr.formal.spin.hdl" />
+        <node concept="1SiIV0" id="1k6eCQnp8CD" role="3bR37C">
+          <node concept="1BurEX" id="1k6eCQnp8CE" role="1SiIV1">
+            <node concept="398BVA" id="1k6eCQnp8CF" role="1BurEY">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8CG" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8CH" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib" />
+                  <node concept="2Ry0Ak" id="1k6eCQnp8CI" role="2Ry0An">
+                    <property role="2Ry0Am" value="lib" />
+                    <node concept="2Ry0Ak" id="1k6eCQnp8CJ" role="2Ry0An">
+                      <property role="2Ry0Am" value="com.microsoft.z3.jar" />
+                    </node>
+                  </node>
+                </node>
+              </node>
+            </node>
           </node>
         </node>
-        <node concept="1BupzO" id="5TezZ1Vej97" role="3bR31x">
+        <node concept="1BupzO" id="1k6eCQnp8CK" role="3bR31x">
           <property role="3ZfqAx" value="models" />
           <property role="1Hdu6h" value="true" />
           <property role="1HemKv" value="true" />
-          <node concept="3LXTmp" id="5TezZ1Vej98" role="1HemKq">
-            <node concept="398BVA" id="5TezZ1Vej8W" role="3LXTmr">
-              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
-              <node concept="2Ry0Ak" id="5TezZ1Vej8X" role="iGT6I">
-                <property role="2Ry0Am" value="languages" />
-                <node concept="2Ry0Ak" id="5TezZ1Vej8Y" role="2Ry0An">
-                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.hdl" />
-                  <node concept="2Ry0Ak" id="5TezZ1Vej8Z" role="2Ry0An">
+          <node concept="3LXTmp" id="1k6eCQnzdNH" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnzdNy" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnzdNz" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="1k6eCQnzdN$" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib" />
+                  <node concept="2Ry0Ak" id="1k6eCQnzdN_" role="2Ry0An">
                     <property role="2Ry0Am" value="models" />
                   </node>
                 </node>
               </node>
             </node>
-            <node concept="3qWCbU" id="5TezZ1Vej99" role="3LXTna">
+            <node concept="3qWCbU" id="1k6eCQnzdNI" role="3LXTna">
               <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
             </node>
           </node>
         </node>
-        <node concept="1SiIV0" id="5OSKzlGxLL_" role="3bR37C">
-          <node concept="3bR9La" id="5OSKzlGxLLA" role="1SiIV1">
-            <ref role="3bR37D" node="7he_lUuoWYb" resolve="com.mbeddr.formal.spin.c.core" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="8xY_IhvyGL" role="3bR37C">
-          <node concept="3bR9La" id="8xY_IhvyGM" role="1SiIV1">
-            <ref role="3bR37D" to="90a9:PE3B26QCrP" resolve="org.apache.commons" />
+        <node concept="3rtmxn" id="8wvJyaWlTM" role="3bR31x">
+          <node concept="3LXTmp" id="8wvJyaWlTN" role="3rtmxm">
+            <node concept="3qWCbU" id="8wvJyaWlTO" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+            <node concept="398BVA" id="8wvJyaWlTP" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="8wvJyaWlTQ" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="8wvJyaWlTR" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.lib" />
+                </node>
+              </node>
+            </node>
           </node>
         </node>
       </node>
-      <node concept="1E1JtD" id="7he_lUup0GQ" role="2G$12L">
+      <node concept="1E1JtA" id="1k6eCQnp8CR" role="2G$12L">
         <property role="BnDLt" value="true" />
-        <property role="TrG5h" value="com.mbeddr.formal.spin.analyses" />
-        <property role="3LESm3" value="80ea7e60-3c36-4583-be96-3e7d3ad3504e" />
-        <node concept="398BVA" id="7he_lUup0GR" role="3LF7KH">
-          <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
-          <node concept="2Ry0Ak" id="7he_lUup0GS" role="iGT6I">
-            <property role="2Ry0Am" value="languages" />
-            <node concept="2Ry0Ak" id="7he_lUup0GT" role="2Ry0An">
-              <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
-              <node concept="2Ry0Ak" id="7he_lUup11q" role="2Ry0An">
-                <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses.mpl" />
+        <property role="TrG5h" value="com.mbeddr.formal.smtlib.z3.rt" />
+        <property role="3LESm3" value="03458680-b827-4dcd-a8ca-ad82e7bdf60e" />
+        <node concept="398BVA" id="1k6eCQnp8CS" role="3LF7KH">
+          <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+          <node concept="2Ry0Ak" id="1k6eCQnp8CT" role="iGT6I">
+            <property role="2Ry0Am" value="solutions" />
+            <node concept="2Ry0Ak" id="1k6eCQnp8CU" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.rt" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8CV" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.rt.msd" />
               </node>
             </node>
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup0H8" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup0H9" role="1SiIV1">
-            <ref role="3bR37D" node="7he_lUuoZ0r" resolve="com.mbeddr.formal.spin" />
-          </node>
-        </node>
-        <node concept="1SiIV0" id="7he_lUup0Hy" role="3bR37C">
-          <node concept="1Busua" id="7he_lUup0Hz" role="1SiIV1">
-            <ref role="1Busuk" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
+        <node concept="1SiIV0" id="1k6eCQnp8CY" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8CZ" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup1h2" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup1h3" role="1SiIV1">
-            <ref role="3bR37D" node="42jqVeFkUuP" resolve="com.mbeddr.formal.base.tooling" />
+        <node concept="1SiIV0" id="1k6eCQnp8D0" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8D1" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup1h4" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup1h5" role="1SiIV1">
-            <ref role="3bR37D" node="7he_lUuoVxm" resolve="com.mbeddr.formal.spin.pluginSolution" />
+        <node concept="1SiIV0" id="1k6eCQnp8D2" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8D3" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:PE3B26QCrP" resolve="org.apache.commons" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup1h6" role="3bR37C">
-          <node concept="3bR9La" id="7he_lUup1h7" role="1SiIV1">
-            <ref role="3bR37D" node="42jqVeFkUub" resolve="com.mbeddr.formal.base.analyses" />
+        <node concept="1SiIV0" id="1k6eCQnp8D4" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8D5" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
           </node>
         </node>
-        <node concept="1SiIV0" id="7he_lUup1h8" role="3bR37C">
-          <node concept="1Busua" id="7he_lUup1h9" role="1SiIV1">
-            <ref role="1Busuk" node="42jqVeFkUub" resolve="com.mbeddr.formal.base.analyses" />
+        <node concept="1SiIV0" id="1k6eCQnp8D6" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnp8D7" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8Cy" resolve="com.mbeddr.formal.smtlib.z3.lib" />
           </node>
         </node>
-        <node concept="1BupzO" id="5TezZ1Vej9_" role="3bR31x">
+        <node concept="1BupzO" id="1k6eCQnp8D8" role="3bR31x">
           <property role="3ZfqAx" value="models" />
           <property role="1Hdu6h" value="true" />
           <property role="1HemKv" value="true" />
-          <node concept="3LXTmp" id="5TezZ1Vej9A" role="1HemKq">
-            <node concept="398BVA" id="5TezZ1Vej9q" role="3LXTmr">
-              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
-              <node concept="2Ry0Ak" id="5TezZ1Vej9r" role="iGT6I">
-                <property role="2Ry0Am" value="languages" />
-                <node concept="2Ry0Ak" id="5TezZ1Vej9s" role="2Ry0An">
-                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
-                  <node concept="2Ry0Ak" id="5TezZ1Vej9t" role="2Ry0An">
+          <node concept="3LXTmp" id="1k6eCQnp8D9" role="1HemKq">
+            <node concept="398BVA" id="1k6eCQnp8Da" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="1k6eCQnp8Db" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="1k6eCQnp8Dc" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.rt" />
+                  <node concept="2Ry0Ak" id="1k6eCQnp8Dd" role="2Ry0An">
                     <property role="2Ry0Am" value="models" />
                   </node>
                 </node>
               </node>
             </node>
-            <node concept="3qWCbU" id="5TezZ1Vej9B" role="3LXTna">
+            <node concept="3qWCbU" id="1k6eCQnp8De" role="3LXTna">
               <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
             </node>
           </node>
         </node>
-        <node concept="3rtmxn" id="7Jv9b4B5bY3" role="3bR31x">
-          <node concept="3LXTmp" id="7Jv9b4B5bY4" role="3rtmxm">
-            <node concept="3qWCbU" id="7Jv9b4B5bY5" role="3LXTna">
+        <node concept="1SiIV0" id="1k6eCQnphtV" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQnphtW" role="1SiIV1">
+            <ref role="3bR37D" node="1k6eCQnp8Bc" resolve="com.mbeddr.formal.smtlib" />
+          </node>
+        </node>
+        <node concept="3rtmxn" id="8wvJyaWlTT" role="3bR31x">
+          <node concept="3LXTmp" id="8wvJyaWlTU" role="3rtmxm">
+            <node concept="3qWCbU" id="8wvJyaWlTV" role="3LXTna">
               <property role="3qWCbO" value="icons/**, resources/**" />
             </node>
-            <node concept="398BVA" id="7Jv9b4B5bY6" role="3LXTmr">
-              <ref role="398BVh" node="7he_lUuoRR9" resolve="mbeddr.formal.spin.code" />
-              <node concept="2Ry0Ak" id="7Jv9b4B5bY7" role="iGT6I">
-                <property role="2Ry0Am" value="languages" />
-                <node concept="2Ry0Ak" id="7Jv9b4B5bY8" role="2Ry0An">
-                  <property role="2Ry0Am" value="com.mbeddr.formal.spin.analyses" />
+            <node concept="398BVA" id="8wvJyaWlTW" role="3LXTmr">
+              <ref role="398BVh" node="1k6eCQnoUp$" resolve="mbeddr.formal.smt.code" />
+              <node concept="2Ry0Ak" id="8wvJyaWlTX" role="iGT6I">
+                <property role="2Ry0Am" value="solutions" />
+                <node concept="2Ry0Ak" id="8wvJyaWlTY" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.smtlib.z3.rt" />
                 </node>
               </node>
             </node>
@@ -11448,141 +12343,147 @@
           </node>
         </node>
       </node>
-      <node concept="1X3_iC" id="1FMyjUPhIJF" role="lGtFl">
-        <property role="3V$3am" value="modules" />
-        <property role="3V$3ak" value="0cf935df-4699-4e9c-a132-fa109541cba3/1500819558095907805/1500819558095907806" />
-        <node concept="1E1JtD" id="4y8PK54$RUo" role="8Wnug">
-          <property role="BnDLt" value="true" />
-          <property role="TrG5h" value="com.mbeddr.formal.safety.gsn.web" />
-          <property role="3LESm3" value="0ca42a58-5150-4a55-89be-ba447ef72356" />
-          <node concept="398BVA" id="4y8PK54$Sis" role="3LF7KH">
-            <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
-            <node concept="2Ry0Ak" id="4y8PK54$SzC" role="iGT6I">
-              <property role="2Ry0Am" value="languages" />
-              <node concept="2Ry0Ak" id="4y8PK54$SON" role="2Ry0An">
-                <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
-                <node concept="2Ry0Ak" id="1FMyjUPe0GX" role="2Ry0An">
-                  <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web.mpl" />
+      <node concept="1E1JtD" id="4y8PK54$RUo" role="2G$12L">
+        <property role="BnDLt" value="true" />
+        <property role="TrG5h" value="com.mbeddr.formal.safety.gsn.web" />
+        <property role="3LESm3" value="0ca42a58-5150-4a55-89be-ba447ef72356" />
+        <node concept="398BVA" id="4y8PK54$Sis" role="3LF7KH">
+          <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
+          <node concept="2Ry0Ak" id="4y8PK54$SzC" role="iGT6I">
+            <property role="2Ry0Am" value="languages" />
+            <node concept="2Ry0Ak" id="4y8PK54$SON" role="2Ry0An">
+              <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
+              <node concept="2Ry0Ak" id="1FMyjUPe0GX" role="2Ry0An">
+                <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web.mpl" />
+              </node>
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="4y8PK54$TBy" role="3bR37C">
+          <node concept="3bR9La" id="4y8PK54$TBz" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="4y8PK54$TB$" role="3bR37C">
+          <node concept="3bR9La" id="4y8PK54$TB_" role="1SiIV1">
+            <ref role="3bR37D" node="7he_lUury9o" resolve="com.mbeddr.formal.safety.gsn" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="4y8PK54$TBA" role="3bR37C">
+          <node concept="3bR9La" id="4y8PK54$TBB" role="1SiIV1">
+            <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
+          </node>
+        </node>
+        <node concept="1SiIV0" id="4y8PK54$TBC" role="3bR37C">
+          <node concept="3bR9La" id="4y8PK54$TBD" role="1SiIV1">
+            <ref role="3bR37D" to="90a9:56Tfdun3uan" resolve="de.itemis.mps.editor.diagram.layout" />
+          </node>
+        </node>
+        <node concept="1BupzO" id="4y8PK54$TBP" role="3bR31x">
+          <property role="3ZfqAx" value="models" />
+          <property role="1Hdu6h" value="true" />
+          <property role="1HemKv" value="true" />
+          <node concept="3LXTmp" id="4y8PK54$TBQ" role="1HemKq">
+            <node concept="398BVA" id="4y8PK54$TBE" role="3LXTmr">
+              <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
+              <node concept="2Ry0Ak" id="4y8PK54$TBF" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="4y8PK54$TBG" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
+                  <node concept="2Ry0Ak" id="4y8PK54$TBH" role="2Ry0An">
+                    <property role="2Ry0Am" value="models" />
+                  </node>
                 </node>
               </node>
             </node>
+            <node concept="3qWCbU" id="4y8PK54$TBR" role="3LXTna">
+              <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
+            </node>
           </node>
-          <node concept="1SiIV0" id="4y8PK54$TBy" role="3bR37C">
-            <node concept="3bR9La" id="4y8PK54$TBz" role="1SiIV1">
+        </node>
+        <node concept="1yeLz9" id="4y8PK54$TBS" role="1TViLv">
+          <property role="TrG5h" value="com.mbeddr.formal.safety.gsn.web#01" />
+          <property role="3LESm3" value="31b0df10-2d1f-4744-8de7-461666d7c2d1" />
+          <node concept="1SiIV0" id="4y8PK54$TBT" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TBU" role="1SiIV1">
               <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
             </node>
           </node>
-          <node concept="1SiIV0" id="4y8PK54$TB$" role="3bR37C">
-            <node concept="3bR9La" id="4y8PK54$TB_" role="1SiIV1">
+          <node concept="1SiIV0" id="4y8PK54$TBV" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TBW" role="1SiIV1">
               <ref role="3bR37D" node="7he_lUury9o" resolve="com.mbeddr.formal.safety.gsn" />
             </node>
           </node>
-          <node concept="1SiIV0" id="4y8PK54$TBA" role="3bR37C">
-            <node concept="3bR9La" id="4y8PK54$TBB" role="1SiIV1">
+          <node concept="1SiIV0" id="4y8PK54$TBX" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TBY" role="1SiIV1">
               <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
             </node>
           </node>
-          <node concept="1SiIV0" id="4y8PK54$TBC" role="3bR37C">
-            <node concept="3bR9La" id="4y8PK54$TBD" role="1SiIV1">
+          <node concept="1SiIV0" id="4y8PK54$TBZ" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TC0" role="1SiIV1">
+              <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
+            </node>
+          </node>
+          <node concept="1SiIV0" id="4y8PK54$TC1" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TC2" role="1SiIV1">
               <ref role="3bR37D" to="90a9:56Tfdun3uan" resolve="de.itemis.mps.editor.diagram.layout" />
             </node>
           </node>
-          <node concept="1BupzO" id="4y8PK54$TBP" role="3bR31x">
-            <property role="3ZfqAx" value="models" />
+          <node concept="1SiIV0" id="4y8PK54$TC3" role="3bR37C">
+            <node concept="3bR9La" id="4y8PK54$TC4" role="1SiIV1">
+              <ref role="3bR37D" to="90a9:1sO539bGQvB" resolve="de.slisson.mps.richtext" />
+            </node>
+          </node>
+          <node concept="1BupzO" id="4y8PK54$TCi" role="3bR31x">
+            <property role="3ZfqAx" value="generator/templates" />
             <property role="1Hdu6h" value="true" />
             <property role="1HemKv" value="true" />
-            <node concept="3LXTmp" id="4y8PK54$TBQ" role="1HemKq">
-              <node concept="398BVA" id="4y8PK54$TBE" role="3LXTmr">
+            <node concept="3LXTmp" id="4y8PK54$TCj" role="1HemKq">
+              <node concept="398BVA" id="4y8PK54$TC5" role="3LXTmr">
                 <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
-                <node concept="2Ry0Ak" id="4y8PK54$TBF" role="iGT6I">
+                <node concept="2Ry0Ak" id="4y8PK54$TC6" role="iGT6I">
                   <property role="2Ry0Am" value="languages" />
-                  <node concept="2Ry0Ak" id="4y8PK54$TBG" role="2Ry0An">
+                  <node concept="2Ry0Ak" id="4y8PK54$TC7" role="2Ry0An">
                     <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
-                    <node concept="2Ry0Ak" id="4y8PK54$TBH" role="2Ry0An">
-                      <property role="2Ry0Am" value="models" />
+                    <node concept="2Ry0Ak" id="4y8PK54$TC8" role="2Ry0An">
+                      <property role="2Ry0Am" value="generator" />
+                      <node concept="2Ry0Ak" id="4y8PK54$TC9" role="2Ry0An">
+                        <property role="2Ry0Am" value="templates" />
+                      </node>
                     </node>
                   </node>
                 </node>
               </node>
-              <node concept="3qWCbU" id="4y8PK54$TBR" role="3LXTna">
+              <node concept="3qWCbU" id="4y8PK54$TCk" role="3LXTna">
                 <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
               </node>
             </node>
           </node>
-          <node concept="1yeLz9" id="4y8PK54$TBS" role="1TViLv">
-            <property role="TrG5h" value="com.mbeddr.formal.safety.gsn.web#01" />
-            <property role="3LESm3" value="31b0df10-2d1f-4744-8de7-461666d7c2d1" />
-            <node concept="1SiIV0" id="4y8PK54$TBT" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TBU" role="1SiIV1">
-                <ref role="3bR37D" to="ffeo:1H905DlDUSw" resolve="MPS.OpenAPI" />
-              </node>
-            </node>
-            <node concept="1SiIV0" id="4y8PK54$TBV" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TBW" role="1SiIV1">
-                <ref role="3bR37D" node="7he_lUury9o" resolve="com.mbeddr.formal.safety.gsn" />
-              </node>
-            </node>
-            <node concept="1SiIV0" id="4y8PK54$TBX" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TBY" role="1SiIV1">
-                <ref role="3bR37D" to="ffeo:mXGwHwhVPj" resolve="JDK" />
-              </node>
-            </node>
-            <node concept="1SiIV0" id="4y8PK54$TBZ" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TC0" role="1SiIV1">
-                <ref role="3bR37D" to="ffeo:7Kfy9QB6KXW" resolve="jetbrains.mps.lang.core" />
-              </node>
-            </node>
-            <node concept="1SiIV0" id="4y8PK54$TC1" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TC2" role="1SiIV1">
-                <ref role="3bR37D" to="90a9:56Tfdun3uan" resolve="de.itemis.mps.editor.diagram.layout" />
-              </node>
-            </node>
-            <node concept="1SiIV0" id="4y8PK54$TC3" role="3bR37C">
-              <node concept="3bR9La" id="4y8PK54$TC4" role="1SiIV1">
-                <ref role="3bR37D" to="90a9:1sO539bGQvB" resolve="de.slisson.mps.richtext" />
-              </node>
-            </node>
-            <node concept="1BupzO" id="4y8PK54$TCi" role="3bR31x">
-              <property role="3ZfqAx" value="generator/templates" />
-              <property role="1Hdu6h" value="true" />
-              <property role="1HemKv" value="true" />
-              <node concept="3LXTmp" id="4y8PK54$TCj" role="1HemKq">
-                <node concept="398BVA" id="4y8PK54$TC5" role="3LXTmr">
-                  <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
-                  <node concept="2Ry0Ak" id="4y8PK54$TC6" role="iGT6I">
-                    <property role="2Ry0Am" value="languages" />
-                    <node concept="2Ry0Ak" id="4y8PK54$TC7" role="2Ry0An">
-                      <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
-                      <node concept="2Ry0Ak" id="4y8PK54$TC8" role="2Ry0An">
-                        <property role="2Ry0Am" value="generator" />
-                        <node concept="2Ry0Ak" id="4y8PK54$TC9" role="2Ry0An">
-                          <property role="2Ry0Am" value="templates" />
-                        </node>
-                      </node>
-                    </node>
-                  </node>
-                </node>
-                <node concept="3qWCbU" id="4y8PK54$TCk" role="3LXTna">
-                  <property role="3qWCbO" value="**/*.mps, **/*.mpsr, **/.model" />
-                </node>
-              </node>
+          <node concept="1SiIV0" id="1k6eCQni9$A" role="3bR37C">
+            <node concept="3bR9La" id="1k6eCQni9$B" role="1SiIV1">
+              <ref role="3bR37D" node="7he_lUurzLh" resolve="com.mbeddr.formal.safety.gsn.ext" />
             </node>
           </node>
-          <node concept="3rtmxn" id="4y8PK54$TQH" role="3bR31x">
-            <node concept="3LXTmp" id="4y8PK54$TQI" role="3rtmxm">
-              <node concept="398BVA" id="4y8PK54$TQJ" role="3LXTmr">
-                <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
-                <node concept="2Ry0Ak" id="4y8PK54$TQK" role="iGT6I">
-                  <property role="2Ry0Am" value="languages" />
-                  <node concept="2Ry0Ak" id="4y8PK54$TQL" role="2Ry0An">
-                    <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
-                  </node>
+        </node>
+        <node concept="3rtmxn" id="4y8PK54$TQH" role="3bR31x">
+          <node concept="3LXTmp" id="4y8PK54$TQI" role="3rtmxm">
+            <node concept="398BVA" id="4y8PK54$TQJ" role="3LXTmr">
+              <ref role="398BVh" node="7he_lUurqtF" resolve="mbeddr.formal.safety.code" />
+              <node concept="2Ry0Ak" id="4y8PK54$TQK" role="iGT6I">
+                <property role="2Ry0Am" value="languages" />
+                <node concept="2Ry0Ak" id="4y8PK54$TQL" role="2Ry0An">
+                  <property role="2Ry0Am" value="com.mbeddr.formal.safety.gsn.web" />
                 </node>
               </node>
-              <node concept="3qWCbU" id="4y8PK54$TQN" role="3LXTna">
-                <property role="3qWCbO" value="icons/**, resources/**" />
-              </node>
             </node>
+            <node concept="3qWCbU" id="4y8PK54$TQN" role="3LXTna">
+              <property role="3qWCbO" value="icons/**, resources/**" />
+            </node>
+          </node>
+        </node>
+        <node concept="1SiIV0" id="1k6eCQni9$p" role="3bR37C">
+          <node concept="3bR9La" id="1k6eCQni9$q" role="1SiIV1">
+            <ref role="3bR37D" node="42jqVeFkUuV" resolve="com.mbeddr.formal.base" />
           </node>
         </node>
       </node>
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/generator/template/main@generator.mps b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/generator/template/main@generator.mps
index 26634dac9..cd5be0ee5 100644
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/generator/template/main@generator.mps
+++ b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/generator/template/main@generator.mps
@@ -159,7 +159,6 @@
       </concept>
       <concept id="1168024337012" name="jetbrains.mps.lang.generator.structure.SourceSubstituteMacro_SourceNodeQuery" flags="in" index="3NFfHV" />
       <concept id="1118786554307" name="jetbrains.mps.lang.generator.structure.LoopMacro" flags="ln" index="1WS0z7">
-        <property id="7430509679011668804" name="counterVarName" index="1qytDF" />
         <child id="1167952069335" name="sourceNodesQuery" index="3Jn$fo" />
       </concept>
       <concept id="1088761943574" name="jetbrains.mps.lang.generator.structure.ReferenceMacro" flags="ln" index="1ZhdrF">
@@ -300,7 +299,7 @@
             <node concept="1Uau1d" id="1MFSGJpnCLg" role="11AoXW">
               <node concept="1UfkGm" id="1MFSGJpnCLr" role="1UfoCz">
                 <node concept="11ACyy" id="1MFSGJpnCLE" role="1U5zfR">
-                  <ref role="11ACyx" node="1MFSGJpnCKu" />
+                  <ref role="11ACyx" node="1MFSGJpnCKu" resolve="a" />
                   <node concept="1ZhdrF" id="1MFSGJpod9R" role="lGtFl">
                     <property role="P3scX" value="9e54e509-552a-4f20-9b96-12a273367cff/7139183404079772121/7139183404079772122" />
                     <property role="2qtEX8" value="var" />
@@ -347,7 +346,6 @@
                   <node concept="29HgVG" id="1MFSGJpocos" role="lGtFl" />
                 </node>
                 <node concept="1WS0z7" id="1MFSGJpocaw" role="lGtFl">
-                  <property role="1qytDF" value="" />
                   <node concept="3JmXsc" id="1MFSGJpocaz" role="3Jn$fo">
                     <node concept="3clFbS" id="1MFSGJpoca$" role="2VODD2">
                       <node concept="3clFbF" id="1MFSGJpocaE" role="3cqZAp">
@@ -364,7 +362,7 @@
               </node>
               <node concept="1UfkGm" id="1MFSGJpnCLP" role="1UfoCz">
                 <node concept="11ACyy" id="1MFSGJpnCM7" role="1U5zfR">
-                  <ref role="11ACyx" node="1MFSGJpnCKI" />
+                  <ref role="11ACyx" node="1MFSGJpnCKI" resolve="b" />
                   <node concept="1ZhdrF" id="1MFSGJpoH0y" role="lGtFl">
                     <property role="P3scX" value="9e54e509-552a-4f20-9b96-12a273367cff/7139183404079772121/7139183404079772122" />
                     <property role="2qtEX8" value="var" />
@@ -411,7 +409,6 @@
                   <node concept="29HgVG" id="1MFSGJpoGTF" role="lGtFl" />
                 </node>
                 <node concept="1WS0z7" id="1MFSGJpoGoi" role="lGtFl">
-                  <property role="1qytDF" value="" />
                   <node concept="3JmXsc" id="1MFSGJpoGol" role="3Jn$fo">
                     <node concept="3clFbS" id="1MFSGJpoGom" role="2VODD2">
                       <node concept="3clFbF" id="1MFSGJpoGos" role="3cqZAp">
@@ -878,9 +875,9 @@
               <node concept="1UfpLS" id="1MFSGJppwk4" role="11ARNb">
                 <node concept="1Uau1c" id="1MFSGJppwkn" role="1U5zfR">
                   <node concept="11BOot" id="1MFSGJppwmG" role="1UfoCz">
-                    <ref role="11BOos" node="1MFSGJppwlc" />
+                    <ref role="11BOos" node="1MFSGJppwlc" resolve="test_fun" />
                     <node concept="11ACyy" id="1MFSGJppwno" role="11yxzb">
-                      <ref role="11ACyx" node="1MFSGJppwiW" />
+                      <ref role="11ACyx" node="1MFSGJppwiW" resolve="a" />
                       <node concept="1WS0z7" id="1MFSGJppN5b" role="lGtFl">
                         <node concept="3JmXsc" id="1MFSGJppN5c" role="3Jn$fo">
                           <node concept="3clFbS" id="1MFSGJppN5d" role="2VODD2">
@@ -920,7 +917,7 @@
                       </node>
                     </node>
                     <node concept="11ACyy" id="1MFSGJprOHd" role="11yxzb">
-                      <ref role="11ACyx" node="1MFSGJppwjk" />
+                      <ref role="11ACyx" node="1MFSGJppwjk" resolve="b" />
                       <node concept="1WS0z7" id="1MFSGJprOHe" role="lGtFl">
                         <node concept="3JmXsc" id="1MFSGJprOHf" role="3Jn$fo">
                           <node concept="3clFbS" id="1MFSGJprOHg" role="2VODD2">
@@ -1007,9 +1004,9 @@
                   </node>
                 </node>
                 <node concept="11BOot" id="1MFSGJppQH3" role="1U5zfT">
-                  <ref role="11BOos" node="1MFSGJppwh1" />
+                  <ref role="11BOos" node="1MFSGJppwh1" resolve="fun" />
                   <node concept="11ACyy" id="1MFSGJpqJWC" role="11yxzb">
-                    <ref role="11ACyx" node="1MFSGJppwiW" />
+                    <ref role="11ACyx" node="1MFSGJppwiW" resolve="a" />
                     <node concept="1WS0z7" id="1MFSGJpqJWD" role="lGtFl">
                       <node concept="3JmXsc" id="1MFSGJpqJWE" role="3Jn$fo">
                         <node concept="3clFbS" id="1MFSGJpqJWF" role="2VODD2">
@@ -1049,7 +1046,7 @@
                     </node>
                   </node>
                   <node concept="11ACyy" id="1MFSGJprGfX" role="11yxzb">
-                    <ref role="11ACyx" node="1MFSGJppwjk" />
+                    <ref role="11ACyx" node="1MFSGJppwjk" resolve="b" />
                     <node concept="1WS0z7" id="1MFSGJprGz1" role="lGtFl">
                       <node concept="3JmXsc" id="1MFSGJprGz2" role="3Jn$fo">
                         <node concept="3clFbS" id="1MFSGJprGz3" role="2VODD2">
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/models/structure.mps b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/models/structure.mps
index 380695314..8c0b3f7bd 100644
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/models/structure.mps
+++ b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib.synthesis/models/structure.mps
@@ -3,6 +3,7 @@
   <persistence version="9" />
   <languages>
     <use id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure" version="9" />
+    <use id="982eb8df-2c96-4bd7-9963-11712ea622e5" name="jetbrains.mps.lang.resources" version="2" />
     <devkit ref="78434eb8-b0e5-444b-850d-e7c4ad2da9ab(jetbrains.mps.devkit.aspect.structure)" />
   </languages>
   <imports>
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/com.mbeddr.formal.smtlib.mpl b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/com.mbeddr.formal.smtlib.mpl
index b624ed467..b57ba1ab7 100644
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/com.mbeddr.formal.smtlib.mpl
+++ b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/com.mbeddr.formal.smtlib.mpl
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <language namespace="com.mbeddr.formal.smtlib" uuid="9e54e509-552a-4f20-9b96-12a273367cff" languageVersion="0" moduleVersion="0">
   <models>
-    <modelRoot contentPath="${module}" type="default">
+    <modelRoot type="default" contentPath="${module}">
       <sourceRoot location="models" />
     </modelRoot>
   </models>
@@ -11,60 +11,13 @@
     </facet>
   </facets>
   <accessoryModels />
-  <generators>
-    <generator alias="main" namespace="com.mbeddr.formal.smtlib#01" uuid="b8f0089b-975c-45b2-bea3-af53811ceb62">
-      <models>
-        <modelRoot contentPath="${module}/generator/template" type="default">
-          <sourceRoot location="." />
-        </modelRoot>
-      </models>
-      <facets>
-        <facet type="java" compile="mps" classes="mps" ext="no">
-          <classes generated="true" path="${module}/generator/classes_gen" />
-        </facet>
-      </facets>
-      <external-templates />
-      <languageVersions>
-        <language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="12" />
-        <language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
-        <language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="1" />
-        <language slang="l:f2801650-65d5-424e-bb1b-463a8781b786:jetbrains.mps.baseLanguage.javadoc" version="2" />
-        <language slang="l:760a0a8c-eabb-4521-8bfd-65db761a9ba3:jetbrains.mps.baseLanguage.logging" version="0" />
-        <language slang="l:a247e09e-2435-45ba-b8d2-07e93feba96a:jetbrains.mps.baseLanguage.tuples" version="0" />
-        <language slang="l:ceab5195-25ea-4f22-9b92-103b95ca8c0c:jetbrains.mps.lang.core" version="2" />
-        <language slang="l:b401a680-8325-4110-8fd3-84331ff25bef:jetbrains.mps.lang.generator" version="4" />
-        <language slang="l:d7706f63-9be2-479c-a3da-ae92af1e64d5:jetbrains.mps.lang.generator.generationContext" version="2" />
-        <language slang="l:289fcc83-6543-41e8-a5ca-768235715ce4:jetbrains.mps.lang.generator.generationParameters" version="0" />
-        <language slang="l:446c26eb-2b7b-4bf0-9b35-f83fa582753e:jetbrains.mps.lang.modelapi" version="0" />
-        <language slang="l:3a13115c-633c-4c5c-bbcc-75c4219e9555:jetbrains.mps.lang.quotation" version="5" />
-        <language slang="l:13744753-c81f-424a-9c1b-cf8943bf4e86:jetbrains.mps.lang.sharedConcepts" version="0" />
-        <language slang="l:7866978e-a0f0-4cc7-81bc-4d213d9375e1:jetbrains.mps.lang.smodel" version="19" />
-        <language slang="l:c7fb639f-be78-4307-89b0-b5959c3fa8c8:jetbrains.mps.lang.text" version="0" />
-        <language slang="l:9ded098b-ad6a-4657-bfd9-48636cfe8bc3:jetbrains.mps.lang.traceable" 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="9e54e509-552a-4f20-9b96-12a273367cff(com.mbeddr.formal.smtlib)" version="0" />
-        <module reference="b8f0089b-975c-45b2-bea3-af53811ceb62(com.mbeddr.formal.smtlib#01)" version="0" />
-        <module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
-      </dependencyVersions>
-      <mapping-priorities />
-    </generator>
-  </generators>
   <sourcePath />
   <dependencies>
     <dependency reexport="false">8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)</dependency>
     <dependency reexport="false">2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)</dependency>
     <dependency reexport="false">03458680-b827-4dcd-a8ca-ad82e7bdf60e(com.mbeddr.formal.smtlib.z3.rt)</dependency>
     <dependency reexport="false">6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)</dependency>
+    <dependency reexport="false">f7821750-33bf-489c-8f64-0850d86d540d(com.mbeddr.formal.smtlib.z3.lib)</dependency>
   </dependencies>
   <languageVersions>
     <language slang="l:9d69e719-78c8-4286-90db-fb19c107d049:com.mbeddr.mpsutil.grammarcells" version="2" />
@@ -120,6 +73,7 @@
     <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="9e54e509-552a-4f20-9b96-12a273367cff(com.mbeddr.formal.smtlib)" version="0" />
+    <module reference="f7821750-33bf-489c-8f64-0850d86d540d(com.mbeddr.formal.smtlib.z3.lib)" version="0" />
     <module reference="03458680-b827-4dcd-a8ca-ad82e7bdf60e(com.mbeddr.formal.smtlib.z3.rt)" 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" />
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/generator/template/main@generator.mps b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/generator/template/main@generator.mps
deleted file mode 100644
index 8767f8ad5..000000000
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/generator/template/main@generator.mps
+++ /dev/null
@@ -1,24 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<model ref="r:0fd0f186-5618-461e-9581-51317618b5f8(main@generator)">
-  <persistence version="9" />
-  <languages>
-    <devkit ref="a2eb3a43-fcc2-4200-80dc-c60110c4862d(jetbrains.mps.devkit.templates)" />
-  </languages>
-  <imports>
-    <import index="d9cz" ref="r:41c1238c-43f1-4441-984e-72955eefcbfb(com.mbeddr.formal.smtlib.structure)" />
-  </imports>
-  <registry>
-    <language id="b401a680-8325-4110-8fd3-84331ff25bef" name="jetbrains.mps.lang.generator">
-      <concept id="1095416546421" name="jetbrains.mps.lang.generator.structure.MappingConfiguration" flags="ig" index="bUwia" />
-    </language>
-    <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
-      <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
-        <property id="1169194664001" name="name" index="TrG5h" />
-      </concept>
-    </language>
-  </registry>
-  <node concept="bUwia" id="104dc5E3w99">
-    <property role="TrG5h" value="main" />
-  </node>
-</model>
-
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/intentions.mps b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/intentions.mps
index 8dc9773c3..bb19e94f9 100644
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/intentions.mps
+++ b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/intentions.mps
@@ -8,6 +8,7 @@
   <imports>
     <import index="kaug" ref="r:521dbd70-b62b-4a68-a516-821505a8eae5(com.mbeddr.formal.smtlib.z3.rt.runner)" />
     <import index="fsan" ref="r:f2b2fa9d-7b24-4c14-9aef-720730021a71(com.mbeddr.formal.smtlib.z3.rt.witness)" />
+    <import index="f7eu" ref="f7821750-33bf-489c-8f64-0850d86d540d/java:com.microsoft.z3(com.mbeddr.formal.smtlib.z3.lib/)" />
     <import index="d9cz" ref="r:41c1238c-43f1-4441-984e-72955eefcbfb(com.mbeddr.formal.smtlib.structure)" implicit="true" />
   </imports>
   <registry>
diff --git a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/structure.mps b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/structure.mps
index 288c305a6..ef1bb8f7d 100644
--- a/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/structure.mps
+++ b/code/languages/com.mbeddr.formal.smt/languages/com.mbeddr.formal.smtlib/models/structure.mps
@@ -3,12 +3,13 @@
   <persistence version="9" />
   <languages>
     <use id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure" version="9" />
+    <use id="982eb8df-2c96-4bd7-9963-11712ea622e5" name="jetbrains.mps.lang.resources" version="2" />
     <devkit ref="78434eb8-b0e5-444b-850d-e7c4ad2da9ab(jetbrains.mps.devkit.aspect.structure)" />
   </languages>
   <imports>
+    <import index="b19z" ref="r:11a68676-9d63-4e1c-b920-59aefe77def3(com.mbeddr.formal.base.structure)" />
+    <import index="ehqg" ref="r:2c1724e1-8ed6-4fe4-9e44-fae13cd2a5ac(com.mbeddr.formal.base.expressions.structure)" />
     <import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" implicit="true" />
-    <import index="ehqg" ref="r:2c1724e1-8ed6-4fe4-9e44-fae13cd2a5ac(com.mbeddr.formal.base.expressions.structure)" implicit="true" />
-    <import index="b19z" ref="r:11a68676-9d63-4e1c-b920-59aefe77def3(com.mbeddr.formal.base.structure)" implicit="true" />
   </imports>
   <registry>
     <language id="c72da2b9-7cce-4447-8389-f407dc1158b7" name="jetbrains.mps.lang.structure">
diff --git a/code/languages/com.mbeddr.formal.smt/solutions/com.mbeddr.formal.smtlib.z3.lib/com.mbeddr.formal.smtlib.z3.lib.msd b/code/languages/com.mbeddr.formal.smt/solutions/com.mbeddr.formal.smtlib.z3.lib/com.mbeddr.formal.smtlib.z3.lib.msd
index faea567e5..3120512ca 100644
--- a/code/languages/com.mbeddr.formal.smt/solutions/com.mbeddr.formal.smtlib.z3.lib/com.mbeddr.formal.smtlib.z3.lib.msd
+++ b/code/languages/com.mbeddr.formal.smt/solutions/com.mbeddr.formal.smtlib.z3.lib/com.mbeddr.formal.smtlib.z3.lib.msd
@@ -1,10 +1,10 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <solution name="com.mbeddr.formal.smtlib.z3.lib" uuid="f7821750-33bf-489c-8f64-0850d86d540d" moduleVersion="0" compileInMPS="true">
   <models>
-    <modelRoot contentPath="${module}" type="default">
+    <modelRoot type="default" contentPath="${module}">
       <sourceRoot location="models" />
     </modelRoot>
-    <modelRoot contentPath="${module}/lib" type="java_classes">
+    <modelRoot type="java_classes" contentPath="${module}/lib">
       <sourceRoot location="com.microsoft.z3.jar" />
     </modelRoot>
   </models>
@@ -18,7 +18,7 @@
   </stubModelEntries>
   <sourcePath />
   <dependencies>
-    <dependency reexport="false">6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)</dependency>
+    <dependency reexport="true">6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)</dependency>
   </dependencies>
   <languageVersions>
     <language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="12" />
diff --git a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/_010_simple_output.mps b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/_010_simple_output.mps
index 14f0e669d..a141048c6 100644
--- a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/_010_simple_output.mps
+++ b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/_010_simple_output.mps
@@ -79,22 +79,22 @@
         </node>
         <node concept="35L7W5" id="3908G2fy9iO" role="1U5zfT">
           <node concept="1U5_Ed" id="3908G2fy9iH" role="35L7Wp">
-            <ref role="1U5_Ec" node="3908G2fy9iF" />
+            <ref role="1U5_Ec" node="3908G2fy9iF" resolve="terminal_4" />
           </node>
           <node concept="1UfqsA" id="3908G2fy9iI" role="35L7Wu">
             <node concept="1U5_Ed" id="3908G2fy9iJ" role="1UfoCz">
-              <ref role="1U5_Ec" node="3908G2fy9ir" />
+              <ref role="1U5_Ec" node="3908G2fy9ir" resolve="terminal_0" />
             </node>
             <node concept="1U5_Ed" id="3908G2fy9iK" role="1UfoCz">
-              <ref role="1U5_Ec" node="3908G2fy9iv" />
+              <ref role="1U5_Ec" node="3908G2fy9iv" resolve="terminal_1" />
             </node>
           </node>
           <node concept="1UfqsD" id="3908G2fy9iL" role="35L7Wh">
             <node concept="1U5_Ed" id="3908G2fy9iM" role="1U5zfR">
-              <ref role="1U5_Ec" node="3908G2fy9iz" />
+              <ref role="1U5_Ec" node="3908G2fy9iz" resolve="terminal_2" />
             </node>
             <node concept="1U5_Ed" id="3908G2fy9iN" role="1U5zfT">
-              <ref role="1U5_Ec" node="3908G2fy9iB" />
+              <ref role="1U5_Ec" node="3908G2fy9iB" resolve="terminal_3" />
             </node>
           </node>
         </node>
diff --git a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/sandbox._010_smoke_synth.mps b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/sandbox._010_smoke_synth.mps
index 750e3d107..b05c19999 100644
--- a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/sandbox._010_smoke_synth.mps
+++ b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib.synthesis/models/sandbox._010_smoke_synth.mps
@@ -135,14 +135,14 @@
       <node concept="1U5apb" id="1MFSGJprTJ3" role="11zN3m" />
       <node concept="1UfkGm" id="1MFSGJppp7h" role="11AoXW">
         <node concept="11ACyy" id="1MFSGJprFo4" role="1U5zfR">
-          <ref role="11ACyx" node="1MFSGJpr2Cl" />
+          <ref role="11ACyx" node="1MFSGJpr2Cl" resolve="b" />
         </node>
         <node concept="1UfqsA" id="1MFSGJppp7j" role="1U5zfT">
           <node concept="11ACyy" id="1MFSGJprFo9" role="1UfoCz">
-            <ref role="11ACyx" node="1MFSGJpr2C5" />
+            <ref role="11ACyx" node="1MFSGJpr2C5" resolve="a" />
           </node>
           <node concept="1U5_Ed" id="1MFSGJppp7l" role="1UfoCz">
-            <ref role="1U5_Ec" node="104dc5EbthM" />
+            <ref role="1U5_Ec" node="104dc5EbthM" resolve="GAP" />
           </node>
         </node>
       </node>
@@ -169,14 +169,14 @@
       </node>
       <node concept="1UfkGm" id="7xXCuh1D$pe" role="11AoXW">
         <node concept="11ACyy" id="7xXCuh1EkE4" role="1U5zfR">
-          <ref role="11ACyx" node="7xXCuh1EkDB" />
+          <ref role="11ACyx" node="7xXCuh1EkDB" resolve="b1" />
         </node>
         <node concept="1UfqsA" id="7xXCuh1D$p_" role="1U5zfT">
           <node concept="11ACyy" id="7xXCuh1EkDX" role="1UfoCz">
-            <ref role="11ACyx" node="7xXCuh1EkDn" />
+            <ref role="11ACyx" node="7xXCuh1EkDn" resolve="a1" />
           </node>
           <node concept="1U5_Ed" id="7xXCuh1D$pB" role="1UfoCz">
-            <ref role="1U5_Ec" node="6cjunGyyaJ9" />
+            <ref role="1U5_Ec" node="6cjunGyyaJ9" resolve="GAP" />
           </node>
         </node>
       </node>
@@ -197,7 +197,7 @@
       <node concept="1Uau1d" id="1MFSGJp8vhR" role="11AoXW">
         <node concept="1UfkGm" id="1MFSGJp8vib" role="1UfoCz">
           <node concept="11ACyy" id="1MFSGJp8viw" role="1U5zfR">
-            <ref role="11ACyx" node="7xXCuh1EkAz" />
+            <ref role="11ACyx" node="7xXCuh1EkAz" resolve="a2" />
           </node>
           <node concept="2IPVmt" id="1MFSGJp8vid" role="1U5zfT">
             <property role="2IPVms" value="2" />
@@ -208,7 +208,7 @@
             <property role="2IPVms" value="3" />
           </node>
           <node concept="11ACyy" id="1MFSGJp8viB" role="1U5zfR">
-            <ref role="11ACyx" node="7xXCuh1EkAN" />
+            <ref role="11ACyx" node="7xXCuh1EkAN" resolve="b2" />
           </node>
         </node>
       </node>
@@ -227,7 +227,7 @@
       <node concept="1Uau1d" id="1MFSGJp8viF" role="11AoXW">
         <node concept="1UfkGm" id="1MFSGJp8viG" role="1UfoCz">
           <node concept="11ACyy" id="1MFSGJp8vj3" role="1U5zfR">
-            <ref role="11ACyx" node="1MFSGJp8vcD" />
+            <ref role="11ACyx" node="1MFSGJp8vcD" resolve="a3" />
           </node>
           <node concept="2IPVmt" id="1MFSGJp8viI" role="1U5zfT">
             <property role="2IPVms" value="3" />
@@ -238,7 +238,7 @@
             <property role="2IPVms" value="4" />
           </node>
           <node concept="11ACyy" id="1MFSGJp8vja" role="1U5zfR">
-            <ref role="11ACyx" node="1MFSGJp8vcF" />
+            <ref role="11ACyx" node="1MFSGJp8vcF" resolve="b3" />
           </node>
         </node>
       </node>
@@ -257,7 +257,7 @@
       <node concept="1Uau1d" id="1MFSGJp8vjh" role="11AoXW">
         <node concept="1UfkGm" id="1MFSGJp8vji" role="1UfoCz">
           <node concept="11ACyy" id="1MFSGJp8vjD" role="1U5zfR">
-            <ref role="11ACyx" node="1MFSGJp8veZ" />
+            <ref role="11ACyx" node="1MFSGJp8veZ" resolve="a4" />
           </node>
           <node concept="2IPVmt" id="1MFSGJp8vjk" role="1U5zfT">
             <property role="2IPVms" value="4" />
@@ -268,7 +268,7 @@
             <property role="2IPVms" value="15" />
           </node>
           <node concept="11ACyy" id="1MFSGJp8vjK" role="1U5zfR">
-            <ref role="11ACyx" node="1MFSGJp8vf1" />
+            <ref role="11ACyx" node="1MFSGJp8vf1" resolve="b4" />
           </node>
         </node>
       </node>
@@ -286,40 +286,40 @@
         </node>
         <node concept="1UfpLS" id="6cjunGyyEVo" role="11ARNb">
           <node concept="11BOot" id="6cjunGyzgZl" role="1U5zfT">
-            <ref role="11BOos" node="7xXCuh1D$mP" />
+            <ref role="11BOos" node="7xXCuh1D$mP" resolve="initialFormula" />
             <node concept="11ACyy" id="7xXCuh1EkGo" role="11yxzb">
-              <ref role="11ACyx" node="6cjunGyyaLA" />
+              <ref role="11ACyx" node="6cjunGyyaLA" resolve="a" />
             </node>
             <node concept="11ACyy" id="7xXCuh1EkGz" role="11yxzb">
-              <ref role="11ACyx" node="6cjunGyyaLY" />
+              <ref role="11ACyx" node="6cjunGyyaLY" resolve="b" />
             </node>
           </node>
           <node concept="1Uau1c" id="1MFSGJp8vjV" role="1U5zfR">
             <node concept="11BOot" id="1MFSGJp8vkz" role="1UfoCz">
-              <ref role="11BOos" node="7xXCuh1D$vh" />
+              <ref role="11BOos" node="7xXCuh1D$vh" resolve="t1" />
               <node concept="11ACyy" id="1MFSGJp8vkY" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLA" />
+                <ref role="11ACyx" node="6cjunGyyaLA" resolve="a" />
               </node>
               <node concept="11ACyy" id="1MFSGJp8vl9" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLY" />
+                <ref role="11ACyx" node="6cjunGyyaLY" resolve="b" />
               </node>
             </node>
             <node concept="11BOot" id="1MFSGJp8vlf" role="1UfoCz">
-              <ref role="11BOos" node="1MFSGJp8vcC" />
+              <ref role="11BOos" node="1MFSGJp8vcC" resolve="t2" />
               <node concept="11ACyy" id="1MFSGJp8vlg" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLA" />
+                <ref role="11ACyx" node="6cjunGyyaLA" resolve="a" />
               </node>
               <node concept="11ACyy" id="1MFSGJp8vlh" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLY" />
+                <ref role="11ACyx" node="6cjunGyyaLY" resolve="b" />
               </node>
             </node>
             <node concept="11BOot" id="1MFSGJp8vlu" role="1UfoCz">
-              <ref role="11BOos" node="1MFSGJp8veY" />
+              <ref role="11BOos" node="1MFSGJp8veY" resolve="t3" />
               <node concept="11ACyy" id="1MFSGJp8vlv" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLA" />
+                <ref role="11ACyx" node="6cjunGyyaLA" resolve="a" />
               </node>
               <node concept="11ACyy" id="1MFSGJp8vlw" role="11yxzb">
-                <ref role="11ACyx" node="6cjunGyyaLY" />
+                <ref role="11ACyx" node="6cjunGyyaLY" resolve="b" />
               </node>
             </node>
           </node>
@@ -379,11 +379,11 @@
       <node concept="1U5apb" id="1MFSGJprTPN" role="11zN3m" />
       <node concept="1UfkGm" id="1MFSGJprTPO" role="11AoXW">
         <node concept="11ACyy" id="1MFSGJprTPP" role="1U5zfR">
-          <ref role="11ACyx" node="1MFSGJprTPL" />
+          <ref role="11ACyx" node="1MFSGJprTPL" resolve="b" />
         </node>
         <node concept="1UfqsA" id="1MFSGJprTPQ" role="1U5zfT">
           <node concept="11ACyy" id="1MFSGJprTPR" role="1UfoCz">
-            <ref role="11ACyx" node="1MFSGJprTPJ" />
+            <ref role="11ACyx" node="1MFSGJprTPJ" resolve="a" />
           </node>
           <node concept="1UbFQc" id="1MFSGJprTQe" role="1UfoCz" />
         </node>
diff --git a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke.mps b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke.mps
index 81224ab82..c890d117d 100644
--- a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke.mps
+++ b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke.mps
@@ -122,7 +122,7 @@
     <node concept="1U56EO" id="104dc5E4ctq" role="1U2RmC">
       <node concept="1U5ao_" id="104dc5E4zQ4" role="1U56ET">
         <node concept="1U5_Ed" id="104dc5E4Is4" role="1U5zfR">
-          <ref role="1U5_Ec" node="104dc5E499u" />
+          <ref role="1U5_Ec" node="104dc5E499u" resolve="aDeclaredConst" />
         </node>
         <node concept="2IPVmt" id="104dc5E4Isb" role="1U5zfT">
           <property role="2IPVms" value="9" />
@@ -132,7 +132,7 @@
     <node concept="1U56EO" id="104dc5E6un_" role="1U2RmC">
       <node concept="1U4LMg" id="104dc5E6uo4" role="1U56ET">
         <node concept="1U5_Ed" id="104dc5E6uoi" role="1U5zfR">
-          <ref role="1U5_Ec" node="104dc5E499u" />
+          <ref role="1U5_Ec" node="104dc5E499u" resolve="aDeclaredConst" />
         </node>
         <node concept="2IPVmt" id="104dc5E6uoq" role="1U5zfT">
           <property role="2IPVms" value="8" />
@@ -150,11 +150,11 @@
     <node concept="1U56EO" id="4tZ7POS58mr" role="1U2RmC">
       <node concept="35L7W5" id="4tZ7POS58n9" role="1U56ET">
         <node concept="1U5_Ed" id="4tZ7POS58nx" role="35L7Wp">
-          <ref role="1U5_Ec" node="4tZ7POS58lF" />
+          <ref role="1U5_Ec" node="4tZ7POS58lF" resolve="iteCond" />
         </node>
         <node concept="1UfkGm" id="4tZ7POS58nC" role="35L7Wu">
           <node concept="1U5_Ed" id="4tZ7POS58nU" role="1U5zfR">
-            <ref role="1U5_Ec" node="104dc5E499u" />
+            <ref role="1U5_Ec" node="104dc5E499u" resolve="aDeclaredConst" />
           </node>
           <node concept="2IPVmt" id="4tZ7POS58o2" role="1U5zfT">
             <property role="2IPVms" value="8" />
@@ -179,7 +179,7 @@
       <node concept="1U5aqE" id="6cjunGyBWnw" role="11zN3m" />
       <node concept="1UfqsA" id="6cjunGyCXa_" role="11AoXW">
         <node concept="11ACyy" id="6cjunGyCXaN" role="1UfoCz">
-          <ref role="11ACyx" node="6cjunGyBWng" />
+          <ref role="11ACyx" node="6cjunGyBWng" resolve="par1" />
         </node>
         <node concept="2IPVmt" id="6cjunGyCXb0" role="1UfoCz">
           <property role="2IPVms" value="1" />
@@ -193,9 +193,9 @@
     <node concept="1U56EO" id="6cjunGyBWm9" role="1U2RmC">
       <node concept="1UfkGm" id="6cjunGyBWqy" role="1U56ET">
         <node concept="11BOot" id="6cjunGyBWqL" role="1U5zfR">
-          <ref role="11BOos" node="6cjunGyBWmI" />
+          <ref role="11BOos" node="6cjunGyBWmI" resolve="foo" />
           <node concept="1U5_Ed" id="6cjunGyBWqX" role="11yxzb">
-            <ref role="1U5_Ec" node="6cjunGyBWm2" />
+            <ref role="1U5_Ec" node="6cjunGyBWm2" resolve="aConst" />
           </node>
         </node>
         <node concept="2IPVmt" id="6cjunGyBWmc" role="1U5zfT">
@@ -222,9 +222,9 @@
     <node concept="1U56EO" id="2l5A0OF1WWq" role="1U2RmC">
       <node concept="1UfkGm" id="2l5A0OF1WWr" role="1U56ET">
         <node concept="11BOot" id="2l5A0OF1WWs" role="1U5zfR">
-          <ref role="11BOos" node="2l5A0OF1WXc" />
+          <ref role="11BOos" node="2l5A0OF1WXc" resolve="foo" />
           <node concept="1U5_Ed" id="2l5A0OF1WWt" role="11yxzb">
-            <ref role="1U5_Ec" node="2l5A0OF1WWo" />
+            <ref role="1U5_Ec" node="2l5A0OF1WWo" resolve="aConst" />
           </node>
         </node>
         <node concept="2IPVmt" id="2l5A0OF1WWu" role="1U5zfT">
@@ -251,13 +251,13 @@
     <node concept="1U56EO" id="2l5A0OF69o0" role="1U2RmC">
       <node concept="1UfkGm" id="2l5A0OF69o1" role="1U56ET">
         <node concept="11BOot" id="2l5A0OF69o2" role="1U5zfR">
-          <ref role="11BOos" node="2l5A0OF69nT" />
+          <ref role="11BOos" node="2l5A0OF69nT" resolve="foo" />
           <node concept="1U5_Ed" id="2l5A0OF69o3" role="11yxzb">
-            <ref role="1U5_Ec" node="2l5A0OF69nX" />
+            <ref role="1U5_Ec" node="2l5A0OF69nX" resolve="aConst" />
           </node>
         </node>
         <node concept="1U5_Ed" id="2l5A0OF69om" role="1U5zfT">
-          <ref role="1U5_Ec" node="2l5A0OF69nX" />
+          <ref role="1U5_Ec" node="2l5A0OF69nX" resolve="aConst" />
         </node>
       </node>
     </node>
@@ -276,7 +276,7 @@
           <node concept="engXH" id="2_LXzlpuXeU" role="engYz">
             <property role="TrG5h" value="pred" />
             <node concept="mKvrX" id="6MrCApUnpto" role="engXD">
-              <ref role="mKvtK" node="2l5A0OF6OA6" />
+              <ref role="mKvtK" node="2l5A0OF6OA6" resolve="Nat" />
             </node>
           </node>
         </node>
@@ -286,14 +286,14 @@
       <property role="TrG5h" value="p" />
       <node concept="1U5apb" id="6MrCApUnpuB" role="1U56Ci" />
       <node concept="mKvrX" id="6MrCApUnpux" role="1U56Cg">
-        <ref role="mKvtK" node="2l5A0OF6OA6" />
+        <ref role="mKvtK" node="2l5A0OF6OA6" resolve="Nat" />
       </node>
     </node>
     <node concept="1U56EO" id="6MrCApUnpvh" role="1U2RmC">
       <node concept="11BOot" id="6MrCApUnpw7" role="1U56ET">
-        <ref role="11BOos" node="6MrCApUnptW" />
+        <ref role="11BOos" node="6MrCApUnptW" resolve="p" />
         <node concept="mYNaY" id="6MrCApUpU$s" role="11yxzb">
-          <ref role="mYNcP" node="2l5A0OF6PZv" />
+          <ref role="mYNcP" node="2l5A0OF6PZv" resolve="zero" />
         </node>
       </node>
     </node>
@@ -302,23 +302,23 @@
         <node concept="11ARNU" id="6MrCApUpU_Z" role="11ARNT">
           <property role="TrG5h" value="x" />
           <node concept="mKvrX" id="6MrCApUpUAg" role="11ARNN">
-            <ref role="mKvtK" node="2l5A0OF6OA6" />
+            <ref role="mKvtK" node="2l5A0OF6OA6" resolve="Nat" />
           </node>
         </node>
         <node concept="1UfpLS" id="6MrCApUpUAw" role="11ARNb">
           <node concept="11BOot" id="6MrCApUpUAI" role="1U5zfR">
-            <ref role="11BOos" node="6MrCApUnptW" />
+            <ref role="11BOos" node="6MrCApUnptW" resolve="p" />
             <node concept="mZ0x0" id="6MrCApUqOlf" role="11yxzb">
-              <ref role="mZ0z7" node="2_LXzlpuXeU" />
+              <ref role="mZ0z7" node="2_LXzlpuXeU" resolve="pred" />
               <node concept="11ACyy" id="7xXCuh1D$hA" role="mWesK">
-                <ref role="11ACyx" node="6MrCApUpU_Z" />
+                <ref role="11ACyx" node="6MrCApUpU_Z" resolve="x" />
               </node>
             </node>
           </node>
           <node concept="11BOot" id="6MrCApUrQjO" role="1U5zfT">
-            <ref role="11BOos" node="6MrCApUnptW" />
+            <ref role="11BOos" node="6MrCApUnptW" resolve="p" />
             <node concept="11ACyy" id="6MrCApUrQk2" role="11yxzb">
-              <ref role="11ACyx" node="6MrCApUpU_Z" />
+              <ref role="11ACyx" node="6MrCApUpU_Z" resolve="x" />
             </node>
           </node>
         </node>
@@ -330,13 +330,13 @@
           <node concept="11ARNU" id="6MrCApUrQmt" role="11ARNT">
             <property role="TrG5h" value="x" />
             <node concept="mKvrX" id="6MrCApUrQmI" role="11ARNN">
-              <ref role="mKvtK" node="2l5A0OF6OA6" />
+              <ref role="mKvtK" node="2l5A0OF6OA6" resolve="Nat" />
             </node>
           </node>
           <node concept="11BOot" id="6MrCApUrQn5" role="11ARNb">
-            <ref role="11BOos" node="6MrCApUnptW" />
+            <ref role="11BOos" node="6MrCApUnptW" resolve="p" />
             <node concept="11ACyy" id="1MFSGJpf4Dr" role="11yxzb">
-              <ref role="11ACyx" node="6MrCApUrQmt" />
+              <ref role="11ACyx" node="6MrCApUrQmt" resolve="x" />
             </node>
           </node>
         </node>
@@ -359,17 +359,17 @@
       <node concept="1U5aqE" id="1MFSGJpcpGc" role="11zN3m" />
       <node concept="1UfqsA" id="1MFSGJpcpGd" role="11AoXW">
         <node concept="11ACyy" id="1MFSGJpcpGe" role="1UfoCz">
-          <ref role="11ACyx" node="1MFSGJpcpGa" />
+          <ref role="11ACyx" node="1MFSGJpcpGa" resolve="par1" />
         </node>
         <node concept="11ACyy" id="1MFSGJpcpHD" role="1UfoCz">
-          <ref role="11ACyx" node="1MFSGJpcpH5" />
+          <ref role="11ACyx" node="1MFSGJpcpH5" resolve="par2" />
         </node>
       </node>
     </node>
     <node concept="1U56EO" id="1MFSGJpcpGk" role="1U2RmC">
       <node concept="1UfkGm" id="1MFSGJpcpGl" role="1U56ET">
         <node concept="11BOot" id="1MFSGJpcpGm" role="1U5zfR">
-          <ref role="11BOos" node="1MFSGJpcpG9" />
+          <ref role="11BOos" node="1MFSGJpcpG9" resolve="add" />
           <node concept="2IPVmt" id="1MFSGJpcpIk" role="11yxzb">
             <property role="2IPVms" value="1" />
           </node>
@@ -399,13 +399,13 @@
         </node>
         <node concept="1UfkGm" id="1MFSGJpdnnj" role="11ARNb">
           <node concept="11BOot" id="1MFSGJpdnnk" role="1U5zfR">
-            <ref role="11BOos" node="1MFSGJpdnnb" />
+            <ref role="11BOos" node="1MFSGJpdnnb" resolve="foo" />
             <node concept="11ACyy" id="1MFSGJpdnoM" role="11yxzb">
-              <ref role="11ACyx" node="1MFSGJpdno4" />
+              <ref role="11ACyx" node="1MFSGJpdno4" resolve="p" />
             </node>
           </node>
           <node concept="11ACyy" id="7vEzmJ3BNV$" role="1U5zfT">
-            <ref role="11ACyx" node="1MFSGJpdno4" />
+            <ref role="11ACyx" node="1MFSGJpdno4" resolve="p" />
           </node>
         </node>
       </node>
@@ -432,31 +432,31 @@
     <node concept="1U2Rm_" id="2FrZhHbXF9T" role="1U2RmC">
       <property role="TrG5h" value="x" />
       <node concept="mKvrX" id="2FrZhHbXFa9" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHbXF9d" />
+        <ref role="mKvtK" node="2FrZhHbXF9d" resolve="Enum" />
       </node>
     </node>
     <node concept="1U2Rm_" id="2FrZhHbXFaf" role="1U2RmC">
       <property role="TrG5h" value="y" />
       <node concept="mKvrX" id="2FrZhHbXFag" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHbXF9d" />
+        <ref role="mKvtK" node="2FrZhHbXF9d" resolve="Enum" />
       </node>
     </node>
     <node concept="1U2Rm_" id="2FrZhHbXFav" role="1U2RmC">
       <property role="TrG5h" value="z" />
       <node concept="mKvrX" id="2FrZhHbXFaw" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHbXF9d" />
+        <ref role="mKvtK" node="2FrZhHbXF9d" resolve="Enum" />
       </node>
     </node>
     <node concept="1U56EO" id="2FrZhHbXFb0" role="1U2RmC">
       <node concept="1xbkZQ" id="2FrZhHbYMgD" role="1U56ET">
         <node concept="1U5_Ed" id="2FrZhHbYMgN" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHbXF9T" />
+          <ref role="1U5_Ec" node="2FrZhHbXF9T" resolve="x" />
         </node>
         <node concept="1U5_Ed" id="2FrZhHbYMgV" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHbXFaf" />
+          <ref role="1U5_Ec" node="2FrZhHbXFaf" resolve="y" />
         </node>
         <node concept="1U5_Ed" id="2FrZhHbYMh7" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHbXFav" />
+          <ref role="1U5_Ec" node="2FrZhHbXFav" resolve="z" />
         </node>
       </node>
     </node>
@@ -482,40 +482,40 @@
     <node concept="1U2Rm_" id="2FrZhHc0DBX" role="1U2RmC">
       <property role="TrG5h" value="x" />
       <node concept="mKvrX" id="2FrZhHc0DBY" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHc0DBT" />
+        <ref role="mKvtK" node="2FrZhHc0DBT" resolve="Enum" />
       </node>
     </node>
     <node concept="1U2Rm_" id="2FrZhHc0DBZ" role="1U2RmC">
       <property role="TrG5h" value="y" />
       <node concept="mKvrX" id="2FrZhHc0DC0" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHc0DBT" />
+        <ref role="mKvtK" node="2FrZhHc0DBT" resolve="Enum" />
       </node>
     </node>
     <node concept="1U2Rm_" id="2FrZhHc0DC1" role="1U2RmC">
       <property role="TrG5h" value="z" />
       <node concept="mKvrX" id="2FrZhHc0DC2" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHc0DBT" />
+        <ref role="mKvtK" node="2FrZhHc0DBT" resolve="Enum" />
       </node>
     </node>
     <node concept="1U2Rm_" id="2FrZhHc0DC3" role="1U2RmC">
       <property role="TrG5h" value="w" />
       <node concept="mKvrX" id="2FrZhHc0DC4" role="1U56Fq">
-        <ref role="mKvtK" node="2FrZhHc0DBT" />
+        <ref role="mKvtK" node="2FrZhHc0DBT" resolve="Enum" />
       </node>
     </node>
     <node concept="1U56EO" id="2FrZhHc0DC5" role="1U2RmC">
       <node concept="1xbkZQ" id="2FrZhHc0DC6" role="1U56ET">
         <node concept="1U5_Ed" id="2FrZhHc0DC7" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHc0DBX" />
+          <ref role="1U5_Ec" node="2FrZhHc0DBX" resolve="x" />
         </node>
         <node concept="1U5_Ed" id="2FrZhHc0DC8" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHc0DBZ" />
+          <ref role="1U5_Ec" node="2FrZhHc0DBZ" resolve="y" />
         </node>
         <node concept="1U5_Ed" id="2FrZhHc0DC9" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHc0DC1" />
+          <ref role="1U5_Ec" node="2FrZhHc0DC1" resolve="z" />
         </node>
         <node concept="1U5_Ed" id="2FrZhHc0DCw" role="1UfoCz">
-          <ref role="1U5_Ec" node="2FrZhHc0DC3" />
+          <ref role="1U5_Ec" node="2FrZhHc0DC3" resolve="w" />
         </node>
       </node>
     </node>
diff --git a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke_tests@tests.mps b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke_tests@tests.mps
index 0f1a15138..0b90bf0aa 100644
--- a/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke_tests@tests.mps
+++ b/code/languages/com.mbeddr.formal.smt/tests/test.com.mbeddr.formal.smtlib/models/_010_smoke_tests@tests.mps
@@ -81,6 +81,15 @@
         <child id="1205770614681" name="actualArgument" index="2XxRq1" />
       </concept>
     </language>
+    <language id="446c26eb-2b7b-4bf0-9b35-f83fa582753e" name="jetbrains.mps.lang.modelapi">
+      <concept id="361130699826193248" name="jetbrains.mps.lang.modelapi.structure.ModelPointer" flags="ng" index="1dCxOl">
+        <property id="1863527487546097494" name="modelId" index="1XweGQ" />
+        <child id="679099339649067980" name="name" index="1j$8Uc" />
+      </concept>
+      <concept id="679099339649053840" name="jetbrains.mps.lang.modelapi.structure.ModelName" flags="ng" index="1j_P7g">
+        <property id="679099339649053841" name="value" index="1j_P7h" />
+      </concept>
+    </language>
     <language id="f61473f9-130f-42f6-b98d-6c438812c2f6" name="jetbrains.mps.baseLanguage.unitTest">
       <concept id="8427750732757990717" name="jetbrains.mps.baseLanguage.unitTest.structure.BinaryAssert" flags="nn" index="3tpDYu">
         <child id="8427750732757990725" name="actual" index="3tpDZA" />
@@ -95,12 +104,14 @@
       </concept>
     </language>
     <language id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel">
-      <concept id="559557797393017698" name="jetbrains.mps.lang.smodel.structure.ModelReferenceExpression" flags="nn" index="BaHAS">
-        <property id="559557797393021807" name="stereotype" index="BaGAP" />
-        <property id="559557797393017702" name="name" index="BaHAW" />
-        <child id="1423104411233404408" name="repo" index="up2gk" />
+      <concept id="4065387505485742666" name="jetbrains.mps.lang.smodel.structure.ModelPointer_ResolveOperation" flags="ng" index="2yCiCJ" />
+      <concept id="4065387505485742749" name="jetbrains.mps.lang.smodel.structure.AbstractPointerResolveOperation" flags="ng" index="2yCiFS">
+        <child id="3648723375513868575" name="repositoryArg" index="Vysub" />
       </concept>
       <concept id="1143226024141" name="jetbrains.mps.lang.smodel.structure.SModelType" flags="in" index="H_c77" />
+      <concept id="1863527487546129879" name="jetbrains.mps.lang.smodel.structure.ModelPointerExpression" flags="ng" index="1Xw6AR">
+        <child id="1863527487546132519" name="modelRef" index="1XwpL7" />
+      </concept>
     </language>
     <language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
       <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
@@ -121,13 +132,21 @@
           <node concept="3cpWsn" id="1MFSGJpcsau" role="3cpWs9">
             <property role="TrG5h" value="m" />
             <node concept="H_c77" id="1MFSGJpcsav" role="1tU5fm" />
-            <node concept="BaHAS" id="1MFSGJpcsaw" role="33vP2m">
-              <property role="BaHAW" value="test.com.mbeddr.formal.smtlib._010_smoke" />
-              <property role="BaGAP" value="" />
-              <node concept="2OqwBi" id="1TZST$TIba6" role="up2gk">
-                <node concept="1jxXqW" id="1TZST$TIaYH" role="2Oq$k0" />
-                <node concept="liA8E" id="1TZST$TIbzW" role="2OqNvi">
-                  <ref role="37wK5l" to="z1c3:~Project.getRepository()" resolve="getRepository" />
+            <node concept="2OqwBi" id="2X_iJQiws9h" role="33vP2m">
+              <node concept="1Xw6AR" id="8wvJyaWmH4" role="2Oq$k0">
+                <node concept="1dCxOl" id="8wvJyaWmH5" role="1XwpL7">
+                  <property role="1XweGQ" value="r:84fe9965-39f2-43f2-b282-99ccfef57495" />
+                  <node concept="1j_P7g" id="8wvJyaWmH6" role="1j$8Uc">
+                    <property role="1j_P7h" value="test.com.mbeddr.formal.smtlib._010_smoke" />
+                  </node>
+                </node>
+              </node>
+              <node concept="2yCiCJ" id="2X_iJQiwsxJ" role="2OqNvi">
+                <node concept="2OqwBi" id="2X_iJQiwsEN" role="Vysub">
+                  <node concept="1jxXqW" id="2X_iJQiwsEO" role="2Oq$k0" />
+                  <node concept="liA8E" id="2X_iJQiwsEP" role="2OqNvi">
+                    <ref role="37wK5l" to="z1c3:~Project.getRepository()" resolve="getRepository" />
+                  </node>
                 </node>
               </node>
             </node>
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/com.mbeddr.formal.safety.tutorial.msd b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/com.mbeddr.formal.safety.tutorial.msd
index a20d45a0b..5f0d9550d 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/com.mbeddr.formal.safety.tutorial.msd
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/com.mbeddr.formal.safety.tutorial.msd
@@ -103,6 +103,7 @@
     <language slang="l:f3061a53-9226-4cc5-a443-f952ceaf5816:jetbrains.mps.baseLanguage" version="12" />
     <language slang="l:fd392034-7849-419d-9071-12563d152375:jetbrains.mps.baseLanguage.closures" version="0" />
     <language slang="l:83888646-71ce-4f1c-9c53-c54016f6ad4f:jetbrains.mps.baseLanguage.collections" version="1" />
+    <language slang="l:760a0a8c-eabb-4521-8bfd-65db761a9ba3:jetbrains.mps.baseLanguage.logging" version="0" />
     <language slang="l:479c7a8c-02f9-43b5-9139-d910cb22f298:jetbrains.mps.core.xml" version="0" />
     <language slang="l:ceab5195-25ea-4f22-9b92-103b95ca8c0c:jetbrains.mps.lang.core" version="2" />
     <language slang="l:1839bec5-cea6-41df-b9e0-c405ff35c41e:jetbrains.mps.lang.editor.imageGen" version="0" />
@@ -121,6 +122,8 @@
     <module reference="e1b41d7d-269e-4a91-a7d8-91bd657028d7(com.fasten.safety.doc2word)" version="0" />
     <module reference="83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)" version="0" />
     <module reference="e6e482a5-282a-4c6d-862a-311affd0586b(com.mbeddr.formal.safety.argument.jira_integration)" version="0" />
+    <module reference="83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)" version="0" />
+    <module reference="e6e482a5-282a-4c6d-862a-311affd0586b(com.mbeddr.formal.safety.argument.jira_integration)" version="0" />
     <module reference="04d81d12-7048-4552-9a53-86a271c0f094(com.mbeddr.formal.safety.argument.visualisation)" version="0" />
     <module reference="e8a04d94-4307-4f88-95a2-25f7c4f39437(com.mbeddr.formal.safety.gsn)" version="0" />
     <module reference="676b5323-9c6d-4b8d-a4fc-5d159c3d8aed(com.mbeddr.formal.safety.gsn.patterns.lib)" version="0" />
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_010_features._080_assurance_cases_linked_to_jira.mps b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_010_features._080_assurance_cases_linked_to_jira.mps
new file mode 100644
index 000000000..75e8e1e34
--- /dev/null
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_010_features._080_assurance_cases_linked_to_jira.mps
@@ -0,0 +1,398 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<model ref="r:c96b4f15-9a2f-4e1a-801a-5f4a74c6f75a(_010_features._080_assurance_cases_linked_to_jira)">
+  <persistence version="9" />
+  <languages>
+    <use id="04d81d12-7048-4552-9a53-86a271c0f094" name="com.mbeddr.formal.safety.argument.visualisation" version="0" />
+    <use id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage" version="12" />
+    <devkit ref="58430e3c-3d97-455c-a27e-8eeba7f8513e(fasten.safety.gsn.artefacts)" />
+  </languages>
+  <imports>
+    <import index="7kfd" ref="r:3707116d-ad40-43b6-b419-75e9e4026c1b(com.mbeddr.formal.safety.argument.jira_integration.util)" />
+  </imports>
+  <registry>
+    <language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
+      <concept id="1116615150612" name="jetbrains.mps.baseLanguage.structure.ClassifierClassExpression" flags="nn" index="3VsKOn">
+        <reference id="1116615189566" name="classifier" index="3VsUkX" />
+      </concept>
+    </language>
+    <language id="04d81d12-7048-4552-9a53-86a271c0f094" name="com.mbeddr.formal.safety.argument.visualisation">
+      <concept id="4644663984576230932" name="com.mbeddr.formal.safety.argument.visualisation.structure.GoalStructureTreeMapConfig" flags="ng" index="1lK_Xt">
+        <property id="1602534339391249114" name="width" index="2xYCaB" />
+        <property id="1602534339391249402" name="height" index="2xYCe7" />
+        <reference id="4644663984576989991" name="goal" index="1lHy9I" />
+        <child id="1736445178716231441" name="builder" index="2TiK2x" />
+      </concept>
+    </language>
+    <language id="92d2ea16-5a42-4fdf-a676-c7604efe3504" name="de.slisson.mps.richtext">
+      <concept id="2557074442922380897" name="de.slisson.mps.richtext.structure.Text" flags="ng" index="19SGf9">
+        <child id="2557074442922392302" name="words" index="19SJt6" />
+      </concept>
+      <concept id="2557074442922438156" name="de.slisson.mps.richtext.structure.Word" flags="ng" index="19SUe$">
+        <property id="2557074442922438158" name="escapedValue" index="19SUeA" />
+      </concept>
+    </language>
+    <language id="e6e482a5-282a-4c6d-862a-311affd0586b" name="com.mbeddr.formal.safety.argument.jira_integration">
+      <concept id="2898135657937856261" name="com.mbeddr.formal.safety.argument.jira_integration.structure.JiraReferenceAttribute" flags="ng" index="2avPw3">
+        <child id="2898135657937865904" name="jiraIssue" index="2avVeQ" />
+      </concept>
+    </language>
+    <language id="fde86f49-830f-414f-9c22-2a9e300eaba6" name="com.mpsbasics.jira">
+      <concept id="3117513243527540113" name="com.mpsbasics.jira.structure.JiraAccessConfig" flags="ng" index="WiOLm">
+        <property id="1219686309520662240" name="forceAnnonymous" index="2gzYNs" />
+      </concept>
+      <concept id="277038075108553068" name="com.mpsbasics.jira.structure.JiraIssueReference" flags="ng" index="1rK$R5">
+        <property id="277038075108561029" name="issueUrl" index="1rKEKG" />
+      </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">
+        <child id="5169995583184591170" name="smodelAttribute" index="lGtFl" />
+      </concept>
+      <concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
+        <property id="1169194664001" name="name" index="TrG5h" />
+      </concept>
+    </language>
+    <language id="8ca79d43-eb45-4791-bdd4-0d6130ff895b" name="de.itemis.mps.editor.diagram.layout">
+      <concept id="6720495385597071406" name="de.itemis.mps.editor.diagram.layout.structure.Layout_Box" flags="ng" index="gqqVs">
+        <property id="6720495385597071504" name="bounds_height" index="gqqTy" />
+        <property id="6720495385597071502" name="bounds_y" index="gqqTW" />
+        <property id="6720495385597071503" name="bounds_width" index="gqqTX" />
+        <property id="6720495385597071501" name="bounds_x" index="gqqTZ" />
+        <property id="4583510071007917016" name="transform" index="TgtnS" />
+      </concept>
+      <concept id="2319506556913310852" name="de.itemis.mps.editor.diagram.layout.structure.Layout_Connection" flags="ng" index="2VclpC">
+        <child id="2319506556913311101" name="anchors" index="2Vcluh" />
+        <child id="4767615435799372763" name="labels" index="3ul5Gx" />
+      </concept>
+      <concept id="2319506556913310727" name="de.itemis.mps.editor.diagram.layout.structure.Point" flags="ng" index="2VclrF">
+        <property id="2319506556913310861" name="x" index="2Vclpx" />
+        <property id="2319506556913310863" name="y" index="2Vclpz" />
+      </concept>
+      <concept id="8963411245960991886" name="de.itemis.mps.editor.diagram.layout.structure.LayoutMap" flags="ng" index="37mRI7">
+        <child id="8963411245960991904" name="entries" index="37mRID" />
+      </concept>
+      <concept id="8963411245960991903" name="de.itemis.mps.editor.diagram.layout.structure.LayoutMapEntry" flags="ng" index="37mRIm">
+        <property id="8963411245960998400" name="key" index="37mO49" />
+        <child id="8963411245960998404" name="value" index="37mO4d" />
+      </concept>
+      <concept id="4767615435799372731" name="de.itemis.mps.editor.diagram.layout.structure.Layout_EdgeLabel" flags="ng" index="3ul5H1">
+        <child id="4767615435799372761" name="position" index="3ul5Gz" />
+      </concept>
+      <concept id="3253043142928125505" name="de.itemis.mps.editor.diagram.layout.structure.RelativePosition" flags="ng" index="3wpmZ1">
+        <child id="3253043142928125557" name="referencePoint" index="3wpmZP" />
+        <child id="3253043142928125559" name="offset" index="3wpmZR" />
+      </concept>
+    </language>
+    <language id="83ed2dfe-f724-46cc-852a-dce086daee3f" name="com.mbeddr.formal.base">
+      <concept id="7402587364850275469" name="com.mbeddr.formal.base.structure.IAttributeContainer" flags="ng" index="2U2l5L">
+        <child id="7402587364850275470" name="attributes" index="2U2l5M" />
+      </concept>
+      <concept id="3687474483974639519" name="com.mbeddr.formal.base.structure.GenericAttributeAnnotationProviderBase" flags="ng" index="2Wz8ku">
+        <property id="3687474483974749023" name="attributeConceptNodeID" index="2Wzj7u" />
+      </concept>
+      <concept id="3687474483974128093" name="com.mbeddr.formal.base.structure.IAnnotationProvidersContainer" flags="ng" index="2WHcHs">
+        <child id="3687474483974128095" name="annotationProviders" index="2WHcHu" />
+      </concept>
+    </language>
+    <language id="e8a04d94-4307-4f88-95a2-25f7c4f39437" name="com.mbeddr.formal.safety.gsn">
+      <concept id="4422827436158313084" name="com.mbeddr.formal.safety.gsn.structure.GenericGSNAttributeAnnotationProvider" flags="ng" index="26s6xy" />
+      <concept id="4266958635905474024" name="com.mbeddr.formal.safety.gsn.structure.Solution" flags="ng" index="2vmhmH" />
+      <concept id="4266958635905267565" name="com.mbeddr.formal.safety.gsn.structure.Goal" flags="ng" index="2vn7WC" />
+      <concept id="4266958635905267510" name="com.mbeddr.formal.safety.gsn.structure.GoalStructure" flags="ng" index="2vn7XN">
+        <child id="4266958635905772385" name="connections" index="2vhqc$" />
+        <child id="4266958635905277632" name="content" index="2vn1q5" />
+      </concept>
+      <concept id="4266958635905286484" name="com.mbeddr.formal.safety.gsn.structure.GoalStructureElementBase" flags="ng" index="2vnc$h">
+        <child id="4266958635905312315" name="text" index="2vnaTY" />
+      </concept>
+      <concept id="2525617932486527053" name="com.mbeddr.formal.safety.gsn.structure.GoalStructureConnectionBase" flags="ng" index="3VeShH">
+        <reference id="2525617932486527189" name="source" index="3VeSjP" />
+        <reference id="2525617932486527190" name="target" index="3VeSjQ" />
+      </concept>
+      <concept id="2525617932486533707" name="com.mbeddr.formal.safety.gsn.structure.SupportedByConnection" flags="ng" index="3VeUTF" />
+    </language>
+  </registry>
+  <node concept="2vn7XN" id="3h2Izualob3">
+    <property role="TrG5h" value="_100_Known_Issues" />
+    <node concept="2vn7WC" id="3h2Izualob4" role="2vn1q5">
+      <property role="TrG5h" value="G01" />
+      <node concept="19SGf9" id="3h2Izualobf" role="2vnaTY">
+        <node concept="19SUe$" id="3h2Izualobw" role="19SJt6">
+          <property role="19SUeA" value="All known issues have &#10;been addressed." />
+        </node>
+      </node>
+    </node>
+    <node concept="37mRI7" id="3h2Izualob5" role="lGtFl">
+      <node concept="37mRIm" id="3h2Izualobh" role="37mRID">
+        <property role="37mO49" value="1639692281461090030" />
+        <node concept="gqqVs" id="3h2Izualobz" role="37mO4d">
+          <property role="gqqTZ" value="233.0" />
+          <property role="gqqTW" value="23.0" />
+          <property role="gqqTX" value="120.0" />
+          <property role="gqqTy" value="80.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobi" role="37mRID">
+        <property role="37mO49" value="1639692281461440660" />
+        <node concept="gqqVs" id="3h2Izualob$" role="37mO4d">
+          <property role="gqqTZ" value="119.0" />
+          <property role="gqqTW" value="173.0" />
+          <property role="gqqTX" value="118.0" />
+          <property role="gqqTy" value="80.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobj" role="37mRID">
+        <property role="37mO49" value="1639692281461705132" />
+        <node concept="gqqVs" id="3h2Izualob_" role="37mO4d">
+          <property role="gqqTX" value="118.0" />
+          <property role="gqqTy" value="80.0" />
+          <property role="gqqTZ" value="254.0" />
+          <property role="gqqTW" value="173.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobk" role="37mRID">
+        <property role="37mO49" value="1639692281461705279" />
+        <node concept="gqqVs" id="3h2IzualobA" role="37mO4d">
+          <property role="gqqTZ" value="20.0" />
+          <property role="gqqTW" value="25.0" />
+          <property role="gqqTX" value="115.0" />
+          <property role="gqqTy" value="94.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobl" role="37mRID">
+        <property role="37mO49" value="1639692281461705115" />
+        <node concept="2VclpC" id="3h2IzualobB" role="37mO4d">
+          <node concept="2VclrF" id="3h2IzualobJ" role="2Vcluh">
+            <property role="2Vclpx" value="293.1014399697487" />
+            <property role="2Vclpz" value="141.33702082946704" />
+          </node>
+          <node concept="2VclrF" id="3h2IzualobK" role="2Vcluh">
+            <property role="2Vclpx" value="200.33702082946704" />
+            <property role="2Vclpz" value="141.33702082946704" />
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobm" role="37mRID">
+        <property role="37mO49" value="1639692281461705590" />
+        <node concept="gqqVs" id="3h2IzualobC" role="37mO4d">
+          <property role="gqqTZ" value="393.0" />
+          <property role="gqqTW" value="174.0" />
+          <property role="gqqTX" value="116.0" />
+          <property role="gqqTy" value="94.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izualobn" role="37mRID">
+        <property role="37mO49" value="1639692281461705732" />
+        <node concept="2VclpC" id="3h2IzualobD" role="37mO4d">
+          <node concept="2VclrF" id="3h2IzualobL" role="2Vcluh">
+            <property role="2Vclpx" value="293.0" />
+            <property role="2Vclpz" value="142.0" />
+          </node>
+          <node concept="2VclrF" id="3h2IzualobM" role="2Vcluh">
+            <property role="2Vclpx" value="470.1016657177453" />
+            <property role="2Vclpz" value="142.0" />
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh4B" role="37mRID">
+        <property role="37mO49" value="3765776986141983428" />
+        <node concept="gqqVs" id="3h2Izuaoh4A" role="37mO4d">
+          <property role="gqqTZ" value="35.0" />
+          <property role="gqqTW" value="12.000100000000003" />
+          <property role="gqqTX" value="190.0" />
+          <property role="gqqTy" value="75.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh4D" role="37mRID">
+        <property role="37mO49" value="3765776986141983430" />
+        <node concept="gqqVs" id="3h2Izuaoh4C" role="37mO4d">
+          <property role="gqqTZ" value="50.0" />
+          <property role="gqqTW" value="215.0" />
+          <property role="gqqTX" value="180.0" />
+          <property role="gqqTy" value="107.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh4F" role="37mRID">
+        <property role="37mO49" value="3765776986141983432" />
+        <node concept="gqqVs" id="3h2Izuaoh4E" role="37mO4d">
+          <property role="gqqTZ" value="258.0" />
+          <property role="gqqTW" value="215.0" />
+          <property role="gqqTX" value="188.0" />
+          <property role="gqqTy" value="107.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh4H" role="37mRID">
+        <property role="37mO49" value="3765776986141983433" />
+        <node concept="gqqVs" id="3h2Izuaoh4G" role="37mO4d">
+          <property role="gqqTZ" value="-23.0" />
+          <property role="gqqTW" value="40.0" />
+          <property role="gqqTX" value="228.0" />
+          <property role="gqqTy" value="128.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh4J" role="37mRID">
+        <property role="37mO49" value="3765776986141983436" />
+        <node concept="gqqVs" id="3h2Izuaoh4I" role="37mO4d">
+          <property role="gqqTZ" value="474.0" />
+          <property role="gqqTW" value="215.0" />
+          <property role="gqqTX" value="198.0" />
+          <property role="gqqTy" value="128.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh5i" role="37mRID">
+        <property role="37mO49" value="3765776986141983434" />
+        <node concept="2VclpC" id="3h2Izuaoh5h" role="37mO4d">
+          <node concept="2VclrF" id="3h2Izuaoh8t" role="2Vcluh">
+            <property role="2Vclpx" value="263" />
+            <property role="2Vclpz" value="102" />
+          </node>
+          <node concept="2VclrF" id="3h2Izuaoh8u" role="2Vcluh">
+            <property role="2Vclpx" value="213" />
+            <property role="2Vclpz" value="113" />
+          </node>
+          <node concept="3ul5H1" id="3h2Izuaoh8v" role="3ul5Gx">
+            <node concept="3wpmZ1" id="3h2Izuaoh8w" role="3ul5Gz">
+              <node concept="2VclrF" id="3h2Izuaoh8x" role="3wpmZR">
+                <property role="2Vclpx" value="0" />
+                <property role="2Vclpz" value="0" />
+              </node>
+              <node concept="2VclrF" id="3h2Izuaoh8y" role="3wpmZP">
+                <property role="2Vclpx" value="263" />
+                <property role="2Vclpz" value="102" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh5m" role="37mRID">
+        <property role="37mO49" value="3765776986141983435" />
+        <node concept="2VclpC" id="3h2Izuaoh5l" role="37mO4d">
+          <node concept="2VclrF" id="3h2Izuaoh8h" role="2Vcluh">
+            <property role="2Vclpx" value="360" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="2VclrF" id="3h2Izuaoh8i" role="2Vcluh">
+            <property role="2Vclpx" value="351" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="3ul5H1" id="3h2Izuaoh8j" role="3ul5Gx">
+            <node concept="3wpmZ1" id="3h2Izuaoh8k" role="3ul5Gz">
+              <node concept="2VclrF" id="3h2Izuaoh8l" role="3wpmZR">
+                <property role="2Vclpx" value="0" />
+                <property role="2Vclpz" value="0" />
+              </node>
+              <node concept="2VclrF" id="3h2Izuaoh8m" role="3wpmZP">
+                <property role="2Vclpx" value="351" />
+                <property role="2Vclpz" value="185" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh5q" role="37mRID">
+        <property role="37mO49" value="3765776986141983437" />
+        <node concept="2VclpC" id="3h2Izuaoh5p" role="37mO4d">
+          <node concept="2VclrF" id="3h2Izuaoh8n" role="2Vcluh">
+            <property role="2Vclpx" value="360" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="2VclrF" id="3h2Izuaoh8o" role="2Vcluh">
+            <property role="2Vclpx" value="572" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="3ul5H1" id="3h2Izuaoh8p" role="3ul5Gx">
+            <node concept="3wpmZ1" id="3h2Izuaoh8q" role="3ul5Gz">
+              <node concept="2VclrF" id="3h2Izuaoh8r" role="3wpmZR">
+                <property role="2Vclpx" value="0" />
+                <property role="2Vclpz" value="0" />
+              </node>
+              <node concept="2VclrF" id="3h2Izuaoh8s" role="3wpmZP">
+                <property role="2Vclpx" value="572" />
+                <property role="2Vclpz" value="185" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2Izuaoh89" role="37mRID">
+        <property role="37mO49" value="3765776986141983431" />
+        <node concept="2VclpC" id="3h2Izuaoh8a" role="37mO4d">
+          <node concept="2VclrF" id="3h2Izuaoh8b" role="2Vcluh">
+            <property role="2Vclpx" value="360" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="2VclrF" id="3h2Izuaoh8c" role="2Vcluh">
+            <property role="2Vclpx" value="139" />
+            <property role="2Vclpz" value="185" />
+          </node>
+          <node concept="3ul5H1" id="3h2Izuaoh8d" role="3ul5Gx">
+            <node concept="3wpmZ1" id="3h2Izuaoh8e" role="3ul5Gz">
+              <node concept="2VclrF" id="3h2Izuaoh8f" role="3wpmZR">
+                <property role="2Vclpx" value="0" />
+                <property role="2Vclpz" value="0" />
+              </node>
+              <node concept="2VclrF" id="3h2Izuaoh8g" role="3wpmZP">
+                <property role="2Vclpx" value="139" />
+                <property role="2Vclpz" value="185" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37mRIm" id="3h2IzuazAkX" role="37mRID">
+        <property role="37mO49" value="3765776986145708545" />
+        <node concept="gqqVs" id="3h2IzuazAkW" role="37mO4d">
+          <property role="gqqTZ" value="12.0" />
+          <property role="gqqTW" value="135.00029836425782" />
+          <property role="gqqTX" value="236.0" />
+          <property role="gqqTy" value="75.0" />
+          <property role="TgtnS" value="1.0;0.0;0.0;1.0;0.0;0.0" />
+        </node>
+      </node>
+    </node>
+    <node concept="26s6xy" id="3h2Izualobe" role="2WHcHu">
+      <property role="2Wzj7u" value="1639692281461329473" />
+    </node>
+    <node concept="2vmhmH" id="3h2Izuaz_C1" role="2vn1q5">
+      <property role="TrG5h" value="S01" />
+      <node concept="2avPw3" id="3h2Izuaz_X6" role="2U2l5M">
+        <node concept="1rK$R5" id="3h2IzuazA4R" role="2avVeQ">
+          <property role="1rKEKG" value="https://jira.atlassian.com/browse/JSWSERVER-26033" />
+        </node>
+      </node>
+      <node concept="19SGf9" id="3h2Izuaz_C2" role="2vnaTY">
+        <node concept="19SUe$" id="3h2Izuaz_C3" role="19SJt6">
+          <property role="19SUeA" value="The Jira issues have&#10;been addressed. " />
+        </node>
+      </node>
+    </node>
+    <node concept="3VeUTF" id="3h2Izuaz_C4" role="2vhqc$">
+      <ref role="3VeSjP" node="3h2Izualob4" resolve="G01" />
+      <ref role="3VeSjQ" node="3h2Izuaz_C1" />
+    </node>
+  </node>
+  <node concept="WiOLm" id="2H3Cssnczqa">
+    <property role="TrG5h" value="access_config" />
+    <property role="2gzYNs" value="true" />
+  </node>
+  <node concept="1lK_Xt" id="2Cw9bCdHvKl">
+    <property role="TrG5h" value="_010_legs_without_evidence" />
+    <property role="2xYCaB" value="500" />
+    <property role="2xYCe7" value="500" />
+    <ref role="1lHy9I" node="3h2Izualob4" resolve="G01" />
+    <node concept="3VsKOn" id="1wp5V2xpii5" role="2TiK2x">
+      <ref role="3VsUkX" to="7kfd:1wp5V2xiScY" resolve="ElementsWithOpenJiraIssues" />
+    </node>
+  </node>
+</model>
+
diff --git a/gradle.lockfile b/gradle.lockfile
index ba8564a55..c552ed1bd 100644
--- a/gradle.lockfile
+++ b/gradle.lockfile
@@ -9,7 +9,7 @@ com.fasterxml.jackson:jackson-bom:2.13.5=modelcheckBackend
 com.fasterxml.woodstox:woodstox-core:6.4.0=modelcheckBackend
 com.jetbrains.jdk:jbr_jcef:17.0.6-b469.82=jbrLinux,jbrMac,jbrWin
 com.jetbrains:mps:2022.3.2=mps
-com.mbeddr:platform:2022.3.24800.9b885e6=languageLibs
+com.mbeddr:platform:2022.3.24838.4b3a10a=languageLibs
 com.xenomachina:kotlin-argparser:2.0.7=executeBackend,generateBackend,modelcheckBackend,remigrateBackend
 com.xenomachina:xenocom:0.0.7=executeBackend,generateBackend,modelcheckBackend,remigrateBackend
 de.itemis.mps.build-backends:execute-generators:1.15.1.98.8f853d3=generateBackend