Some preliminary code to add parametric model checking to GUI.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9386 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/properties/GUIMultiProperties.java

@@ -79,6 +79,9 @@ import javax.swing.event.ListSelectionListener;
 
 import org.jfree.data.xy.XYDataItem;
 
+import param.BigRational;
+import param.Function;
+import param.RegionValues;
 import parser.Values;
 import parser.ast.Expression;
 import parser.ast.ModulesFile;
@@ -160,7 +163,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 	private JScrollPane expScroller;
 	private JTextField fileTextField;
 	private Action newProps, openProps, saveProps, savePropsAs, insertProps, verifySelected, newProperty, editProperty, newConstant, removeConstant, newLabel,
-			removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults, exportResultsListText, exportResultsListCSV,
+			removeLabel, newExperiment, deleteExperiment, stopExperiment, parametric, viewResults, plotResults, exportResultsListText, exportResultsListCSV,
 			exportResultsMatrixText, exportResultsMatrixCSV, simulate, details, exportLabelsPlain, exportLabelsMatlab;;
 
 	// Current properties
@@ -639,6 +642,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 
 		// newExperiment: enabled if there is exactly one prop selected and it is valid
 		newExperiment.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
+		// parametric: enabled if there is exactly one prop selected and it is valid
+		parametric.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
 		// deleteExperiments: enabled if one or more experiments selected
 		deleteExperiment.setEnabled(experiments.getSelectedRowCount() > 0);
 		// viewResults: enabled if at least one experiment is selected
@@ -893,6 +898,24 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 			}
 		}
 
+		// How to plot a parametric result...
+		/*if (selected.length == 1) {
+			GUIProperty gp = propList.getProperty(selected[0]);
+			if (gp.getResult().getResult() instanceof RegionValues) {
+				Graph graph = new Graph("Param");
+				SeriesKey sk = graph.addSeries("param");
+				RegionValues vals = (RegionValues) gp.getResult().getResult();
+				param.Function f = vals.getResult(0).getInitStateValueAsFunction();
+				int n = 100;
+				for (int i = 0; i < n; i++) {
+					BigRational br = f.evaluate(new param.Point(new BigRational[] {new BigRational(i, n)}));
+					XYDataItem di = new XYDataItem(((double)i)/n, br.doubleValue());
+					graph.addPointToSeries(sk, di);
+				}
+				this.getGraphHandler().addGraph(graph);
+			}
+		}*/
+		
 		// For a single property with a displayable counterexample, offer to do show it
 		if (selected.length == 1) {
 			GUIProperty gp = propList.getProperty(selected[0]);
@@ -1415,6 +1438,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 				editProperty.setEnabled(propList.getSelectedProperties().size() > 0);
 
 				newExperiment.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
+				parametric.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
 
 				if (showDeleters == false) {
 					simulate.setEnabled(false);
@@ -1422,6 +1446,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 					details.setEnabled(false);
 					editProperty.setEnabled(false);
 					newExperiment.setEnabled(false);
+					parametric.setEnabled(false);
 				}
 
 				propertiesPopup.show(e.getComponent(), e.getX(), e.getY());
@@ -1508,6 +1533,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 				details.setEnabled(propList.existsValidSelectedProperties());
 				editProperty.setEnabled(propList.getSelectedProperties().size() > 0);
 				newExperiment.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
+				parametric.setEnabled(propList.getNumSelectedProperties() == 1 && propList.getValidSelectedProperties().size() == 1);
 
 				if (showDeleters == false) {
 					simulate.setEnabled(false);
@@ -1515,6 +1541,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 					details.setEnabled(false);
 					editProperty.setEnabled(false);
 					newExperiment.setEnabled(false);
+					parametric.setEnabled(false);
 				}
 
 				propertiesPopup.show(e.getComponent(), e.getX(), e.getY());
@@ -1743,6 +1770,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 			propMenu.add(verifySelected);
 			propMenu.add(simulate);
 			propMenu.add(newExperiment);
+			//propMenu.add(parametric);
 			JMenu exportlabelsMenu = new JMenu("Export labels");
 			exportlabelsMenu.setMnemonic('E');
 			exportlabelsMenu.setIcon(GUIPrism.getIconFromImage("smallExport.png"));
@@ -1782,8 +1810,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 		propertiesPopup.add(new JSeparator());
 		propertiesPopup.add(verifySelected);
 		propertiesPopup.add(simulate);
-		//experiment
 		propertiesPopup.add(newExperiment);
+		//propertiesPopup.add(parametric);
 		propertiesPopup.add(details);
 		propertiesPopup.add(new JSeparator());
 		propertiesPopup.add(GUIPrism.getClipboardPlugin().getCutAction());
@@ -2061,6 +2089,18 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 		plotResults.putValue(Action.NAME, "Plot results");
 		plotResults.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png"));
 
+		parametric = new AbstractAction()
+		{
+			public void actionPerformed(ActionEvent e)
+			{
+				a_newExperiment();
+			}
+		};
+		parametric.putValue(Action.LONG_DESCRIPTION, "Perform parametric model checking");
+		parametric.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P));
+		parametric.putValue(Action.NAME, "Parametric");
+		parametric.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png"));
+
 		exportResultsListText = new AbstractAction()
 		{
 			public void actionPerformed(ActionEvent e)