Fix issues found by model checker (ex typesystem).

This commit is contained in:
Fedor Isakov 2019-01-31 11:29:28 +01:00
parent dc1965fdc9
commit 9243c00c65
5 changed files with 18 additions and 75 deletions

View File

@ -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>

View File

@ -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>

View File

@ -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">

View File

@ -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>

View File

@ -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" />