Commit 28c0ba20 authored by Pietro Braghieri's avatar Pietro Braghieri

add comments

parent 44aba80d
......@@ -38,7 +38,9 @@ public class CheckModelTest extends NuxmvBase
{
final File file = new File(model);
// Instantiate the tool function
final CheckModel function = new CheckModel(file.toURI());
function.setAlgorithmType(CheckModel.AlgorithmType.bmc);
function.setCheckType(CheckModel.CheckType.ltlspec);
......@@ -201,6 +203,10 @@ public class CheckModelTest extends NuxmvBase
try
{
/*
* the pair left is the exit value, the pair middle is the standard output as a string,
* the pair right is the standard error as a string
*/
final Triple<Integer, String, String> output = runner.runTool(timeout);
assertNotNull(output);
assertTrue("Exit status is == 0", output.getLeft() != 0);
......
......@@ -32,7 +32,7 @@ public class CheckContractCompositeImplementationTest extends OcraBase
@Before
public void beforeMethod()
{
// If Win OS, this test is not included because it always fails on Win platform (due to a bug in OCRA)
// 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"));
}
......@@ -84,6 +84,10 @@ public class CheckContractCompositeImplementationTest extends OcraBase
try
{
/*
* the pair left is the exit value, the pair middle is the standard output as a string,
* the pair right is the standard error as a string
*/
final Triple<Integer, String, String> output = runner.runTool(timeout);
assertNotNull(output);
//assertTrue(output.getRight(), output.getRight().isEmpty());
......
......@@ -31,12 +31,13 @@ public class CheckContractImplementationTest extends OcraBase
@Before
public void beforeMethod()
{
// If Win OS, this test is not included because it always fails on Win platform (due to a bug in OCRA)
// 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"));
}
@Test
public void testCheckContractImplementation() {
public void testCheckContractImplementation()
{
final File folder = new File(modelsDir);
final File[] listOfFiles = folder.listFiles(new FilenameFilter() {
......
......@@ -28,7 +28,8 @@ import eu.fbk.tools.adapter.ToolRunner;
public class CheckContractRefinementTest extends OcraBase
{
@Test
public void testCheckContractRefinement() {
public void testCheckContractRefinement()
{
final File folder = new File(modelsDir);
final File[] listOfFiles = folder.listFiles(new FilenameFilter() {
......@@ -53,6 +54,7 @@ public class CheckContractRefinementTest extends OcraBase
final File contractFile = new File(contractModel);
// Instantiate the tool function
final CheckContractRefinement function = new CheckContractRefinement(contractFile.toURI());
function.setTimeModel(OcraFunction.TimeModel.discrete);
......@@ -127,6 +129,10 @@ public class CheckContractRefinementTest extends OcraBase
try
{
/*
* the pair left is the exit value, the pair middle is the standard output as a string,
* the pair right is the standard error as a string
*/
final Triple<Integer, String, String> output = runner.runTool(timeout);
assertNotNull(output);
assertTrue(!output.getMiddle().isEmpty());
......
......@@ -53,6 +53,10 @@ public class ComputeFaultTreeTest extends XSapBase
try
{
/*
* the pair left is the exit value, the pair middle is the standard output as a string,
* the pair right is the standard error as a string
*/
final Triple<Integer, String, String> output = runner.runTool(timeout);
assertNotNull("Result is null", output);
assertTrue("Output is empty", !output.getMiddle().isEmpty());
......
Markdown is supported
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