Skip to content
This repository has been archived by the owner on May 28, 2024. It is now read-only.

Commit

Permalink
Disallowusage of OCRA constraints outside OCRA
Browse files Browse the repository at this point in the history 
To not pollute nusmv language models with OCRA expression/constraint
concepts, additional MPS constrants are introduced. All OCRA expressions
now extend the interface IOcraExpression, which is only allowed
('can be child of') inside OCRA contracts.

mbeddr#54

Signed-off-by: Arne Nordmann (CR/AEA2) <[email protected]>
  • Loading branch information
@norro
norro committed Oct 19, 2020
1 parent 501daa8 commit 81dd0df
Show file tree
Hide file tree
Showing 5 changed files with 153 additions and 4 deletions.
45 changes: 45 additions & 0 deletions ...uages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
<?xml version="1.0" encoding="UTF-8"?>
<language namespace="com.mbeddr.formal.ocra" uuid="5ccce04a-9411-450d-8af4-a858c6f99d1e" languageVersion="0" moduleVersion="0">
<models>
<modelRoot contentPath="${module}" type="default">
<sourceRoot location="models" />
</modelRoot>
</models>
<facets>
<facet type="java">
<classes generated="true" path="${module}/classes_gen" />
</facet>
</facets>
<accessoryModels />
<sourcePath />
<languageVersions>
<language slang="l:ceab5195-25ea-4f22-9b92-103b95ca8c0c:jetbrains.mps.lang.core" version="2" />
<language slang="l:f4ad079d-bc71-4ffb-9600-9328705cf998:jetbrains.mps.lang.descriptor" version="0" />
</languageVersions>
<dependencyVersions>
<module reference="3f233e7f-b8a6-46d2-a57f-795d56775243(Annotations)" version="0" />
<module reference="6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)" version="0" />
<module reference="6ed54515-acc8-4d1e-a16c-9fd6cfe951ea(MPS.Core)" version="0" />
<module reference="1ed103c3-3aa6-49b7-9c21-6765ee11f224(MPS.Editor)" version="0" />
<module reference="498d89d2-c2e9-11e2-ad49-6cf049e62fe5(MPS.IDEA)" version="0" />
<module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
<module reference="742f6602-5a2f-4313-aa6e-ae1cd4ffdc61(MPS.Platform)" version="0" />
<module reference="83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)" version="0" />
<module reference="b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions)" version="0" />
<module reference="001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)" version="0" />
<module reference="5ccce04a-9411-450d-8af4-a858c6f99d1e(com.mbeddr.formal.ocra)" version="0" />
<module reference="f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)" version="0" />
<module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="9e98f4e2-decf-4e97-bf80-9109e8b759aa(jetbrains.mps.lang.feedback.context)" version="0" />
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
</dependencyVersions>
<extendedLanguages>
<extendedLanguage>001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)</extendedLanguage>
<extendedLanguage>f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)</extendedLanguage>
<extendedLanguage>b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions)</extendedLanguage>
</extendedLanguages>
</language>

