From 9243c00c6598eab4cb5b468800c5187a36df80e3 Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Thu, 31 Jan 2019 11:29:28 +0100
Subject: [PATCH] Fix issues found by model checker (ex typesystem).

---
 .../generator/template/main@generator.mps     | 11 +--
 .../models/plugin.mps                         |  2 +-
 .../models/firstOrderLogic@tests.mps          |  4 +-
 .../jetbrains.mps.baseLanguageExt.types.mps   | 72 ++-----------------
 .../models/features.mps                       |  4 +-
 5 files changed, 18 insertions(+), 75 deletions(-)

diff --git a/coderules/languages/jetbrains.mps.logic/generator/template/main@generator.mps b/coderules/languages/jetbrains.mps.logic/generator/template/main@generator.mps
index aded5cd4..8be26dbb 100644
--- a/coderules/languages/jetbrains.mps.logic/generator/template/main@generator.mps
+++ b/coderules/languages/jetbrains.mps.logic/generator/template/main@generator.mps
@@ -12,6 +12,7 @@
     <use id="35320f26-77cb-4c55-be9f-a97a27770af1" name="jetbrains.mps.logic" version="2" />
     <use id="83888646-71ce-4f1c-9c53-c54016f6ad4f" name="jetbrains.mps.baseLanguage.collections" version="1" />
     <use id="df345b11-b8c7-4213-ac66-48d2a9b75d88" name="jetbrains.mps.baseLanguageInternal" version="0" />
+    <use id="d4615e3b-d671-4ba9-af01-2b78369b0ba7" name="jetbrains.mps.lang.pattern" version="1" />
     <devkit ref="fbc25dd2-5da4-483a-8b19-70928e1b62d7(jetbrains.mps.devkit.general-purpose)" />
   </languages>
   <imports>
@@ -1589,14 +1590,14 @@
                 </node>
               </node>
               <node concept="3clFbF" id="3gNap3g_70f" role="3cqZAp">
-                <node concept="2YIFZM" id="3gNap3g_bV_" role="3clFbG">
-                  <ref role="37wK5l" to="oy3s:3gNap3fZcVn" resolve="asValue" />
+                <node concept="2YIFZM" id="1Lr58WG4AYV" role="3clFbG">
                   <ref role="1Pybhc" to="oy3s:677NV565N1x" resolve="LogicalUtil" />
-                  <node concept="37vLTw" id="3gNap3g_bVA" role="37wK5m">
+                  <ref role="37wK5l" to="oy3s:3gNap3gwG50" resolve="asValue" />
+                  <node concept="37vLTw" id="1Lr58WG4AYW" role="37wK5m">
                     <ref role="3cqZAo" node="3gNap3g_70d" resolve="logical" />
-                    <node concept="29HgVG" id="3gNap3g_bVB" role="lGtFl" />
+                    <node concept="29HgVG" id="1Lr58WG4AYX" role="lGtFl" />
                   </node>
-                  <node concept="raruj" id="3gNap3g_bVC" role="lGtFl" />
+                  <node concept="raruj" id="1Lr58WG4AYY" role="lGtFl" />
                 </node>
               </node>
             </node>
diff --git a/coderules/solutions/jetbrains.mps.coderules.ui/models/plugin.mps b/coderules/solutions/jetbrains.mps.coderules.ui/models/plugin.mps
index 9b8ec551..cfddfa40 100644
--- a/coderules/solutions/jetbrains.mps.coderules.ui/models/plugin.mps
+++ b/coderules/solutions/jetbrains.mps.coderules.ui/models/plugin.mps
@@ -7922,7 +7922,7 @@
                                   </node>
                                 </node>
                                 <node concept="liA8E" id="19wqdqOqxsP" role="2OqNvi">
-                                  <ref role="37wK5l" to="bj13:~LogicalOwner.logical():jetbrains.mps.logic.reactor.logical.Logical" resolve="logical" />
+                                  <ref role="37wK5l" to="oy3s:4TCblo5MS1o" resolve="logical" />
                                 </node>
                               </node>
                             </node>
