Enhanced verification result json

plugins/core/hu.bme.mit.gamma.property.language/.launch/Launch Runtime Eclipse.launch

@@ -26,13 +26,13 @@
     <stringAttribute key="org.eclipse.jdt.launching.SOURCE_PATH_PROVIDER" value="org.eclipse.pde.ui.workbenchClasspathProvider"/>
     <stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xms2G -Xmx2G"/>
     <stringAttribute key="pde.version" value="3.3"/>
-    <stringAttribute key="product" value="org.eclipse.platform.ide"/>
+    <stringAttribute key="product" value="hu.bme.mit.gamma.sysml.headless.sysmlProduct"/>
     <booleanAttribute key="show_selected_only" value="false"/>
     <stringAttribute key="templateConfig" value="${target_home}/configuration/config.ini"/>
     <booleanAttribute key="tracing" value="false"/>
     <booleanAttribute key="useCustomFeatures" value="false"/>
     <booleanAttribute key="useDefaultConfig" value="true"/>
     <booleanAttribute key="useDefaultConfigArea" value="true"/>
-    <booleanAttribute key="useProduct" value="true"/>
+    <booleanAttribute key="useProduct" value="false"/>
     <booleanAttribute key="usefeatures" value="false"/>
 </launchConfiguration>

plugins/core/hu.bme.mit.gamma.statechart.language.ui/.classpath

@@ -1,13 +1,13 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<classpath>
-	<classpathentry kind="src" path="src"/>
-	<classpathentry excluding="**/.gitignore" kind="src" path="xtend-gen"/>
-	<classpathentry excluding="**/.gitignore" kind="src" path="src-gen"/>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17">
-		<attributes>
-			<attribute name="module" value="true"/>
-		</attributes>
-	</classpathentry>
-	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
-	<classpathentry kind="output" path="bin"/>
-</classpath>
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+	<classpathentry kind="src" path="src"/>
+	<classpathentry excluding="**/.gitignore" kind="src" path="xtend-gen"/>
+	<classpathentry excluding="**/.gitignore" kind="src" path="src-gen"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17">
+		<attributes>
+			<attribute name="module" value="true"/>
+		</attributes>
+	</classpathentry>
+	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+	<classpathentry kind="output" path="bin"/>
+</classpath>

plugins/core/hu.bme.mit.gamma.statechart.language.ui/META-INF/MANIFEST.MF

@@ -1,36 +1,36 @@
-Manifest-Version: 1.0
-Bundle-ManifestVersion: 2
-Bundle-Name: Gamma Statechart Language UI
-Bundle-Vendor: BME-FTSRG
-Bundle-Version: 2.9.0.qualifier
-Bundle-SymbolicName: hu.bme.mit.gamma.statechart.language.ui; singleton:=true
-Bundle-ActivationPolicy: lazy
-Require-Bundle: hu.bme.mit.gamma.statechart.language,
- hu.bme.mit.gamma.statechart.language.ide,
- hu.bme.mit.gamma.statechart.model,
- org.eclipse.xtext.ui,
- org.eclipse.xtext.ui.shared,
- org.eclipse.xtext.ui.codetemplates.ui,
- org.eclipse.ui.editors;bundle-version="3.5.0",
- org.eclipse.ui.ide;bundle-version="3.5.0",
- org.eclipse.ui,
- org.eclipse.compare,
- org.eclipse.xtext.builder,
- hu.bme.mit.gamma.action.language.ui,
- hu.bme.mit.gamma.expression.language.ui,
- hu.bme.mit.gamma.language.util,
- org.eclipse.jdt.core,
- org.eclipse.xtend.lib,
- org.eclipse.core.runtime,
- org.eclipse.core.resources,
- org.eclipse.pde.core,
- org.eclipse.ui.forms
-Import-Package: org.apache.log4j
-Bundle-RequiredExecutionEnvironment: JavaSE-17
-Export-Package: hu.bme.mit.gamma.statechart.language.ui.contentassist,
- hu.bme.mit.gamma.statechart.language.ui.internal,
- hu.bme.mit.gamma.statechart.language.ui.quickfix,
- hu.bme.mit.gamma.statechart.language.ui.serializer,
- hu.bme.mit.gamma.statechart.language.ui.wizard
-Bundle-Activator: hu.bme.mit.gamma.statechart.language.ui.internal.LanguageActivator
-Automatic-Module-Name: hu.bme.mit.gamma.statechart.language.ui
+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: Gamma Statechart Language UI
+Bundle-Vendor: BME-FTSRG
+Bundle-Version: 2.9.0.qualifier
+Bundle-SymbolicName: hu.bme.mit.gamma.statechart.language.ui; singleton:=true
+Bundle-ActivationPolicy: lazy
+Require-Bundle: hu.bme.mit.gamma.statechart.language,
+ hu.bme.mit.gamma.statechart.language.ide,
+ hu.bme.mit.gamma.statechart.model,
+ org.eclipse.xtext.ui,
+ org.eclipse.xtext.ui.shared,
+ org.eclipse.xtext.ui.codetemplates.ui,
+ org.eclipse.ui.editors;bundle-version="3.5.0",
+ org.eclipse.ui.ide;bundle-version="3.5.0",
+ org.eclipse.ui,
+ org.eclipse.compare,
+ org.eclipse.xtext.builder,
+ hu.bme.mit.gamma.action.language.ui,
+ hu.bme.mit.gamma.expression.language.ui,
+ hu.bme.mit.gamma.language.util,
+ org.eclipse.jdt.core,
+ org.eclipse.xtend.lib,
+ org.eclipse.core.runtime,
+ org.eclipse.core.resources,
+ org.eclipse.pde.core,
+ org.eclipse.ui.forms
+Import-Package: org.apache.log4j
+Bundle-RequiredExecutionEnvironment: JavaSE-17
+Export-Package: hu.bme.mit.gamma.statechart.language.ui.contentassist,
+ hu.bme.mit.gamma.statechart.language.ui.internal,
+ hu.bme.mit.gamma.statechart.language.ui.quickfix,
+ hu.bme.mit.gamma.statechart.language.ui.serializer,
+ hu.bme.mit.gamma.statechart.language.ui.wizard
+Bundle-Activator: hu.bme.mit.gamma.statechart.language.ui.internal.LanguageActivator
+Automatic-Module-Name: hu.bme.mit.gamma.statechart.language.ui

plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/VerificationHandler.java

@@ -72,6 +72,8 @@
 
 public class VerificationHandler extends TaskHandler {
 
+	public final List<VerificationResult> retrievedVerificationResults = new ArrayList<>();
+
 	protected boolean serializeTraces; // Denotes whether traces are serialized
 	protected boolean serializeTest; // Denotes whether test code is generated
 	protected String testFolderUri;
@@ -160,7 +162,6 @@ public void execute(Verification verification) throws IOException, InterruptedEx
 		boolean isOptimize = verification.isOptimize();
 
 		// Retrieved traces
-		List<VerificationResult> retrievedVerificationResults = new ArrayList<VerificationResult>();
 		List<ExecutionTrace> retrievedTraces = new ArrayList<ExecutionTrace>();
 
 		// Map for collecting both supported property representations
@@ -237,13 +238,16 @@ public void execute(Verification verification) throws IOException, InterruptedEx
 				traceUtil.addComment(trace, serializedFormula);
 			}
 
-			TimeUnit timeUnit = TimeUnit.MILLISECONDS;
-			long elapsed = stopwatch.elapsed(timeUnit);
-			String elapsedString = elapsed + " " + timeUnit;
+			long elapsedMS = stopwatch.elapsed(TimeUnit.MILLISECONDS);
+
+			VerificationResult resultTemp = new VerificationResult();
+			resultTemp.setQuery(serializedFormula);
+			resultTemp.setResult(verificationResult);
+			resultTemp.setParameters(arguments);
+			resultTemp.setExecutionTimeMS(elapsedMS);
+			resultTemp.setTraceSvgPath(targetFolderUri + "/" + svgFileName + retrievedVerificationResults.size() + ".svg");			
 
-			retrievedVerificationResults.add(
-				new VerificationResult(
-					serializedFormula, verificationResult, arguments, elapsedString));
+			retrievedVerificationResults.add(resultTemp);
 
 			// Checking if some of the unchecked properties are already covered
 			if (isOptimize) {
@@ -460,26 +464,52 @@ public void serialize(String resultFolderUri, String resultFileName,
 			fileUtil.saveString(resultFolderUri + File.separator + fileName, jsonResult);
 		}
 
-		@SuppressWarnings("unused")
-		public static class VerificationResult {
+		public static class VerificationResult {			
+			private String traceSvgPath = "";
+			private long executionTimeMS = -1;			
+			private String query = "";
+			private ThreeStateBoolean result = ThreeStateBoolean.UNDEF;
+			private String[] parameters = { };
+
+			public String getTraceSvgPath() {
+				return traceSvgPath;
+			}
+
+			public void setTraceSvgPath(String value) {
+				traceSvgPath = value;
+			}
+
+			public long getExecutionTimeMS() {
+				return executionTimeMS;
+			}
 
-			private String query;
-			private ThreeStateBoolean result;
-			private String[] parameters;
-			private String executionTime;
+			public void setExecutionTimeMS(long value) {
+				executionTimeMS = value;
+			}
+
+			public String getQuery() {
+				return query;
+			}
+
+			public void setQuery(String value) {
+				query = value;
+			}
+
+			public ThreeStateBoolean getResult() {
+				return result;
+			}
 
-			public VerificationResult(String query, ThreeStateBoolean result) {
-				this(query, result, null, null);
+			public void setResult(ThreeStateBoolean value) {
+				result = value;
 			}
 
-			public VerificationResult(String query, ThreeStateBoolean result,
-					String[] parameters, String executionTime) {
-				this.query = query;
-				this.result = result;
-				this.parameters = parameters;
-				this.executionTime = executionTime;
+			public String[] getParameters() {
+				return parameters;
 			}
 
+			public void setParameters(String[] value) {
+				parameters = value;
+			}
 		}
 
 	}

plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend

@@ -59,6 +59,10 @@ class JavaUtil {
 		return last
 	}
 
+	def <T> Iterable<T> exceptLast(Collection<T> collection) {
+		return collection.take(collection.size - 1)
+	}
+
 	def <T> T removeLast(List<T> list) {
 		return list.remove(list.size - 1)
 	}

plugins/core/hu.bme.mit.gamma.validation/.classpath

@@ -1,8 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <classpath>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17">
+		<attributes>
+			<attribute name="module" value="true"/>
+		</attributes>
+	</classpathentry>
 	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
-	<classpathentry kind="src" path="src/"/>
-	<classpathentry kind="src" path="src-gen/"/>
+	<classpathentry kind="src" path="src"/>
+	<classpathentry kind="src" path="src-gen"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

plugins/core/hu.bme.mit.gamma.validation/.settings/org.eclipse.jdt.core.prefs

@@ -1,7 +1,10 @@
 eclipse.preferences.version=1
 org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
-org.eclipse.jdt.core.compiler.compliance=11
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
+org.eclipse.jdt.core.compiler.compliance=17
 org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
 org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=11
+org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
+org.eclipse.jdt.core.compiler.release=enabled
+org.eclipse.jdt.core.compiler.source=17