Merge branch '13-add-new-parameter-for-ocra_check_validation_prop' into 'master'

Resolve "Add new parameter for ocra_check_validation_prop"

Closes #13

See merge request !13

bundles/eu.fbk.tools.adapter.core/src/main/java/eu/fbk/tools/adapter/ocra/CheckValidationProperty.java

@@ -111,7 +111,7 @@ public class CheckValidationProperty extends OcraFunction
 	/**
 	 * Sets the whole architecture flag
 	 *
-	 * @param wholeArchitecture the new whole architecture
+	 * @param wholeArchitecture true if the whole architecture should be considered
 	 */
 	public void setWholeArchitecture(Boolean wholeArchitecture)
 	{
@@ -305,8 +305,15 @@ public class CheckValidationProperty extends OcraFunction
 				break;
 
 			case ToolParameterConstants.PARAM_WHOLE_ARCHITECTURE:
-				wholeArchitecture = Boolean.valueOf(parameter.value);
-				break;
+				try
+				{
+					wholeArchitecture = Boolean.valueOf(parameter.value);
+				}
+				catch (Exception e)
+				{
+					logger.error("Invalid " + parameter.name +": " + parameter.value == null ? "null value" : parameter.value);
+				}
+				break;	
 
 			case ToolParameterConstants.PARAM_PROPERTY_VALIDATION_TYPE:
 				try

bundles/eu.fbk.tools.adapter.ui/plugin.xml

@@ -449,6 +449,12 @@
                 optional="true"
                 values="true, false">
          </commandParameter>
+         <commandParameter
+               id="whole_architecture"
+               name="Whole Architecture"
+               optional="true"
+               values="true, false">
+         </commandParameter>
       </command>
        <command
             categoryId="eu.fbk.tools.adapter"

bundles/eu.fbk.tools.adapter.ui/src/main/java/eu/fbk/tools/adapter/ui/commands/contract/CheckValidationPropertyCommand.java

@@ -35,6 +35,8 @@ public class CheckValidationPropertyCommand extends AbstractCheckContractCommand
 
 	private CheckValidationProperty function;
 
+	private Boolean wholeArchitecture;
+
 	public CheckValidationPropertyCommand()
 	{
 		super("Check Validation Property");
@@ -63,14 +65,16 @@ public class CheckValidationPropertyCommand extends AbstractCheckContractCommand
 		}
 
 		function.setContractModel(FileUtils.stringToURI(contractFileName));
-
 		function.setTimeModel(timeModel);
+
 		function.setDisableAsyncConstraints(disableAsyncConstraints);
 
 		function.setComponentName(event.getParameter("component_name"));
 		function.setPropertyName(event.getParameter("property_name"));
 		function.setPossibility(event.getParameter("possibility"));
 		function.setProperties(event.getParameter("properties"));
+		wholeArchitecture = Boolean.valueOf(event.getParameter("whole_architecture"));
+		function.setWholeArchitecture(wholeArchitecture);
 
 		final String propertyValidationType = event.getParameter("property_validation_type");
 		if( propertyValidationType != null )
@@ -88,6 +92,9 @@ public class CheckValidationPropertyCommand extends AbstractCheckContractCommand
 			}
 		}
 
