diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java index 17e4090163fc867dde9332eb9af49ef96444676c..f799f4ebac4ae3bffc35729638559c25b882b7ab 100644 --- a/src/main/java/cli/Action.java +++ b/src/main/java/cli/Action.java @@ -59,14 +59,15 @@ import myutil.Conversion; import myutil.FileUtils; import myutil.PluginManager; import myutil.TraceManager; +import org.apache.batik.anim.timing.Trace; import proverifspec.ProVerifOutputAnalyzer; import proverifspec.ProVerifOutputListener; import proverifspec.ProVerifQueryAuthResult; import proverifspec.ProVerifQueryResult; -import tmltranslator.TMLMapping; -import tmltranslator.TMLMappingTextSpecification; -import tmltranslator.TMLModeling; -import tmltranslator.TMLTextSpecification; +import tmltranslator.*; +import tmltranslator.mutations.ApplyDiplodocusMutationException; +import tmltranslator.mutations.DiplodocusMutation; +import tmltranslator.mutations.ParseDiplodocusMutationException; import ui.MainGUI; import ui.avatarinteractivesimulation.AvatarInteractiveSimulationActions; import ui.avatarinteractivesimulation.JFrameAvatarInteractiveSimulation; @@ -112,6 +113,10 @@ public class Action extends Command implements ProVerifOutputListener { private final static String CHECKSYNTAX = "check-syntax"; private final static String REMOVE_TIME = "remove-time-operators"; + private final static String DIPLO_MUTATION = "diplodocus-mutation"; + private final static String DIPLO_MUTATION_BATCH = "diplodocus-mutation-batch"; + private final static String DIPLO_DRAW = "diplodocus-print"; + private final static String DIPLO_PRINT = "diplodocus-draw"; private final static String DIPLO_INTERACTIVE_SIMULATION = "diplodocus-interactive-simulation"; private final static String DIPLO_FORMAL_VERIFICATION = "diplodocus-formal-verification"; private final static String DIPLO_ONETRACE_SIMULATION = "diplodocus-onetrace-simulation"; @@ -580,6 +585,118 @@ public class Action extends Command implements ProVerifOutputListener { } }; + Command drawDiplodocusModel = new Command() { + public String getCommand() { + return DIPLO_DRAW; + } + + public String getShortCommand() { + return "dd"; + } + + public String getDescription() { + return "Draws the current DIPLODOCUS (TML, TMARCHI, TMAP) model"; + } + + public String getUsage() { + return "\n"; + } + + + public String executeCommand(String command, Interpreter interpreter) { + + if (!interpreter.isTToolStarted()) { + return Interpreter.TTOOL_NOT_STARTED; + } + + + TMLModeling<?> tmlModel = interpreter.mgui.gtm.getTMLModeling(); + TMLMapping tmlMapping = interpreter.mgui.gtm.getTMLMapping(); + + if (tmlModel == null && tmlMapping == null) { + return "No model"; + } else{ + if (tmlModel != null){ + try { + interpreter.mgui.drawTMLSpecification(tmlModel,"TMLModel"); + } catch (MalformedTMLDesignException e) { + TraceManager.addDev("Exception in drawing TML model :" + e.getMessage()); + } + } + if (tmlMapping != null){ + try { + interpreter.mgui.drawTMAPSpecification(tmlMapping, "TMLMapping"); + } catch (MalformedTMLDesignException e) { + TraceManager.addDev("Exception in drawing TML model :" + e.getMessage()); + } + } + } + return null; + } + }; + + + Command makeMutationFromDiplodocus = new Command() { + public String getCommand() { + return DIPLO_MUTATION; + } + + public String getShortCommand() { + return "dm"; + } + + public String getDescription() { + return "Performs a mutation on an DIPLODOCUS (TML, TMAP or TARCHI) model"; + } + + public String getUsage() { + return "[DIPLODOCUS MUTATION]\n"; + } + + public String getExample() { + return "dm rm connection between task1.chOut and task2.chIn"; + } + + public String executeCommand(String command, Interpreter interpreter) { + + if (!interpreter.isTToolStarted()) { + return Interpreter.TTOOL_NOT_STARTED; + } + + String[] commands = command.split(" "); + if (commands.length < 1) { + return Interpreter.BAD; + } + + TMLModeling<?> tmlModel = interpreter.mgui.gtm.getTMLModeling(); + TMLMapping tmlMapping = interpreter.mgui.gtm.getTMLMapping(); + + try { + DiplodocusMutation dm = DiplodocusMutation.createFromString(command); + if (dm != null) { + switch (dm.getMutationType()){ + case "TMLmutation": + if(tmlModel == null){ + return "No TML model"; + } else{ + dm.apply(tmlModel); + } + //case "TARCHImutation": + + //case "TMAPmutation": + } + } + } catch (ParseDiplodocusMutationException e) { + TraceManager.addDev("Exception in parsing mutation: " + e.getMessage()); + } catch (ApplyDiplodocusMutationException e) { + TraceManager.addDev("Exception in applying mutation: " + e.getMessage()); + } + + return null; + } + + }; + // Diplodocus interactive simulation Command diplodocusInteractiveSimulation = new Command() { public String getCommand() { @@ -1185,7 +1302,7 @@ public class Action extends Command implements ProVerifOutputListener { } public String getDescription() { - return "Perform a mutation on an AVATAR spec"; + return "Performs a mutation on an AVATAR spec"; } public String getUsage() { @@ -2147,6 +2264,8 @@ public class Action extends Command implements ProVerifOutputListener { addAndSortSubcommand(checkSyntax); addAndSortSubcommand(removeTimeOperators); + addAndSortSubcommand(makeMutationFromDiplodocus); + addAndSortSubcommand(drawDiplodocusModel); addAndSortSubcommand(generateRGFromAvatar); addAndSortSubcommand(diplodocusInteractiveSimulation); addAndSortSubcommand(diplodocusFormalVerification); diff --git a/src/main/java/tmltranslator/mutations/AddTaskMutation.java b/src/main/java/tmltranslator/mutations/AddTaskMutation.java index e5ac0342498a7efd1dc7264ec899217afbf8362d..5a924cc4f6b994757853b83219ccc641649e760a 100644 --- a/src/main/java/tmltranslator/mutations/AddTaskMutation.java +++ b/src/main/java/tmltranslator/mutations/AddTaskMutation.java @@ -8,9 +8,8 @@ public class AddTaskMutation extends TaskMutation { super(_taskName); } - public TMLTask createElement(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException{ - List<TMLTask> tasks = _tmlModel.getTasks(); - for (TMLTask task : tasks){ + public TMLTask createElement(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException{ + for (TMLTask task : _tmlModel.getTasks()){ if (task.getName().equals(getTaskName())){ throw new ApplyDiplodocusMutationException("A task named " + getTaskName() + " already exists in the current model."); } @@ -20,7 +19,7 @@ public class AddTaskMutation extends TaskMutation { } @Override - public void apply(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException { + public void apply(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException { TMLTask task = createElement(_tmlModel); _tmlModel.addTask(task); } @@ -33,6 +32,7 @@ public class AddTaskMutation extends TaskMutation { } String _taskName = tokens[index + 1]; AddTaskMutation mutation = new AddTaskMutation(_taskName); + mutation.setMutationType("TMLmutation"); return mutation; } } diff --git a/src/main/java/tmltranslator/mutations/DiplodocusMutation.java b/src/main/java/tmltranslator/mutations/DiplodocusMutation.java index f9bc549720e2d458a5791104ee0e836d624279a3..a9ae06e66804307fda48ce625d102b6b2150b487 100644 --- a/src/main/java/tmltranslator/mutations/DiplodocusMutation.java +++ b/src/main/java/tmltranslator/mutations/DiplodocusMutation.java @@ -7,7 +7,17 @@ public abstract class DiplodocusMutation { super(); } - public abstract void apply(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException; + protected String mutationType; + + public void setMutationType(String type){ + mutationType = type; + } + + public String getMutationType(){ + return mutationType; + } + + public abstract void apply(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException; public static DiplodocusMutation createFromString(String toParse) throws ParseDiplodocusMutationException { toParse = toParse.trim(); diff --git a/src/main/java/tmltranslator/mutations/RemoveTaskMutation.java b/src/main/java/tmltranslator/mutations/RemoveTaskMutation.java index d13086c1a09a1f938815ee56e0afc0ba04a16aee..a8bc27cb01cdc81b8e0c8164d46a8c2afc92abc6 100644 --- a/src/main/java/tmltranslator/mutations/RemoveTaskMutation.java +++ b/src/main/java/tmltranslator/mutations/RemoveTaskMutation.java @@ -2,6 +2,7 @@ package tmltranslator.mutations; import tmltranslator.TMLModeling; import tmltranslator.TMLTask; +import java.util.List; public class RemoveTaskMutation extends TaskMutation { @@ -9,27 +10,29 @@ public class RemoveTaskMutation extends TaskMutation { super(_taskName); } - public TMLTask getElement(TMLModeling _tmlModel){ + public TMLTask getElement(TMLModeling<?> _tmlModel){ return getTask(_tmlModel); } @Override - public void apply(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException { + public void apply(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException { TMLTask task = getElement(_tmlModel); if (task == null){ throw new ApplyDiplodocusMutationException("The task named " + getTaskName() + " does not exist in the current model."); } - _tmlModel.getTasks().remove(task); + List<TMLTask> taskList = _tmlModel.getTasks(); + taskList.remove(task); } public static RemoveTaskMutation createFromString(String toParse) throws ParseDiplodocusMutationException{ String[] tokens = DiplodocusMutationParser.tokenise(toParse); int index = DiplodocusMutationParser.indexOf(tokens, "TASK"); if (tokens.length == index + 1) { - throw new ParseDiplodocusMutationException("Block name missing. Expected syntax is [add task taskName]"); + throw new ParseDiplodocusMutationException("Block name missing. Expected syntax is [remove task taskName]"); } String _taskName = tokens[index + 1]; RemoveTaskMutation mutation = new RemoveTaskMutation(_taskName); + mutation.setMutationType("TMLmutation"); return mutation; } diff --git a/src/main/java/tmltranslator/mutations/TaskMutation.java b/src/main/java/tmltranslator/mutations/TaskMutation.java index d21366ddbcb8922584d9b4507eed12d6896d3735..6f1d854c6cbc535f7a49aa50e62a944fe8582017 100644 --- a/src/main/java/tmltranslator/mutations/TaskMutation.java +++ b/src/main/java/tmltranslator/mutations/TaskMutation.java @@ -18,14 +18,21 @@ public abstract class TaskMutation extends DiplodocusMutation { return taskName; } - protected TMLTask getTask(TMLModeling _tmlmodel){ - return _tmlmodel.getTMLTaskByName(taskName); + protected TMLTask getTask(TMLModeling<?> _tmlmodel){ + String appName = ""; + if (_tmlmodel.getTasks().size() != 0){ + appName = _tmlmodel.getTasks().get(0).getName().split("__")[0]; + } + return _tmlmodel.getTMLTaskByName(appName + "__" + taskName); } public static TaskMutation createFromString(String toParse) throws ParseDiplodocusMutationException { switch (DiplodocusMutationParser.findMutationToken(toParse)){ case "ADD": return AddTaskMutation.createFromString(toParse); + case "RM": + case "REMOVE": + return RemoveTaskMutation.createFromString(toParse); } return null; }