5 changes: 5 additions & 0 deletions code/languages/com.mbeddr.formal.ocra/com.mbeddr.formal.ocra.mpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@
<dependency reexport="false">83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base)</dependency>
<dependency reexport="false">2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)</dependency>
<dependency reexport="false">6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)</dependency>
<dependency reexport="false">c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)</dependency>
<dependency reexport="false">001b2375-3bd5-4d5e-9958-6b3f62dc8548(com.mbeddr.formal.nusmv)</dependency>
</dependencies>
<languageVersions>
<language slang="l:9d69e719-78c8-4286-90db-fb19c107d049:com.mbeddr.mpsutil.grammarcells" version="1" />
Expand Down Expand Up @@ -70,9 +72,12 @@
<module reference="f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage)" version="0" />
<module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="d936855b-48da-4812-a8a0-2bfddd633ac5(jetbrains.mps.lang.behavior.api)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
<module reference="a9e4c532-c5f5-4bb7-99ef-42abb73bbb70(jetbrains.mps.lang.descriptor.aspects)" version="0" />
<module reference="9e98f4e2-decf-4e97-bf80-9109e8b759aa(jetbrains.mps.lang.feedback.context)" version="0" />
<module reference="d7eb0a2a-bd50-4576-beae-e4a89db35f20(jetbrains.mps.lang.scopes.runtime)" version="0" />
<module reference="c72da2b9-7cce-4447-8389-f407dc1158b7(jetbrains.mps.lang.structure)" version="0" />
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
</dependencyVersions>
<extendedLanguages>
Expand Down
2 changes: 0 additions & 2 deletions code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.behavior.mps
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,13 @@
<use id="7866978e-a0f0-4cc7-81bc-4d213d9375e1" name="jetbrains.mps.lang.smodel" version="17" />
<use id="af65afd8-f0dd-4942-87d9-63a55f2a9db1" name="jetbrains.mps.lang.behavior" version="2" />
<use id="d8f591ec-4d86-4af2-9f92-a9e93c803ffa" name="jetbrains.mps.lang.scopes" version="0" />
<use id="7a5dda62-9140-4668-ab76-d5ed1746f2b2" name="jetbrains.mps.lang.typesystem" version="5" />
<devkit ref="fbc25dd2-5da4-483a-8b19-70928e1b62d7(jetbrains.mps.devkit.general-purpose)" />
</languages>
<imports>
<import index="tpcu" ref="r:00000000-0000-4000-0000-011c89590282(jetbrains.mps.lang.core.behavior)" />
<import index="hqls" ref="r:9be6a7f5-8948-4321-86ee-36906d4a48b4(com.mbeddr.formal.ocra.structure)" />
<import index="tpck" ref="r:00000000-0000-4000-0000-011c89590288(jetbrains.mps.lang.core.structure)" />
<import index="o8zo" ref="r:314576fc-3aee-4386-a0a5-a38348ac317d(jetbrains.mps.scope)" />
<import index="c17a" ref="8865b7a8-5271-43d3-884c-6fd1d9cfdd34/java:org.jetbrains.mps.openapi.language(MPS.OpenAPI/)" />
<import index="w873" ref="r:0de03bcd-6ad8-423c-b85e-ae3dd18ed2b3(com.mbeddr.formal.base.behavior)" />
<import index="ox2v" ref="r:9d0d3f45-3600-4f52-892b-d59f24c624ff(com.mbeddr.formal.base.expressions.behavior)" implicit="true" />
</imports>
Expand Down
34 changes: 34 additions & 0 deletions code/languages/com.mbeddr.formal.ocra/models/com.mbeddr.formal.ocra.constraints.mps
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,14 @@
<use id="13744753-c81f-424a-9c1b-cf8943bf4e86" name="jetbrains.mps.lang.sharedConcepts" version="0" />
<use id="3ad5badc-1d9c-461c-b7b1-fa2fcd0a0ae7" name="jetbrains.mps.lang.context" version="0" />
<use id="ad93155d-79b2-4759-b10c-55123e763903" name="jetbrains.mps.lang.messages" version="0" />
<use id="f2801650-65d5-424e-bb1b-463a8781b786" name="jetbrains.mps.baseLanguage.javadoc" version="2" />
<devkit ref="00000000-0000-4000-0000-5604ebd4f22c(jetbrains.mps.devkit.aspect.constraints)" />
</languages>
<imports>
<import index="o8zo" ref="r:314576fc-3aee-4386-a0a5-a38348ac317d(jetbrains.mps.scope)" />
<import index="hqls" ref="r:9be6a7f5-8948-4321-86ee-36906d4a48b4(com.mbeddr.formal.ocra.structure)" />
<import index="ehqg" ref="r:2c1724e1-8ed6-4fe4-9e44-fae13cd2a5ac(com.mbeddr.formal.base.expressions.structure)" />
<import index="tpcn" ref="r:00000000-0000-4000-0000-011c8959028b(jetbrains.mps.lang.structure.behavior)" />
<import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" implicit="true" />
</imports>
<registry>
Expand Down Expand Up @@ -76,10 +78,12 @@
</concept>
</language>
<language id="3f4bc5f5-c6c1-4a28-8b10-c83066ffa4a1" name="jetbrains.mps.lang.constraints">
<concept id="6702802731807351367" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAChild" flags="in" index="9S07l" />
<concept id="6702802731807420587" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_CanBeAParent" flags="ig" index="9SLcT" />
<concept id="8966504967485224688" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_contextNode" flags="nn" index="2rP1CM" />
<concept id="4303308395523343364" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_link" flags="ng" index="2DA6wF" />
<concept id="4303308395523096213" name="jetbrains.mps.lang.constraints.structure.ConstraintFunctionParameter_childConcept" flags="ng" index="2DD5aU" />
<concept id="1147468365020" name="jetbrains.mps.lang.constraints.structure.ConstraintsFunctionParameter_node" flags="nn" index="EsrRn" />
<concept id="5564765827938091039" name="jetbrains.mps.lang.constraints.structure.ConstraintFunction_ReferentSearchScope_Scope" flags="ig" index="3dgokm" />
<concept id="8401916545537438642" name="jetbrains.mps.lang.constraints.structure.InheritedNodeScopeFactory" flags="ng" index="1dDu$B">
<reference id="8401916545537438643" name="kind" index="1dDu$A" />
Expand All @@ -90,6 +94,7 @@
<concept id="1213093968558" name="jetbrains.mps.lang.constraints.structure.ConceptConstraints" flags="ng" index="1M2fIO">
<reference id="1213093996982" name="concept" index="1M2myG" />
<child id="6702802731807532712" name="canBeParent" index="9SGkU" />
<child id="6702802731807737306" name="canBeChild" index="9Vyp8" />
<child id="1213100494875" name="referent" index="1Mr941" />
<child id="1213101058038" name="defaultScope" index="1MtirG" />
</concept>
Expand All @@ -108,6 +113,7 @@
<concept id="4693937538533521280" name="jetbrains.mps.lang.smodel.structure.OfConceptOperation" flags="ng" index="v3k3i">
<child id="4693937538533538124" name="requestedConcept" index="v3oSu" />
</concept>
<concept id="1173122760281" name="jetbrains.mps.lang.smodel.structure.Node_GetAncestorsOperation" flags="nn" index="z$bX8" />
<concept id="2396822768958367367" name="jetbrains.mps.lang.smodel.structure.AbstractTypeCastExpression" flags="nn" index="$5XWr">
<child id="6733348108486823193" name="leftExpression" index="1m5AlR" />
<child id="3906496115198199033" name="conceptArgument" index="3oSUPX" />
Expand Down Expand Up @@ -145,6 +151,9 @@
</concept>
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
<property id="1193676396447" name="virtualPackage" index="3GE5qa" />
</concept>
<concept id="1169194658468" name="jetbrains.mps.lang.core.structure.INamedConcept" flags="ng" index="TrEIO">
<property id="1169194664001" name="name" index="TrG5h" />
</concept>
Expand All @@ -154,6 +163,7 @@
<child id="540871147943773366" name="argument" index="25WWJ7" />
</concept>
<concept id="1160666733551" name="jetbrains.mps.baseLanguage.collections.structure.AddAllElementsOperation" flags="nn" index="X8dFx" />
<concept id="1176501494711" name="jetbrains.mps.baseLanguage.collections.structure.IsNotEmptyOperation" flags="nn" index="3GX2aA" />
</language>
</registry>
<node concept="1M2fIO" id="1QMZQ046hgc">
Expand Down Expand Up @@ -564,5 +574,29 @@
</node>
</node>
</node>
<node concept="1M2fIO" id="46t5MkZs$er">
<property role="3GE5qa" value="constraints" />
<ref role="1M2myG" to="hqls:46t5MkZsy$k" resolve="IOCRAConstraint" />
<node concept="9S07l" id="46t5MkZs$LM" role="9Vyp8">
<node concept="3clFbS" id="46t5MkZs$LN" role="2VODD2">
<node concept="3clFbF" id="46t5MkZs_p3" role="3cqZAp">
<node concept="2OqwBi" id="46t5MkZsFET" role="3clFbG">
<node concept="2OqwBi" id="46t5MkZsBFb" role="2Oq$k0">
<node concept="2OqwBi" id="46t5MkZs_Ae" role="2Oq$k0">
<node concept="EsrRn" id="46t5MkZs_p2" role="2Oq$k0" />
<node concept="z$bX8" id="46t5MkZsA4e" role="2OqNvi" />
</node>
<node concept="v3k3i" id="46t5MkZsDG$" role="2OqNvi">
<node concept="chp4Y" id="46t5MkZsFrx" role="v3oSu">
<ref role="cht4Q" to="hqls:1WjQLbKt0ti" resolve="Contract" />
</node>
</node>
</node>
<node concept="3GX2aA" id="46t5MkZsG9k" role="2OqNvi" />
</node>
</node>
</node>
</node>
</node>
</model>

Loading

0 comments on commit 81dd0df

Please sign in to comment.