Remove redundant starttime variable with starttimestamp.

[Refactor][Toolbox]

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java

@@ -146,24 +146,8 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
     // should be put in the user output widget
     protected boolean isTLCStarted = false;
 
-    /**
-     *  Set to the starting time of the current TLC run.
-     *  Actually, it is set to the time when the TLC Start
-     *  message is processed.  Thus, there is no guarantee
-     *  that this time bears any relation to startTimeStamp.
-     */
-    protected long startTime = 0;
-
     protected int numWorkers = 0;
 
-    /**
-     * @return the startTime
-     */
-    public long getStartTime()
-    {
-        return startTime;
-    }
-
     public TLCModelLaunchDataProvider(Model model)
     {
         this.model = model;
@@ -190,7 +174,6 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
 
         coverageInfo = new Vector<CoverageInformationItem>();
         progressInformation = new Vector<StateSpaceInformationItem>();
-        startTime = 0;
         startTimestamp = Long.MIN_VALUE;
         finishTimestamp = Long.MIN_VALUE;
         tlcMode = "";
@@ -431,7 +414,6 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
                 case EC.TLC_STARTING:
                     isTLCStarted = true;
                     this.startTimestamp = GeneralOutputParsingHelper.parseTLCTimestamp(outputMessage);
-                    this.startTime = System.currentTimeMillis();
 
                     informPresenter(ITLCModelLaunchDataPresenter.START_TIME);
                     break;

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java

@@ -109,7 +109,6 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
     private Text startTimestampText;
     // startTime is provided by the TLCModelLaunchDataProvider's getStartTime()
     // method.
-    private long startTime = 0;
     private Text finishTimestampText;
     private Text tlcModeText;
     private Text lastCheckpointTimeText;
@@ -192,7 +191,6 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
 	                    	break;
 	                    }
 						ResultPage.this.startTimestampText.setText(new Date(ResultPage.this.startTimestamp).toString());
-	                    ResultPage.this.startTime = dataProvider.getStartTime();
 	                    break;
 	                case END_TIME:
 	                    long finishTimestamp = dataProvider.getFinishTimestamp();
@@ -381,7 +379,6 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
     		}
     		this.startTimestampText.setText("");
     		this.startTimestamp = 0;
-    		this.startTime = 0;
     		this.finishTimestampText.setText("");
     		this.tlcModeText.setText("");
     		this.lastCheckpointTimeText.setText("");
@@ -1223,7 +1220,7 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
                         data[0] = 0;
                         times[0] = 0;
 
-                        long startTime = resultPage.startTime;
+                        long startTime = resultPage.startTimestamp;
                         TLCUIActivator.getDefault().logDebug("first reported time - starttime = "
                                 + (ssInfo[0].getTime().getTime() - startTime));
                         if (startTime > ssInfo[0].getTime().getTime() - 1000)