Merge pull request #2030 from lf-lang/diagram-reaction-names

Show reaction names in diagrams

core/src/main/java/org/lflang/diagram/synthesis/LinguaFrancaSynthesis.java

@@ -221,7 +221,7 @@ public class LinguaFrancaSynthesis extends AbstractDiagramSynthesis<Model> {
       SynthesisOption.createCheckOption("Dependency Cycle Detection", true);
 
   public static final SynthesisOption SHOW_USER_LABELS =
-      SynthesisOption.createCheckOption("User Labels (@label in JavaDoc)", true)
+      SynthesisOption.createCheckOption("User Labels (@label attribute)", true)
           .setCategory(APPEARANCE);
   public static final SynthesisOption SHOW_HYPERLINKS =
       SynthesisOption.createCheckOption("Expand/Collapse Hyperlinks", false)
@@ -237,6 +237,9 @@ public class LinguaFrancaSynthesis extends AbstractDiagramSynthesis<Model> {
       SynthesisOption.createCheckOption("Multiport Widths", false).setCategory(APPEARANCE);
   public static final SynthesisOption SHOW_REACTION_CODE =
       SynthesisOption.createCheckOption("Reaction Code", false).setCategory(APPEARANCE);
+
+  public static final SynthesisOption SHOW_REACTION_NAMES =
+      SynthesisOption.createCheckOption("Reaction Names", false).setCategory(APPEARANCE);
   public static final SynthesisOption SHOW_REACTION_ORDER_EDGES =
       SynthesisOption.createCheckOption("Reaction Order Edges", false).setCategory(APPEARANCE);
   public static final SynthesisOption SHOW_REACTOR_HOST =
@@ -288,6 +291,7 @@ public List<SynthesisOption> getDisplayedSynthesisOptions() {
         USE_ALTERNATIVE_DASH_PATTERN,
         SHOW_PORT_NAMES,
         SHOW_MULTIPORT_WIDTH,
+        SHOW_REACTION_NAMES,
         SHOW_REACTION_CODE,
         SHOW_REACTION_ORDER_EDGES,
         SHOW_REACTOR_HOST,

core/src/main/java/org/lflang/diagram/synthesis/styles/LinguaFrancaShapeExtensions.java

@@ -414,11 +414,22 @@ public KPolygon addReactionFigure(KNode node, ReactionInstance reaction) {
         minHeight);
     _kContainerRenderingExtensions.setGridPlacement(contentContainer, 1);
 
-    if (reactor.reactions.size() > 1) {
-      KText textToAdd =
-          _kContainerRenderingExtensions.addText(
-              contentContainer, Integer.toString(reactor.reactions.indexOf(reaction) + 1));
-      _kRenderingExtensions.setFontBold(textToAdd, true);
+    // Display the reaction name or its index.
+    String reactionText = null;
+    if (getBooleanValue(LinguaFrancaSynthesis.SHOW_REACTION_NAMES)) {
+      reactionText = reaction.getName();
+    } else if (reactor.reactions.size() > 1) {
+      reactionText = Integer.toString(reactor.reactions.indexOf(reaction) + 1);
+    }
+    if (!StringExtensions.isNullOrEmpty(reactionText)) {
+      KText textToAdd = _kContainerRenderingExtensions.addText(contentContainer, reactionText);
+      if (getBooleanValue(LinguaFrancaSynthesis.SHOW_REACTION_NAMES)) {
+        // show reaction names in normal font and slightly smaller (like port names)
+        _kRenderingExtensions.setFontSize(textToAdd, 8);
+      } else {
+        // show the reaction index in bold font
+        _kRenderingExtensions.setFontBold(textToAdd, true);
+      }
       _linguaFrancaStyleExtensions.noSelectionStyle(textToAdd);
       DiagramSyntheses.suppressSelectability(textToAdd);
     }

core/src/main/java/org/lflang/generator/ReactionInstance.java

@@ -29,6 +29,7 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
+import org.eclipse.xtext.xbase.lib.StringExtensions;
 import org.lflang.TimeValue;
 import org.lflang.ast.ASTUtils;
 import org.lflang.lf.Action;
@@ -352,14 +353,20 @@ public List<TimeValue> getInferredDeadlinesList() {
   }
 
   /**
-   * Return the name of this reaction, which is 'reaction_n', where n is replaced by the reaction
-   * index.
+   * Return the name of this reaction.
+   *
+   * <p>If the reaction is not named, this returns 'reaction_n', where n is replaced by the reaction
+   * index + 1.
    *
    * @return The name of this reaction.
    */
   @Override
   public String getName() {
-    return "reaction_" + this.index;
+    if (StringExtensions.isNullOrEmpty(getDefinition().getName())) {
+      return "reaction_" + (this.index + 1);
+    } else {
+      return getDefinition().getName();
+    }
   }
 
   /**

test/C/src/verifier/ADASModel.lf

@@ -82,7 +82,7 @@ reactor Dashboard {
 @property(
     name = "responsive",
     tactic = "bmc",
-    spec = "G[0, 10 ms]((ADASModel_l_reaction_0 && (F[0](ADASModel_p_requestStop == 1))) ==> (F[0, 55 ms]( ADASModel_b_brakesApplied == 1 )))",
+    spec = "G[0, 10 ms]((ADASModel_l_reaction_1 && (F[0](ADASModel_p_requestStop == 1))) ==> (F[0, 55 ms]( ADASModel_b_brakesApplied == 1 )))",
     expect = true)
 main reactor ADASModel {
   c = new Camera()

test/C/src/verifier/AircraftDoor.lf

@@ -37,7 +37,7 @@ reactor Door {
 @property(
     name = "vision_works",
     tactic = "bmc",
-    spec = "((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_0 ==> (AircraftDoor_door_doorOpen == 1))))",
+    spec = "((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_1 ==> (AircraftDoor_door_doorOpen == 1))))",
     expect = true)
 main reactor AircraftDoor {
   controller = new Controller()

test/C/src/verifier/Alarm.lf

@@ -31,7 +31,7 @@ reactor Controller {
 @property(
     name = "machine_stops_within_1_sec",
     tactic = "bmc",
-    spec = "G[0, 1 sec]((Alarm_c_reaction_0) ==> F(0, 1 sec](Alarm_c_reaction_1)))",
+    spec = "G[0, 1 sec]((Alarm_c_reaction_1) ==> F(0, 1 sec](Alarm_c_reaction_2)))",
     expect = true)
 main reactor {
   c = new Controller()

test/C/src/verifier/PingPongVerifier.lf

@@ -58,7 +58,7 @@ reactor Pong {
 @property(
     name = "no_two_consecutive_pings",
     tactic = "bmc",
-    spec = "G[0, 4 nsec](PingPongVerifier_ping_reaction_1 ==> X(!PingPongVerifier_ping_reaction_1))",
+    spec = "G[0, 4 nsec](PingPongVerifier_ping_reaction_2 ==> X(!PingPongVerifier_ping_reaction_2))",
     expect = false)
 main reactor PingPongVerifier {
   ping = new Ping()

test/C/src/verifier/Ring.lf

@@ -36,7 +36,7 @@ reactor Node {
 @property(
     name = "full_circle",
     tactic = "bmc",
-    spec = "F[0, 10 nsec](Ring_s_reaction_2)",
+    spec = "F[0, 10 nsec](Ring_s_reaction_3)",
     expect = true)
 main reactor {
   s = new Source()

test/C/src/verifier/SafeSend.lf

@@ -50,7 +50,7 @@ reactor Server {
 @property(
     name = "success",
     tactic = "bmc",
-    spec = "(F[0, 1 sec](SafeSend_c_reaction_1))",
+    spec = "(F[0, 1 sec](SafeSend_c_reaction_2))",
     expect = true)
 main reactor {
   c = new Client()

test/C/src/verifier/TrainDoor.lf

@@ -31,7 +31,7 @@ reactor Door {
 @property(
     name = "train_does_not_move_until_door_closes",
     tactic = "bmc",
-    spec = "(!TrainDoor_t_reaction_0)U[0, 1 sec](TrainDoor_d_reaction_0)",
+    spec = "(!TrainDoor_t_reaction_1)U[0, 1 sec](TrainDoor_d_reaction_1)",
     expect = false)
 main reactor {
   c = new Controller()

test/C/src/verifier/UnsafeSend.lf

@@ -50,7 +50,7 @@ reactor Server {
 @property(
     name = "success",
     tactic = "bmc",
-    spec = "(F[0, 5 nsec](UnsafeSend_c_reaction_1))",
+    spec = "(F[0, 5 nsec](UnsafeSend_c_reaction_2))",
     expect = false)
 main reactor {
   c = new Client()