Report the number of initial states as first item reported in the

ResultPage's statistic table (with diameter of 0). [Feature][Toolbox][Changelog]
tlaplus · May 28, 2018 · 076f0c7 · 076f0c7
1 parent 01fbd4c
commit 076f0c7
Show file tree

Hide file tree

Showing 4 changed files with 88 additions and 1 deletion.
diff --git a/....test/src/org/lamport/tla/toolbox/tool/tlc/output/data/StateSpaceInformationItemTest.java b/....test/src/org/lamport/tla/toolbox/tool/tlc/output/data/StateSpaceInformationItemTest.java
@@ -35,5 +35,53 @@ public void testParse() {
 		assertEquals(658832, parsed.getSpm());
 		assertEquals(9127, parsed.getDistinctSPM());
 	}
+
+	/**
+	 * Test method for
+	 * {@link org.lamport.tla.toolbox.tool.tlc.output.data.StateSpaceInformationItem#parseInit(java.lang.String)}
+	 * .
+	 */
+	public void testParseInit() {
+		StateSpaceInformationItem parsed = StateSpaceInformationItem
+				.parseInit("Finished computing initial states: 123456789 distinct states generated.");
+		assertEquals(0, parsed.getDiameter());
+		assertEquals(123456789, parsed.getDistinctStates());
+		assertEquals(123456789, parsed.getFoundStates());
+		assertEquals(123456789, parsed.getLeftStates());
+		assertEquals(0, parsed.getSpm());
+		assertEquals(0, parsed.getDistinctSPM());
+	}
+
+	public void testParseInit2() {
+		StateSpaceInformationItem parsed = StateSpaceInformationItem
+				.parseInit("Finished computing initial states: 1 distinct state generated.");
+		assertEquals(0, parsed.getDiameter());
+		assertEquals(1, parsed.getDistinctStates());
+		assertEquals(1, parsed.getFoundStates());
+		assertEquals(1, parsed.getLeftStates());
+		assertEquals(0, parsed.getSpm());
+		assertEquals(0, parsed.getDistinctSPM());
+	}
+
+	public void testParseInit3() {
+		StateSpaceInformationItem parsed = StateSpaceInformationItem
+				.parseInit("Finished computing initial states: 123456789 states generated, with 123 of them distinct.");
+		assertEquals(0, parsed.getDiameter());
+		assertEquals(123, parsed.getDistinctStates());
+		assertEquals(123456789, parsed.getFoundStates());
+		assertEquals(123, parsed.getLeftStates());
+		assertEquals(0, parsed.getSpm());
+		assertEquals(0, parsed.getDistinctSPM());
+	}
 
+	public void testParseInit4() {
+		StateSpaceInformationItem parsed = StateSpaceInformationItem
+				.parseInit("Finished computing initial states: 2 states generated, with 1 of them distinct.");
+		assertEquals(0, parsed.getDiameter());
+		assertEquals(1, parsed.getDistinctStates());
+		assertEquals(2, parsed.getFoundStates());
+		assertEquals(1, parsed.getLeftStates());
+		assertEquals(0, parsed.getSpm());
+		assertEquals(0, parsed.getDistinctSPM());
+	}
 }
diff --git a/...ol.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/StateSpaceInformationItem.java b/...ol.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/StateSpaceInformationItem.java
@@ -4,6 +4,8 @@
 import java.text.ParseException;
 import java.text.SimpleDateFormat;
 import java.util.Date;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 import org.lamport.tla.toolbox.tool.tlc.ui.TLCUIActivator;
 
@@ -52,8 +54,16 @@ private StateSpaceInformationItem(Date time, long diameter,
 		this.spm = spm;
 		this.distinctSPM = distinctSPM;
 	}
+
+	private StateSpaceInformationItem(long foundStates, long distinctStates) {
+		this(new Date(), 0, foundStates, distinctStates, distinctStates, 0, 0);
+	}
 
-    /**
+	private StateSpaceInformationItem(long distinctStates) {
+		this(distinctStates, distinctStates);
+	}
+
+   /**
 	 * @return the isMostRecent
 	 */
 	public boolean isMostRecent() {
@@ -184,6 +194,31 @@ public static StateSpaceInformationItem parse(String outputMessage) {
 		return null;
 	}
 
+	public static StateSpaceInformationItem parseInit(final String outputMessage) {
+		// Handles  EC.TLC_INIT_GENERATED1 and EC.TLC_INIT_GENERATED2.-
+		// From MP#getMessage:
+        //   b.append("Finished computing initial states: %1% distinct state%2% generated.");
+        //   b.append("Finished computing initial states: %1% state%2% generated, with %3% of them distinct.");
+
+		Pattern pattern = Pattern.compile("^Finished computing initial states: ([0-9]+) distinct state[s]* generated.$");
+		Matcher matcher = pattern.matcher(outputMessage);
+		if (matcher.find()) {
+			final long distinctStates = Long.parseLong(matcher.group(1));
+			return new StateSpaceInformationItem(distinctStates);
+		}
+
+		pattern = Pattern.compile(
+				"^Finished computing initial states: ([0-9]+) states generated, with ([0-9]+) of them distinct.$");
+		matcher = pattern.matcher(outputMessage);
+		if (matcher.find()) {
+			final long foundStates = Long.parseLong(matcher.group(1));
+			final long distinctStates = Long.parseLong(matcher.group(2));
+			return new StateSpaceInformationItem(foundStates, distinctStates);
+		}
+		return null;
+	}
+
+
     /**
      * @param outputMessage
      * @return

diff --git a/...l.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java b/...l.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
@@ -368,6 +368,9 @@ public void onOutput(ITypedRegion region, String text)
                     break;
                 case EC.TLC_INIT_GENERATED1:
                 case EC.TLC_INIT_GENERATED2:
+					if (addOrReplaceProgressInformation(StateSpaceInformationItem.parseInit(outputMessage))) {
+						informPresenter(ITLCModelLaunchDataPresenter.PROGRESS);
+					}
                 case EC.TLC_INIT_GENERATED3:
                 case EC.TLC_INIT_GENERATED4:
                     this.setCurrentStatus(COMPUTING_REACHABLE);

diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
@@ -192,6 +192,7 @@ public void modelCheck() throws Exception
         }
 
         report("init processed");
+
         // Finished if there is no next state predicate:
         if (this.actions.length == 0)
         {