From 1d43a7d18cfb8aee5bf01a52e2f49939aaaa3f37 Mon Sep 17 00:00:00 2001
From: Fabian Vu <fabian.vu@hhu.de>
Date: Tue, 14 Jan 2025 15:39:54 +0100
Subject: [PATCH] Rename floor to level
---
.../generators/ExpressionGenerator.java | 2 +-
.../generators/OperationGenerator.java | 4 +-
.../codegenerator/drone/DroneCommunicator.mch | 228 ++++++++++++++++++
.../drone/DroneCommunicator_Mockup.mch | 4 +
.../drone/DroneMainController.mch | 2 +-
.../codegenerator/liftbenchmarks/Lift.mch | 10 +-
.../stups/codegenerator/project10/Lift.mch | 10 +-
.../hhu/stups/codegenerator/project5/Lift.mch | 10 +-
.../hhu/stups/codegenerator/project6/Lift.mch | 10 +-
.../stups/codegenerator/project6/Lift2.mch | 10 +-
.../hhu/stups/codegenerator/project7/Lift.mch | 10 +-
.../hhu/stups/codegenerator/project8/Lift.mch | 10 +-
.../hhu/stups/codegenerator/project9/Lift.mch | 10 +-
13 files changed, 277 insertions(+), 43 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/drone/DroneCommunicator.mch
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 4232c115a..7511077e7 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 8a61e3389..6be74b619 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 000000000..f3d895782
--- /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 0ada38950..4e0334891 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 7733c48bb..11d756c27 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 bc57c76fd..5c5658de9 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 177693d12..b8b78f4fa 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 177693d12..b8b78f4fa 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 c8d98c5aa..7f994d031 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 e497996fe..53e1dca67 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 c8d98c5aa..7f994d031 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 177693d12..b8b78f4fa 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 177693d12..b8b78f4fa 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
--
GitLab