Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Issue 46 projection exprs #103

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Issue 46 projection exprs #103

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
00f1f13
Modify grammar to place ArraySubExpr and SelectionExpr in clique
kfhoech Mar 16, 2022
a2fbac1
Regernate AGREE language artifacts
kfhoech Mar 16, 2022
3a63e3b
Add a test for the new array/selection parsing clique
kfhoech Mar 16, 2022
ae54a31
Update plugin management versions
kfhoech Mar 16, 2022
2eae852
Update api error filters to quash errors in generated files
kfhoech Mar 16, 2022
37b7ad8
Merge branch 'master' into issue-46-projection-exprs
kfhoech Mar 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)",
org.osate.aadl2;bundle-version="[2.0.0,5.0.0)",
org.osate.ui;bundle-version="[6.0.0,7.0.0)",
org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)",
com.rockwellcollins.atc.agree;bundle-version="[3.0.0,4.0.0)",
com.rockwellcollins.atc.agree.ui;bundle-version="[3.0.0,4.0.0)",
com.rockwellcollins.atc.agree;bundle-version="[4.0.0,5.0.0)",
com.rockwellcollins.atc.agree.ui;bundle-version="[4.0.0,5.0.0)",
org.osate.ge;bundle-version="[2.0.0,4.0.0)",
org.eclipse.emf.ecore;bundle-version="[2.23.0,3.0.0)",
com.collins.trustedsystems.z3;bundle-version="[4.0.0,5.0.0)",
Expand Down
2 changes: 1 addition & 1 deletion com.rockwellcollins.atc.agree.codegen/META-INF/MANIFEST.MF
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)",
org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)",
org.osate.aadl2;bundle-version="[4.0.0,5.0.0)",
com.rockwellcollins.atc.agree.analysis;bundle-version="[2.8.0,3.0.0)",
com.rockwellcollins.atc.agree;bundle-version="[3.0.0,4.0.0)",
com.rockwellcollins.atc.agree;bundle-version="[4.0.0,5.0.0)",
org.osate.annexsupport;bundle-version="[3.0.0,5.0.0)",
org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)",
org.eclipse.core.resources;bundle-version="[3.9.1,4.0.0)",
Expand Down
2 changes: 1 addition & 1 deletion com.rockwellcollins.atc.agree.doc/META-INF/MANIFEST.MF
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: AGREE Documentation
Bundle-SymbolicName: com.rockwellcollins.atc.agree.doc;singleton:=true
Bundle-Version: 2.8.1.qualifier
Bundle-Version: 2.9.0.qualifier
Bundle-Vendor: ROCKWELLCOLLINS
Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)",
org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)"
Expand Down
2 changes: 1 addition & 1 deletion com.rockwellcollins.atc.agree.doc/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
<version>2.8.1-SNAPSHOT</version>
</parent>
<artifactId>com.rockwellcollins.atc.agree.doc</artifactId>
<version>2.8.1-SNAPSHOT</version>
<version>2.9.0-SNAPSHOT</version>
<packaging>eclipse-plugin</packaging>

<build>
Expand Down
272 changes: 271 additions & 1 deletion ...ellcollins.atc.agree.tests/src/com/rockwellcollins/atc/agree/tests/AgreeParsingTest.xtend
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,17 +32,25 @@ import org.eclipse.xtext.testing.XtextRunner
import com.itemis.xtext.testing.XtextTest

import org.osate.aadl2.AadlPackage
import org.osate.aadl2.DataSubcomponent
import org.osate.aadl2.DefaultAnnexLibrary
import org.osate.aadl2.DefaultAnnexSubclause

import com.rockwellcollins.atc.agree.agree.AgreeContract
import com.rockwellcollins.atc.agree.agree.AgreeContractLibrary
import com.rockwellcollins.atc.agree.agree.AgreeContractSubclause
import com.rockwellcollins.atc.agree.agree.Arg
import com.rockwellcollins.atc.agree.agree.ArraySubExpr
import com.rockwellcollins.atc.agree.agree.AssumeStatement
import com.rockwellcollins.atc.agree.agree.BinaryExpr
import com.rockwellcollins.atc.agree.agree.ConstStatement
import com.rockwellcollins.atc.agree.agree.GuaranteeStatement
import com.rockwellcollins.atc.agree.agree.IntLitExpr
import com.rockwellcollins.atc.agree.agree.NamedElmExpr
import com.rockwellcollins.atc.agree.agree.PrimType
import com.rockwellcollins.atc.agree.agree.SelectionExpr

