Merge Current master into 4259

Issue-Ref: 4259
Issue-Url: #4259




Signed-off-by: Konstantin Blaschke <blaschke@fortiss.org>

com.microsoft.z3/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: com.microsoft.z3
 Bundle-ManifestVersion: 2
 Bundle-Name: Microsoft Z3 API
 Bundle-SymbolicName: com.microsoft.z3;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-ClassPath: lib/com.microsoft.z3.jar,
  .
 Bundle-Vendor: fortiss GmbH

eu.fbk.af3.tools.diagram.ui/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: eu.fbk.af3.tools.diagram.ui
 Bundle-ManifestVersion: 2
 Bundle-Name: Diagram Document Creator UI
 Bundle-SymbolicName: eu.fbk.af3.tools.diagram.ui;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-Activator: eu.fbk.af3.tools.diagram.ui.DiagramUIActivator
 Require-Bundle: eu.fbk.af3.tools.diagram;bundle-version="1.0.0",
  org.fortiss.af3.component.ui,

eu.fbk.af3.tools.diagram/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: eu.fbk.af3.tools.diagram
 Bundle-ManifestVersion: 2
 Bundle-Name: Diagram Document Creator
 Bundle-SymbolicName: eu.fbk.af3.tools.diagram
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-Activator: eu.fbk.af3.tools.diagram.Activator
 Bundle-Vendor: FBK (Fondazione Bruno Kessler)
 Require-Bundle: org.eclipse.core.runtime,

org.fortiss.af3.allocation.ui/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.allocation.ui
 Bundle-ManifestVersion: 2
 Bundle-Name: fortiss AF3 Allocation UI
 Bundle-SymbolicName: org.fortiss.af3.allocation.ui;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-Activator: org.fortiss.af3.allocation.ui.AF3AllocationUIActivator
 Require-Bundle: org.eclipse.ui.ide;visibility:=reexport,
  org.fortiss.af3.allocation;visibility:=reexport,

org.fortiss.af3.allocation/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.allocation
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
 Bundle-SymbolicName: org.fortiss.af3.allocation;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin

org.fortiss.af3.component.ui/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.component.ui
 Bundle-ManifestVersion: 2
 Bundle-Name: AF3 Component UI
 Bundle-SymbolicName: org.fortiss.af3.component.ui;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-Activator: org.fortiss.af3.component.ui.AF3ComponentUIActivator
 Require-Bundle: org.fortiss.af3.expression.ui;visibility:=reexport,
  org.fortiss.af3.component;visibility:=reexport,

org.fortiss.af3.component.ui/src/org/fortiss/af3/component/ui/properties/.ratings

-ComponentSpecificationPropertySection.java be24b5576d00c15484fd21abc5cd1a5ebaecb221 GREEN
+ComponentSpecificationPropertySection.java 6f5762541fc3f69f604f6cd0ab638497e9b2832e GREEN
 PortDataPropagation.java cf1d76c93964e6c0bb947c0aea51666628260008 GREEN
 PortInitValueSection.java ba26a87fbf4d0bce69e57d108b9939cfa5ab8fa8 GREEN
 PortSpecificationPropertySection.java 9a17f8151345e1c87b303327e19f973185a59540 GREEN

org.fortiss.af3.component.ui/src/org/fortiss/af3/component/ui/properties/ComponentSpecificationPropertySection.java

@@ -39,9 +39,6 @@ public final class ComponentSpecificationPropertySection extends PropertySection
 	/** Stores the current input. */
 	private Component component;
 
-	/** The selected {@link CausalityComponentSpecification}. */
-	private CausalityComponentSpecification specification;
-
 	/** Stores causality flag button. */
 	private Button stronglyCausalButton;
 
