diff options
author | 2022-08-10 18:07:00 +0200 | |
---|---|---|
committer | 2022-08-10 18:07:00 +0200 | |
commit | f0ad5f232acf41c421ec164fb3cf097ef93214ff (patch) | |
tree | f0565984c69691a2f821979272ed417ddb3f869d | |
parent | feat(language): add support for count operator (diff) | |
download | refinery-f0ad5f232acf41c421ec164fb3cf097ef93214ff.tar.gz refinery-f0ad5f232acf41c421ec164fb3cf097ef93214ff.tar.zst refinery-f0ad5f232acf41c421ec164fb3cf097ef93214ff.zip |
refactor(language): simplify count notation
Also change refinement operator based on feedback from colleagues
7 files changed, 12 insertions, 28 deletions
diff --git a/subprojects/frontend/src/index.tsx b/subprojects/frontend/src/index.tsx index 0616007a..78e469cd 100644 --- a/subprojects/frontend/src/index.tsx +++ b/subprojects/frontend/src/index.tsx | |||
@@ -37,7 +37,7 @@ pred invalidTaxStatus(Person p) <-> | |||
37 | rule createChild(p, newPerson): | 37 | rule createChild(p, newPerson): |
38 | may children(p, newPerson), | 38 | may children(p, newPerson), |
39 | may !equals(newPerson, newPerson) | 39 | may !equals(newPerson, newPerson) |
40 | ==> new q: newPerson, | 40 | ==> new q <: newPerson, |
41 | children(p, q), | 41 | children(p, q), |
42 | taxStatus(q, child). | 42 | taxStatus(q, child). |
43 | 43 | ||
diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index 58c398a3..f3794e27 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar | |||
@@ -58,10 +58,8 @@ Conjunction { ("," | Literal)+ } | |||
58 | OrOp { ";" } | 58 | OrOp { ";" } |
59 | 59 | ||
60 | Literal { | 60 | Literal { |
61 | Modality? ( | 61 | Modality? (NotOp | ckw<"count">)? Modality? Atom |
62 | NotOp? Modality? Atom ((":" | "=") LogicValue)? | | 62 | ((":=" | "<:") LogicValue | ComparisonOp int)? |
63 | ckw<"count"> "{" Modality? Atom "}" ComparisonOp int | ||
64 | ) | ||
65 | } | 63 | } |
66 | 64 | ||
67 | Atom { RelationName "+"? ParameterList<Argument> } | 65 | Atom { RelationName "+"? ParameterList<Argument> } |
@@ -69,7 +67,7 @@ Atom { RelationName "+"? ParameterList<Argument> } | |||
69 | Consequent { ("," | Action)+ } | 67 | Consequent { ("," | Action)+ } |
70 | 68 | ||
71 | Action { | 69 | Action { |
72 | ckw<"new"> VariableName (":" VariableName)? | | 70 | ckw<"new"> VariableName ("<:" VariableName)? | |
73 | ckw<"delete"> VariableName | | 71 | ckw<"delete"> VariableName | |
74 | Literal | 72 | Literal |
75 | } | 73 | } |
@@ -146,7 +144,7 @@ sep1<separator, content> { content (separator content)* } | |||
146 | "\"" (![\\"\n] | "\\" (![\n] | "\n"))* "\"" | 144 | "\"" (![\\"\n] | "\\" (![\n] | "\n"))* "\"" |
147 | } | 145 | } |
148 | 146 | ||
149 | ComparisonOp { ">" | ">=" | "<" | "<=" | "=:=" | "=!=" } | 147 | ComparisonOp { ">" | ">=" | "<" | "<=" | "==" } |
150 | 148 | ||
151 | NotOp { "!" } | 149 | NotOp { "!" } |
152 | 150 | ||
diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index f1332549..07bc0793 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird | |||
@@ -7,7 +7,7 @@ | |||
7 | <semanticResources>build/resources/main/model/problem.genmodel</semanticResources> | 7 | <semanticResources>build/resources/main/model/problem.genmodel</semanticResources> |
8 | <ownedViews xmi:type="viewpoint:DView" uid="_CsAAYKA4EeuqkpDnuik1sg"> | 8 | <ownedViews xmi:type="viewpoint:DView" uid="_CsAAYKA4EeuqkpDnuik1sg"> |
9 | <viewpoint xmi:type="description:Viewpoint" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']"/> | 9 | <viewpoint xmi:type="description:Viewpoint" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']"/> |
10 | <ownedRepresentationDescriptors xmi:type="viewpoint:DRepresentationDescriptor" uid="_CsYa4KA4EeuqkpDnuik1sg" name="problem" repPath="#_CsUwgKA4EeuqkpDnuik1sg" changeId="64f6664f-dd08-49f2-896c-4f190f761e4b"> | 10 | <ownedRepresentationDescriptors xmi:type="viewpoint:DRepresentationDescriptor" uid="_CsYa4KA4EeuqkpDnuik1sg" name="problem" repPath="#_CsUwgKA4EeuqkpDnuik1sg" changeId="be03322f-9027-4fa2-be8d-12768ad02214"> |
11 | <description xmi:type="description_1:DiagramDescription" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']"/> | 11 | <description xmi:type="description_1:DiagramDescription" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']"/> |
12 | <target xmi:type="ecore:EPackage" href="src/main/resources/model/problem.ecore#/"/> | 12 | <target xmi:type="ecore:EPackage" href="src/main/resources/model/problem.ecore#/"/> |
13 | </ownedRepresentationDescriptors> | 13 | </ownedRepresentationDescriptors> |
@@ -597,15 +597,11 @@ | |||
597 | <styles xmi:type="notation:FontStyle" xmi:id="_RN1AMRg0Ee2_erjsEmF9GQ" fontName="Noto Sans" fontHeight="8"/> | 597 | <styles xmi:type="notation:FontStyle" xmi:id="_RN1AMRg0Ee2_erjsEmF9GQ" fontName="Noto Sans" fontHeight="8"/> |
598 | <layoutConstraint xmi:type="notation:Location" xmi:id="_RN1AMhg0Ee2_erjsEmF9GQ"/> | 598 | <layoutConstraint xmi:type="notation:Location" xmi:id="_RN1AMhg0Ee2_erjsEmF9GQ"/> |
599 | </children> | 599 | </children> |
600 | <children xmi:type="notation:Node" xmi:id="_SGDosBg0Ee2_erjsEmF9GQ" type="3010" element="_SFkggBg0Ee2_erjsEmF9GQ"> | ||
601 | <styles xmi:type="notation:FontStyle" xmi:id="_SGDosRg0Ee2_erjsEmF9GQ" fontName="Noto Sans" fontHeight="8"/> | ||
602 | <layoutConstraint xmi:type="notation:Location" xmi:id="_SGDoshg0Ee2_erjsEmF9GQ"/> | ||
603 | </children> | ||
604 | <styles xmi:type="notation:SortingStyle" xmi:id="_LinJ1Rg0Ee2_erjsEmF9GQ"/> | 600 | <styles xmi:type="notation:SortingStyle" xmi:id="_LinJ1Rg0Ee2_erjsEmF9GQ"/> |
605 | <styles xmi:type="notation:FilteringStyle" xmi:id="_LinJ1hg0Ee2_erjsEmF9GQ"/> | 601 | <styles xmi:type="notation:FilteringStyle" xmi:id="_LinJ1hg0Ee2_erjsEmF9GQ"/> |
606 | </children> | 602 | </children> |
607 | <styles xmi:type="notation:ShapeStyle" xmi:id="_LinJ0Rg0Ee2_erjsEmF9GQ" fontName="Noto Sans" fontHeight="8"/> | 603 | <styles xmi:type="notation:ShapeStyle" xmi:id="_LinJ0Rg0Ee2_erjsEmF9GQ" fontName="Noto Sans" fontHeight="8"/> |
608 | <layoutConstraint xmi:type="notation:Bounds" xmi:id="_LinJ0hg0Ee2_erjsEmF9GQ" x="2223" y="180" width="143" height="135"/> | 604 | <layoutConstraint xmi:type="notation:Bounds" xmi:id="_LinJ0hg0Ee2_erjsEmF9GQ" x="2223" y="180" width="120" height="111"/> |
609 | </children> | 605 | </children> |
610 | <styles xmi:type="notation:DiagramStyle" xmi:id="_CsZB8qA4EeuqkpDnuik1sg"/> | 606 | <styles xmi:type="notation:DiagramStyle" xmi:id="_CsZB8qA4EeuqkpDnuik1sg"/> |
611 | <edges xmi:type="notation:Edge" xmi:id="_4eaYwKA8EeuqkpDnuik1sg" type="4001" element="_4eU5TqA8EeuqkpDnuik1sg" source="_D1D6MKA4EeuqkpDnuik1sg" target="_xsq_MKA8EeuqkpDnuik1sg"> | 607 | <edges xmi:type="notation:Edge" xmi:id="_4eaYwKA8EeuqkpDnuik1sg" type="4001" element="_4eU5TqA8EeuqkpDnuik1sg" source="_D1D6MKA4EeuqkpDnuik1sg" target="_xsq_MKA8EeuqkpDnuik1sg"> |
@@ -3680,14 +3676,6 @@ | |||
3680 | </ownedStyle> | 3676 | </ownedStyle> |
3681 | <actualMapping xmi:type="description_1:NodeMapping" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']/@defaultLayer/@containerMappings[name='EC%20EEnum']/@subNodeMappings[name='EC%20EEnumLiteral']"/> | 3677 | <actualMapping xmi:type="description_1:NodeMapping" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']/@defaultLayer/@containerMappings[name='EC%20EEnum']/@subNodeMappings[name='EC%20EEnumLiteral']"/> |
3682 | </ownedElements> | 3678 | </ownedElements> |
3683 | <ownedElements xmi:type="diagram:DNodeListElement" uid="_SFkggBg0Ee2_erjsEmF9GQ" name="NOT_EQ" tooltipText=""> | ||
3684 | <target xmi:type="ecore:EEnumLiteral" href="src/main/resources/model/problem.ecore#//ComparisonOp/NOT_EQ"/> | ||
3685 | <semanticElements xmi:type="ecore:EEnumLiteral" href="src/main/resources/model/problem.ecore#//ComparisonOp/NOT_EQ"/> | ||
3686 | <ownedStyle xmi:type="diagram:BundledImage" uid="_SFlHkBg0Ee2_erjsEmF9GQ" labelAlignment="LEFT"> | ||
3687 | <description xmi:type="style:BundledImageDescription" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']/@defaultLayer/@containerMappings[name='EC%20EEnum']/@subNodeMappings[name='EC%20EEnumLiteral']/@style"/> | ||
3688 | </ownedStyle> | ||
3689 | <actualMapping xmi:type="description_1:NodeMapping" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']/@defaultLayer/@containerMappings[name='EC%20EEnum']/@subNodeMappings[name='EC%20EEnumLiteral']"/> | ||
3690 | </ownedElements> | ||
3691 | </ownedDiagramElements> | 3679 | </ownedDiagramElements> |
3692 | <description xmi:type="description_1:DiagramDescription" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']"/> | 3680 | <description xmi:type="description_1:DiagramDescription" href="platform:/plugin/org.eclipse.emf.ecoretools.design/description/ecore.odesign#//@ownedViewpoints[name='Design']/@ownedRepresentations[name='Entities']"/> |
3693 | <filterVariableHistory xmi:type="diagram:FilterVariableHistory" uid="_CsWlsKA4EeuqkpDnuik1sg"/> | 3681 | <filterVariableHistory xmi:type="diagram:FilterVariableHistory" uid="_CsWlsKA4EeuqkpDnuik1sg"/> |
diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index 5f42341d..8f1bc355 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore | |||
@@ -189,6 +189,5 @@ | |||
189 | <eLiterals name="GREATER" value="2"/> | 189 | <eLiterals name="GREATER" value="2"/> |
190 | <eLiterals name="GREATER_EQ" value="3"/> | 190 | <eLiterals name="GREATER_EQ" value="3"/> |
191 | <eLiterals name="EQ" value="4"/> | 191 | <eLiterals name="EQ" value="4"/> |
192 | <eLiterals name="NOT_EQ" value="5"/> | ||
193 | </eClassifiers> | 192 | </eClassifiers> |
194 | </ecore:EPackage> | 193 | </ecore:EPackage> |
diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel index 60dec198..fbaf9d65 100644 --- a/subprojects/language-model/src/main/resources/model/problem.genmodel +++ b/subprojects/language-model/src/main/resources/model/problem.genmodel | |||
@@ -28,7 +28,6 @@ | |||
28 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/GREATER"/> | 28 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/GREATER"/> |
29 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/GREATER_EQ"/> | 29 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/GREATER_EQ"/> |
30 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/EQ"/> | 30 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/EQ"/> |
31 | <genEnumLiterals ecoreEnumLiteral="problem.ecore#//ComparisonOp/NOT_EQ"/> | ||
32 | </genEnums> | 31 | </genEnums> |
33 | <genClasses ecoreClass="problem.ecore#//Problem"> | 32 | <genClasses ecoreClass="problem.ecore#//Problem"> |
34 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference problem.ecore#//Problem/nodes"/> | 33 | <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference problem.ecore#//Problem/nodes"/> |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index 93d066af..74b0d50e 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -64,23 +64,23 @@ NegativeLiteral: | |||
64 | modality=Modality? "!" atom=Atom; | 64 | modality=Modality? "!" atom=Atom; |
65 | 65 | ||
66 | enum ComparisonOp: | 66 | enum ComparisonOp: |
67 | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="=:=" | NOT_EQ="=!=" ; | 67 | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="=="; |
68 | 68 | ||
69 | CountLiteral: | 69 | CountLiteral: |
70 | modality=Modality? "count" "{" atom=Atom "}" op=ComparisonOp threshold=INT; | 70 | modality=Modality? "count" atom=Atom op=ComparisonOp threshold=INT; |
71 | 71 | ||
72 | Action: | 72 | Action: |
73 | AssertionAction | DeleteAction | NewAction; | 73 | AssertionAction | DeleteAction | NewAction; |
74 | 74 | ||
75 | AssertionAction: | 75 | AssertionAction: |
76 | value=ShortLogicValue? atom=Atom | | 76 | value=ShortLogicValue? atom=Atom | |
77 | atom=Atom (overwrite?="=" | ":") value=LogicValue; | 77 | atom=Atom (overwrite?=":=" | "<:") value=LogicValue; |
78 | 78 | ||
79 | DeleteAction: | 79 | DeleteAction: |
80 | "delete" variableOrNode=[VariableOrNode|QualifiedName]; | 80 | "delete" variableOrNode=[VariableOrNode|QualifiedName]; |
81 | 81 | ||
82 | NewAction: | 82 | NewAction: |
83 | "new" variable=NewVariable (":" parent=[VariableOrNode|QualifiedName])?; | 83 | "new" variable=NewVariable ("<:" parent=[VariableOrNode|QualifiedName])?; |
84 | 84 | ||
85 | NewVariable: | 85 | NewVariable: |
86 | name=Identifier; | 86 | name=Identifier; |
diff --git a/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem b/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem index 5e913b51..323e03f1 100644 --- a/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem +++ b/subprojects/language/src/main/resources/tools/refinery/language/builtin.problem | |||
@@ -1,7 +1,7 @@ | |||
1 | problem builtin. | 1 | problem builtin. |
2 | 2 | ||
3 | abstract class node { | 3 | abstract class node { |
4 | refers node[] equals opposite equals. | 4 | refers node[] equals opposite equals |
5 | } | 5 | } |
6 | 6 | ||
7 | pred exists(node node). | 7 | pred exists(node node). |