diff --git a/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps b/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
index 703030e4..47feb095 100644
--- a/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
+++ b/samples/fitch/solutions/samples.fitch.demo/models/firstOrderLogic@tests.mps
@@ -11,7 +11,7 @@
     <import index="z1c3" ref="6ed54515-acc8-4d1e-a16c-9fd6cfe951ea/java:jetbrains.mps.project(MPS.Core/)" />
     <import index="yhz9" ref="r:72b177ed-1924-4265-b8f3-64e062fd2eed(samples.fitch.firstOrderLogic.structure)" />
     <import index="ious" ref="r:2deee13f-4a3d-4229-ad45-9e5b85327419(samples.fitch.demo.firstOrderLogic)" />
-    <import index="tj24" ref="r:0fbbb63a-fd15-46e1-8136-78049f6d6e63(jetbrains.mps.typechecking.service)" implicit="true" />
+    <import index="tj24" ref="r:0fbbb63a-fd15-46e1-8136-78049f6d6e63(jetbrains.mps.typechecking.service)" />
   </imports>
   <registry>
     <language id="8585453e-6bfb-4d80-98de-b16074f1d86c" name="jetbrains.mps.lang.test">
@@ -144,8 +144,8 @@
           <node concept="2OqwBi" id="27bTNFfbwI2" role="2Hmdds">
             <node concept="2OqwBi" id="27bTNFfbwI3" role="2Oq$k0">
               <node concept="2YIFZM" id="27bTNFfbwI4" role="2Oq$k0">
-                <ref role="1Pybhc" to="tj24:1N_0WA5JxZO" resolve="TestLaunchTypechecking" />
                 <ref role="37wK5l" to="tj24:27bTNFfaOo$" resolve="ofNode" />
+                <ref role="1Pybhc" to="tj24:1N_0WA5JxZO" resolve="TestLaunchTypechecking" />
                 <node concept="2OqwBi" id="27bTNFfbZPj" role="37wK5m">
                   <node concept="2WthIp" id="27bTNFfbZPk" role="2Oq$k0" />
                   <node concept="2XshWL" id="27bTNFfbZPl" role="2OqNvi">
diff --git a/samples/mpscore/languages/jetbrains.mps.baseLanguageExt/models/jetbrains.mps.baseLanguageExt.types.mps b/samples/mpscore/languages/jetbrains.mps.baseLanguageExt/models/jetbrains.mps.baseLanguageExt.types.mps
index 15f59315..da3f3af5 100644
--- a/samples/mpscore/languages/jetbrains.mps.baseLanguageExt/models/jetbrains.mps.baseLanguageExt.types.mps
+++ b/samples/mpscore/languages/jetbrains.mps.baseLanguageExt/models/jetbrains.mps.baseLanguageExt.types.mps
@@ -3941,8 +3941,8 @@
                     <node concept="3A2sRY" id="6EY0p2ypW$V" role="2Oq$k0">
                       <ref role="3A2yKK" node="6EY0p2ym$1M" resolve="bmc" />
                     </node>
-                    <node concept="3TrEf2" id="6EY0p2ymPo7" role="2OqNvi">
-                      <ref role="3Tt5mk" to="tpee:hwllgre" resolve="instanceMethodDeclaration" />
+                    <node concept="3TrEf2" id="1Lr58WG6VPd" role="2OqNvi">
+                      <ref role="3Tt5mk" to="tpee:fz7wK6H" resolve="baseMethodDeclaration" />
                     </node>
                   </node>
                   <node concept="3Tsc0h" id="6EY0p2ymPo8" role="2OqNvi">
@@ -3981,8 +3981,8 @@
                         <node concept="3A2sRY" id="6EY0p2ypZHe" role="2Oq$k0">
                           <ref role="3A2yKK" node="6EY0p2ym$1M" resolve="bmc" />
                         </node>
