Commit 63052f2f authored by Pietro Braghieri's avatar Pietro Braghieri
Browse files

update nuxmv executable to 2.0.0

fix timed nuxmv check model
parent 65a10e71
......@@ -43,7 +43,7 @@ public class NuxmvRunner extends ToolRunner
@Override
public String getMinToolVersion()
{
return "1.1.0";
return "2.0.0";
}
......@@ -63,6 +63,11 @@ public class NuxmvRunner extends ToolRunner
cmdArray.add("-source");
cmdArray.add(cmdFile.getAbsolutePath());
if( ((NuxmvFunction)toolFunction).isTimed() )
{
cmdArray.add("-time");
}
}
else
{
......
......@@ -279,4 +279,57 @@ public class CheckModelTest extends NuxmvBase
runner.cleanSessionWorkspace();
}
}
@Test
public void testCheckTimedBmcLtlspec()
{
// the behavioral model to be checked
final String model = modelsDir+"/timed/correct.smv";
System.out.print("Processing file: " + model + " ... ");
ToolRunner runner = null;
try
{
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);
function.setTimed(true);
if( oslcMode )
{
runner = getOslcRunner(function);
}
else
{
//final NuxmvRunner runner = new NuxmvRunner(toolsDir+executableName);
runner = getRunner();
runner.setWorkspaceDir(workspaceDir);
}
runner.setDebugMode(false);
runner.setToolFunction(function);
final Triple<Integer, String, String> output = runner.runTool(timeout);
assertNotNull("Output is null", output);
assertTrue("Exit status is != 0", output.getLeft() == 0);
assertTrue("Output is empty", !output.getMiddle().isEmpty());
System.out.println("done");
runner.cleanSessionWorkspace();
}
catch (TimeoutException e)
{
assertTrue("Timeout error checking model [" + model + "]", false);
}
finally {
runner.cleanSessionWorkspace();
}
}
}
@TIME_DOMAIN continuous
MODULE main
FROZENVAR
froz_r : real;
froz_i : integer;
VAR
p : boolean;
i : integer;
s : 0..10;
r : real;
DEFINE
def := 10;
-- just syntax
INIT time < (2 + def) | 2 * 4 > time | 50 mod 2 = time | 4 / 2 != time & time >= 45 * 2 / 4 mod 6 - 1 & time <= 45 * 2 / 4 mod 6 - 1 | time < froz_r * froz_i + 5 | time = s | time > i * 2 | time <= r;
TRANS time < (2 + def) | time > 2 * 4 | time = 50 mod 2 | time != 4 / 2 & time >= 45 * 2 / 4 mod 6 - 1 & time <= 45 * 2 / 4 mod 6 - 1 | time < froz_r * froz_i + 8 | time = next(s) | time > next(i * 2) | time <= r - next(r);
INVAR TRUE -> time < (2 + def) & time < 2 * 4 & time < froz_r * froz_i + 9 & time < s + r - i;
ASSIGN
init(p) := time < (2 + def) | time > 2 * 4 | time = 50 mod 2 | time != 4 / 2 & time >= 45 * 2 / 4 mod 6 - 1 & time <= 45 * 2 / 4 mod 6 - 1 | time < froz_r * froz_i + 20 | time = s - 3 | time > i / 2 | time <= r;
next(p) := time < (2 + def) | time > 2 * 4 | time = 50 mod 2 | time != 4 / 2 & time >= 45 * 2 / 4 mod 6 - 1 & time <= 45 * 2 / 4 mod 6 - 1 | time < froz_r * froz_i + 25 | time = next(s - r) | time > next(i * 2) | time <= r - next(r);
LTLSPEC G F (time < (2 + def) | time > 2 * 4 | time = 50 mod 2 | time != 4 / 2 & time >= 45 * 2 / 4 mod 6 - 1 & time <= 45 * 2 / 4 mod 6 - 1 | time < froz_r * froz_i + 8) | time = next(s) | time > next(i * 2) | time <= r - next(r);
LTLSPEC G F (time > 3.2 + froz_i & time > 6.2 + froz_i) | time = next(s) | time > next(i * 2) | time <= r - next(r);
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