Skip to content
Snippets Groups Projects
Commit 4af9c8c5 authored by tempiaa's avatar tempiaa
Browse files

New test added. Changed folder configuration

parent 4edaea66
No related branches found
No related tags found
1 merge request!325Avatar model-checker improvements
Showing
with 18557 additions and 10 deletions
...@@ -46,7 +46,6 @@ import java.util.Map; ...@@ -46,7 +46,6 @@ import java.util.Map;
import launcher.LauncherException; import launcher.LauncherException;
import launcher.RshClient; import launcher.RshClient;
import rationals.properties.isEmpty;
import ui.GTURTLEModeling; import ui.GTURTLEModeling;
import ui.MainGUI; import ui.MainGUI;
import ui.TGComponent; import ui.TGComponent;
...@@ -174,7 +173,7 @@ public class ModelCheckerValidator { ...@@ -174,7 +173,7 @@ public class ModelCheckerValidator {
rshc.sendFileData(fn + ".xml", gtm.getLastUPPAALSpecification().getStringSpec()); rshc.sendFileData(fn + ".xml", gtm.getLastUPPAALSpecification().getStringSpec());
int uResult, index; int uResult, index;
String name, query; String query;
if (dStudy) { if (dStudy) {
System.out.println("Deadlock Study"); System.out.println("Deadlock Study");
...@@ -193,7 +192,6 @@ public class ModelCheckerValidator { ...@@ -193,7 +192,6 @@ public class ModelCheckerValidator {
String s = cq.uppaalQuery; String s = cq.uppaalQuery;
index = s.indexOf('$'); index = s.indexOf('$');
if ((index != -1)) { if ((index != -1)) {
name = s.substring(index + 1, s.length());
query = s.substring(0, index); query = s.substring(0, index);
uResult = workQuery(gtm, rshc, "E<> " + query, fn); uResult = workQuery(gtm, rshc, "E<> " + query, fn);
match = false; match = false;
...@@ -229,7 +227,6 @@ public class ModelCheckerValidator { ...@@ -229,7 +227,6 @@ public class ModelCheckerValidator {
String s = cq.uppaalQuery; String s = cq.uppaalQuery;
index = s.indexOf('$'); index = s.indexOf('$');
if ((index != -1)) { if ((index != -1)) {
name = s.substring(index + 1, s.length());
query = s.substring(0, index); query = s.substring(0, index);
uResult = workQuery(gtm, rshc, "A<> " + query, fn); uResult = workQuery(gtm, rshc, "A<> " + query, fn);
match = false; match = false;
......
...@@ -272,5 +272,34 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret ...@@ -272,5 +272,34 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
assertTrue(outputResult.toString().contains("true")); assertTrue(outputResult.toString().contains("true"));
} }
@Test
public void testValidatePressureController_V2 () {
String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val3";
String script;
outputResult = new StringBuilder();
File f = new File(filePath);
assertTrue(myutil.FileUtils.checkFileForOpen(f));
script = myutil.FileUtils.loadFileData(f);
assertTrue(script.length() > 0);
//Load configuration for UPPAAL paths
String config = "../../bin/config.xml";
try {
ConfigurationTTool.loadConfiguration(config, true);
SpecConfigTTool.setBasicConfigFile(config);
} catch (Exception e) {
System.out.println("Error loading configuration from file: " + config);
}
Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
interpret.interpret();
assertTrue(outputResult.toString().contains("true"));
}
} }
print dir print dir
set model resources/test/cli/input/CoffeeMachine_Avatar.xml set model resources/test/cli/models/CoffeeMachine_Avatar.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir print dir
set model resources/test/cli/input/CoffeeMachine_Avatar.xml set model resources/test/cli/models/CoffeeMachine_Avatar.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir print dir
set model resources/test/cli/input/CoffeeMachine_Avatar.xml set model resources/test/cli/models/CoffeeMachine_Avatar.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir print dir
set model resources/test/cli/input/AirbusDoor_V2.xml set model resources/test/cli/models/AirbusDoor_V2.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir print dir
set model resources/test/cli/input/CoffeeMachine_Avatar.xml set model resources/test/cli/models/CoffeeMachine_Avatar.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir print dir
set model resources/test/cli/input/AirbusDoor_V2.xml set model resources/test/cli/models/AirbusDoor_V2.xml
#print The model to be opened is: $model #print The model to be opened is: $model
action start action start
wait 2 wait 2
......
print dir
set model resources/test/cli/models/PressureController.xml
#print The model to be opened is: $model
action start
wait 2
#toto
action open $model
wait 4
action check-syntax
action avatar-rg-validate -ra -la -s -d ../../../uppaal/
action quit
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment