Quasi-static scheduler based on PretVM

core/src/main/java/org/lflang/AttributeUtils.java

@@ -142,6 +142,33 @@ public static String getAttributeValue(EObject node, String attrName) {
     return value;
   }
 
+  /**
+   * Return the first argument, which has the type Time, specified for the attribute.
+   *
+   * <p>This should be used if the attribute is expected to have a single argument whose type is
+   * Time. If there is no argument, null is returned.
+   */
+  public static Time getFirstArgumentTime(Attribute attr) {
+    if (attr == null || attr.getAttrParms().isEmpty()) {
+      return null;
+    }
+    return attr.getAttrParms().get(0).getTime();
+  }
+
+  /**
+   * Search for an attribute with the given name on the given AST node and return its first argument
+   * as Time.
+   *
+   * <p>This should only be used on attributes that are expected to have a single argument with type
+   * Time.
+   *
+   * <p>Returns null if the attribute is not found or if it does not have any arguments.
+   */
+  public static Time getAttributeTime(EObject node, String attrName) {
+    final var attr = findAttributeByName(node, attrName);
+    return getFirstArgumentTime(attr);
+  }
+
   /**
    * Search for an attribute with the given name on the given AST node and return its first argument
    * as a String.
@@ -241,6 +268,15 @@ public static boolean hasCBody(Reaction reaction) {
     return findAttributeByName(reaction, "_c_body") != null;
   }
 
+  /** Return a time value that represents the WCET of a reaction. */
+  public static TimeValue getWCET(Reaction reaction) {
+    Time wcet = getAttributeTime(reaction, "wcet");
+    if (wcet == null) return TimeValue.MAX_VALUE;
+    int value = wcet.getInterval();
+    TimeUnit unit = TimeUnit.fromName(wcet.getUnit());
+    return new TimeValue(value, unit);
+  }
+
   /** Return the declared label of the node, as given by the @label annotation. */
   public static String getLabel(EObject node) {
     return getAttributeValue(node, "label");

core/src/main/java/org/lflang/LinguaFranca.xtext

@@ -257,7 +257,7 @@ Attribute:
 ;
 
 AttrParm:
-    (name=ID '=')? value=Literal;
+    (name=ID '=')? (value=Literal | time=Time);
 
 /////////// For target parameters
 

core/src/main/java/org/lflang/TimeTag.java

@@ -0,0 +1,58 @@
+package org.lflang;
+
+/**
+ * Class representing a logical time tag, which is a pair that consists of a timestamp and a
+ * microstep.
+ */
+public class TimeTag implements Comparable<TimeTag> {
+
+  public static final TimeTag ZERO = new TimeTag(TimeValue.ZERO, 0L);
+  public static final TimeTag FOREVER = new TimeTag(TimeValue.MAX_VALUE, Long.MAX_VALUE);
+
+  public final TimeValue time;
+  public final Long microstep;
+
+  /** Constructor */
+  public TimeTag(TimeValue time, Long microstep) {
+    this.time = time;
+    this.microstep = microstep;
+  }
+
+  /** Copy constructor */
+  public TimeTag(TimeTag that) {
+    this.time = that.time;
+    this.microstep = that.microstep;
+  }
+
+  /**
+   * Whether this time tag represents FOREVER, which is interpreted as the maximum TimeValue.
+   *
+   * @return True if the tag is FOREVER, false otherwise.
+   */
+  public boolean isForever() {
+    return time.equals(TimeValue.MAX_VALUE);
+  }
+
+  /**
+   * When comparing two time tags, first compare their time fields. If they are equal, compare their
+   * microsteps.
+   */
+  @Override
+  public int compareTo(TimeTag t) {
+    if (this.time.compareTo(t.time) < 0) return -1;
+    else if (this.time.compareTo(t.time) > 0) return 1;
+    else return this.microstep.compareTo(t.microstep);
+  }
+
+  @Override
+  public boolean equals(Object o) {
+    if (this == o) return true;
+    if (o instanceof TimeTag t && this.compareTo(t) == 0) return true;
+    return false;
+  }
+
+  @Override
+  public String toString() {
+    return "( " + this.time + ", " + this.microstep + " )";
+  }
+}

core/src/main/java/org/lflang/analyses/statespace/Event.java

@@ -1,14 +1,15 @@
 package org.lflang.analyses.statespace;
 
+import org.lflang.TimeTag;
 import org.lflang.generator.TriggerInstance;
 
-/** A node in the state space diagram representing a step in the execution of an LF program. */
+/** A class representing a tagged signal, for analytical purposes */
 public class Event implements Comparable<Event> {
 
   private final TriggerInstance<?> trigger;
-  private Tag tag;
+  private TimeTag tag;
 
-  public Event(TriggerInstance trigger, Tag tag) {
+  public Event(TriggerInstance trigger, TimeTag tag) {
     this.trigger = trigger;
     this.tag = tag;
   }
@@ -41,7 +42,7 @@ public String toString() {
     return "(" + trigger.getFullName() + ", " + tag + ")";
   }
 
-  public Tag getTag() {
+  public TimeTag getTag() {
     return tag;
   }
 

core/src/main/java/org/lflang/analyses/statespace/EventQueue.java

@@ -2,10 +2,7 @@
 
 import java.util.PriorityQueue;
 
-/**
- * An event queue implementation that sorts events in the order of _time tags_ and _trigger names_
- * based on the implementation of compareTo() in the Event class.
- */
+/** An event queue for analyzing the logical behavior of an LF program */
 public class EventQueue extends PriorityQueue<Event> {
 
   /**

core/src/main/java/org/lflang/analyses/statespace/StateInfo.java

@@ -2,23 +2,29 @@
 
 import java.util.ArrayList;
 import java.util.HashMap;
+import org.lflang.TimeTag;
 
 /** A class that represents information in a step in a counterexample trace */
 public class StateInfo {
 
   public ArrayList<String> reactions = new ArrayList<>();
-  public Tag tag;
+  public TimeTag tag;
   public HashMap<String, String> variables = new HashMap<>();
   public HashMap<String, String> triggers = new HashMap<>();
   public HashMap<String, String> scheduled = new HashMap<>();
   public HashMap<String, String> payloads = new HashMap<>();
 
   public void display() {
-    System.out.println("reactions: " + reactions);
-    System.out.println("tag: " + tag);
-    System.out.println("variables: " + variables);
-    System.out.println("triggers: " + triggers);
-    System.out.println("scheduled: " + scheduled);
-    System.out.println("payloads: " + payloads);
+    System.out.println(
+        String.join(
+            "\n",
+            "/**************************/",
+            "reactions: " + reactions,
+            "tag: " + tag,
+            "variables: " + variables,
+            "triggers: " + triggers,
+            "scheduled: " + scheduled,
+            "payloads: " + payloads,
+            "/**************************/"));
   }
 }

core/src/main/java/org/lflang/analyses/statespace/StateSpaceDiagram.java

@@ -1,14 +1,21 @@
 package org.lflang.analyses.statespace;
 
+import java.io.IOException;
+import java.nio.file.Path;
 import java.util.List;
 import java.util.Set;
 import java.util.stream.Collectors;
 import org.lflang.TimeValue;
 import org.lflang.generator.CodeBuilder;
 import org.lflang.generator.ReactionInstance;
 import org.lflang.graph.DirectedGraph;
+import org.lflang.pretvm.ExecutionPhase;
 
-/** A directed graph representing the state space of an LF program. */
+/**
+ * A directed graph representing the state space of an LF program.
+ *
+ * @author Shaokai J. Lin
+ */
 public class StateSpaceDiagram extends DirectedGraph<StateSpaceNode> {
 
   /** The first node of the state space diagram. */
@@ -29,13 +36,19 @@ public class StateSpaceDiagram extends DirectedGraph<StateSpaceNode> {
    */
   public StateSpaceNode loopNodeNext;
 
-  /** The logical time elapsed for each loop iteration. */
-  public long loopPeriod;
+  /**
+   * The logical time elapsed for each loop iteration. With the assumption of "logical time =
+   * physical time," this is also the hyperperiod in physical time.
+   */
+  public long hyperperiod;
+
+  /** The exploration phase in which this diagram is generated */
+  public ExecutionPhase phase;
 
   /** A dot file that represents the diagram */
   private CodeBuilder dot;
 
-  /** */
+  /** A flag that indicates whether we want the dot to be compact */
   private final boolean compactDot = false;
 
   /** Before adding the node, assign it an index. */
@@ -56,7 +69,7 @@ public StateSpaceNode getDownstreamNode(StateSpaceNode node) {
   public void display() {
     System.out.println("*************************************************");
     System.out.println("* Pretty printing worst-case state space diagram:");
-    long timestamp;
+    TimeValue time;
     StateSpaceNode node = this.head;
     if (node == null) {
       System.out.println("* EMPTY");
@@ -68,14 +81,15 @@ public void display() {
       node.display();
 
       // Store the tag of the prior step.
-      timestamp = node.getTag().timestamp;
+      time = node.getTag().time;
 
       // Assume a unique next state.
       node = getDownstreamNode(node);
 
       // Compute time difference
       if (node != null) {
-        TimeValue tsDiff = TimeValue.fromNanoSeconds(node.getTag().timestamp - timestamp);
+        TimeValue tsDiff =
+            TimeValue.fromNanoSeconds(node.getTag().time.toNanoSeconds() - time.toNanoSeconds());
         System.out.println("*     => Advance time by " + tsDiff);
       }
     }
@@ -87,7 +101,8 @@ public void display() {
     if (this.loopNode != null) {
       // Compute time difference
       TimeValue tsDiff =
-          TimeValue.fromNanoSeconds(loopNodeNext.getTag().timestamp - tail.getTag().timestamp);
+          TimeValue.fromNanoSeconds(
+              loopNodeNext.getTag().time.toNanoSeconds() - tail.getTag().time.toNanoSeconds());
       System.out.println("*     => Advance time by " + tsDiff);
 
       System.out.println("* Goes back to loop node: state " + this.loopNode.getIndex());
@@ -107,7 +122,7 @@ public CodeBuilder generateDot() {
       dot = new CodeBuilder();
       dot.pr("digraph G {");
       dot.indent();
-      if (this.loopNode != null) {
+      if (this.isCyclic()) {
         dot.pr("layout=circo;");
       }
       dot.pr("rankdir=LR;");
@@ -173,7 +188,8 @@ public CodeBuilder generateDot() {
       StateSpaceNode next = getDownstreamNode(this.head);
       while (current != null && next != null && current != this.tail) {
         TimeValue tsDiff =
-            TimeValue.fromNanoSeconds(next.getTag().timestamp - current.getTag().timestamp);
+            TimeValue.fromNanoSeconds(
+                next.getTag().time.toNanoSeconds() - current.getTag().time.toNanoSeconds());
         dot.pr(
             "S"
                 + current.getIndex()
@@ -192,8 +208,9 @@ public CodeBuilder generateDot() {
 
       if (loopNode != null) {
         TimeValue tsDiff =
-            TimeValue.fromNanoSeconds(loopNodeNext.getTag().timestamp - tail.getTag().timestamp);
-        TimeValue period = TimeValue.fromNanoSeconds(loopPeriod);
+            TimeValue.fromNanoSeconds(
+                loopNodeNext.getTag().time.toNanoSeconds() - tail.getTag().time.toNanoSeconds());
+        TimeValue period = TimeValue.fromNanoSeconds(hyperperiod);
         dot.pr(
             "S"
                 + current.getIndex()
@@ -216,4 +233,24 @@ public CodeBuilder generateDot() {
     }
     return this.dot;
   }
+
+  public void generateDotFile(Path dir, String filename) {
+    try {
+      Path path = dir.resolve(filename);
+      CodeBuilder dot = generateDot();
+      dot.writeToFile(path.toString());
+    } catch (IOException e) {
+      throw new RuntimeException(e);
+    }
+  }
+
+  /** Check if the diagram is periodic by checking if the loop node is set. */
+  public boolean isCyclic() {
+    return loopNode != null;
+  }
+
+  /** Check if the diagram is empty. */
+  public boolean isEmpty() {
+    return (head == null);
+  }
 }