diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index 96ae20dd..94518b32 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -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(); diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index b1498206..ade10fe6 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -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); + } } diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 0ca9e4d9..c442a049 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -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));