+		// for debug purpose
+		logger.debug("Consider the whole architecture: " + function.getWholeArchitecture());
+
 		if( isDevelopmentModeEnabled() )
 		{
 			final Display display = getWorkbench().getDisplay();
@@ -97,13 +104,15 @@ public class CheckValidationPropertyCommand extends AbstractCheckContractCommand
 				public void run()
 				{
 					final ValidationPropertyParametersDialog dialog = 
-							new ValidationPropertyParametersDialog(activeShell, function, asyncExecution, disableAsyncConstraints);
+							new ValidationPropertyParametersDialog(activeShell, function, asyncExecution, 
+									wholeArchitecture, disableAsyncConstraints);
 
 					dialog.open();
 
 					if( dialog.goAhead() )
 					{
 						asyncExecution = dialog.getAsyncExecution();
+						function.setWholeArchitecture(dialog.getWholeArchitecture());
 						function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
 					}
 				}

bundles/eu.fbk.tools.adapter.ui/src/main/java/eu/fbk/tools/adapter/ui/dialog/contract/ValidationPropertyParametersDialog.java

@@ -45,9 +45,11 @@ public class ValidationPropertyParametersDialog extends Dialog {
 	private Text   propertiesText;
 	private Combo  propertyValidationTypeCombo;
 	private Button asyncCheckBox;
+	private Button wholeArchitectureBox;
 	private Button disableAsyncConstraintsBox;
 
 	private Boolean asyncExecution = false;
+	private Boolean wholeArchitecture = false;
 	private Boolean disableAsyncConstraints = false;
 
 	private String [] timeModels = {TimeModel.discrete.name(), TimeModel.hybrid.name(), TimeModel.timed.name()};
@@ -68,7 +70,7 @@ public class ValidationPropertyParametersDialog extends Dialog {
 	}
 
 	public ValidationPropertyParametersDialog(Shell parentShell, CheckValidationProperty function, 
-			Boolean asyncExecution, Boolean disableAsyncConstraints)
+			Boolean asyncExecution, Boolean wholeArchitecture, Boolean disableAsyncConstraints)
 
 	{
 		this(parentShell);
@@ -77,6 +79,8 @@ public class ValidationPropertyParametersDialog extends Dialog {
 
 		this.asyncExecution = asyncExecution == null ? false : asyncExecution;
 
+		this.wholeArchitecture = wholeArchitecture == null ? false : wholeArchitecture;
+
 		this.disableAsyncConstraints = disableAsyncConstraints == null ? false : disableAsyncConstraints;
 	}
 
@@ -113,8 +117,10 @@ public class ValidationPropertyParametersDialog extends Dialog {
 
 		asyncExecution = asyncCheckBox.getSelection();
 
-		disableAsyncConstraints = disableAsyncConstraintsBox.getSelection();
+		wholeArchitecture = wholeArchitectureBox.getSelection();
 
+		disableAsyncConstraints = disableAsyncConstraintsBox.getSelection();
+		
 		goAhead = true;
 
 		super.okPressed();
@@ -182,6 +188,10 @@ public class ValidationPropertyParametersDialog extends Dialog {
 		propertyValidationTypeCombo.setLayoutData(gd_combo);
 		setComboValues(propertyValidationTypeCombo, propertyValidationTypes, function.getPropertyValidationType() == null ? "" : function.getPropertyValidationType().name());
 
+	    wholeArchitectureBox = new Button(container, SWT.CHECK);
+	    wholeArchitectureBox.setText("Consider the whole architecture");
+	    wholeArchitectureBox.setSelection(wholeArchitecture);
+
 	    disableAsyncConstraintsBox = new Button(container, SWT.CHECK);
 	    disableAsyncConstraintsBox.setText("Disable Async Constraints");
 	    disableAsyncConstraintsBox.setSelection(disableAsyncConstraints);
@@ -215,6 +225,10 @@ public class ValidationPropertyParametersDialog extends Dialog {
 		return asyncExecution;
 	}
 
+	public Boolean getWholeArchitecture() {
+		return wholeArchitecture;
+	}
+
 	public Boolean getDisableAsyncConstraints() {
 		return disableAsyncConstraints;
 	}

tests/eu.fbk.tools.adapter.test/src/main/java/eu/fbk/tools/adapter/ocra/CheckContractCompositeImplementationTest.java

@@ -33,7 +33,7 @@ public class CheckContractCompositeImplementationTest extends OcraBase
 	public void beforeMethod()
 	{
 		// If Win OS, this test is not included because it temporary fails on Win platform (due to a bug in OCRA)
-	    Assume.assumeFalse(System.getProperty("os.name").toLowerCase().startsWith("win"));
+//	    Assume.assumeFalse(System.getProperty("os.name").toLowerCase().startsWith("win"));
 	}
 	
 	@Test

tests/eu.fbk.tools.adapter.test/src/main/java/eu/fbk/tools/adapter/ocra/CheckContractImplementationTest.java

@@ -32,7 +32,7 @@ public class CheckContractImplementationTest extends OcraBase
 	public void beforeMethod()
 	{
 		// If Win OS, this test is not included because it temporary fails on Win platform (due to a bug in OCRA)
-	    Assume.assumeFalse(System.getProperty("os.name").toLowerCase().startsWith("win"));
+//	    Assume.assumeFalse(System.getProperty("os.name").toLowerCase().startsWith("win"));
 	}
 	
 	@Test

tests/eu.fbk.tools.adapter.test/src/main/java/eu/fbk/tools/adapter/ocra/CheckContractRefinementTest.java

@@ -168,9 +168,9 @@ public class CheckContractRefinementTest extends OcraBase
 			{
 				assertTrue("Timeout error checking model [" + file.getName() + "]", false);
 			}
-			catch (Throwable t)
-			{
-			}
+//			catch (Throwable t)
+//			{
+//			}
 			finally
 			{
 				runner.cleanSessionWorkspace();

tests/eu.fbk.tools.adapter.test/src/main/java/eu/fbk/tools/adapter/ocra/CheckValidationPropertyTest.java

@@ -23,6 +23,7 @@ import org.apache.commons.lang3.tuple.Triple;
 import org.junit.Test;
 
 import eu.fbk.tools.adapter.ToolRunner;
+import eu.fbk.tools.adapter.ocra.CheckValidationProperty.PropertyValidationType;
 
 public class CheckValidationPropertyTest extends OcraBase
 {
@@ -77,8 +78,12 @@ public class CheckValidationPropertyTest extends OcraBase
 			{
 				final Triple<Integer, String, String> output = runner.runTool(timeout);
 				assertNotNull(output);
+				assertTrue(output.getLeft() == 0);
 				assertTrue(!output.getMiddle().isEmpty());
-				assertTrue(output.getRight().isEmpty());
+				if (!output.getRight().isEmpty())
+				{
+					assertTrue(!output.getRight().toLowerCase().contains("error"));
+				}
 
 				final CheckContractResultBuilder resultBuilder = new CheckContractResultBuilder();
 				assertNotNull(resultBuilder.unmarshalResult(runner.getResultFile()));
@@ -124,8 +129,12 @@ public class CheckValidationPropertyTest extends OcraBase
 		{
 			final Triple<Integer, String, String> output = runner.runTool(timeout);
 			assertNotNull(output);
+			assertTrue(output.getLeft() == 0);
 			assertTrue(!output.getMiddle().isEmpty());
-			assertTrue(output.getRight().isEmpty());
+			if (!output.getRight().isEmpty())
+			{
+				assertTrue(!output.getRight().toLowerCase().contains("error"));
+			}
 
 			final CheckContractResultBuilder resultBuilder = new CheckContractResultBuilder();
 			final OcraOutput result = resultBuilder.unmarshalResult(runner.getResultFile());
@@ -143,4 +152,87 @@ public class CheckValidationPropertyTest extends OcraBase
 			runner.cleanSessionWorkspace();
 		}
 	}
+	
+	@Test
+	public void testCheckWholeArchitectureValidationProperty() {
+		final File folder = new File(modelsDir+File.separator+"whole_architecture_validation_property");
+		final File[] listOfFiles = folder.listFiles(new FilenameFilter() {
+
+			@Override
+			public boolean accept(File dir, String name)
+			{
+				return name.endsWith(".oss") ? true : false;
+			}
+		});
+
+		Arrays.sort(listOfFiles);
+
+		final int files = listOfFiles.length;
+
+		System.out.println();
+		System.out.println("Found " +  files + " models to be tested");
+		
+		int i = 1;
+		for (File file : listOfFiles)
+		{
+			final String contractModel = file.getAbsolutePath();
+
+			final File contractFile  = new File(contractModel);
+
+			// Instantiate the tool function
+			final CheckValidationProperty function = new CheckValidationProperty(contractFile.toURI());
+			function.setTimeModel(OcraFunction.TimeModel.discrete);
+			function.setWholeArchitecture(true);
+			function.setComponentName("ALL");
+			function.setPropertyValidationType(PropertyValidationType.consistency);
+			function.setProperties("ALL");
+
+			ToolRunner runner;
+
+			if( oslcMode )
+			{
+				runner = getOslcRunner(function);
+			}
+			else
+			{
+				runner = getRunner();
+			}
+			
+			runner.setWorkspaceDir(workspaceDir);
+			runner.setDebugMode(false);
+			runner.setToolFunction(function);
+
+			System.out.print("[" + i + "/" + files + "]"+ "Processing model: " + file.getName() + " ... ");
+			i++;
+
+			try
+			{
+				final Triple<Integer, String, String> output = runner.runTool(timeout);
+				
+				assertNotNull(output);
+				assertTrue(output.getLeft() == 0);
+				assertTrue(!output.getMiddle().isEmpty());
+				if (!output.getRight().isEmpty())
+				{
+					assertTrue(!output.getRight().toLowerCase().contains("error"));
+				}
+
+				final CheckContractResultBuilder resultBuilder = new CheckContractResultBuilder();
+				assertNotNull(resultBuilder.unmarshalResult(runner.getResultFile()));
+
+				System.out.println("done");
+			}
+			catch (TimeoutException e)
+			{
+				assertTrue("Timeout error checking model [" + file.getName() + "]", false);
+			}
+//			catch (Throwable t)
+//			{
+//			}
+			finally
+			{
+				runner.cleanSessionWorkspace();
+			}
+		}
+	}
 }

tests/eu.fbk.tools.adapter.test/src/main/resources/models/whole_architecture_validation_property/WBS_ARP_v1_crosslevel.oss

+COMPONENT simple system
+
+INTERFACE
+
+INPUT PORT Pedal_Pos1: boolean;
+INPUT PORT Pedal_Pos2: boolean;
+OUTPUT PORT Brake: boolean;
+
+CONTRACT brake
+  assume: Pedal_Pos1 iff Pedal_Pos2;
+  guarantee: (Pedal_Pos1 or Pedal_Pos2) implies (in the future Brake);
+
+REFINEMENT
+
+SUB bscu: BSCU;
+SUB hydr: Hydraulic;
+
+CONNECTION bscu.Pedal_Pos1 := Pedal_Pos1;
+CONNECTION bscu.Pedal_Pos2 := Pedal_Pos2;
+CONNECTION Brake := hydr.Brake;
+CONNECTION hydr.CMD_AS := bscu.CMD_AS;
+CONNECTION hydr.Valid := bscu.Valid;
+
+CONTRACT brake REFINEDBY bscu.bscu1.cmd, bscu.bscu2.cmd,
+                         bscu.bscu1.valid, bscu.bscu2.valid,
+                         bscu.switch.select, hydr.brake;
+
+COMPONENT BSCU
+
+INTERFACE
+
+INPUT PORT Pedal_Pos1: boolean;
+INPUT PORT Pedal_Pos2: boolean;
+OUTPUT PORT CMD_AS: boolean;
+OUTPUT PORT Valid: boolean;
+
+
+REFINEMENT
+
+SUB bscu1: subBSCU;
+SUB bscu2: subBSCU;
+SUB switch: Select_Switch;
+
+CONNECTION bscu1.Pedal_Pos := Pedal_Pos1;
+CONNECTION bscu2.Pedal_Pos := Pedal_Pos2;
+CONNECTION Valid := bscu1.Valid or bscu2.Valid;
+CONNECTION switch.In1 := bscu1.CMD_AS;
+CONNECTION switch.In2 := bscu2.CMD_AS;
+CONNECTION switch.Select := bscu1.Valid;
+CONNECTION CMD_AS := switch.Out;
+
+COMPONENT subBSCU
+
+INTERFACE
+
+INPUT PORT Pedal_Pos: boolean;
+OUTPUT PORT CMD_AS: boolean;
+OUTPUT PORT Valid: boolean;
+
+CONTRACT cmd
+assume: true;
+guarantee:
+  always ( Pedal_Pos implies then CMD_AS); 
+
+CONTRACT valid
+assume: true;
+guarantee:
+  Valid and always ((Pedal_Pos and not then CMD_AS) iff then not Valid);
+
+
+
+COMPONENT Select_Switch
+
+INTERFACE
+
+INPUT PORT In1: boolean;
+INPUT PORT In2: boolean;
+INPUT PORT Select: boolean;
+OUTPUT PORT Out: boolean;
+
+CONTRACT select
+assume:
+  TRUE;
+guarantee:
+  always ((Select implies (In1 implies Out)) and
+  	  ((not Select) implies (In2 implies Out)));
+
+
+COMPONENT Hydraulic
+
+INTERFACE
+
+INPUT PORT CMD_AS: boolean;
+INPUT PORT Valid: boolean;
+OUTPUT PORT Brake: boolean;
+
+CONTRACT brake
+assume:
+  TRUE;
+guarantee:
+  always ((CMD_AS or not Valid) implies (in the future (Brake) ));
+