Skip to content
Snippets Groups Projects
Commit c17c1ce5 authored by Bastien Sultan's avatar Bastien Sultan
Browse files

[JURASSIC AMULET] adding new commands to the CLI and patching two operators

parent 3775eb9b
No related branches found
No related tags found
1 merge request!478Adding a compiler for JURASSIC AMULET
...@@ -59,14 +59,15 @@ import myutil.Conversion; ...@@ -59,14 +59,15 @@ import myutil.Conversion;
import myutil.FileUtils; import myutil.FileUtils;
import myutil.PluginManager; import myutil.PluginManager;
import myutil.TraceManager; import myutil.TraceManager;
import org.apache.batik.anim.timing.Trace;
import proverifspec.ProVerifOutputAnalyzer; import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifOutputListener; import proverifspec.ProVerifOutputListener;
import proverifspec.ProVerifQueryAuthResult; import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult; import proverifspec.ProVerifQueryResult;
import tmltranslator.TMLMapping; import tmltranslator.*;
import tmltranslator.TMLMappingTextSpecification; import tmltranslator.mutations.ApplyDiplodocusMutationException;
import tmltranslator.TMLModeling; import tmltranslator.mutations.DiplodocusMutation;
import tmltranslator.TMLTextSpecification; import tmltranslator.mutations.ParseDiplodocusMutationException;
import ui.MainGUI; import ui.MainGUI;
import ui.avatarinteractivesimulation.AvatarInteractiveSimulationActions; import ui.avatarinteractivesimulation.AvatarInteractiveSimulationActions;
import ui.avatarinteractivesimulation.JFrameAvatarInteractiveSimulation; import ui.avatarinteractivesimulation.JFrameAvatarInteractiveSimulation;
...@@ -112,6 +113,10 @@ public class Action extends Command implements ProVerifOutputListener { ...@@ -112,6 +113,10 @@ public class Action extends Command implements ProVerifOutputListener {
private final static String CHECKSYNTAX = "check-syntax"; private final static String CHECKSYNTAX = "check-syntax";
private final static String REMOVE_TIME = "remove-time-operators"; 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_INTERACTIVE_SIMULATION = "diplodocus-interactive-simulation";
private final static String DIPLO_FORMAL_VERIFICATION = "diplodocus-formal-verification"; private final static String DIPLO_FORMAL_VERIFICATION = "diplodocus-formal-verification";
private final static String DIPLO_ONETRACE_SIMULATION = "diplodocus-onetrace-simulation"; private final static String DIPLO_ONETRACE_SIMULATION = "diplodocus-onetrace-simulation";
...@@ -580,6 +585,118 @@ public class Action extends Command implements ProVerifOutputListener { ...@@ -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 // Diplodocus interactive simulation
Command diplodocusInteractiveSimulation = new Command() { Command diplodocusInteractiveSimulation = new Command() {
public String getCommand() { public String getCommand() {
...@@ -1185,7 +1302,7 @@ public class Action extends Command implements ProVerifOutputListener { ...@@ -1185,7 +1302,7 @@ public class Action extends Command implements ProVerifOutputListener {
} }
public String getDescription() { public String getDescription() {
return "Perform a mutation on an AVATAR spec"; return "Performs a mutation on an AVATAR spec";
} }
public String getUsage() { public String getUsage() {
...@@ -2147,6 +2264,8 @@ public class Action extends Command implements ProVerifOutputListener { ...@@ -2147,6 +2264,8 @@ public class Action extends Command implements ProVerifOutputListener {
addAndSortSubcommand(checkSyntax); addAndSortSubcommand(checkSyntax);
addAndSortSubcommand(removeTimeOperators); addAndSortSubcommand(removeTimeOperators);
addAndSortSubcommand(makeMutationFromDiplodocus);
addAndSortSubcommand(drawDiplodocusModel);
addAndSortSubcommand(generateRGFromAvatar); addAndSortSubcommand(generateRGFromAvatar);
addAndSortSubcommand(diplodocusInteractiveSimulation); addAndSortSubcommand(diplodocusInteractiveSimulation);
addAndSortSubcommand(diplodocusFormalVerification); addAndSortSubcommand(diplodocusFormalVerification);
......
...@@ -8,9 +8,8 @@ public class AddTaskMutation extends TaskMutation { ...@@ -8,9 +8,8 @@ public class AddTaskMutation extends TaskMutation {
super(_taskName); super(_taskName);
} }
public TMLTask createElement(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException{ public TMLTask createElement(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException{
List<TMLTask> tasks = _tmlModel.getTasks(); for (TMLTask task : _tmlModel.getTasks()){
for (TMLTask task : tasks){
if (task.getName().equals(getTaskName())){ if (task.getName().equals(getTaskName())){
throw new ApplyDiplodocusMutationException("A task named " + getTaskName() + " already exists in the current model."); throw new ApplyDiplodocusMutationException("A task named " + getTaskName() + " already exists in the current model.");
} }
...@@ -20,7 +19,7 @@ public class AddTaskMutation extends TaskMutation { ...@@ -20,7 +19,7 @@ public class AddTaskMutation extends TaskMutation {
} }
@Override @Override
public void apply(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException { public void apply(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException {
TMLTask task = createElement(_tmlModel); TMLTask task = createElement(_tmlModel);
_tmlModel.addTask(task); _tmlModel.addTask(task);
} }
...@@ -33,6 +32,7 @@ public class AddTaskMutation extends TaskMutation { ...@@ -33,6 +32,7 @@ public class AddTaskMutation extends TaskMutation {
} }
String _taskName = tokens[index + 1]; String _taskName = tokens[index + 1];
AddTaskMutation mutation = new AddTaskMutation(_taskName); AddTaskMutation mutation = new AddTaskMutation(_taskName);
mutation.setMutationType("TMLmutation");
return mutation; return mutation;
} }
} }
...@@ -7,7 +7,17 @@ public abstract class DiplodocusMutation { ...@@ -7,7 +7,17 @@ public abstract class DiplodocusMutation {
super(); 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 { public static DiplodocusMutation createFromString(String toParse) throws ParseDiplodocusMutationException {
toParse = toParse.trim(); toParse = toParse.trim();
......
...@@ -2,6 +2,7 @@ package tmltranslator.mutations; ...@@ -2,6 +2,7 @@ package tmltranslator.mutations;
import tmltranslator.TMLModeling; import tmltranslator.TMLModeling;
import tmltranslator.TMLTask; import tmltranslator.TMLTask;
import java.util.List;
public class RemoveTaskMutation extends TaskMutation { public class RemoveTaskMutation extends TaskMutation {
...@@ -9,27 +10,29 @@ public class RemoveTaskMutation extends TaskMutation { ...@@ -9,27 +10,29 @@ public class RemoveTaskMutation extends TaskMutation {
super(_taskName); super(_taskName);
} }
public TMLTask getElement(TMLModeling _tmlModel){ public TMLTask getElement(TMLModeling<?> _tmlModel){
return getTask(_tmlModel); return getTask(_tmlModel);
} }
@Override @Override
public void apply(TMLModeling _tmlModel) throws ApplyDiplodocusMutationException { public void apply(TMLModeling<?> _tmlModel) throws ApplyDiplodocusMutationException {
TMLTask task = getElement(_tmlModel); TMLTask task = getElement(_tmlModel);
if (task == null){ if (task == null){
throw new ApplyDiplodocusMutationException("The task named " + getTaskName() + " does not exist in the current model."); 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{ public static RemoveTaskMutation createFromString(String toParse) throws ParseDiplodocusMutationException{
String[] tokens = DiplodocusMutationParser.tokenise(toParse); String[] tokens = DiplodocusMutationParser.tokenise(toParse);
int index = DiplodocusMutationParser.indexOf(tokens, "TASK"); int index = DiplodocusMutationParser.indexOf(tokens, "TASK");
if (tokens.length == index + 1) { 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]; String _taskName = tokens[index + 1];
RemoveTaskMutation mutation = new RemoveTaskMutation(_taskName); RemoveTaskMutation mutation = new RemoveTaskMutation(_taskName);
mutation.setMutationType("TMLmutation");
return mutation; return mutation;
} }
......
...@@ -18,14 +18,21 @@ public abstract class TaskMutation extends DiplodocusMutation { ...@@ -18,14 +18,21 @@ public abstract class TaskMutation extends DiplodocusMutation {
return taskName; return taskName;
} }
protected TMLTask getTask(TMLModeling _tmlmodel){ protected TMLTask getTask(TMLModeling<?> _tmlmodel){
return _tmlmodel.getTMLTaskByName(taskName); 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 { public static TaskMutation createFromString(String toParse) throws ParseDiplodocusMutationException {
switch (DiplodocusMutationParser.findMutationToken(toParse)){ switch (DiplodocusMutationParser.findMutationToken(toParse)){
case "ADD": case "ADD":
return AddTaskMutation.createFromString(toParse); return AddTaskMutation.createFromString(toParse);
case "RM":
case "REMOVE":
return RemoveTaskMutation.createFromString(toParse);
} }
return null; return null;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment