Commit 00c7fccd authored by Ludovic Apvrille's avatar Ludovic Apvrille

Resolving bug on empty transition handling

parent dfba7d59
SRCS = generated_src/main.c generated_src/MainBlock.c
\ No newline at end of file
SRCS = generated_src/main.c generated_src/MeasurementDisplayer2.c generated_src/MeasurementDisplayer1.c generated_src/MeasurementGenerator.c
\ No newline at end of file
......@@ -384,7 +384,12 @@ public class AvatarTransition extends AvatarStateMachineElement {
ret += s.trim() + " / ";
}
}
String s = guard.toString();
String s = "";
if (guard == null) {
s = "";
} else {
s = guard.toString();
}
if (s.trim().length() > 0) {
ret += "guard " + s.trim() + " / ";
}
......
......@@ -178,10 +178,14 @@ public class AVATAR2CPOSIX {
mainFile = new MainFile("main", plugin);
taskFiles = new Vector<TaskFile>();
TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec);
avspec.removeCompositeStates();
avspec.removeLibraryFunctionCalls();
avspec.removeTimers();
//TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec);
if (avspec.hasApplicationCode() && includeUserCode) {
mainFile.appendToBeforeMainCode("/* User code */\n");
......@@ -590,6 +594,7 @@ public class AVATAR2CPOSIX {
}
if (_asme.nbOfNexts() == 1) {
TraceManager.addDev("Only one next in state " + _asme.getNiceName() + " in block " + _block.getName());
return ret + makeBehaviourFromElement(_block, _asme.getNext(0), false);
}
......@@ -597,7 +602,7 @@ public class AVATAR2CPOSIX {
// Put in list all
// 1) Only immediatly executable transitions
// 1) Only immediately executable transitions
for (i = 0; i < _asme.nbOfNexts(); i++) {
if (_asme.getNext(i) instanceof AvatarTransition) {
AvatarTransition at = (AvatarTransition) (_asme.getNext(i));
......@@ -609,6 +614,7 @@ public class AVATAR2CPOSIX {
ret += makeSignalAction(at, i);
} else {
// nothing special to do : immediate choice
TraceManager.addDev("Make immediate action in block" + _block.getName());
ret += makeImmediateAction(at, i);
}
}
......
......@@ -413,19 +413,19 @@ public class Action extends Command {
};
subcommands.add(start);
subcommands.add(open);
subcommands.add(quit);
subcommands.add(checkSyntax);
subcommands.add(diplodocusInteractiveSimulation);
subcommands.add(diplodocusFormalVerification);
subcommands.add(diplodocusOneTraceSimulation);
subcommands.add(diplodocusGenerateTML);
subcommands.add(diplodocusUPPAAL);
subcommands.add(navigateLeftPanel);
subcommands.add(generic);
addAndSortSubcommand(start);
addAndSortSubcommand(open);
addAndSortSubcommand(quit);
addAndSortSubcommand(checkSyntax);
addAndSortSubcommand(diplodocusInteractiveSimulation);
addAndSortSubcommand(diplodocusFormalVerification);
addAndSortSubcommand(diplodocusOneTraceSimulation);
addAndSortSubcommand(diplodocusGenerateTML);
addAndSortSubcommand(diplodocusUPPAAL);
addAndSortSubcommand(navigateLeftPanel);
addAndSortSubcommand(generic);
}
}
......@@ -126,7 +126,8 @@ public class Command implements CommandInterface {
h+= "\t" + c.getHelp();
}*/
StringBuffer b = new StringBuffer(dec + "* " + getCommand() + " (" + getShortCommand() + "): " + getUsage() + "\n" + dec + getDescription() +
StringBuffer b = new StringBuffer(dec + "* " + getCommand() + " (" + getShortCommand() + "): " + getUsage() + "\n" + dec + " " +
getDescription() +
"\n");
if (getExample().length() > 0) {
b.append(dec + "Example: " + getExample() + "\n");
......@@ -172,4 +173,19 @@ public class Command implements CommandInterface {
return couldBe;
}
public void addAndSortSubcommand(Command c) {
/*if (subcommands.size() == 0) {
subcommands.add(c);
}*/
int index = 0;
for (Command cmd: subcommands) {
if (c.getCommand().compareTo(cmd.getCommand()) < 0) {
break;
}
index ++;
}
subcommands.add(index, c);
}
}
......@@ -61,8 +61,8 @@ import java.util.*;
*/
public class Interpreter implements Runnable, TerminalProviderInterface {
public final static Command[] commands = {new Help(), new Quit(), new Action(),
new Set(), new Wait(), new Print(), new History(), new TestSpecific(), new TML()};
public final static Command[] commands = {new Action(), new Help(), new History(), new Print(), new Quit(),
new TestSpecific(), new TML(), new Set(), new Wait()};
// Errors
public final static String UNKNOWN = "Unknown command";
......
......@@ -127,7 +127,7 @@ public class Print extends Command {
return null;
}
};
subcommands.add(tabs);
addAndSortSubcommand(tabs);
}
......
......@@ -109,7 +109,7 @@ public class TML extends Command {
return loadSpec(command);
}
};
subcommands.add(load);
addAndSortSubcommand(load);
Command checkSyntax = new Command() {
public String getCommand() { return "checksyntax"; }
......@@ -121,7 +121,7 @@ public class TML extends Command {
return checkSyntax();
}
};
subcommands.add(checkSyntax);
addAndSortSubcommand(checkSyntax);
Command loadz3lib = new Command() {
public String getCommand() { return "loadz3lib"; }
......@@ -133,7 +133,7 @@ public class TML extends Command {
return loadZ3lib(command);
}
};
subcommands.add(loadz3lib);
addAndSortSubcommand(loadz3lib);
Command z3 = new Command() {
public String getCommand() { return "z3opt"; }
......@@ -145,7 +145,7 @@ public class TML extends Command {
return z3OptimalMappingAnalysis();
}
};
subcommands.add(z3);
addAndSortSubcommand(z3);
Command z3f = new Command() {
public String getCommand() { return "z3fea"; }
......@@ -157,7 +157,7 @@ public class TML extends Command {
return z3FeasibleMappingAnalysis();
}
};
subcommands.add(z3f);
addAndSortSubcommand(z3f);
Command saveResult = new Command() {
public String getCommand() { return "save-result"; }
......@@ -169,7 +169,7 @@ public class TML extends Command {
return saveResult(command);
}
};
subcommands.add(saveResult);
addAndSortSubcommand(saveResult);
Command saveResultMapping = new Command() {
public String getCommand() { return "save-result-tml-mapping"; }
......@@ -181,7 +181,7 @@ public class TML extends Command {
return saveResultTMLMapping(command);
}
};
subcommands.add(saveResultMapping);
addAndSortSubcommand(saveResultMapping);
......
......@@ -1873,7 +1873,7 @@ public class AvatarDesignPanelTranslator {
// Remove all internal start states
asm.removeAllInternalStartStates();
// Make hierachy between states and elements
// Make hierarchy between states and elements
for (TGComponent tgc : componentsToBeTranslated/*asmdp.getAllComponentList ()*/) {
if (tgc != null && tgc.getFather() != null) {
AvatarStateMachineElement element1 = (AvatarStateMachineElement) (listE.getObject(tgc));
......@@ -1893,7 +1893,12 @@ public class AvatarDesignPanelTranslator {
// if (tgc instanceof AvatarSMDConnector) {
// AvatarSMDConnector asmdco = (AvatarSMDConnector) tgc;
// Issue #69
if (!prunedConectors.contains(connector)) {
TraceManager.addDev("Found connector in block " + block.getOwnerName() + " between " +
connector.getTGComponent1() + " and " + connector.getTGComponent2());
if (prunedConectors.contains(connector)) {
TraceManager.addDev("******************************** PRUNED connector: " + connector);
} else {
//TraceManager.addDev("Must handle connector: " + connector);
FindNextEnabledAvatarSMDConnectingPointVisitor visitor = new FindNextEnabledAvatarSMDConnectingPointVisitor(prunedConectors, componentsToBeTranslated);
connector.getTGConnectingPointP1().acceptBackward(visitor);
final TGConnectingPoint conPoint1 = visitor.getEnabledComponentPoint();
......@@ -1909,15 +1914,22 @@ public class AvatarDesignPanelTranslator {
// TGComponent tgc1 = asmdp.getComponentToWhichBelongs (asmdco.getTGConnectingPointP1());
// TGComponent tgc2 = asmdp.getComponentToWhichBelongs (asmdco.getTGConnectingPointP2());
if (tgc1 == null || tgc2 == null) {
TraceManager.addDev("Tgcs null in Avatar translation");
TraceManager.addDev("TGCs nulls in Avatar translation");
} else {
final AvatarStateMachineElement element1 = (AvatarStateMachineElement) (listE.getObject(tgc1));
final AvatarStateMachineElement element2 = (AvatarStateMachineElement) (listE.getObject(tgc2));
/*if (element1 == null || element2 == null) {
TraceManager.addDev("**************** ERROR: one of the two elements is NULL");
}*/
if (element1 != null && element2 != null) {
final AvatarSMDConnector avatarSmdConnector = (AvatarSMDConnector) connector;
if (asm.findEmptyTransition(element1, element2) == null) {
TraceManager.addDev("Handling connector");
//if (asm.findEmptyTransition(element1, element2) == null) {
//TraceManager.addDev("-- Empty transition");
final AvatarTransition at = new AvatarTransition(_ab, "avatar transition", connector);
createTransitionInfo(at, avatarSmdConnector);
// AvatarTransition at = new AvatarTransition (_ab, "avatar transition", tgc);
......@@ -2029,7 +2041,7 @@ public class AvatarDesignPanelTranslator {
ce.setTGComponent(connector);
addCheckingError(ce);
}
}
//}
}
}
}
......
......@@ -9497,8 +9497,10 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
}
menu.addSeparator();
menu.add(newVerificationProperty);
if (experimentalOn) {
menu.addSeparator();
menu.add(newVerificationProperty);
}
}
......
......@@ -237,6 +237,16 @@ public abstract class TGConnector extends TGCScalableWithInternalComponent {
return p2;
}
public TGComponent getTGComponent1() {
TDiagramPanel tdp = getTDiagramPanel();
return tdp.getComponentToWhichBelongs(p1);
}
public TGComponent getTGComponent2() {
TDiagramPanel tdp = getTDiagramPanel();
return tdp.getComponentToWhichBelongs(p2);
}
public void setP1(TGConnectingPoint p) {
p1 = p;
}
......
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