-                        <node concept="3TrEf2" id="6EY0p2ymPop" role="2OqNvi">
-                          <ref role="3Tt5mk" to="tpee:hwllgre" resolve="instanceMethodDeclaration" />
+                        <node concept="3TrEf2" id="1Lr58WG6WIE" role="2OqNvi">
+                          <ref role="3Tt5mk" to="tpee:fz7wK6H" resolve="baseMethodDeclaration" />
                         </node>
                       </node>
                       <node concept="3TrEf2" id="6EY0p2ymPoq" role="2OqNvi">
@@ -4330,64 +4330,6 @@
             </node>
           </node>
         </node>
-        <node concept="3cpWs8" id="6EY0p2ymzWy" role="3cqZAp">
-          <node concept="3cpWsn" id="6EY0p2ymzWz" role="3cpWs9">
-            <property role="TrG5h" value="subs" />
-            <node concept="3rvAFt" id="6EY0p2ymzW$" role="1tU5fm">
-              <node concept="3Tqbb2" id="6EY0p2ymzW_" role="3rvQeY" />
-              <node concept="26uTi9" id="6EY0p2ymzWA" role="3rvSg0" />
-            </node>
-            <node concept="2ShNRf" id="6EY0p2ymzWB" role="33vP2m">
-              <node concept="3rGOSV" id="6EY0p2ymzWC" role="2ShVmc">
-                <node concept="3Tqbb2" id="6EY0p2ymzWD" role="3rHrn6" />
-                <node concept="26uTi9" id="6EY0p2ymzWE" role="3rHtpV" />
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="2Gpval" id="6EY0p2ymzWF" role="3cqZAp">
-          <node concept="2GrKxI" id="6EY0p2ymzWG" role="2Gsz3X">
-            <property role="TrG5h" value="tv" />
-          </node>
-          <node concept="3clFbS" id="6EY0p2ymzWH" role="2LFqv$">
-            <node concept="3clFbF" id="6EY0p2ymzWI" role="3cqZAp">
-              <node concept="37vLTI" id="6EY0p2ymzWJ" role="3clFbG">
-                <node concept="10Nm6u" id="6EY0p2ymzWK" role="37vLTx" />
-                <node concept="3EllGN" id="6EY0p2ymzWL" role="37vLTJ">
-                  <node concept="2GrUjf" id="6EY0p2ymzWM" role="3ElVtu">
-                    <ref role="2Gs0qQ" node="6EY0p2ymzWG" resolve="tv" />
-                  </node>
-                  <node concept="37vLTw" id="6EY0p2ymzWN" role="3ElQJh">
-                    <ref role="3cqZAo" node="6EY0p2ymzWz" resolve="subs" />
-                  </node>
-                </node>
-              </node>
-            </node>
-          </node>
-          <node concept="2OqwBi" id="6EY0p2ymzWO" role="2GsD0m">
-            <node concept="2OqwBi" id="6EY0p2ymzWP" role="2Oq$k0">
-              <node concept="2OqwBi" id="6EY0p2ymzWQ" role="2Oq$k0">
-                <node concept="37vLTw" id="6EY0p2ymzWR" role="2Oq$k0">
-                  <ref role="3cqZAo" node="6EY0p2ymzVu" resolve="decl" />
-                </node>
-                <node concept="3Tsc0h" id="6EY0p2ymzWS" role="2OqNvi">
-                  <ref role="3TtcxE" to="tpee:g96eVAe" resolve="typeVariableDeclaration" />
-                </node>
-              </node>
-              <node concept="3QWeyG" id="6EY0p2ymzWT" role="2OqNvi">
-                <node concept="37vLTw" id="6EY0p2ymzWU" role="576Qk">
-                  <ref role="3cqZAo" node="6EY0p2ymzVX" resolve="usedVars" />
-                </node>
-              </node>
-            </node>
-            <node concept="3QWeyG" id="6EY0p2ymzWV" role="2OqNvi">
-              <node concept="37vLTw" id="6EY0p2ymzWW" role="576Qk">
-                <ref role="3cqZAo" node="6EY0p2ymzWp" resolve="clsVars" />
-              </node>
-            </node>
-          </node>
-        </node>
-        <node concept="3clFbH" id="6EY0p2ymzWX" role="3cqZAp" />
         <node concept="3clFbH" id="6EY0p2ymzYu" role="3cqZAp" />
         <node concept="3cpWs8" id="6EY0p2ymzYv" role="3cqZAp">
           <node concept="3cpWsn" id="6EY0p2ymzYw" role="3cpWs9">
