Commit abe2377e authored by Pietro Braghieri's avatar Pietro Braghieri
Browse files

add timed_domain to behaviour command

parent 2f57c18a
......@@ -124,11 +124,27 @@ public class CheckModel extends NuxmvFunction
return false;
}
final String currentCheck = getCheckType().name() + (getAlgorithmType() == null ? "" : "_" + getAlgorithmType().name());
if( !getAdmittedChecks().contains(currentCheck) )
if( !isTimed() )
{
logger.error("Unsupported Check Type value: check_" + currentCheck);
return false;
final String currentCheck = getCheckType().name() + (getAlgorithmType() == null ? "" : "_" + getAlgorithmType().name());
if( !getAdmittedChecks().contains(currentCheck) )
{
logger.error("Unsupported Check type value: check_" + currentCheck);
return false;
}
}
else
{
switch( getCheckType() )
{
case invar:
case ltlspec:
break;
default:
logger.error("Unsupported Check type value: timed_check_" + getCheckType().name());
return false;
}
}
return super.validateParameters();
......@@ -137,18 +153,22 @@ public class CheckModel extends NuxmvFunction
@Override
protected void prepareCommands()
{
String goCommandName = "go";
if( getAlgorithmType() != null )
String goCommandName = "go_";
if( isTimed() )
{
goCommandName += "time";
}
else if( getAlgorithmType() != null )
{
switch( getAlgorithmType() )
{
case bmc:
goCommandName += "_" + getAlgorithmType().name();
goCommandName += getAlgorithmType().name();
break;
case ic3:
goCommandName += "_msat";
goCommandName += "msat";
break;
default:
......@@ -159,12 +179,13 @@ public class CheckModel extends NuxmvFunction
final ToolCommand goCommand = new ToolCommand(goCommandName);
String checkCommandName = "check_";
String checkCommandName = isTimed() ? "timed_check_" : "check_";
if( getCheckType() != null )
{
checkCommandName += getCheckType().name();
if ( getAlgorithmType() != null )
if ( !isTimed() && getAlgorithmType() != null )
{
checkCommandName += "_" + getAlgorithmType().name();
}
......@@ -172,7 +193,7 @@ public class CheckModel extends NuxmvFunction
final ToolCommand checkCommand = new ToolCommand(checkCommandName);
if( getAlgorithmType() != null )
if( !isTimed() && getAlgorithmType() != null )
{
switch( getAlgorithmType() )
{
......@@ -203,7 +224,7 @@ public class CheckModel extends NuxmvFunction
commands.add(new ToolCommand("set on_failure_script_quits"));
if( getAlgorithmType() == AlgorithmType.ic3 )
if( !isTimed() && getAlgorithmType() == AlgorithmType.ic3 )
{
commands.add(new ToolCommand("set").addArgument("input_file", quote(getLocalFile(getBehaviourModel()))));
}
......@@ -287,7 +308,7 @@ public class CheckModel extends NuxmvFunction
set.add("invar");
set.add("invar_bmc");
set.add("invar_ic3");
return set;
}
}
......@@ -56,6 +56,8 @@ public abstract class NuxmvFunction extends ToolFunction
private CheckType checkType;
private Integer boundLength;
private boolean timed = false;
protected NuxmvFunction()
......@@ -156,6 +158,26 @@ public abstract class NuxmvFunction extends ToolFunction
{
this.checkType = checkType;
}
/**
* Checks if is timed.
*
* @return true, if is timed
*/
public boolean isTimed()
{
return timed;
}
/**
* Sets the timed.
*
* @param timed the new timed
*/
public void setTimed(boolean timed)
{
this.timed = timed;
}
/**
* Gets the bound length.
......
......@@ -524,6 +524,12 @@
id="property"
name="Property"
optional="true">
</commandParameter>
<commandParameter
id="timed"
name="Timed"
optional="true"
values="true, false">
</commandParameter>
<commandParameter
id="algorithm_type"
......
......@@ -65,6 +65,22 @@ public class CheckModelCommand extends AbstractCheckModelCommand
// set the function parameters
function.setBehaviourModel(FileUtils.stringToURI(behaviourFileName));
final String isTimed = event.getParameter("timed");
if( isTimed != null )
{
try
{
function.setTimed((Boolean.valueOf(isTimed)));
}
catch (Exception e)
{
displayError(getCommandDescription(), "Invalid timed parameter value, can't execute the command.");
logger.error("Invalid timed parameter value: " + isTimed);
return false;
}
}
final String checkType = event.getParameter("check_type");
if( checkType != null )
......
......@@ -37,16 +37,17 @@ public class ModelCheckingParametersDialog extends Dialog {
private CheckModel function;
private Button timedDomainCheckBox;
private Combo comboCheckType;
private Combo comboAlgorithmType;
private Text propertyText;
private Button asyncCheckBox;
private Boolean asyncExecution = false;
private String [] checkTypes = {"invar", "ltlspec", "ctlspec"};
private String [] algorithmTypes = {"", "bmc", "ic3"};
private Boolean asyncExecution = false;
private String title = "nuXmv parameters";
......@@ -93,7 +94,10 @@ public class ModelCheckingParametersDialog extends Dialog {
/** {@inheritDoc} */
@Override
protected void okPressed() {
protected void okPressed()
{
function.setTimed(timedDomainCheckBox.getSelection());
try
{
function.setCheckType(CheckType.valueOf(comboCheckType.getItems()[comboCheckType.getSelectionIndex()]));
......@@ -133,6 +137,10 @@ public class ModelCheckingParametersDialog extends Dialog {
protected Control createDialogArea(Composite parent) {
parent.setToolTipText("");
final Composite container = (Composite)super.createDialogArea(parent);
timedDomainCheckBox = new Button(container, SWT.CHECK);
timedDomainCheckBox.setText("Timed Domain");
timedDomainCheckBox.setSelection(function.isTimed());
final Composite container2 = new Composite(container, SWT.NONE);
container2.setLayout(new GridLayout(2, false));
......@@ -171,17 +179,18 @@ public class ModelCheckingParametersDialog extends Dialog {
propertyText.setText(function.getFormula());
}
asyncCheckBox = new Button(container, SWT.CHECK);
asyncCheckBox.setText("OSLC Asynchronous Execution");
asyncCheckBox.setSelection(asyncExecution);
asyncCheckBox = new Button(container, SWT.CHECK);
asyncCheckBox.setText("OSLC Asynchronous Execution");
asyncCheckBox.setSelection(asyncExecution);
new Label(container, SWT.NONE);
new Label(container, SWT.NONE);
new Label(container, SWT.NONE);
final Composite container3 = new Composite(container, SWT.NONE);
GridLayout gl_container3 = new GridLayout(1, false);
container3.setLayout(gl_container3);
container3.setLayoutData(new GridData(SWT.FILL, SWT.FILL, false, false));
final Composite container3 = new Composite(container, SWT.NONE);
GridLayout gl_container3 = new GridLayout(1, false);
container3.setLayout(gl_container3);
container3.setLayoutData(new GridData(SWT.FILL, SWT.FILL, false, false));
return container;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment