Commit 9a8d5445 authored by Luca Cristoforetti's avatar Luca Cristoforetti
Browse files

Merge branch '8-new-flag-in-ocra-invocation' into 'master'

Resolve "New flag in OCRA invocation"

Closes #8

See merge request !8
parents a1f5997c 91eb0f79
Pipeline #123462 passed with stages
in 10 minutes and 20 seconds
......@@ -52,7 +52,8 @@ public interface ToolParameterConstants
final String PARAM_PRINT_WITNESS = "witness";
final String PARAM_CHECK_WITNESS = "checkWitness";
final String PARAM_SOFTWARE_MODEL = "k2Model";
final String PARAM_SOFTWARE_PROPERTY = "k2Property";
final String PARAM_SOFTWARE_PROPERTY = "k2Property";
final String PARAM_DISABLE_ASYNC_CONSTRAINTS= "disableAsyncConstraints";
final String PARAM_MAP_KEY_PREFIX = "$";
......
......@@ -15,6 +15,7 @@ import java.net.URI;
import java.net.URISyntaxException;
import java.util.List;
import org.apache.commons.lang3.BooleanUtils;
import org.apache.commons.lang3.StringUtils;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
......@@ -56,6 +57,8 @@ public abstract class OcraFunction extends ToolFunction
private URI contractModel;
private Integer boundLength;
private Boolean disableAsyncConstraints;
protected OcraFunction()
{
......@@ -180,6 +183,26 @@ public abstract class OcraFunction extends ToolFunction
this.boundLength = boundLength;
}
/**
* Gets the disableAsyncConstraints flag.
*
* @return true if the disable flag is set
*/
public Boolean getDisableAsyncConstraints()
{
return disableAsyncConstraints;
}
/**
* Sets the disableAsyncConstraints flag.
*
* @param disableAsyncConstraints
*/
public void setDisableAsyncConstraints(Boolean disableAsyncConstraints)
{
this.disableAsyncConstraints = disableAsyncConstraints;
}
@Override
public List<ToolFunctionParameter> getParameters()
{
......@@ -205,6 +228,12 @@ public abstract class OcraFunction extends ToolFunction
parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_BOUND_LENGTH, boundLength.toString()));
}
if( disableAsyncConstraints != null )
{
parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_DISABLE_ASYNC_CONSTRAINTS,
disableAsyncConstraints.toString()));
}
return parameters;
}
......@@ -257,6 +286,14 @@ public abstract class OcraFunction extends ToolFunction
}
break;
case ToolParameterConstants.PARAM_DISABLE_ASYNC_CONSTRAINTS:
disableAsyncConstraints = BooleanUtils.toBooleanObject(parameter.value);
if (disableAsyncConstraints == null)
{
logger.error("Invalid " + parameter.name +": " + parameter.value == null ? "null value" : parameter.value);
}
break;
default:
super.setParameter(parameter);
break;
......
......@@ -67,6 +67,12 @@ public class OcraRunner extends ToolRunner
cmdArray.add("-ocra-discrete-time");
}
if( ((OcraFunction)toolFunction).getDisableAsyncConstraints() != null &&
((OcraFunction)toolFunction).getDisableAsyncConstraints())
{
cmdArray.add("-ocra-disable-async-constraints");
}
cmdArray.add("-source");
cmdArray.add(cmdFile.getAbsolutePath());
}
......
......@@ -35,6 +35,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -68,6 +74,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -119,6 +131,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -152,6 +170,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -191,6 +215,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -223,12 +253,18 @@
name="Result File Destination"
optional="true">
</commandParameter>
<commandParameter
<commandParameter
id="internal_execution"
name="Internal Execution"
optional="true"
values="true, false">
</commandParameter>
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -290,6 +326,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -341,6 +383,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -395,6 +443,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......@@ -449,6 +503,12 @@
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="disable_async_constraints"
name="Disable Async Constraints"
optional="true"
values="true, false">
</commandParameter>
</command>
<command
categoryId="eu.fbk.tools.adapter"
......
......@@ -32,6 +32,8 @@ public abstract class AbstractCheckContractCommand extends AbstractToolCommand
protected String contractFileName = null;
protected OcraFunction.TimeModel timeModel = null;
protected Boolean disableAsyncConstraints = null;
public AbstractCheckContractCommand(String commandDescription)
{
......@@ -90,6 +92,30 @@ public abstract class AbstractCheckContractCommand extends AbstractToolCommand
logger.debug("Set time model to default value: " + timeModel.name());
}
disableAsyncConstraints = null;
final String disableAsyncConstraintsParameter = event.getParameter("disable_async_constraints");
if( !StringUtils.isBlank(disableAsyncConstraintsParameter) )
{
try
{
disableAsyncConstraints = Boolean.valueOf(disableAsyncConstraintsParameter);
logger.debug("Set disableAsyncConstraints to: " + disableAsyncConstraints);
}
catch (Exception e)
{
displayError(getCommandDescription(), "Internal error: unexpected value of disable_async_constraints parameter, can't execute the command.");
logger.error("Unexpected value of disable_async_constraints parameter: " + disableAsyncConstraintsParameter + " . Allowed values are: true, false.");
return false;
}
}
if( disableAsyncConstraints == null)
{
disableAsyncConstraints = false;
logger.debug("Set disableAsyncConstraints to default value: " + disableAsyncConstraints);
}
return true;
}
}
......@@ -86,6 +86,8 @@ public class CheckContractCompositeImplementationCommand extends AbstractCheckCo
function.setTimeModel(timeModel);
function.setDisableAsyncConstraints(disableAsyncConstraints);
final String algorithmType = event.getParameter("algorithm_type");
if( !StringUtils.isBlank(algorithmType) )
{
......@@ -127,13 +129,15 @@ public class CheckContractCompositeImplementationCommand extends AbstractCheckCo
@Override
public void run()
{
final ContractCompositeImplementationParametersDialog dialog = new ContractCompositeImplementationParametersDialog(activeShell, function, asyncExecution);
final ContractCompositeImplementationParametersDialog dialog =
new ContractCompositeImplementationParametersDialog(activeShell, function, asyncExecution, disableAsyncConstraints);
dialog.open();
if( dialog.goAhead() )
{
asyncExecution = dialog.getAsyncExecution();
function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
}
}
};
......
......@@ -89,6 +89,8 @@ public class CheckContractImplementationCommand extends AbstractCheckContractCom
function.setTimeModel(timeModel);
function.setDisableAsyncConstraints(disableAsyncConstraints);
final String algorithmType = event.getParameter("algorithm_type");
if( !StringUtils.isBlank(algorithmType) )
{
......@@ -151,13 +153,15 @@ public class CheckContractImplementationCommand extends AbstractCheckContractCom
@Override
public void run()
{
final ContractImplementationParametersDialog dialog = new ContractImplementationParametersDialog(activeShell, function, asyncExecution);
final ContractImplementationParametersDialog dialog =
new ContractImplementationParametersDialog(activeShell, function, asyncExecution, disableAsyncConstraints);
dialog.open();
if( dialog.goAhead() )
{
asyncExecution = dialog.getAsyncExecution();
function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
}
}
};
......
......@@ -72,6 +72,7 @@ public class CheckContractRefinementCommand extends AbstractCheckContractCommand
function.setContractName(event.getParameter("contract_name"));
wholeArchitecture = Boolean.valueOf(event.getParameter("whole_architecture"));
function.setWholeArchitecture(wholeArchitecture);
function.setDisableAsyncConstraints(disableAsyncConstraints);
// for debug purpose
if( function.getContractName() != null )
......@@ -109,14 +110,15 @@ public class CheckContractRefinementCommand extends AbstractCheckContractCommand
@Override
public void run()
{
final ContractRefinementParametersDialog dialog =
new ContractRefinementParametersDialog(activeShell, function, asyncExecution, wholeArchitecture);
final ContractRefinementParametersDialog dialog = new ContractRefinementParametersDialog(activeShell, function,
asyncExecution, wholeArchitecture, disableAsyncConstraints);
dialog.open();
if( dialog.goAhead() )
{
asyncExecution = dialog.getAsyncExecution();
function.setWholeArchitecture(dialog.getWholeArchitecture());
function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
}
}
};
......
......@@ -65,6 +65,7 @@ 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"));
......@@ -95,13 +96,15 @@ public class CheckValidationPropertyCommand extends AbstractCheckContractCommand
@Override
public void run()
{
final ValidationPropertyParametersDialog dialog = new ValidationPropertyParametersDialog(activeShell, function, asyncExecution);
final ValidationPropertyParametersDialog dialog =
new ValidationPropertyParametersDialog(activeShell, function, asyncExecution, disableAsyncConstraints);
dialog.open();
if( dialog.goAhead() )
{
asyncExecution = dialog.getAsyncExecution();
function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
}
}
};
......
......@@ -56,6 +56,7 @@ public class ComputeFaultTreeCommand extends AbstractCheckContractCommand
function.setContractModel(FileUtils.stringToURI(contractFileName));
function.setTimeModel(timeModel);
function.setDisableAsyncConstraints(disableAsyncConstraints);
return true;
}
......
......@@ -56,6 +56,7 @@ public class GenerateMiterCommand extends AbstractCheckContractCommand
}
function.setContractModel(FileUtils.stringToURI(contractFileName));
function.setDisableAsyncConstraints(disableAsyncConstraints);
final String mappingFileName = getFileNameParameter(event, ID_PARAMETER_MAP_FILE, "txt", "Choose the map file");
function.setComponentsMapping(FileUtils.stringToURI(mappingFileName));
......@@ -101,13 +102,15 @@ public class GenerateMiterCommand extends AbstractCheckContractCommand
@Override
public void run()
{
final GenerateMiterArchitectureParametersDialog dialog = new GenerateMiterArchitectureParametersDialog(activeShell, function, asyncExecution);
final GenerateMiterArchitectureParametersDialog dialog =
new GenerateMiterArchitectureParametersDialog(activeShell, function, asyncExecution, disableAsyncConstraints);
dialog.open();
if( dialog.goAhead() )
{
asyncExecution = dialog.getAsyncExecution();
function.setDisableAsyncConstraints(dialog.getDisableAsyncConstraints());
}
}
};
......
......@@ -47,6 +47,7 @@ public class GetParametersFromParamArchitectureCommand extends AbstractCheckCont
}
function.setContractModel(FileUtils.stringToURI(contractFileName));
function.setDisableAsyncConstraints(disableAsyncConstraints);
return true;
}
......
......@@ -65,6 +65,7 @@ public class InstantiateParamArchitectureCommand extends AbstractCheckContractCo
function.setContractModel(FileUtils.stringToURI(contractFileName));
function.setArchitectureParameters(FileUtils.stringToURI(paramList));
function.setDisableAsyncConstraints(disableAsyncConstraints);
return true;
}
......
......@@ -79,6 +79,8 @@ public class PrintImplementationTemplateCommand extends AbstractCheckContractCom
function.setTimeModel(timeModel);
function.setDisableAsyncConstraints(disableAsyncConstraints);
final String componentName = event.getParameter("component_name");
function.setComponentName(componentName);
......
......@@ -80,6 +80,8 @@ public class PrintSystemImplementationCommand extends AbstractCheckContractComma
function.setTimeModel(timeModel);
function.setDisableAsyncConstraints(disableAsyncConstraints);
final String oldModelFormat = event.getParameter("old_model_format");
if( !StringUtils.isBlank(oldModelFormat) )
{
......
......@@ -42,9 +42,11 @@ public class ContractCompositeImplementationParametersDialog extends Dialog {
private Spinner boundLengthSpinner;
private Button oldSmvFormatCheckBox;
private Button asyncCheckBox;
private Button disableAsyncConstraintsBox;
private Boolean asyncExecution = false;
private Boolean disableAsyncConstraints = false;
private String [] timeModels = {TimeModel.discrete.name(), TimeModel.hybrid.name()};
private String [] algorithmTypes = {"", "auto", "bdd", "bmc","ic3"};
......@@ -62,19 +64,22 @@ public class ContractCompositeImplementationParametersDialog extends Dialog {
setShellStyle(SWT.TITLE);
}
public ContractCompositeImplementationParametersDialog(Shell parentShell, CheckContractCompositeImplementation function, Boolean asyncExecution)
public ContractCompositeImplementationParametersDialog(Shell parentShell,
CheckContractCompositeImplementation function, Boolean asyncExecution, Boolean disableAsyncConstraints)
{
this(parentShell);
this.function = function;
this.asyncExecution = asyncExecution == null ? false : asyncExecution;
this.disableAsyncConstraints = disableAsyncConstraints == null ? false : disableAsyncConstraints;
}
@Override
protected void configureShell(Shell newShell) {
super.configureShell(newShell);
newShell.setText("Contract Implementation Parameters");
newShell.setText("Contract Composite Implementation Parameters");
}
/** {@inheritDoc} */
......@@ -104,6 +109,8 @@ public class ContractCompositeImplementationParametersDialog extends Dialog {
asyncExecution = asyncCheckBox.getSelection();
disableAsyncConstraints = disableAsyncConstraintsBox.getSelection();
goAhead = true;
super.okPressed();
......@@ -161,6 +168,10 @@ public class ContractCompositeImplementationParametersDialog extends Dialog {
oldSmvFormatCheckBox.setText("Old SMV format");
oldSmvFormatCheckBox.setSelection(function.getOldSmvFormat() == null ? false : function.getOldSmvFormat());
disableAsyncConstraintsBox = new Button(container, SWT.CHECK);
disableAsyncConstraintsBox.setText("Disable Async Constraints");
disableAsyncConstraintsBox.setSelection(disableAsyncConstraints);
asyncCheckBox = new Button(container, SWT.CHECK);
asyncCheckBox.setText("OSLC Asynchronous Execution");
asyncCheckBox.setSelection(asyncExecution);
......@@ -190,6 +201,10 @@ public class ContractCompositeImplementationParametersDialog extends Dialog {
return asyncExecution;
}
public Boolean getDisableAsyncConstraints() {
return disableAsyncConstraints;
}
private void setComboValues(Combo combo, String[] admittedValues, String currentValue)
{
combo.setItems(admittedValues);
......
......@@ -46,9 +46,11 @@ public class ContractImplementationParametersDialog extends Dialog {
private Spinner boundLengthSpinner;
private Button oldSmvFormatCheckBox;
private Button asyncCheckBox;
private Button disableAsyncConstraintsBox;
private Boolean asyncExecution = false;
private Boolean disableAsyncConstraints = false;
private String [] timeModels = {TimeModel.discrete.name(), TimeModel.hybrid.name()};
private String [] algorithmTypes = {"", "auto", "bdd", "bmc","ic3"};
......@@ -66,13 +68,16 @@ public class ContractImplementationParametersDialog extends Dialog {
setShellStyle(SWT.TITLE);
}
public ContractImplementationParametersDialog(Shell parentShell, CheckContractImplementation function, Boolean asyncExecution)
public ContractImplementationParametersDialog(Shell parentShell, CheckContractImplementation function,
Boolean asyncExecution, Boolean disableAsyncConstraints)
{
this(parentShell);
this.function = function;
this.asyncExecution = asyncExecution == null ? false : asyncExecution;
this.disableAsyncConstraints = disableAsyncConstraints == null ? false : disableAsyncConstraints;
}
@Override
......@@ -108,6 +113,8 @@ public class ContractImplementationParametersDialog extends Dialog {
function.setOldSmvFormat(oldSmvFormatCheckBox.getSelection());
asyncExecution = asyncCheckBox.getSelection();
disableAsyncConstraints = disableAsyncConstraintsBox.getSelection();
goAhead = true;
......@@ -181,6 +188,10 @@ public class ContractImplementationParametersDialog extends Dialog {
oldSmvFormatCheckBox.setText("Old SMV format");
oldSmvFormatCheckBox.setSelection(function.getOldSmvFormat() == null ? false : function.getOldSmvFormat());
disableAsyncConstraintsBox = new Button(container, SWT.CHECK);
disableAsyncConstraintsBox.setText("Disable Async Constraints");
disableAsyncConstraintsBox.setSelection(disableAsyncConstraints);
asyncCheckBox = new Button(container, SWT.CHECK);
asyncCheckBox.setText("OSLC Asynchronous Execution");