import com.rockwellcollins.atc.agree.tests.testsupport.TestHelper
import com.rockwellcollins.atc.agree.agree.PrimType

@RunWith(XtextRunner)
@InjectWith(AgreeInjectorProvider)
Expand Down Expand Up @@ -149,4 +157,266 @@ class AgreeParsingTest extends XtextTest {
]
}

@Test
def void testProjectionExpressionClique() {
val model = '''
package Array_Parse
public
with Base_Types;
with Data_Model;

data Alpha
properties
Data_Model::Data_Representation => Struct;
end Alpha;

data implementation Alpha.impl
subcomponents
x : data Base_Types::Integer;
y : data Base_Types::Integer;
end Alpha.impl;

data Beta
properties
Data_Model::Data_Representation => Struct;
end Beta;

data implementation Beta.impl
subcomponents
m : data Alpha.impl[2];
end Beta.impl;

system Epsilon
features
inp : in data port Beta.impl;
annex agree {**
-- This parses
assume A001 "Input" : (inp.m[1]).x = 1;
-- This should now parse
assume A002 "Input" : inp.m[1].x = 1;

eq x : Beta.Impl;
-- This parses
guarantee G001 "Local rule" : (x.m[1]).x = 1;
-- This should now parse
guarantee G002 "Local rule" : x.m[1].x = 1;

type RecS1 = struct { x : int, y : int };
type RecS2 = struct { m : RecS1[2] };
eq y : RecS2;
-- This parses
guarantee G003 "Local rule" : (y.m[1]).x = 1;
-- This should now parse
guarantee G004 "Local rule" : y.m[1].x = 1;

**};
end Epsilon;

end Array_Parse;
'''

val testFileResult = issues = testHelper.testString(model)

EcoreUtil2.getAllContentsOfType(testFileResult.resource.contents.head, AgreeContract).head => [
specs.filter(AssumeStatement).filter["A001".equals(name)].head => [
Assert.assertTrue('A001 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('A001 left .x field instanceof DataSubcomponent', field instanceof DataSubcomponent)
Assert.assertEquals('A001 left .x field named "x"', 'x', field.name)
// assert field is child of Alpha.Impl
Assert.assertTrue('A001 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('A001 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('A001 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('A001 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('A001 left x.m field instanceof DataSubcomponent', field instanceof DataSubcomponent)
// Assert field is child of Beta.Impl
Assert.assertTrue('A001 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('A001 left x.m target named "inp"', 'inp', elm.name)
// Assert elm is input port feature
]
]
]
]
Assert.assertEquals('A001 op equals "="', '=', op)
Assert.assertTrue('A001 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('A001 right expr value equals "1"', '1', ^val)
]
]
]
specs.filter(AssumeStatement).filter["A002".equals(name)].head => [
Assert.assertTrue('A002 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('A002 left .x field instanceof DataSubcomponent', field instanceof DataSubcomponent)
Assert.assertEquals('A002 left .x field named "x"', 'x', field.name)
// assert field is child of Alpha.Impl
Assert.assertTrue('A002 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('A002 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('A002 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('A002 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('A002 left x.m field instanceof DataSubcomponent', field instanceof DataSubcomponent)
// Assert field is child of Beta.Impl
Assert.assertTrue('A002 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('A002 left x.m target named "inp"', 'inp', elm.name)
// Assert elm is input port feature
]
]
]
]
Assert.assertEquals('A002 op equals "="', '=', op)
Assert.assertTrue('A002 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('A002 right expr value equals "1"', '1', ^val)
]
]
]
specs.filter(GuaranteeStatement).filter["G001".equals(name)].head => [
Assert.assertTrue('G001 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('G001 left .x field instanceof DataSubcomponent', field instanceof DataSubcomponent)
Assert.assertEquals('G001 left .x field named "x"', 'x', field.name)
// assert field is child of Alpha.Impl
Assert.assertTrue('G001 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('G001 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('G001 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('G001 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('G001 left x.m field instanceof DataSubcomponent', field instanceof DataSubcomponent)
// Assert field is child of Beta.Impl
Assert.assertTrue('G001 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('G001 left x.m target named "x"', 'x', elm.name)
// Assert elm is EqStatement
]
]
]
]
Assert.assertEquals('G001 op equals "="', '=', op)
Assert.assertTrue('G001 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('G001 right expr value equals "1"', '1', ^val)
]
]
]
specs.filter(GuaranteeStatement).filter["G002".equals(name)].head => [
Assert.assertTrue('G002 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('G002 left .x field instanceof DataSubcomponent', field instanceof DataSubcomponent)
Assert.assertEquals('G002 left .x field named "x"', 'x', field.name)
// assert field is child of Alpha.Impl
Assert.assertTrue('G002 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('G002 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('G002 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('G002 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('G002 left x.m field instanceof DataSubcomponent', field instanceof DataSubcomponent)
// Assert field is child of Beta.Impl
Assert.assertTrue('G002 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('G002 left x.m target named "x"', 'x', elm.name)
// Assert elm is EqStatement
]
]
]
]
Assert.assertEquals('G002 op equals "="', '=', op)
Assert.assertTrue('G002 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('G002 right expr value equals "1"', '1', ^val)
]
]
]
specs.filter(GuaranteeStatement).filter["G003".equals(name)].head => [
Assert.assertTrue('G001 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('G003 left .x field instanceof Arg', field instanceof Arg)
Assert.assertEquals('G003 left .x field named "x"', 'x', field.name)
// assert field is child of RecS1
Assert.assertTrue('G003 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('G003 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('G003 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('G003 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('G003 left x.m field instanceof Arg', field instanceof Arg)
// Assert field is child of RecS2
Assert.assertTrue('G003 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('G003 left x.m target named "y"', 'y', elm.name)
// Assert elm is EqStatement
]
]
]
]
Assert.assertEquals('G003 op equals "="', '=', op)
Assert.assertTrue('G003 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('G003 right expr value equals "1"', '1', ^val)
]
]
]
specs.filter(GuaranteeStatement).filter["G004".equals(name)].head => [
Assert.assertTrue('G0041 expr instanceof BinaryExpr', expr instanceof BinaryExpr)
(expr as BinaryExpr) => [
Assert.assertTrue(left instanceof SelectionExpr)
(left as SelectionExpr) => [
Assert.assertTrue('G004 left .x field instanceof Arg', field instanceof Arg)
Assert.assertEquals('G004 left .x field named "x"', 'x', field.name)
// assert field is child of RecS1
Assert.assertTrue('G004 left (x.m[1]) target instanceof ArraySubExpr', target instanceof ArraySubExpr)
(target as ArraySubExpr) => [
Assert.assertTrue('G004 left (x.m[1]) index instanceof IntLitExpr', index instanceof IntLitExpr)
(index as IntLitExpr) => [
Assert.assertEquals('G004 left (x.m[1]) index value equals "1"', '1', ^val)
]
Assert.assertTrue('G004 left x.m instanceof SelectionExpr', expr instanceof SelectionExpr)
(expr as SelectionExpr) => [
Assert.assertTrue('G004 left x.m field instanceof Arg', field instanceof Arg)
// Assert field is child of RecS2
Assert.assertTrue('G004 left x.m target instanceof NamedElmExpr', target instanceof NamedElmExpr)
(target as NamedElmExpr) => [
Assert.assertEquals('G001 left x.m target named "y"', 'y', elm.name)
// Assert elm is EqStatement
]
]
]
]
Assert.assertEquals('G004 op equals "="', '=', op)
Assert.assertTrue('G004 right instanceof IntLitExpr', right instanceof IntLitExpr)
(right as IntLitExpr) => [
Assert.assertEquals('G004 right expr value equals "1"', '1', ^val)
]
]
]
]
}

}
Loading