s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Removed unnecessary double formatting code. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1419 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
d406c932fc
commit
b010ae3f92
3 changed files with 23 additions and 20 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      prism/src/prism/PrismUtils.java
  2. 28
      prism/src/userinterface/simulator/GUISimulator.java
  3. 6
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

9
prism/src/prism/PrismUtils.java
View File

@ -181,14 +181,9 @@ public class PrismUtils
private static DecimalFormat formatterDouble2dp = new DecimalFormat("#0.00");
/**
* Format a double, using PRISM settings.
* Format a double.
*/
public static String formatDouble(PrismSettings settings, double d)
{
return formatDouble(settings, new Double(d));
}
public static String formatDouble(PrismSettings settings, Double d)
public static String formatDouble(int precision, double d)
{
Formatter formatter = new Formatter();

28
prism/src/userinterface/simulator/GUISimulator.java
View File

@ -176,7 +176,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
});
modelTypeLabel.setText("Unknown");
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), 0.0));
totalTimeLabel.setText(formatDouble(0.0));
pathLengthLabel.setText("0");
txtFilter = new GUIPrismFileFilter[1];
@ -391,7 +391,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathActive = true;
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
definedConstantsLabel.setText((uCon.getDefinedConstantsString().length() == 0) ? "None" : uCon
.getDefinedConstantsString());
@ -448,7 +448,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10,
(int) pathTable.getPreferredSize().getWidth(), (int) pathTable.getPreferredSize().getHeight()));
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
@ -492,7 +492,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10,
(int) pathTable.getPreferredSize().getWidth(), (int) pathTable.getPreferredSize().getHeight()));
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
@ -519,7 +519,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
pathFormulaeList.repaint();
@ -537,7 +537,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
pathFormulaeList.repaint();
@ -555,7 +555,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
pathFormulaeList.repaint();
@ -589,7 +589,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTableModel.updatePathTable();
updateTableModel.updateUpdatesTable();
totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
stateLabelList.repaint();
pathFormulaeList.repaint();
@ -629,8 +629,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathTable.scrollRectToVisible(new Rectangle(0, pathTable.getHeight() - 10, pathTable.getWidth(),
pathTable.getHeight()));
totalTimeLabel.setText(PrismUtils
.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime()));
totalTimeLabel.setText(formatDouble(engine.getTotalPathTime()));
pathLengthLabel.setText("" + (engine.getPathSize() - 1));
setComputing(false);
@ -3441,4 +3440,13 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
}
}
}
/**
* Utility function to format floating point numbers.
*/
public String formatDouble(double d)
{
// getPrism().getSettings().
return PrismUtils.formatDouble(6, d);
}
}

6
prism/src/userinterface/simulator/GUISimulatorPathTable.java
View File

@ -288,7 +288,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
}
else
{
stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue())));
stringValue = (simulator.formatDouble((Double)timeValue.getValue()));
if (timeValue.isCumulative())
this.setToolTipText("Cumulative time up until state " + (row));
else
@ -298,7 +298,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
else if (value instanceof GUISimulator.VariableValue)
{
GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value;
stringValue = (variableValue.getValue() instanceof Double) ? (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)variableValue.getValue()))) : variableValue.getValue().toString();
stringValue = (variableValue.getValue() instanceof Double) ? (simulator.formatDouble(((Double)variableValue.getValue()))) : variableValue.getValue().toString();
this.setToolTipText("Value of variable \"" + variableValue.getVariable().getName() + "\" in state " + (row));
}
@ -320,7 +320,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
}
else
{
stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue());
stringValue = simulator.formatDouble(rewardValue.getRewardValue());
if (rewardValue.getRewardStructureColumn().isCumulativeReward())
this.setToolTipText("Cumulative reward of reward structure " + rewardName + " up until state " + (row));

Write Preview
Loading…
Cancel
Save