@@ -80,6 +77,7 @@ public final class ComponentSpecificationPropertySection extends PropertySection
 	@Override
 	public void refresh() {
 		super.refresh();
+		CausalityComponentSpecification specification = component.getCausalitySpecification();
 		if(specification == null) {
 			return;
 		}

org.fortiss.af3.component.ui/src/org/fortiss/af3/component/ui/utils/.ratings

 CodeUtils.java 3400dfe4b6221c7d83c72d72c2b849e29ea33e54 GREEN
 ComponentCompletionProposalUtils.java df2ca7d318e170b13daf01ef3ed9811a3dfff057 GREEN
 ComponentFieldAssistUtils.java b11bbeafe69d985d5bb46354c34f15420537d511 GREEN
-FMUUtils.java 15e15ffca7580bf99faf5462760a666c05c7bfac GREEN
+FMUUtils.java 06b3496b5144340108b4e437bf53a29b14945c38 GREEN
 SimulationPerspectiveListener.java 78a649ae6db6e553f58b7583bc423d83d160fec4 GREEN
 SimulationUtils.java 6b81b0653c9f75dd599660c17f9fbfcdc18d7a1e GREEN

org.fortiss.af3.component.ui/src/org/fortiss/af3/component/ui/utils/FMUUtils.java

@@ -45,7 +45,7 @@ public class FMUUtils {
 		Shell currentShell = getWorkbench().getActiveWorkbenchWindow().getShell();
 
 		String message = "";
-		String baseMsg = "The \"samplingTime\" function must ";
+		String baseMsg = "- The \"samplingTime\" function must ";
 
 		Double samplingTime = null;
 		if(dd != null) {
@@ -67,7 +67,7 @@ public class FMUUtils {
 						}
 						Return returnStatement = (Return)singleStatement;
 						if(!(returnStatement.getValue() instanceof DoubleConst)) {
-							message += baseMsg + "return a constant value.";
+							message += baseMsg + "return a constant value." + lineSeparator();
 						} else {
 							samplingTime = ((DoubleConst)returnStatement.getValue()).getValue();
 						}
@@ -75,8 +75,12 @@ public class FMUUtils {
 				}
 			}
 			if(samplingTime == null) {
-				message += baseMsg + "be defined in the data dictionary.";
+				message += baseMsg + "be defined in the data dictionary." + lineSeparator();
 			}
+		} else {
+			message +=
+					baseMsg + "be defined in a data dictionary, but no data dictionary exist yet." +
+							lineSeparator();
 		}
 		if(!message.equals("")) {
 			InputDialog durationDialog = new InputDialog(currentShell, "Frequency",

org.fortiss.af3.component/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.component
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
 Bundle-SymbolicName: org.fortiss.af3.component;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin

org.fortiss.af3.cosimulation.ui/META-INF/MANIFEST.MF

@@ -3,14 +3,14 @@ Automatic-Module-Name: org.fortiss.af3.cosimulation.ui
 Bundle-ManifestVersion: 2
 Bundle-Name: AF3 Cosimulation UI
 Bundle-SymbolicName: org.fortiss.af3.cosimulation.ui;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-Activator: org.fortiss.af3.cosimulation.ui.AF3CosimulationUIActivator
 Require-Bundle: org.eclipse.ui.ide;bundle-version="3.7.0";visibility:=reexport,
  org.fortiss.af3.project.ui;bundle-version="1.0.0";visibility:=reexport,
  org.fortiss.tooling.base.ui;bundle-version="1.0.0";visibility:=reexport,
  org.fortiss.af3.component,
  org.fortiss.af3.cosimulation;bundle-version="1.0.0",
- org.fortiss.af3.component.ui;bundle-version="2.21.0"
+ org.fortiss.af3.component.ui;bundle-version="2.22.0"
 Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-11
 Bundle-Vendor: fortiss GmbH

org.fortiss.af3.cosimulation/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.cosimulation
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
 Bundle-SymbolicName: org.fortiss.af3.cosimulation;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin

org.fortiss.af3.exploration.smt/META-INF/MANIFEST.MF

@@ -3,7 +3,7 @@ Automatic-Module-Name: org.fortiss.af3.exploration.smt
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
 Bundle-SymbolicName: org.fortiss.af3.exploration.smt;singleton:=true
-Bundle-Version: 2.21.0.qualifier
+Bundle-Version: 2.22.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/.ratings

-Z3Backend.java a6296539968d2d573cc0dddde845bb087f461862 GREEN
+Z3Backend.java 2173b82586cc7aa09413d03b159676efa8a98789 GREEN

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/Z3Backend.java

@@ -50,8 +50,8 @@ import org.fortiss.af3.exploration.smt.solver.SolverRun;
  */
 public class Z3Backend implements IDSEBackend {
 
-	/** Default timeout value in ms. */
-	private static int DEFAULT_TIMEOUT = 50 * 1000;
+	/** Default timeout value in seconds. */
+	private static int DEFAULT_TIMEOUT_S = 1800;
 
 	/** {@inheritDoc} */
 	@Override
@@ -77,15 +77,15 @@ public class Z3Backend implements IDSEBackend {
 	/** {@inheritDoc} */
 	@Override
 	public SolverSettings getSolverSettings() {
-		return createSolverSettings(DEFAULT_TIMEOUT, 0);
+		return createSolverSettings(DEFAULT_TIMEOUT_S, 0);
 	}
 
 	/** {@inheritDoc} */
 	@Override
 	public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
 			SolverSettings settings, IProgressMonitor monitor) throws Exception {
-		int timeout = settings.getTermination().getTimeoutMS().getValue();
-		SolverRun solverRun = createSolverRun(spec, timeout);
+		int timeout_s = settings.getTermination().getTimeoutS().getValue();
+		SolverRun solverRun = createSolverRun(spec, timeout_s);
 
 		if(isDebugVerboseEnabled()) {
 			// prints on screen the list of constraints for this run
@@ -105,15 +105,16 @@ public class Z3Backend implements IDSEBackend {
 	 * Creates a {@link SolverRun} instance that is specific for the {@link ISynthesisCategory}s of
 	 * the given {@link ExplorationSpecification}.
 	 */
-	public SolverRun createSolverRun(ExplorationSpecification spec, int timeout) throws Exception {
+	public SolverRun createSolverRun(ExplorationSpecification spec, int timeout_s)
+			throws Exception {
 		Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
 		if(synthTypes.contains(IDeploymentSynthesis.class) &&
 				synthTypes.contains(IScheduleSynthesis.class)) {
-			return new DeploScheduleRun(spec, timeout);
+			return new DeploScheduleRun(spec, timeout_s);
 		} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
-			return new DeploymentRun(spec, timeout);
+			return new DeploymentRun(spec, timeout_s);
 		} else if(synthTypes.contains(IScheduleSynthesis.class)) {
-			return new ScheduleRun(spec, timeout);
+			return new ScheduleRun(spec, timeout_s);
 		} else {
 			throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
 					" was found for the given set of syntheses to perform.");

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/.ratings

-ContextWrapper.java 4018822acbbad7d76602fc1daeba0354f4cb811c GREEN
+ContextWrapper.java 2cb55bd2638871d1132528ba7ccb412db3c9d2a0 GREEN
 DeploScheduleRun.java 67ddb09735979f42446e6f57404595042bac4c34 GREEN
 DeploymentRun.java 011bb1c7245d0e1eb19cc438577501b6b951422d GREEN
-ScheduleRun.java 811619b895532e1b7b87b55ca61325f6abe4b529 GREEN
-SolverRun.java 5d8e56cc48032f3a462c11c767cb7fa73c6f2b4b GREEN
+ScheduleRun.java d85ef8813bf15bb7d84ce0b149b7568618055231 GREEN
+SolverRun.java faa3e934db14cdbb483ddd0cd860263488e2a869 GREEN

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/ContextWrapper.java

@@ -27,32 +27,36 @@ import com.microsoft.z3.Context;
  */
 public class ContextWrapper extends Context {
 
-	/** Solver timeout (in ms). */
-	int timeoutMS;
+	/** Solver timeout (in seconds). */
+	int timeout_s;
 
 	/** Flag whether to track unsat constraints. */
 	boolean trackConstraints;
 
+	/** Multiplication factor for converting seconds to milliseconds. */
+	final static int FACTOR_S_TO_MS = 1000;
+
 	/** Constructor. The caller is responsible for closing it (try-with-resource is recommended). */
-	public ContextWrapper(int timeoutMS, boolean trackConstraints) {
-		super(createParameters(timeoutMS, trackConstraints));
-		this.timeoutMS = timeoutMS;
+	public ContextWrapper(int timeout_s, boolean trackConstraints) {
+		super(createParameters(timeout_s, trackConstraints));
+		this.timeout_s = timeout_s;
 		this.trackConstraints = trackConstraints;
 	}
 
 	/** Helper method to provide parameter {@link Map} in constructor. */
-	private static Map<String, String> createParameters(int timeoutMS, boolean trackConstraints) {
+	private static Map<String, String> createParameters(int timeout_s, boolean trackConstraints) {
 		Map<String, String> parameters = new HashMap<>();
-		parameters.put("timeout", Integer.toString(timeoutMS));
+		// Z3 expects a timeout in ms
+		parameters.put("timeout", Integer.toString(timeout_s * FACTOR_S_TO_MS));
 		if(trackConstraints) {
 			parameters.put("proof", "true");
 		}
 		return parameters;
 	}
 
-	/** Getter for {@link #timeoutMS}. */
-	public int getTimeoutMS() {
-		return timeoutMS;
+	/** Getter for {@link #timeout_s}. */
+	public int getTimeoutS() {
+		return timeout_s;
 	}
 
 	/** Getter for {@link #trackConstraints}. */

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/ScheduleRun.java

@@ -52,8 +52,8 @@ import com.microsoft.z3.Model;
 public class ScheduleRun extends SolverRun {
 
 	/** Constructor. */
-	public ScheduleRun(ExplorationSpecification expSpec, int timeoutMS) throws Exception {
-		super(expSpec, timeoutMS, "Schedule");
+	public ScheduleRun(ExplorationSpecification expSpec, int timeout_s) throws Exception {
+		super(expSpec, timeout_s, "Schedule");
 	}
 
 	/** {@inheritDoc} */

org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/SolverRun.java

@@ -94,18 +94,18 @@ public abstract class SolverRun {
 	/** References the {@link ExplorationSpecification} defining the feasible region. */
 	protected final ExplorationSpecification expSpec;
 
-	/** Timeout (in ms) after which solver is terminated. */
-	private int timeoutMS;
+	/** Timeout (in seconds) after which solver is terminated. */
+	private int timeout_s;
 
 	/** Prefix to be used when exporting solutions. */
 	private String solutionNamePrefix;
 
 	/** Constructor. */
-	public SolverRun(ExplorationSpecification expSpec, int timeoutMS,
+	public SolverRun(ExplorationSpecification expSpec, int timeout_s,
 			final String solutionNamePrefix) throws Exception {
 
 		this.expSpec = expSpec;
-		this.timeoutMS = timeoutMS;
+		this.timeout_s = timeout_s;
 		this.solutionNamePrefix = solutionNamePrefix;
 
 		List<IExplorationConstraint<?>> basicConstraints = defineBasicConstraints();
@@ -149,7 +149,7 @@ public abstract class SolverRun {
 				monitor.beginTask("Z3", numberOfRuns + 1);
 			}
 
-			try(ContextWrapper context = new ContextWrapper(timeoutMS, false)) {
+			try(ContextWrapper context = new ContextWrapper(timeout_s, false)) {
 				DSMLtoSMTTransformator transformator = new DSMLtoSMTTransformator(context, expSpec);
 
 				if(numExplorationObjectives == 0) {
@@ -162,7 +162,7 @@ public abstract class SolverRun {
 			}
 
 			if(expSolution.getSolutionState() == UNSAT) {
-				try(ContextWrapper trackingCtx = new ContextWrapper(timeoutMS, true)) {
+				try(ContextWrapper trackingCtx = new ContextWrapper(timeout_s, true)) {
 					DSMLtoSMTTransformator transformator =
 							new DSMLtoSMTTransformator(trackingCtx, expSpec);
 					if(!solveNonOptimized(transformator, expSolution, monitor)) {
@@ -287,8 +287,8 @@ public abstract class SolverRun {
 			SingleExplorationSolution singleSolution = createSingleExplorationSolution();
 			singleSolution.setName(solutionNamePrefix + " " + i);
 			logZ3info("Solving problem with optimizer with parameters\n" +
-					solver.getParameterDescriptions() + "\ntimeout: " + context.getTimeoutMS() +
-					"ms");
+					solver.getParameterDescriptions() + "\ntimeout: " + context.getTimeoutS() +
+					"s");
 			long currentTimeMillis = currentTimeMillis();
 			if(z3CancelThread != null) {
 				z3CancelThread.start();
@@ -298,9 +298,9 @@ public abstract class SolverRun {
 				return false;
 			}
 
-			long time = (currentTimeMillis() - currentTimeMillis) / 1000;
+			long time_s = (currentTimeMillis() - currentTimeMillis) / 1000;
 			logZ3info(check + " Solved problem with optimizer with parameters " +
-					solver.getParameterDescriptions() + " Time: " + time + "s");
+					solver.getParameterDescriptions() + " Time: " + time_s + "s");
 			// Optimize solver sometimes says unsat although it produces a result. Because of
 			// this, go on if the result list is not empty.
 			if(check.equals(Status.UNSATISFIABLE)) {
@@ -413,7 +413,7 @@ public abstract class SolverRun {
 
 		ContextWrapper context = transformation.getContext();
 		logZ3info("Solving problem without optimizer with parameters\n" +
-				solver.getParameterDescriptions() + "\ntimeout: " + context.getTimeoutMS() + "ms");
+				solver.getParameterDescriptions() + "\ntimeout: " + context.getTimeoutS() + "s");
 		long currentTimeMillis = currentTimeMillis();
 
 		Z3CancelThread z3CancelThread = null;