Skip to content

Commit

Permalink
Add support for empty implementations and AADL data ports without types
Browse files Browse the repository at this point in the history
  • Loading branch information
@daniel-larraz
daniel-larraz committed Jul 13, 2022
1 parent 6126c3e commit cc247a2
Show file tree
Hide file tree
Showing 2 changed files with 52 additions and 49 deletions.
3 changes: 2 additions & 1 deletion ...ndle/verdict-lustre-translator/src/main/java/edu/uiowa/clc/verdict/lustre/VDM2Lustre.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -628,7 +628,8 @@ public void visit(Port port, Node node) {

// Change Null DataType to Integer Default Type
if (dataType == null) {
port.setType(defaultType());
dataType = defaultType();
port.setType(dataType);
}

node_parameter.setDataType(dataType);
Expand Down
98 changes: 50 additions & 48 deletions ...verdict-lustre-translator/src/main/java/edu/uiowa/clc/verdict/lustre/VDMLustre2Kind2.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import java.util.TreeMap;
import java.util.stream.Collectors;
import verdict.vdm.vdm_data.DataType;
import verdict.vdm.vdm_data.PlainType;
import verdict.vdm.vdm_data.RecordField;
import verdict.vdm.vdm_data.SubrangeType;
import verdict.vdm.vdm_data.TypeDeclaration;
Expand Down Expand Up @@ -97,7 +98,9 @@ private static ProgramBuilder visit(LustreProgram modelProgram) {
if (node.isIsImported() != null && node.isIsImported()) {
pb.importNode(visitImportedComponent(node));
} else {
if (node.getBody().isIsMain() != null && node.getBody().isIsMain()) {
if (node.getBody() != null
&& node.getBody().isIsMain() != null
&& node.getBody().isIsMain()) {
pb.setMain(node.getName());
}
pb.addNode(visitComponent(node));
Expand All @@ -115,48 +118,45 @@ private static ProgramBuilder visit(LustreProgram modelProgram) {
* @return the Kind 2 Lustre type
*/
private static Type visit(DataType modelType) {
if (modelType == null) {
// Change Null DataType to Integer Type
modelType = new DataType();
modelType.setPlainType(PlainType.INT);
}
if (modelType.getPlainType() != null) {
return TypeUtil.named(modelType.getPlainType().value());
}

if (modelType.getUserDefinedType() != null) {
} else if (modelType.getUserDefinedType() != null) {
return TypeUtil.named(modelType.getUserDefinedType());
}

if (modelType.getSubrangeType() != null) {
} else if (modelType.getSubrangeType() != null) {
SubrangeType subrange = modelType.getSubrangeType();
return TypeUtil.intSubrange(subrange.getLowerBound(), subrange.getUpperBound());
}

if (modelType.getArrayType() != null) {
} else if (modelType.getArrayType() != null) {
return TypeUtil.array(
visit(modelType.getArrayType().getDataType()),
Integer.parseInt(modelType.getArrayType().getDimension()));
}

if (modelType.getTupleType() != null) {
} else if (modelType.getTupleType() != null) {
return TypeUtil.tuple(
modelType.getTupleType().getDataType().stream()
.map(dt -> visit(dt))
.collect(Collectors.toList()));
}

if (modelType.getEnumType() != null) {
} else if (modelType.getEnumType() != null) {
return TypeUtil.enumeration(modelType.getEnumType().getEnumValue());
}

if (modelType.getRecordType() != null) {
} else if (modelType.getRecordType() != null) {
// fields in the map have the same order as the RecordFields in the RecordField
// list
Map<String, Type> fields = new TreeMap<>((x, y) -> -1);
for (RecordField field : modelType.getRecordType().getRecordField()) {
fields.put(field.getName(), visit(field.getType()));
}
return TypeUtil.record(fields);
} else {
System.out.println("Warning: Bogus DataType detected! Replaced with Integer type");
modelType.setPlainType(PlainType.INT);
return TypeUtil.named(modelType.getPlainType().value());
}

throw new IllegalArgumentException(
"Datatype should either be: plain, user-defined, subrange, array, tuple, enum, or record type.");
// throw new IllegalArgumentException(
// "Datatype should either be: plain, user-defined, subrange, array, tuple, enum, or
// record type.");
}

/**
Expand Down Expand Up @@ -475,39 +475,41 @@ private static ComponentBuilder visitComponent(Node modelNode) {
nb.setContractBody(visit(modelNode.getContract()));
}

for (ConstantDeclaration constDecl : modelNode.getBody().getConstantDeclaration()) {
if (constDecl.getDataType() != null) {
if (constDecl.getDefinition() != null) {
nb.createLocalConst(
constDecl.getName(),
visit(constDecl.getDataType()),
visit(constDecl.getDefinition()));
if (modelNode.getBody() != null) {
for (ConstantDeclaration constDecl : modelNode.getBody().getConstantDeclaration()) {
if (constDecl.getDataType() != null) {
if (constDecl.getDefinition() != null) {
nb.createLocalConst(
constDecl.getName(),
visit(constDecl.getDataType()),
visit(constDecl.getDefinition()));
} else {
nb.createLocalConst(constDecl.getName(), visit(constDecl.getDataType()));
}
} else {
nb.createLocalConst(constDecl.getName(), visit(constDecl.getDataType()));
nb.createLocalConst(constDecl.getName(), visit(constDecl.getDefinition()));
}
} else {
nb.createLocalConst(constDecl.getName(), visit(constDecl.getDefinition()));
}
}

for (VariableDeclaration varDecl : modelNode.getBody().getVariableDeclaration()) {
nb.createLocalVar(varDecl.getName(), visit(varDecl.getDataType()));
}
for (VariableDeclaration varDecl : modelNode.getBody().getVariableDeclaration()) {
nb.createLocalVar(varDecl.getName(), visit(varDecl.getDataType()));
}

for (NodeEquation equation : modelNode.getBody().getEquation()) {
nb.addEquation(
equation.getLhs().getIdentifier().stream()
.map(var -> ExprUtil.id(var))
.collect(Collectors.toList()),
visit(equation.getRhs()));
}
for (NodeEquation equation : modelNode.getBody().getEquation()) {
nb.addEquation(
equation.getLhs().getIdentifier().stream()
.map(var -> ExprUtil.id(var))
.collect(Collectors.toList()),
visit(equation.getRhs()));
}

for (Expression assertion : modelNode.getBody().getAssertion()) {
nb.addAssertion(visit(assertion));
}
for (Expression assertion : modelNode.getBody().getAssertion()) {
nb.addAssertion(visit(assertion));
}

for (NodeProperty property : modelNode.getBody().getProperty()) {
nb.addProperty(property.getName(), visit(property.getExpression()));
for (NodeProperty property : modelNode.getBody().getProperty()) {
nb.addProperty(property.getName(), visit(property.getExpression()));
}
}

return nb;
Expand Down

0 comments on commit cc247a2

Please sign in to comment.