@@ -29391,7 +29333,7 @@
               <node concept="ns1u0" id="5XJPBczymaB" role="3A8w4Q">
                 <ref role="ns1xF" node="JOGAOsVt2M" resolve="charType" />
                 <node concept="nsMwS" id="5XJPBczymaC" role="ns1xD">
-                  <ref role="nsMwP" node="JOGAOsVt2L" resolve="val" />
+                  <ref role="nsMwP" node="JOGAOsVt2P" resolve="val" />
                   <node concept="37vLTw" id="5XJPBczymaD" role="nsMwV">
                     <ref role="3cqZAo" node="5XJPBczymav" resolve="charValue" />
                   </node>
@@ -29460,7 +29402,7 @@
               <node concept="ns1u0" id="5XJPBczy$GH" role="3A8w4Q">
                 <ref role="ns1xF" node="JOGAOsVt2Q" resolve="shortType" />
                 <node concept="nsMwS" id="5XJPBczy$GI" role="ns1xD">
-                  <ref role="nsMwP" node="JOGAOsVt2P" resolve="val" />
+                  <ref role="nsMwP" node="JOGAOsVt2T" resolve="val" />
                   <node concept="3cmrfG" id="5XJPBczyH3P" role="nsMwV">
                     <property role="3cmrfH" value="0" />
                   </node>
@@ -29715,7 +29657,7 @@
                   <node concept="ns1u0" id="5XJPBczy$Rj" role="3A8w4Q">
                     <ref role="ns1xF" node="JOGAOsVt2U" resolve="longType" />
                     <node concept="nsMwS" id="5XJPBczy$Rk" role="ns1xD">
-                      <ref role="nsMwP" node="JOGAOsVt2T" resolve="val" />
+                      <ref role="nsMwP" node="JOGAOsVt2X" resolve="val" />
                       <node concept="37vLTw" id="5XJPBczUoxh" role="nsMwV">
                         <ref role="3cqZAo" node="5XJPBczUoxf" resolve="finalValue" />
                       </node>
diff --git a/samples/mpscore/solutions/typechecking.samples.baseLanguage/models/features.mps b/samples/mpscore/solutions/typechecking.samples.baseLanguage/models/features.mps
index 99da5707..e5218427 100644
--- a/samples/mpscore/solutions/typechecking.samples.baseLanguage/models/features.mps
+++ b/samples/mpscore/solutions/typechecking.samples.baseLanguage/models/features.mps
@@ -1884,8 +1884,8 @@
         </node>
         <node concept="3clFbF" id="70Wv0dJ5qpF" role="3cqZAp">
           <node concept="2OqwBi" id="70Wv0dJ5qpG" role="3clFbG">
-            <node concept="37vLTw" id="70Wv0dJ5qpH" role="2Oq$k0">
-              <ref role="3cqZAo" node="70Wv0dJ5pNI" resolve="c" />
+            <node concept="37vLTw" id="1Lr58WG8UN6" role="2Oq$k0">
+              <ref role="3cqZAo" node="70Wv0dJ5qpK" resolve="a" />
             </node>
             <node concept="liA8E" id="70Wv0dJ5qpI" role="2OqNvi">
               <ref role="37wK5l" to="wyt6:~Object.toString():java.lang.String" resolve="toString" />