diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index f1739433..75d67e16 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -23,6 +23,7 @@ package prism; import java.io.File; +import java.util.Formatter; public class PrismUtils { @@ -106,6 +107,42 @@ public class PrismUtils return f+i; } } + + public static String formatDouble(PrismSettings settings, double d) + { + return formatDouble(settings, new Double(d)); + } + + public static String formatDouble(PrismSettings settings, Double d) + { + Formatter formatter = new Formatter(); + + formatter.format("%.6g",d); // [the way to format scientific notation with 6 being the precision] + + + String res = formatter.toString().trim(); + System.out.print(res); + + int trailingZeroEnd = res.lastIndexOf('e'); + if (trailingZeroEnd == -1) + trailingZeroEnd = res.length(); + + int x = trailingZeroEnd -1; + + while (x > 0 && res.charAt(x) == '0') + x--; + + if (res.charAt(x) == '.') + x++; + + res = res.substring(0,x + 1) + res.substring(trailingZeroEnd, res.length()); + System.out.println( "-> " + res); + + //formatter.format("%.6f",d); //(just decimals) + //formatter.format("%1$.2e", d); // [the way to format scientific notation with 6 being the precision] + + return res; + } } //------------------------------------------------------------------------------ diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index e564d80d..c062701a 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -153,7 +153,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect modelTypeLabel.setText("Unknown"); - totalTimeLabel.setText("0.0"); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), 0.0)); pathLengthLabel.setText("0"); txtFilter = new GUIPrismFileFilter[1]; @@ -292,8 +292,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect Values initialState; try { - //pathTable.setAutoResizeMode(JTable.AUTO_RESIZE_SUBSEQUENT_COLUMNS); - // get properties constants/labels PropertiesFile pf; try @@ -391,7 +389,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect engineBuilt = true; pathActive = true; - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); definedConstantsLabel.setText((uCon.getDefinedConstantsString().length() == 0) ? "None" : uCon.getDefinedConstantsString()); @@ -451,7 +449,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect updateTableModel.updateUpdatesTable(); pathTable.scrollRectToVisible(new Rectangle(0, (int)pathTable.getPreferredSize().getHeight() - 10, (int)pathTable.getPreferredSize().getWidth(), (int)pathTable.getPreferredSize().getHeight()) ); - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); stateLabelList.repaint(); @@ -497,7 +495,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); stateLabelList.repaint(); pathFormulaeList.repaint(); @@ -515,7 +513,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); stateLabelList.repaint(); pathFormulaeList.repaint(); @@ -573,7 +571,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); stateLabelList.repaint(); pathFormulaeList.repaint(); @@ -615,7 +613,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTable.scrollRectToVisible(new Rectangle(0, pathTable.getHeight() - 10, pathTable.getWidth(), pathTable.getHeight()) ); - totalTimeLabel.setText(""+engine.getTotalPathTime()); + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); pathLengthLabel.setText(""+(engine.getPathSize()-1)); setComputing(false); @@ -998,7 +996,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect tablePanel = new javax.swing.JPanel(); tableScroll = new javax.swing.JScrollPane(); pathTable = new javax.swing.JTable(); - pathTable = new GUISimulatorPathTable(pathTableModel, engine); + pathTable = new GUISimulatorPathTable(this, pathTableModel, engine); setLayout(new java.awt.BorderLayout()); diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 4a04e762..037d57e3 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -22,15 +22,18 @@ package userinterface.simulator; +import simulator.*; +import prism.*; +import userinterface.util.*; + import javax.swing.*; import javax.swing.table.*; -import userinterface.util.*; import java.awt.*; import java.awt.geom.*; import javax.swing.border.*; import java.text.*; import java.awt.font.*; -import simulator.*; + import javax.swing.plaf.basic.*; import javax.swing.plaf.*; import javax.swing.event.*; @@ -45,18 +48,20 @@ public class GUISimulatorPathTable extends GUIGroupedTable private GUISimulator.PathTableModel ptm; private PathRowHeader pathRowHeader; - private SimulatorEngine engine; + private SimulatorEngine engine; + private GUISimulator simulator; private JList header; private GUISimulatorPathTable.RowHeaderListModel headerModel; /** Creates a new instance of GUISimulatorPathTable */ - public GUISimulatorPathTable(GUISimulator.PathTableModel ptm, SimulatorEngine engine) + public GUISimulatorPathTable(GUISimulator simulator, GUISimulator.PathTableModel ptm, SimulatorEngine engine) { super(ptm); this.ptm = ptm; + this.simulator = simulator; this.engine = engine; - + setColumnSelectionAllowed(false); getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); @@ -78,7 +83,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable setDefaultRenderer(Object.class, new PathChangeTableRenderer(true)); - //setAutoResizeMode(JTable.AUTO_RESIZE_SUBSEQUENT_COLUMNS); + } public void switchToChangeRenderer() @@ -375,7 +380,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable { GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value; - String stringValue = variableValue.getValue().toString(); + String stringValue = (variableValue.getValue() instanceof Double) ? (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)variableValue.getValue()))) : variableValue.getValue().toString(); double width = getStringWidth(stringValue, g2); @@ -414,7 +419,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable { GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value; - String stringValue = (rewardValue.isRewardValueUnknown()) ? "?" : rewardValue.getRewardValue().toString(); + String stringValue = (rewardValue.isRewardValueUnknown()) ? "?" : PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue()); double width = getStringWidth(stringValue, g2); @@ -452,7 +457,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable else if (value instanceof GUISimulator.TimeValue) { GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value; - String stringValue = (timeValue.isTimeValueUnknown()) ? "?" : timeValue.getValue().toString(); + String stringValue = (timeValue.isTimeValueUnknown()) ? "?" : PrismUtils.formatDouble(simulator.getPrism().getSettings(), timeValue.getValue()); double width = getStringWidth(stringValue, g2);