From 9c599f246076a596463dab96d28897c5b82ba77e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 24 Nov 2010 12:39:27 +0000 Subject: [PATCH] GUI offers graph creation for interval props (even if it will not yet display them properly). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2283 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/properties/GUIMultiProperties.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 889ef74c..b5ee26ab 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -357,7 +357,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List error("Cannot create an experiment because there are no constants with undefined values"); return; } - int result = GUIExperimentPicker.defineConstantsWithDialog(this.getGUI(), uCon, type instanceof TypeInt || type instanceof TypeDouble, gp + boolean offerGraph = type instanceof TypeInt || type instanceof TypeDouble || type instanceof TypeInterval; + int result = GUIExperimentPicker.defineConstantsWithDialog(this.getGUI(), uCon, offerGraph, gp .isValidForSimulation()); if (result == GUIExperimentPicker.VALUES_DONE_SHOW_GRAPH || result == GUIExperimentPicker.VALUES_DONE_SHOW_GRAPH_AND_SIMULATE) { showGraphDialog = true; @@ -561,7 +562,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List if (experiments.getSelectedRowCount() == 1) { GUIExperiment exp = experiments.getExperiment(experiments.getSelectedRow()); Type type = exp.getPropertyType(); - plotResults.setEnabled(type instanceof TypeInt || type instanceof TypeDouble); + plotResults.setEnabled(type instanceof TypeInt || type instanceof TypeDouble || type instanceof TypeInterval); } else { plotResults.setEnabled(false); } @@ -946,7 +947,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List exp = experiments.getExperiment(experiments.getSelectedRow()); // check its type type = exp.getPropertyType(); - if (!(type instanceof TypeInt || type instanceof TypeDouble)) { + if (!(type instanceof TypeInt || type instanceof TypeDouble || type instanceof TypeInterval)) { message("Can only plot results if the property is of type int or double"); return; }