From eccdb5b19bb3c9bfe91fbec4d525bd19f7db29fb Mon Sep 17 00:00:00 2001 From: Sophie Coudert <sophie.coudert@telecom-paris.fr> Date: Wed, 20 Nov 2024 16:33:32 +0100 Subject: [PATCH] one serial test added: test okFrom --- .../tosysmlv2/AvatarFromSysML.java | 8 +- src/main/java/cli/Action.java | 22 +- src/main/java/cli/Interpreter.java | 1 + .../test/java/cli/CLIAvatar2SysMLV2Test.java | 47 ++- .../resources/cli/input/scriptavsysml_okfrom | 11 + ...scriptavsysml => scriptavsysml_tothenfrom} | 0 .../cli/models/avSysML_withTimer.sysml | 303 ++++++++++++++++++ 7 files changed, 383 insertions(+), 9 deletions(-) create mode 100644 ttool/src/test/resources/cli/input/scriptavsysml_okfrom rename ttool/src/test/resources/cli/input/{scriptavsysml => scriptavsysml_tothenfrom} (100%) create mode 100644 ttool/src/test/resources/cli/models/avSysML_withTimer.sysml diff --git a/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java b/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java index 37e98413db..80505866d4 100644 --- a/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java +++ b/src/main/java/avatartranslator/tosysmlv2/AvatarFromSysML.java @@ -129,7 +129,7 @@ public class AvatarFromSysML { String errorMsg = "cannot initialize parser from file " + _fileName; addError(new AvatarFromSysMLError(AvatarFromSysMLError.ERROR, errorMsg)); TraceManager.addDev(errorMsg); - return new AvatarSpecification("DummySpec", null); + return null; } // Run parser and get parser errors @@ -139,7 +139,7 @@ public class AvatarFromSysML { for(AvatarFromSysMLError e : parser.getErrors()) TraceManager.addDev(e.toString()); errors = parser.getErrors(); - return new AvatarSpecification("DummySpec", null); + return null; } errors = stxSpec.getErrors(); @@ -161,7 +161,7 @@ public class AvatarFromSysML { for(AvatarFromSysMLError e : errors) TraceManager.addDev(e.toString()); TraceManager.addDev("Building failed with exception " + ex.toString()); - return new AvatarSpecification("DummySpec", null); + return null; } // TODO: move error handling boolean hasError = false; @@ -170,7 +170,7 @@ public class AvatarFromSysML { hasError = true; TraceManager.addDev(e.toString()); } - if (hasError) return new AvatarSpecification("DummySpec", null); + if (hasError) return null; else return avSpec; } diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java index e460bea663..9682aa8eeb 100644 --- a/src/main/java/cli/Action.java +++ b/src/main/java/cli/Action.java @@ -50,6 +50,8 @@ import avatartranslator.mutation.ApplyMutationException; import avatartranslator.mutation.AvatarMutation; import avatartranslator.mutation.ParseMutationException; import avatartranslator.tosysmlv2.AVATAR2SysMLV2; +import avatartranslator.tosysmlv2.AvatarFromSysML; +import avatartranslator.tosysmlv2.AvatarFromSysMLError; import common.ConfigurationTTool; import common.SpecConfigTTool; import graph.AUTGraph; @@ -2479,12 +2481,26 @@ public class Action extends Command implements ProVerifOutputListener { return Interpreter.BAD; } - as = AvatarSpecification.makeFromSysMLV2(commands[0]); + AvatarFromSysML builder = new AvatarFromSysML(); + AvatarSpecification tmpAs = builder.sysMLtoSpec(commands[0]); - if (interpreter.mgui != null) { - interpreter.mgui.gtm.setAvatarSpecification(as); + if (tmpAs != null) { + as = tmpAs; + if (interpreter.mgui != null) { + System.out.println("!!!!!!!!!!!! GTM " + interpreter.mgui.gtm + " !!!!!!!!!!"); + interpreter.mgui.gtm.setAvatarSpecification(as); + } } + List<AvatarFromSysMLError> errors = builder.getErrors(); + TraceManager.addUser("parsing done, " + errors.size() + " errors found"); + boolean hasError = false; + for (AvatarFromSysMLError e : errors) { + if (e.getLevel() > AvatarFromSysMLError.WARNING) + hasError = true; + TraceManager.addUser(e.toString()); + } + if (hasError || tmpAs == null) return Interpreter.BAD_SYSMLV2_SPEC; return null; } }; diff --git a/src/main/java/cli/Interpreter.java b/src/main/java/cli/Interpreter.java index 101e0f00c2..b15cd4dff1 100644 --- a/src/main/java/cli/Interpreter.java +++ b/src/main/java/cli/Interpreter.java @@ -81,6 +81,7 @@ public class Interpreter implements Runnable, TerminalProviderInterface { public final static String BAD_FILE = "Badly formatted file"; public final static String AVATAR_NO_SPEC = "No Avatar specification"; public final static String BAD_AVATAR_SPEC = "Avatar specification is incorrect"; + public final static String BAD_SYSMLV2_SPEC = "Avatar SysML V2 specification is incorrect"; public final static String TML_NO_SPEC = "No TML specification"; public final static String TMAP_NO_SPEC = "No TMAP specification"; public final static String NO_WINDOW = "The targeted window does not exist"; diff --git a/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java b/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java index e00481e12e..08399418ee 100644 --- a/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java +++ b/ttool/src/test/java/cli/CLIAvatar2SysMLV2Test.java @@ -67,6 +67,9 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu final static String PATH_TO_EXPECTED_FILE = "cli/expected/"; final static String PATH_TO_MODELS = "cli/models/"; private final String[] toThenFrom = {"CoffeeMachine_Avatar", "avSysML_mixedexample", "PressureController"}; // + private final String[] okFrom = {"avSysML_withTimer"}; // + private final int[] okFromStates = {8}; + private final int[] okFromTrans = {8}; private StringBuilder outputResult; @@ -90,7 +93,7 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu @Test public void testToThenFrom() { - String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptavsysml"; + String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptavsysml_tothenfrom"; String script; outputResult = new StringBuilder(); @@ -141,10 +144,50 @@ public class CLIAvatar2SysMLV2Test extends AbstractTest implements InterpreterOu assertTrue(oristates == tgtstates); assertTrue(oritrans == tgttrans); } + } + @Test + public void okFrom() { + String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptavsysml_okfrom"; + String script; + + outputResult = new StringBuilder(); + File f = new File(filePath); + assertTrue(myutil.FileUtils.checkFileForOpen(f)); - // Graph minimization + script = myutil.FileUtils.loadFileData(f); + assertTrue(script.length() > 0); + String header = "print dir\n set model resources/test/cli/models/"; + boolean show = false; + int size = okFrom.length; + for(int i = 0; i < size; i++) { + String model = okFrom[i]; + System.out.println("Testing Model " + model + "................................."); + String modelScript = header + model + ".sysml\n" + script; + Interpreter interpret = new Interpreter(modelScript, this, show); + interpret.clearAvatarSpecification(); + String error = interpret.interpretUntilError(); + assertTrue(error == null || error.equals("")); + // Must now load the graph + filePath = "avsysml_tgt.aut"; + f = new File(filePath); + assertTrue(myutil.FileUtils.checkFileForOpen(f)); + String data = myutil.FileUtils.loadFileData(f); + + assertTrue(data.length() > 0); + AUTGraph graph = new AUTGraph(); + graph.buildGraph(data); + graph.computeStates(); + int tgtstates = graph.getNbOfStates(); + int tgttrans = graph.getNbOfTransitions(); + int oristates = okFromStates[i]; + int oritrans = okFromTrans[i]; + + System.out.println("states=" + oristates + ", " + tgtstates + " -- transitions=" + oritrans + ", " + tgttrans); + assertTrue(oristates == tgtstates); + assertTrue(oritrans == tgttrans); + } } } diff --git a/ttool/src/test/resources/cli/input/scriptavsysml_okfrom b/ttool/src/test/resources/cli/input/scriptavsysml_okfrom new file mode 100644 index 0000000000..62cb7e8d0b --- /dev/null +++ b/ttool/src/test/resources/cli/input/scriptavsysml_okfrom @@ -0,0 +1,11 @@ +a als2 $model +wait 1 +a start +wait 1 +a new +a ad +a sf avsysml2 +a save +action check-syntax +action avatar-rg -g avsysml_tgt.aut +action quit diff --git a/ttool/src/test/resources/cli/input/scriptavsysml b/ttool/src/test/resources/cli/input/scriptavsysml_tothenfrom similarity index 100% rename from ttool/src/test/resources/cli/input/scriptavsysml rename to ttool/src/test/resources/cli/input/scriptavsysml_tothenfrom diff --git a/ttool/src/test/resources/cli/models/avSysML_withTimer.sysml b/ttool/src/test/resources/cli/models/avSysML_withTimer.sysml new file mode 100644 index 0000000000..4724987544 --- /dev/null +++ b/ttool/src/test/resources/cli/models/avSysML_withTimer.sysml @@ -0,0 +1,303 @@ +package AvatarInstance { + private import AvatarGeneral::*; + private import AvatarBlockTypes::*; + private import AvatarCommunication::*; + private import AvatarTransitionServer::*; + + // DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$ + + attribute def '@dt:Point' :> '#AvatarDataType' { + attribute 'x' : Integer default := 0; + attribute 'y' : Integer default := 0; + } + + // COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$ + + // Relation '@SYN0:B0-B1_0'============= + part '@SYN0:B0-B1_0': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1_0', '@private'=true); + + // Channel '@syn:B0.in0<B1_0.out1'------------- + part '@syn:B0.in0<B1_0.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1_0'); + binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1_0.out1'; + binding : '#OutSignalBinding' bind '@blk:B1_0'.'@sig:out1' = '@syn:B0.in0<B1_0.out1'; + +// Message of signal '@blk:B0'.'@sig:in0'............ + part def '@MSG:B0.in0' :> '#InMessage' { + private part '@channel' : '#Channel' = '@syn:B0.in0<B1_0.out1'; + attribute 'x' : Integer; + attribute 'p' : '@dt:Point'; + attribute 'b' : Boolean; + } + +// Message of signal '@blk:B1_0'.'@sig:out1'............ + part def '@MSG:B1_0.out1' :> '#OutMessage', '@MSG:B0.in0' { + attribute 'x' redefines 'x'; + attribute 'p' redefines 'p'; + attribute 'b' redefines 'b'; + } + + // Channel '@syn:B0.out0>B1_0.in1'------------- + part '@syn:B0.out0>B1_0.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1_0'); + binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1_0.in1'; + binding : '#InSignalBinding' bind '@blk:B1_0'.'@sig:in1' = '@syn:B0.out0>B1_0.in1'; + +// Message of signal '@blk:B1_0'.'@sig:in1'............ + part def '@MSG:B1_0.in1' :> '#InMessage' { + private part '@channel' : '#Channel' = '@syn:B0.out0>B1_0.in1'; + attribute 'x' : Integer; + attribute 'p' : '@dt:Point'; + attribute 'b' : Boolean; + } + +// Message of signal '@blk:B0'.'@sig:out0'............ + part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1_0.in1' { + attribute 'x' redefines 'x'; + attribute 'p' redefines 'p'; + attribute 'b' redefines 'b'; + } + + // BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$ + + // Block '@blk:B1'============= + part '@blk:B1' : '#AvatarBlock' { + + // state-machine ------------------- + exhibit state '@statemachine' : '#AvatarStateMachine' { + + entry action '@st:start' :'#AvatarStartState'; + + transition : '#AvatarTransition' first '@st:start' + then '@st:stop'; + + exit action '@st:stop' :'#AvatarStopState'; + } + + // Sub-Blocks øøøøøøøøøøøøøøøøøøøøøøø + + // Block '@blk:B1_0'============= + part '@blk:B1_0' : '#AvatarBlock' { + + // Attributes --------------------- + attribute '$x' : Integer := 0; + attribute '$b' : Boolean := false; + attribute '$p' : '@dt:Point'; + + // Signals --------------------- + part '@sig:in1' : '#Channel'; + part '@sig:out1' : '#Channel'; + + // Timers --------------------- + part '@tmr:t': '#AvatarTimer' = '#AvatarTimer'(); + + // state-machine ------------------- + exhibit state '@statemachine' : '#AvatarStateMachine' { + + state '@st:send.out1.0' : '#AvatarSendState'; + + transition : '#AvatarTransition' first '@st:send.out1.0' + then '@st:stop'; + + state '@st:standard.state2' : '#AvatarStandardState' = '#AvatarStandardState'( + '@pool' = {( + '#AvatarExpireTimerRequest'( + '@channel'= '@tmr:t'.'@expire' + ), + '#AvatarResetTimerRequest'( + '@index' = 2, + '@channel'= '@tmr:t'.'@reset', + '@payload' = '#TimerResetMsg'() + ) + )} + ); + + transition : '#AvatarTransition' first '@st:standard.state2' if '@index' == 1 + then '@st:expire.t.0'; + + transition : '#AvatarTransition' first '@st:standard.state2' if '@index' == 2 + then '@st:reset.t.0'; + + state '@st:expire.t.0' : '#AvatarExpireTimerState'; + + transition : '#AvatarTransition' first '@st:expire.t.0' + then '@st:standard.state1'; + + state '@st:standard.state1' : '#AvatarStandardState' = '#AvatarStandardState'( + '@pool' = {( + '#AvatarSetTimerRequest'( + '@channel'= '@tmr:t'.'@set', + '@payload' = '#TimerSetMsg'(10) + ), + '#ReceiveRequest'( + '@index' = 2, + '@channel'= '@sig:in1' + ) + )} + ); + + transition : '#AvatarTransition' first '@st:standard.state1' if '@index' == 1 + then '@st:set.t.0'; + + transition : '#AvatarTransition' first '@st:standard.state1' if '@index' == 2 + do action : '#ReceiveAction' { + item '@msg' : '@MSG:B1_0.in1' = '@payload' as '@MSG:B1_0.in1'; + first start; + then assign '$x' := '@msg'.'x'; + then assign '$p' := '@msg'.'p'; + then assign '$b' := '@msg'.'b'; + then done; + } then '@st:receive.in1.0'; + + state '@st:set.t.0' : '#AvatarSetTimerState'; + + transition : '#AvatarTransition' first '@st:set.t.0' + then '@st:standard.state2'; + + exit action '@st:stop' :'#AvatarStopState'; + + state '@st:reset.t.0' : '#AvatarResetTimerState'; + + transition : '#AvatarTransition' first '@st:reset.t.0' + then '@st:standard.state2'; + + entry action '@st:start' :'#AvatarStartState'; + + transition : '#AvatarTransition' first '@st:start' + then '@st:standard.state1'; + + state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'( + '@request' = { + '#SendRequest'( + '@channel'= '@sig:out1', + '@payload' = '@MSG:B1_0.out1'( + '$x', + '$p', + '$b' ) + ) + } + ); + + transition : '#AvatarTransition' first '@st:receive.in1.0' + then '@st:send.out1.0'; + } + } + } + + // Block '@blk:B0'============= + part '@blk:B0' : '#AvatarBlock' { + + // Attributes --------------------- + attribute '$x' : Integer default := 0; + attribute '$b' : Boolean default := false; + attribute '$p' : '@dt:Point'; + attribute '$y' : Integer default := 0; + + // Methods --------------------- + calc '$make': '#AvatarCalcMethod' { + attribute 'x' : Integer; + attribute 'y' : Integer; + return : '@dt:Point'; + } + calc '$getx': '#AvatarCalcMethod' { + attribute 'p' : '@dt:Point'; + return : Integer; + } + action '$foo': '#AvatarVoidMethod' { + attribute 'b' : Boolean; + attribute 'p' : '@dt:Point'; + attribute 'x' : Integer; + } + + // Signals --------------------- + part '@sig:in0' : '#Channel'; + part '@sig:out0' : '#Channel'; + + // state-machine ------------------- + exhibit state '@statemachine' : '#AvatarStateMachine' { + + state '@st:receive.in0.0' : '#AvatarReceiveState'; + + transition : '#AvatarTransition' first '@st:receive.in0.0' + then '@st:stop'; + + state '@st:send.out0.0' : '#AvatarSendState'; + + transition : '#AvatarTransition' first '@st:send.out0.0' + do action : '#TransitionAction' { + first start; + then assign '$p':= '$make'('$x', '$y'); + then assign '$x':= '$getx'('$p'); + then done; + } then '@st:random.0'; + + entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'( + '@request' = { + '#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x')) + } + ); + + transition : '#AvatarTransition' first '@st:start' + do action : '#TransitionAction' { + first start; + then assign '$x':= 1; + then assign '$b':= true; + then assign '$p'::'x':= '$x'; + then done; + } then '@st:presend.out0.0'; + + state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' ( + '@request' = { + '#SendRequest'( + '@channel'= '@sig:out0', + '@payload' = '@MSG:B0.out0'( + '$x', + '$p', + '$b' ) + ) + } + ); + + transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0'; + + state '@st:random.0' : '#AvatarRandomState' = '#AvatarRandomState'( + '@request' = { + if '$p'.'x' > 4 ? + '#immediate_request' + else '#nok_request'(1) + }, + '@state_action' = '#Assignment'( + '@target' = '$x', + '@value' = '#bound_random'(0, '$p'.'y') + ) + ); + + transition : '#AvatarTransition' first '@st:random.0' + do action : '#TransitionAction' { + first start; + then action = '$foo'('$b', '$p', '$x'); + then done; + } then '@st:prereceive.in0.0'; + + state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' ( + '@request' = { + '#ReceiveRequest'( + '@channel'= '@sig:in0' + ) + } + ); + + transition : '#AvatarTransition' first '@st:prereceive.in0.0' + do action : '#ReceiveAction' { + item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0'; + first start; + then assign '$x' := '@msg'.'x'; + then assign '$p' := '@msg'.'p'; + then assign '$b' := '@msg'.'b'; + then done; + } then '@st:receive.in0.0'; + + exit action '@st:stop' :'#AvatarStopState'; + } + } + // Block Shortcut Links $$$$$$$$$$$$ + part '@blk:B1_0' : '#AvatarBlock' :> '@blk:B1'.'@blk:B1_0' = '@blk:B1'.'@blk:B1_0'; +} -- GitLab