Organize AGREE counterexample and TCG test case views by inputs/outpu…

…ts/state
loonwerks · Dec 7, 2021 · 4039444 · 4039444
1 parent bee4dc6
commit 4039444
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 6 deletions.
diff --git a/.../src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleContentProvider.java b/.../src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleContentProvider.java
@@ -0,0 +1,66 @@
+package com.rockwellcollins.atc.agree.analysis.views;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+import org.eclipse.emf.ecore.EObject;
+
+import jkind.api.ui.counterexample.CategoryHeader;
+import jkind.api.ui.counterexample.CounterexampleContentProvider;
+import jkind.api.ui.counterexample.SignalGrouper;
+import jkind.api.ui.counterexample.Spacer;
+import jkind.lustre.values.Value;
+import jkind.results.Counterexample;
+import jkind.results.Signal;
+import jkind.results.layout.Layout;
+
+public class AgreeCounterexampleContentProvider extends CounterexampleContentProvider {
+
+	private final Layout layout;
+	private final Map<String, EObject> refMap;
+
+	public AgreeCounterexampleContentProvider(Layout layout, Map<String, EObject> refMap) {
+		super(layout);
+		this.layout = layout;
+		this.refMap = refMap;
+	}
+
+	@Override
+	public Object[] getElements(Object inputElement) {
+		Counterexample cex = (Counterexample) inputElement;
+		List<Object> result = new ArrayList<>();
+
+		boolean first = true;
+		for (String category : layout.getCategories()) {
+			List<Signal<Value>> signals = cex.getCategorySignals(layout, category);
+			if (!signals.isEmpty()) {
+				if (first) {
+					first = false;
+				} else {
+					result.add(new Spacer());
+				}
+				result.add(new CategoryHeader(category));
+				List<Signal<Value>> inputSignals = signals.stream().filter(it -> {
+					EObject ref = refMap.get(it.getName());
+					return (ref instanceof org.osate.aadl2.Port) && ((org.osate.aadl2.Port) ref).isIn();
+				}).collect(Collectors.toList());
+				List<Signal<Value>> outputSignals = signals.stream().filter(it -> {
+					EObject ref = refMap.get(it.getName());
+					return (ref instanceof org.osate.aadl2.Port) && ((org.osate.aadl2.Port) ref).isOut();
+				}).collect(Collectors.toList());
+				List<Signal<Value>> otherSignals = signals.stream()
+						.filter(it -> !(inputSignals.contains(it) || outputSignals.contains(it)))
+						.collect(Collectors.toList());
+				result.addAll(SignalGrouper.group(null, Stream.of(inputSignals, otherSignals, outputSignals)
+						.flatMap(Collection::stream).collect(Collectors.toList())));
+			}
+		}
+
+		return result.toArray();
+	}
+
+}
diff --git a/...lysis/src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleTreeViewer.java b/...lysis/src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleTreeViewer.java
@@ -20,6 +20,9 @@
  */
 package com.rockwellcollins.atc.agree.analysis.views;
 
+import java.util.Map;
+
+import org.eclipse.emf.ecore.EObject;
 import org.eclipse.jface.layout.TreeColumnLayout;
 import org.eclipse.jface.viewers.ColumnViewerToolTipSupport;
 import org.eclipse.jface.viewers.ColumnWeightData;
@@ -28,7 +31,6 @@
 import org.eclipse.swt.SWT;
 import org.eclipse.swt.widgets.Composite;
 
-import jkind.api.ui.counterexample.CounterexampleContentProvider;
 import jkind.api.ui.counterexample.CounterexampleNameLabelProvider;
 import jkind.results.Counterexample;
 import jkind.results.layout.Layout;
@@ -48,20 +50,20 @@ public void setFocus() {
 		}
 	}
 
-	public void setInput(Counterexample cex, Layout layout) {
-		initializeTreeViewer(layout);
+	public void setInput(Counterexample cex, Layout layout, Map<String, EObject> refMap) {
+		initializeTreeViewer(layout, refMap);
 		createColumns(cex);
 		treeViewer.setInput(cex);
 		composite.layout(true);
 	}
 
-	private void initializeTreeViewer(Layout layout) {
+	private void initializeTreeViewer(Layout layout, Map<String, EObject> refMap) {
 		if (treeViewer != null) {
 			treeViewer.getControl().dispose();
 		}
 		treeViewer = new TreeViewer(composite, SWT.MULTI | SWT.FULL_SELECTION);
 
-		treeViewer.setContentProvider(new CounterexampleContentProvider(layout));
+		treeViewer.setContentProvider(new AgreeCounterexampleContentProvider(layout, refMap));
 		treeViewer.getTree().setHeaderVisible(true);
 		treeViewer.getTree().setLinesVisible(true);
 	}

diff --git a/...ee.analysis/src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleView.java b/...ee.analysis/src/com/rockwellcollins/atc/agree/analysis/views/AgreeCounterexampleView.java
@@ -20,6 +20,7 @@
  */
 package com.rockwellcollins.atc.agree.analysis.views;
 
+import java.util.Collections;
 import java.util.Map;
 import java.util.Stack;
 
@@ -54,7 +55,7 @@ public void setFocus() {
 	}
 
 	public void setInput(Counterexample cex, Layout layout, Map<String, EObject> refMap) {
-		tree.setInput(cex, layout);
+		tree.setInput(cex, layout, refMap);
 		this.refMap = refMap;
 		tree.getTreeViewer().addDoubleClickListener(event -> {
 			if (event.getSelection() instanceof IStructuredSelection) {
@@ -66,6 +67,10 @@ public void setInput(Counterexample cex, Layout layout, Map<String, EObject> ref
 		});
 	}
 
+	public void setInput(Counterexample cex, Layout layout) {
+		setInput(cex, layout, Collections.<String, EObject> emptyMap());
+	}
+
 	private void open(SignalGroup group) {
 		if (!group.isSingleton()) {
 			return;