From 6767ae6a2bf8ce5c54705d95aa814c85a37ae22a Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Thu, 31 Oct 2024 14:00:40 +0100
Subject: [PATCH] Support generation of external functions (must be
implemented) for Java
---
.../generators/MachineGenerator.java | 16 +++++++++-
.../generators/OperationGenerator.java | 2 ++
.../generators/SubstitutionGenerator.java | 3 +-
.../hhu/stups/codegenerator/CppTemplate.stg | 5 ++-
.../hhu/stups/codegenerator/JavaTemplate.stg | 31 ++++++++++++++++---
.../de/hhu/stups/codegenerator/TsTemplate.stg | 3 ++
.../codegenerator/java/TestMachines.java | 5 +++
.../hhu/stups/codegenerator/Lift_External.mch | 15 +++++++++
8 files changed, 72 insertions(+), 8 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/Lift_External.mch
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
index c5265a128..836aa2e9b 100755
--- a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
@@ -276,6 +276,13 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
TemplateHandler.add(machine, "props", modelCheckingGenerator.generateModelCheckingProBProp(node));
}
TemplateHandler.add(machine, "machineString", modelCheckingGenerator.generateToString());
+ TemplateHandler.add(machine, "externalFunctions", machineNode.getOperations()
+ .stream()
+ .filter(op -> op.getName().startsWith("EXTERNAL_"))
+ .map(op -> generateExternalFunction(op.getName(), op.getParams()
+ .stream()
+ .map(DeclarationNode::getName).collect(Collectors.toList())))
+ .collect(Collectors.toList()));
generateBody(node, machine);
return machine.render();
}
@@ -365,6 +372,13 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
TemplateHandler.add(machine, "structs", recordStructGenerator.generateStructs());
}
+ private String generateExternalFunction(String name, List<String> parameters) {
+ ST template = currentGroup.getInstanceOf("external_function");
+ TemplateHandler.add(template, "name", name);
+ TemplateHandler.add(template, "parameters", parameters);
+ return template.render();
+ }
+
private List<String> generateProjectionClasses() {
List<String> projectionClasses = new ArrayList<>();
for(OperationNode operation : machineNode.getOperations()) {
@@ -428,7 +442,6 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
}
private String generateCopyConstructor(MachineNode node) {
-
ST template = currentGroup.getInstanceOf("copy_constructor");
TemplateHandler.add(template, "machine", nameHandler.handle(node.getName()));
List<DeclarationNode> parameters = new ArrayList<>(node.getConstants());
@@ -444,6 +457,7 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
TemplateHandler.add(template, "parameters", declarationGenerator.generateDeclarations(parameters, OperationGenerator.DeclarationType.PARAMETER, false));
TemplateHandler.add(template, "assignments", assignments);
+ TemplateHandler.add(template, "hasExternals", node.getOperations().stream().anyMatch(op -> op.getName().startsWith("EXTERNAL_")));
return template.render();
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java
index 2ef5b5469..54d851f26 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java
@@ -121,7 +121,9 @@ public class OperationGenerator {
.filter(identifier -> !globals.contains(identifier.getName()))
.collect(Collectors.toList()), DeclarationType.LOCAL_DECLARATION, false));
TemplateHandler.add(operation, "operationName", nameHandler.handleIdentifier(node.getName(), INCLUDED_MACHINES));
+ TemplateHandler.add(operation, "isExternal", node.getName().startsWith("EXTERNAL_"));
TemplateHandler.add(operation, "parameters", declarationGenerator.generateDeclarations(node.getParams(), DeclarationType.PARAMETER, false));
+ TemplateHandler.add(operation, "parameterNames", node.getParams().stream().map(DeclarationNode::getName).collect(Collectors.toList()));
TemplateHandler.add(operation, "returnParameters", declarationGenerator.generateDeclarations(node.getOutputParams(), DeclarationType.PARAMETER, true));
return operation;
}
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
index 15d3733d2..927c971bd 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/SubstitutionGenerator.java
@@ -162,7 +162,8 @@ public class SubstitutionGenerator {
TemplateHandler.add(initialization, "copy", copy);
TemplateHandler.add(initialization, "forVisualization", machineGenerator.isForVisualisation());
TemplateHandler.add(initialization, "forModelChecking", machineGenerator.isForModelChecking());
-
+ TemplateHandler.add(initialization, "hasExternalFunctions", machineGenerator.getMachineNode().getOperations()
+ .stream().anyMatch(op -> op.getName().startsWith("EXTERNAL_")));
return initialization.render();
}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
index 4807e7844..2a6377c51 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
@@ -1792,4 +1792,7 @@ include_initialization() ::= <<
transition_cache_declaration(type, identifier, operationHasParams) ::= <<
>>
-set_initialization(identifier, type, enums) ::= <<>>
\ No newline at end of file
+set_initialization(identifier, type, enums) ::= <<>>
+
+external_function(name, parameters) ::= <<
+>>
\ No newline at end of file
diff --git a/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
index 599d193c4..fc4b0607e 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
@@ -3,7 +3,7 @@ abstract, assert, boolean, break, byte, case, catch, char, class, continue, defa
>>
-machine(forModelChecking, imports, machine, projectionClasses, structs, constants_declarations, includes, enums, sets, declarations, initialization, mainMethod, copyConstructor, operations, addition, getters, transitions, projection, invariant, copy, hash_equal, modelcheck, lambdaFunctions, choicePoints, choicePointsGetters, choicePointOperationFlags, choicePointOperationFlagGetters, choicePointOperationFlagResets, choicePointOperationTriggered, choicePointOperationTriggeredResets, choicePointOperationTriggeredFlags, choicePointOperationApplies) ::= <<
+machine(forModelChecking, imports, machine, projectionClasses, structs, constants_declarations, includes, enums, sets, declarations, initialization, mainMethod, copyConstructor, operations, addition, getters, transitions, projection, invariant, copy, hash_equal, modelcheck, lambdaFunctions, choicePoints, choicePointsGetters, choicePointOperationFlags, choicePointOperationFlagGetters, choicePointOperationFlagResets, choicePointOperationTriggered, choicePointOperationTriggeredResets, choicePointOperationTriggeredFlags, choicePointOperationApplies, externalFunctions) ::= <<
<imports; separator="\n">
<if(forModelChecking)>
import java.util.HashMap;
@@ -36,6 +36,13 @@ import de.hhu.stups.btypes.BUtils;
public class <machine> {
+ <if(externalFunctions)>
+ public interface ExternalFunctionsInterface {
+ <externalFunctions; separator="\n">
+ }
+
+ private final ExternalFunctionsInterface _externalFunctions;
+ <endif>
<if(forModelChecking)>
private static final Var ASSOC;
@@ -283,7 +290,7 @@ record(struct, parameters) ::= <<
new <struct>(<parameters; separator=", ">)
>>
-initialization(machine, properties, values, body, iterationConstruct, propertiesCheck) ::= <<
+initialization(machine, properties, values, body, iterationConstruct, propertiesCheck, hasExternalFunctions) ::= <<
<if(properties)>
<if(values)>
static {
@@ -299,7 +306,10 @@ static {
<endif>
<endif>
-public <machine>() {
+public <machine>(<if(hasExternalFunctions)>ExternalFunctionsInterface _externalFunctions<endif>) {
+ <if(hasExternalFunctions)>
+ this._externalFunctions = _externalFunctions;
+ <endif>
<body>
}
>>
@@ -307,11 +317,15 @@ public <machine>() {
method() ::= <<
>>
-operation(returnType, operationName, parameters, locals, body, return) ::= <<
+operation(returnType, operationName, parameters, locals, body, return, isExternal, parameterNames) ::= <<
public <returnType> <operationName>(<parameters; separator=", ">) {
+ <if(isExternal)>
+ _externalFunctions.<operationName>(<parameterNames; separator=", ">);
+ <else>
<locals; separator="\n">
<body>
<return>
+ <endif>
}
>>
@@ -523,8 +537,11 @@ public boolean <invariantFunction>() {
}
>>
-copy_constructor(machine, assignments) ::= <<
+copy_constructor(machine, assignments, hasExternals) ::= <<
public <machine>(<machine> copy) {
+ <if(hasExternals)>
+ this._externalFunctions = copy._externalFunctions;
+ <endif>
<assignments; separator="\n">
}
>>
@@ -1849,3 +1866,7 @@ transition_cache_declaration(type, identifier, operationHasParams) ::= <<
>>
set_initialization(identifier, type, enums) ::= <<>>
+
+external_function(name, parameters) ::= <<
+void <name>(<parameters; separator=",">);
+>>
\ No newline at end of file
diff --git a/src/main/resources/de/hhu/stups/codegenerator/TsTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/TsTemplate.stg
index 653161df6..5704ddb90 100755
--- a/src/main/resources/de/hhu/stups/codegenerator/TsTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/TsTemplate.stg
@@ -1442,3 +1442,6 @@ transition_cache_declaration(type, identifier, operationHasParams) ::= <<
>>
set_initialization(identifier, type, enums) ::= <<>>
+
+external_function(name, parameters) ::= <<
+>>
\ No newline at end of file
diff --git a/src/test/java/de/hhu/stups/codegenerator/java/TestMachines.java b/src/test/java/de/hhu/stups/codegenerator/java/TestMachines.java
index d8ca22ef2..7a7dae359 100644
--- a/src/test/java/de/hhu/stups/codegenerator/java/TestMachines.java
+++ b/src/test/java/de/hhu/stups/codegenerator/java/TestMachines.java
@@ -662,6 +662,11 @@ public class TestMachines extends TestJava {
testJavaMC("Lift_MC_Large");
}
+ @Test
+ public void testLift_MC_External() throws Exception {
+ testJava("Lift_External");
+ }
+
@Ignore
@Test
public void testNondeterministic_MC() throws Exception {
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Lift_External.mch b/src/test/resources/de/hhu/stups/codegenerator/Lift_External.mch
new file mode 100644
index 000000000..45c8853ff
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/Lift_External.mch
@@ -0,0 +1,15 @@
+MACHINE Lift_External
+
+VARIABLES floor
+
+INVARIANT floor : 0..100 /* NAT */
+
+INITIALISATION floor := 0
+
+OPERATIONS
+
+ inc = PRE floor<100 THEN floor := floor + 1 END ;
+ dec = PRE floor>0 THEN floor := floor - 1 END;
+ EXTERNAL_SEND = skip
+
+END
\ No newline at end of file
--
GitLab