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