diff --git a/plugins/core/hu.bme.mit.gamma.property.language/.launch/Launch Runtime Eclipse.launch b/plugins/core/hu.bme.mit.gamma.property.language/.launch/Launch Runtime Eclipse.launch
index d551748b2..b7593a3b9 100644
--- a/plugins/core/hu.bme.mit.gamma.property.language/.launch/Launch Runtime Eclipse.launch
+++ b/plugins/core/hu.bme.mit.gamma.property.language/.launch/Launch Runtime Eclipse.launch
@@ -26,13 +26,13 @@
-
+
-
+
diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language.ui/.classpath b/plugins/core/hu.bme.mit.gamma.statechart.language.ui/.classpath
index afe6c1a1a..b4f7c6be2 100644
--- a/plugins/core/hu.bme.mit.gamma.statechart.language.ui/.classpath
+++ b/plugins/core/hu.bme.mit.gamma.statechart.language.ui/.classpath
@@ -1,13 +1,13 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language.ui/META-INF/MANIFEST.MF b/plugins/core/hu.bme.mit.gamma.statechart.language.ui/META-INF/MANIFEST.MF
index 153a5c43d..73339d306 100644
--- a/plugins/core/hu.bme.mit.gamma.statechart.language.ui/META-INF/MANIFEST.MF
+++ b/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
diff --git a/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/VerificationHandler.java b/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/VerificationHandler.java
index c18d9d04a..7affd16e7 100644
--- a/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/VerificationHandler.java
+++ b/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 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 retrievedVerificationResults = new ArrayList();
List retrievedTraces = new ArrayList();
// 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;
+ }
}
}
diff --git a/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend b/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend
index fabfdb3db..f7746c21c 100644
--- a/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend
+++ b/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend
@@ -59,6 +59,10 @@ class JavaUtil {
return last
}
+ def Iterable exceptLast(Collection collection) {
+ return collection.take(collection.size - 1)
+ }
+
def T removeLast(List list) {
return list.remove(list.size - 1)
}
diff --git a/plugins/core/hu.bme.mit.gamma.validation/.classpath b/plugins/core/hu.bme.mit.gamma.validation/.classpath
index 7d9246e1f..7359b62f7 100644
--- a/plugins/core/hu.bme.mit.gamma.validation/.classpath
+++ b/plugins/core/hu.bme.mit.gamma.validation/.classpath
@@ -1,8 +1,12 @@
-
+
+
+
+
+
-
-
+
+
diff --git a/plugins/core/hu.bme.mit.gamma.validation/.settings/org.eclipse.jdt.core.prefs b/plugins/core/hu.bme.mit.gamma.validation/.settings/org.eclipse.jdt.core.prefs
index f4d933e4e..d4540a53f 100644
--- a/plugins/core/hu.bme.mit.gamma.validation/.settings/org.eclipse.jdt.core.prefs
+++ b/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