diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/ExpressionGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/ExpressionGenerator.java
index 4232c115a636b898d5e20d9bf14500bdf380b7b0..7511077e7cced71b152501ee467e6f6deb3925d7 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/ExpressionGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/ExpressionGenerator.java
@@ -252,7 +252,7 @@ public class ExpressionGenerator {
} else if(node instanceof RecordFieldAccessNode) {
return visitRecordFieldAccessNode((RecordFieldAccessNode) node);
}
- throw new RuntimeException("Given node is not implemented: " + node.getClass());
+ throw new RuntimeException("Given node is not implemented: " + node.getClass() + " at line " + node.getSourceCodePosition().getStartLine());
}
/*
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 8a61e33895cf7c266bf3705bd86db701d12029fd..6be74b61920da48c8153a9333818713a80abf68c 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/OperationGenerator.java
@@ -104,7 +104,9 @@ public class OperationGenerator {
return "";
}
} else {
- TemplateHandler.add(operation, "body", machineGenerator.visitSubstitutionNode(node.getSubstitution(), null));
+ if(!node.getName().startsWith("EXTERNAL_")) {
+ TemplateHandler.add(operation, "body", machineGenerator.visitSubstitutionNode(node.getSubstitution(), null));
+ }
}
TemplateHandler.add(operation, "lastStateCount", machineGenerator.getCurrentStateCount());
return operation.render();
diff --git a/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator.mch b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator.mch
new file mode 100644
index 0000000000000000000000000000000000000000..f3d895782431bbb10831bcf41420e0f7102d1a4a
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator.mch
@@ -0,0 +1,228 @@
+MACHINE DroneCommunicator// USES LibraryZMQ_RPC
+DEFINITIONS
+ "LibraryZMQ_RPC.def";
+ "LibraryReals.def";
+ SET_PREF_MAX_OPERATIONS == 0;
+CONSTANTS DRONE_URL
+PROPERTIES DRONE_URL:STRING & DRONE_URL = "radio://0/80/2M/5700B500F4"
+VARIABLES init, socket, cycle
+INVARIANT
+ init:BOOL &
+ socket:INTEGER &
+ cycle:INTEGER
+INITIALISATION
+ init := FALSE;
+ socket := 0;
+ cycle := 1
+
+OPERATIONS
+ EXTERNAL_Init =
+ SELECT init = FALSE THEN
+ socket := ZMQ_RPC_INIT("tcp://localhost:22272");
+ init := TRUE
+ END;
+
+ EXTERNAL_open_link =
+ SELECT init = TRUE THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "open_link", {("url" |-> RpcString(DRONE_URL)), ("reinit" |-> RpcBoolean(TRUE))}))
+ END
+ END;
+
+ /*
+ Available commanders:
+ "motion" - cflib.positioning.motion_commander.MotionCommander
+ "high_level" - cflib.crazyflie.high_level_commander.HighLevelCommander
+ "position_high_level" (the default) - cflib.positioning.position_hl_commander.PositionHlCommander
+ */
+ EXTERNAL_open_link_with_commander_type(commander) =
+ SELECT
+ init = TRUE
+ & commander : STRING
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "open_link", {("url" |-> RpcString(DRONE_URL)), ("reinit" |-> RpcBoolean(TRUE)), ("commander" |-> RpcString(commander))}))
+ END
+ END;
+
+ EXTERNAL_close_link =
+ SELECT init = TRUE THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "close_link", {("url" |-> RpcString(DRONE_URL))}))
+ END
+ END;
+
+ EXTERNAL_register_sensors =
+ SELECT init = TRUE THEN
+ VAR res1, res2, res3 IN
+ res1 := RpcSuccess~(ZMQ_RPC_SEND(socket, "register_log", {
+ ("url" |-> RpcString(DRONE_URL)),
+ ("name" |-> RpcString("Telemetry")),
+ ("variables" |-> RpcArray([
+ RpcString("stateEstimate.x"),
+ RpcString("stateEstimate.y"),
+ RpcString("stateEstimate.z"),
+ RpcString("stateEstimate.roll"),
+ RpcString("stateEstimate.pitch"),
+ RpcString("stateEstimate.yaw")
+ ]))}));
+ res2 := RpcSuccess~(ZMQ_RPC_SEND(socket, "register_log", {
+ ("url" |-> RpcString(DRONE_URL)),
+ ("name" |-> RpcString("Power")),
+ ("variables" |-> RpcArray([
+ RpcString("pm.batteryLevel")
+ ]))}));
+ res3 := RpcSuccess~(ZMQ_RPC_SEND(socket, "register_log", {
+ ("url" |-> RpcString(DRONE_URL)),
+ ("name" |-> RpcString("Ranging")),
+ ("variables" |-> RpcArray([
+ RpcString("range.front"),
+ RpcString("range.back"),
+ RpcString("range.up"),
+ RpcString("range.left"),
+ RpcString("range.right"),
+ RpcString("range.zrange")
+ ]))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Takeoff =
+ SELECT init = TRUE THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "takeoff", {("url" |-> RpcString(DRONE_URL))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Land =
+ SELECT init = TRUE THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "land", {("url" |-> RpcString(DRONE_URL))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Left(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "left", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Right(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "right", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Up(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "up", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Down(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "down", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Forward(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "forward", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ EXTERNAL_Drone_Backward(dist) =
+ SELECT
+ init = TRUE &
+ dist : 0..2000
+ THEN
+ VAR res IN
+ res := RpcSuccess~(ZMQ_RPC_SEND(socket, "backward", {("url" |-> RpcString(DRONE_URL)), ("distance" |-> RpcFloat(RDIV(real(dist), real(1000))))}))
+ END
+ END;
+
+ out <-- EXTERNAL_Drone_GetX =
+ SELECT init = TRUE THEN
+ out := floor(RMUL(1000.0, RpcFloat~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("stateEstimate.x"))})))));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetY =
+ SELECT init = TRUE THEN
+ out := floor(RMUL(1000.0, RpcFloat~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("stateEstimate.y"))})))));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetZ =
+ SELECT init = TRUE THEN
+ out := floor(RMUL(1000.0, RpcFloat~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("stateEstimate.z"))})))));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetBattery =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("pm.batteryLevel"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetFrontDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.front"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetBackDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.back"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetUpDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.up"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetDownDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.zrange"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetLeftDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.left"))})));
+ cycle := cycle + 1
+ END;
+
+ out <-- EXTERNAL_Drone_GetRightDistance =
+ SELECT init = TRUE THEN
+ out := RpcInteger~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> RpcString(DRONE_URL)), ("name" |-> RpcString("range.right"))})));
+ cycle := cycle + 1
+ END;
+
+ EXTERNAL_Destroy =
+ SELECT init = TRUE THEN
+ ZMQ_RPC_DESTROY(socket);
+ init := FALSE
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator_Mockup.mch b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator_Mockup.mch
index 0ada38950496d633255f2ec7b5d885c14a6badd0..4e0334891b112db547790b57c8330a72121687a5 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator_Mockup.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator_Mockup.mch
@@ -1,4 +1,8 @@
MACHINE DroneCommunicator_Mockup
+DEFINITIONS
+ "LibraryZMQ_RPC.def";
+ "LibraryReals.def";
+ SET_PREF_MAX_OPERATIONS == 0;
CONSTANTS DRONE_URL
PROPERTIES DRONE_URL:STRING & DRONE_URL = "radio://0/80/2M/5700B500F4"
VARIABLES init, socket, cycle
diff --git a/src/test/resources/de/hhu/stups/codegenerator/drone/DroneMainController.mch b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneMainController.mch
index 7733c48bb01205a5926b77a80a3726c6eec4d76e..11d756c2750f8359328b9f861f06c0355316c4c5 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/drone/DroneMainController.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/drone/DroneMainController.mch
@@ -1,5 +1,5 @@
MACHINE DroneMainController
-INCLUDES DroneSafetyController, DroneCommunicator_Mockup
+INCLUDES DroneSafetyController, DroneCommunicator
OPERATIONS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/liftbenchmarks/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/liftbenchmarks/Lift.mch
index bc57c76fd4177c464e0c77a80ea34e3999654352..5c5658de9cee6bcac99efed7951ce10a4f14cbb7 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/liftbenchmarks/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/liftbenchmarks/Lift.mch
@@ -1,15 +1,15 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
+ inc = PRE level<100 THEN level := level + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END
+ dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project10/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project10/Lift.mch
index 177693d12a75feb3e843ae651fe76ff6ca910ea3..b8b78f4fa1eb79983da852b97e778ff29d9f07ed 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project10/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project10/Lift.mch
@@ -1,14 +1,14 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project5/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project5/Lift.mch
index 177693d12a75feb3e843ae651fe76ff6ca910ea3..b8b78f4fa1eb79983da852b97e778ff29d9f07ed 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project5/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project5/Lift.mch
@@ -1,14 +1,14 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project6/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project6/Lift.mch
index c8d98c5aa24aae96fa6a118f6e910244cc7d763f..7f994d0316bf12eca8520028f9db25492db203de 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project6/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project6/Lift.mch
@@ -1,15 +1,15 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END;
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END;
open_door = skip;
close_door = skip
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project6/Lift2.mch b/src/test/resources/de/hhu/stups/codegenerator/project6/Lift2.mch
index e497996fe26e96ce940343ffce86c2824c52fd9d..53e1dca6757533e0ff022b6d7935a495e73ee28e 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project6/Lift2.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project6/Lift2.mch
@@ -2,16 +2,16 @@ REFINEMENT Lift2
REFINES Lift
-VARIABLES floor, door_open
+VARIABLES level, door_open
-INVARIANT floor : 0..100 & door_open : BOOL
+INVARIANT level : 0..100 & door_open : BOOL
-INITIALISATION floor := 0 || door_open := FALSE
+INITIALISATION level := 0 || door_open := FALSE
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END;
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END;
open_door = PRE door_open=FALSE THEN door_open := TRUE END ;
close_door = PRE door_open=TRUE THEN door_open := FALSE END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project7/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project7/Lift.mch
index c8d98c5aa24aae96fa6a118f6e910244cc7d763f..7f994d0316bf12eca8520028f9db25492db203de 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project7/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project7/Lift.mch
@@ -1,15 +1,15 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END;
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END;
open_door = skip;
close_door = skip
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project8/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project8/Lift.mch
index 177693d12a75feb3e843ae651fe76ff6ca910ea3..b8b78f4fa1eb79983da852b97e778ff29d9f07ed 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project8/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project8/Lift.mch
@@ -1,14 +1,14 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/project9/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/project9/Lift.mch
index 177693d12a75feb3e843ae651fe76ff6ca910ea3..b8b78f4fa1eb79983da852b97e778ff29d9f07ed 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/project9/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/project9/Lift.mch
@@ -1,14 +1,14 @@
MACHINE Lift
-VARIABLES floor
+VARIABLES level
-INVARIANT floor : 0..100 /* NAT */
+INVARIANT level : 0..100 /* NAT */
-INITIALISATION floor := 0
+INITIALISATION level := 0
OPERATIONS
- inc = PRE floor<100 THEN floor := floor + 1 END ;
- dec = PRE floor>0 THEN floor := floor - 1 END
+ inc = PRE level<100 THEN level := level + 1 END ;
+ dec = PRE level>0 THEN level := level - 1 END
END
\ No newline at end of file