From da04376ad6eef5c7505aadfcbe0636c2d3856e50 Mon Sep 17 00:00:00 2001 From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr> Date: Tue, 18 May 2010 15:08:01 +0000 Subject: [PATCH] First AVATAR to TIF support --- src/translator/TURTLETranslator.java | 3 + src/ui/AvatarDesignPanel.java | 4 + src/ui/AvatarDesignPanelTranslator.java | 1189 +++++++++++++++++++ src/ui/AvatarSignal.java | 15 + src/ui/GTURTLEModeling.java | 40 + src/ui/MainGUI.java | 54 +- src/ui/avatarbd/AvatarBDBlock.java | 5 + src/ui/avatarbd/AvatarBDPortConnector.java | 4 +- src/ui/avatarsmd/AvatarSMDState.java | 23 + src/ui/window/JDialogModelChecking.java | 4 +- src/ui/window/JDialogSelectAvatarBlock.java | 372 ++++++ 11 files changed, 1703 insertions(+), 10 deletions(-) create mode 100644 src/ui/AvatarDesignPanelTranslator.java create mode 100755 src/ui/window/JDialogSelectAvatarBlock.java diff --git a/src/translator/TURTLETranslator.java b/src/translator/TURTLETranslator.java index 05cd65a5c7..be8c513d4b 100755 --- a/src/translator/TURTLETranslator.java +++ b/src/translator/TURTLETranslator.java @@ -589,6 +589,9 @@ public class TURTLETranslator { if (k != 0) { sb.append(", "); } + if (g.getLotosName() == null) { + g.setLotosName(g.getName()); + } sb.append(g.getLotosName()); } sb.append("]| "); diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java index b4b685e3b3..74745193fa 100644 --- a/src/ui/AvatarDesignPanel.java +++ b/src/ui/AvatarDesignPanel.java @@ -68,6 +68,10 @@ public class AvatarDesignPanel extends TURTLEPanel { tabbedPane.addChangeListener(cl); tabbedPane.addMouseListener(new TURTLEPanelPopupListener(this, mgui)); } + + public AvatarBDPanel getAvatarBDPanel() { + return abdp; + } public AvatarSMDPanel getAvatarSMDPanel(String name) { AvatarSMDPanel asmdp; diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java new file mode 100644 index 0000000000..8e26cc59ca --- /dev/null +++ b/src/ui/AvatarDesignPanelTranslator.java @@ -0,0 +1,1189 @@ +/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille +* +* ludovic.apvrille AT enst.fr +* +* This software is a computer program whose purpose is to allow the +* edition of TURTLE analysis, design and deployment diagrams, to +* allow the generation of RT-LOTOS or Java code from this diagram, +* and at last to allow the analysis of formal validation traces +* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP +* from INRIA Rhone-Alpes. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +* +* /** +* Class AvatarDesignPanelTranslator +* Creation: 18/05/2010 +* @author Ludovic APVRILLE +* @see +*/ + +package ui; + +import java.util.*; + + + +import myutil.*; +import ui.avatarbd.*; +import ui.avatarsmd.*; + +import translator.*; +import ui.window.*; + + +public class AvatarDesignPanelTranslator { + protected AvatarDesignPanel adp; + protected Vector checkingErrors, warnings; + protected CorrespondanceTGElement listE; // usual list + protected CorrespondanceTGElement listB; // list for particular element -> first element of group of blocks + protected LinkedList <TDiagramPanel> panels; + protected LinkedList <ActivityDiagram> activities; + + public AvatarDesignPanelTranslator(AvatarDesignPanel _adp) { + adp = _adp; + reinit(); + } + + public void reinit() { + checkingErrors = new Vector(); + warnings = new Vector(); + listE = new CorrespondanceTGElement(); + listB = new CorrespondanceTGElement(); + panels = new LinkedList <TDiagramPanel>(); + activities = new LinkedList <ActivityDiagram>(); + } + + public Vector getErrors() { + return checkingErrors; + } + + public Vector getWarnings() { + return warnings; + } + + public CorrespondanceTGElement getCorrespondanceTGElement() { + return listE; + } + + public TURTLEModeling generateTURTLEModeling() { + LinkedList<AvatarBDBlock> blocks = adp.getAvatarBDPanel().getFullBlockList(); + return generateTURTLEModeling(blocks, ""); + } + + public TURTLEModeling generateTURTLEModeling(Vector blocks, String preName) { + LinkedList<AvatarBDBlock> ll = new LinkedList<AvatarBDBlock>(); + for(int i=0; i<blocks.size(); i++) { + ll.add((AvatarBDBlock)blocks.get(i)); + } + return generateTURTLEModeling(ll, preName); + } + + public TURTLEModeling generateTURTLEModeling(LinkedList<AvatarBDBlock> blocks, String preName) { + TURTLEModeling tmodel = new TURTLEModeling(); + createTClassesFromBlocks(tmodel, blocks, preName); + createRelationsBetweenTClasses(tmodel, blocks, preName); + //addTClasses(adp, blocks, preName, tmodel); + //addRelations(adp, tmodel); + return tmodel; + } + + private void addCheckingError(CheckingError ce) { + if (checkingErrors == null) { + checkingErrors = new Vector(); + } + checkingErrors.addElement(ce); + } + + private void addWarning(CheckingError ce) { + if (warnings == null) { + warnings = new Vector(); + } + warnings.addElement(ce); + } + + public void createTClassesFromBlocks(TURTLEModeling tm, LinkedList<AvatarBDBlock> blocks, String preName) { + TClass t; + Vector v; + int i; + TAttribute a; + Param p; + AvatarMethod am; + Gate g; + AvatarSignal as; + + for(AvatarBDBlock block: blocks) { + t = new TClass(preName + block.getBlockName(), true); + + tm.addTClass(t); + listE.addCor(t, block, preName); + + // Create attributes + v = block.getAttributeList(); + for(i=0; i<v.size(); i++) { + a = (TAttribute)(v.elementAt(i)); + if ((a.getType() == TAttribute.NATURAL) || (a.getType() == TAttribute.INTEGER)){ + p = new Param(a.getId(), Param.NAT, a.getInitialValue()); + p.setAccess(a.getAccessString()); + t.addParameter(p); + } + if (a.getType() == TAttribute.BOOLEAN) { + p = new Param(a.getId(), Param.BOOL, a.getInitialValue()); + p.setAccess(a.getAccessString()); + t.addParameter(p); + } + } + + // Create internal gates + v = block.getMethodList(); + for(i=0; i<v.size(); i++) { + am = (AvatarMethod)(v.get(i)); + g = new Gate(am.getId(), Gate.GATE, false); + t.addGate(g); + } + + // Create external gates from signals + v = block.getSignalList(); + for(i=0; i<v.size(); i++) { + as = (AvatarSignal)(v.get(i)); + if (as.getInOut() == AvatarSignal.IN) { + g = new Gate(as.getId(), Gate.INGATE, false); + } else { + g = new Gate(as.getId(), Gate.OUTGATE, false); + } + t.addGate(g); + } + + // Activity Diagram + buildStateMachineDiagram(tm, block, t); + } + } + + private void buildStateMachineDiagram(TURTLEModeling tm, AvatarBDBlock block, TClass t) { + int j; + //TActivityDiagramPanel tadp; + AvatarSMDPanel asmdp = block.getAvatarSMDPanel(); + String name = block.getBlockName(); + TDiagramPanel tdp; + + if (asmdp == null) { + return; + } + + tdp = (TDiagramPanel)asmdp; + + int indexTdp = panels.indexOf(tdp); + if (indexTdp > -1) { + TraceManager.addDev("Found similar diagram for " + block.getBlockName()); + t.setActivityDiagram((activities.get(indexTdp)).duplicate(t)); + + //System.out.println("AD of " + t.getName() + "="); + //t.getActivityDiagram().print(); + + // Must fill correspondances! + ADComponent ad0, ad1; + TGComponent tgcad; + for(int adi=0; adi<t.getActivityDiagram().size(); adi++) { + ad0 = (ADComponent)(t.getActivityDiagram().get(adi)); + ad1 = (ADComponent)(activities.get(indexTdp).get(adi)); + tgcad = listE.getTG(ad1); + if (tgcad != null ){ + //System.out.println("Adding correspondance for " + ad0); + listE.addCor(ad0, tgcad); + } + } + + return; + } + + // search for start state + LinkedList list = asmdp.getComponentList(); + Iterator iterator = list.listIterator(); + TGComponent tgc; + TGComponent tss = null; + int cptStart = 0; + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDStartState){ + tss = tgc; + cptStart ++; + } + } + + if (tss == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "No start state in the state machine diagram of " + name); + ce.setTClass(t); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + if (cptStart > 1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in the state machine diagram of " + name); + ce.setTClass(t); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + // This shall also be true for all composite state: at most one start state! + tgc = checkForStartStateOfCompositeStates(asmdp); + if (tgc != null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in composite state"); + ce.setTClass(t); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + return; + } + + // Creation of the activity diagram + ADStart ads; + ADStop adstop; + ads = new ADStart(); + + listE.addCor(ads, tss); + ActivityDiagram ad = new ActivityDiagram(ads); + + adstop = new ADStop(); + ads.addNext(adstop); + ad.add(adstop); + + t.setActivityDiagram(ad); + + panels.add(tdp); + activities.add(ad); + } + + // Checks whether all states with internal state machines have at most one start state + private TGComponent checkForStartStateOfCompositeStates(AvatarSMDPanel _panel) { + TGComponent tgc; + ListIterator iterator = _panel.getComponentList().listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDState) { + tgc = (((AvatarSMDState)(tgc)).checkForStartStateOfCompositeStates()); + if (tgc != null) { + return tgc; + } + } + } + return null; + } + + + + /*private void addTDataAttributes(TAttribute a, TClass t, ClassDiagramPanelInterface tdp, TURTLEModeling tm) { + //System.out.println("Find data: " + a.getId() + " getTypeOther=" + a.getTypeOther()); + if (tdp instanceof TClassDiagramPanel) { + TCDTData tdata = ((TClassDiagramPanel)tdp).findTData(a.getTypeOther()); + if (tdata == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown type: " + a.getTypeOther()); + ce.setTClass(t); + ce.setTDiagramPanel((TDiagramPanel)tdp); + addCheckingError(ce); + return ; + } + + Vector v = tdata.getAttributes(); + TAttribute b; Param p; + for(int i=0; i<v.size(); i++) { + b = (TAttribute)(v.elementAt(i)); + if (b.getType() == TAttribute.NATURAL) { + p = new Param(a.getId() + "__" + b.getId(), Param.NAT, b.getInitialValue()); + p.setAccess(a.getAccessString()); + t.addParameter(p); + } + if (b.getType() == TAttribute.BOOLEAN) { + p = new Param(a.getId() + "__" + b.getId(), Param.BOOL, b.getInitialValue()); + p.setAccess(a.getAccessString()); + t.addParameter(p); + } + + if (b.getType() == TAttribute.QUEUE_NAT) { + p = new Param(a.getId() + "__" + b.getId(), Param.QUEUE_NAT, b.getInitialValue()); + p.setAccess(a.getAccessString()); + t.addParameter(p); + } + } + } + + } + + private void buildActivityDiagram(TClass t) { + int j; + //TActivityDiagramPanel tadp; + ActivityDiagramPanelInterface adpi; + TDiagramPanel tdp; + //t.printParams(); + + // find the panel of this TClass + TClassInterface tci = (TClassInterface)(listE.getTG(t)); + + String name = tci.getClassName(); + int index_name = name.indexOf(':'); + // instance + if (index_name != -1) { + name = name.substring(index_name+2, name.length()); + } + + adpi = tci.getBehaviourDiagramPanel(); + if (adpi == null) { + return; + } + + tdp = (TDiagramPanel)adpi; + + int indexTdp = panels.indexOf(tdp); + if (indexTdp > -1) { + System.out.println("Found similar activity diagram for " + t.getName()); + t.setActivityDiagram(activities.get(indexTdp).duplicate(t)); + + //System.out.println("AD of " + t.getName() + "="); + //t.getActivityDiagram().print(); + + // Must fill correspondances! + + ADComponent ad0, ad1; + TGComponent tgcad; + for(int adi=0; adi<t.getActivityDiagram().size(); adi++) { + ad0 = (ADComponent)(t.getActivityDiagram().get(adi)); + ad1 = (ADComponent)(activities.get(indexTdp).get(adi)); + tgcad = listE.getTG(ad1); + if (tgcad != null ){ + //System.out.println("Adding correspondance for " + ad0); + listE.addCor(ad0, tgcad); + } + } + + return; + } + + // search for start state + LinkedList list = adpi.getComponentList(); + Iterator iterator = list.listIterator(); + TGComponent tgc; + TGComponent tss = null; + int cptStart = 0; + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof TADStartState){ + tss = tgc; + cptStart ++; + } else if (tgc instanceof TOSADStartState) { + tss = tgc; + cptStart ++; + } + } + + if (tss == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "No start state in the activity diagram of " + name); + ce.setTClass(t); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + if (cptStart > 1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in the activity diagram of " + name); + ce.setTClass(t); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + TADActionState tadas; + + ADStart ads; + //ADActionState ada; + ADActionStateWithGate adag; + ADActionStateWithParam adap; + ADActionStateWithMultipleParam adamp; + ADChoice adch; + ADDelay add; + ADJunction adj; + ADLatency adl; + ADParallel adp; + ADSequence adseq; + ADPreempt adpre; + ADStop adst; + ADTimeInterval adti; + ADTLO adtlo; + ADTimeCapture adtc; + String s, s1; + Gate g; + Param p; + + int nbActions; + String sTmp; + + int startIndex = listE.getSize(); + + // Creation of the activity diagram + ads = new ADStart(); + listE.addCor(ads, tss); + ActivityDiagram ad = new ActivityDiagram(ads); + t.setActivityDiagram(ad); + + panels.add(tdp); + activities.add(ad); + + + //System.out.println("Making activity diagram of " + t.getName()); + + // Creation of other elements + iterator = list.listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + + if (tgc instanceof TADActionState) { + tadas = (TADActionState)tgc; + s = ((TADActionState)tgc).getAction(); + s = s.trim(); + //remove ';' if last character + if (s.substring(s.length()-1, s.length()).compareTo(";") == 0) { + s = s.substring(0, s.length()-1); + } + nbActions = Conversion.nbChar(s, ';') + 1; + //System.out.println("Nb Actions in state: " + nbActions); + + s = TURTLEModeling.manageDataStructures(t, s); + + g = t.getGateFromActionState(s); + p = t.getParamFromActionState(s); + if ((g != null) && (nbActions == 1)){ + //System.out.println("Action state with gate found " + g.getName() + " value:" + t.getActionValueFromActionState(s)); + adag = new ADActionStateWithGate(g); + ad.addElement(adag); + s1 = t.getActionValueFromActionState(s); + //System.out.println("s1=" + s1); + //System.out.println("Adding type"); + s1 = TURTLEModeling.manageGateDataStructures(t, s1); + + //System.out.println("hi"); + if (s1 == null) { + //System.out.println("ho"); + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Invalid expression: " + t.getActionValueFromActionState(s)); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + //return; + } else { + tadas.setStateAction(ErrorHighlight.GATE); + s1 = TURTLEModeling.addTypeToDataReceiving(t, s1); + + adag.setActionValue(s1); + //System.out.println("Adding correspondance tgc=" + tgc + "adag=" + adag); + listE.addCor(adag, tgc); + listB.addCor(adag, tgc); + } + } else if ((p != null) && (nbActions == 1)){ + //System.out.println("Action state with param found " + p.getName() + " value:" + t.getExprValueFromActionState(s)); + if (t.getExprValueFromActionState(s).trim().startsWith("=")) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, s + " should not start with a '=='"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + } + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, t.getExprValueFromActionState(s))); + listE.addCor(adap, tgc); + listB.addCor(adap, tgc); + tadas.setStateAction(ErrorHighlight.ATTRIBUTE); + + } else if ((p != null) && (nbActions > 1)){ + //System.out.println("Action state with multi param found " + p.getName() + " value:" + t.getExprValueFromActionState(s)); + // Checking params + CheckingError ce; + Vector v; + for(j=0; j<nbActions; j++) { + sTmp = TURTLEModeling.manageDataStructures(t,((TADActionState)(tgc)).getAction(j)); + if (sTmp == null) { + ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Action state (0) (" + s + "): \"" + s + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + } + + p = t.getParamFromActionState(sTmp); + if (p == null) { + ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Action state (1) (" + s + "): \"" + sTmp + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + } + } + + + tadas.setStateAction(ErrorHighlight.ATTRIBUTE); + ADComponent adtmp = null; + for(j=0; j<nbActions; j++) { + sTmp = TURTLEModeling.manageDataStructures(t,((TADActionState)(tgc)).getAction(j)); + p = t.getParamFromActionState(sTmp); + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + if (adtmp != null) { + adtmp.addNext(adap); + } else { + listB.addCor(adap, tgc); + } + adtmp = adap; + adap.setActionValue(t.getExprValueFromActionState(sTmp)); + } + + listE.addCor(adtmp, tgc); + + } else { + // Is it of kind: tdata = tdata'? + int index = s.indexOf("="); + if (index > -1) { + String name0 = s.substring(0,index).trim(); + String name1 = s.substring(index+1,s.length()).trim(); + Vector attributes = tci.getAttributes(); + int index0 = -1; + int index1 = -1; + TAttribute ta, ta0 = null, ta1 = null; + + for(j=0; j<attributes.size(); j++) { + ta = (TAttribute)(attributes.get(j)); + if (ta.getId().compareTo(name0) == 0) { + index0 = j; + ta0 = ta; + } + if (ta.getId().compareTo(name1) == 0) { + index1 = j; + ta1 = ta; + } + } + + if (((index0 != -1) && (index1 != -1)) && (ta0.getTypeOther().compareTo(ta1.getTypeOther()) == 0)) { + // Expand the equality! + tadas.setStateAction(ErrorHighlight.ATTRIBUTE); + + String nameTmp; + Vector v0 = t.getParamStartingWith(ta0.getId()+ "__"); + ADComponent adtmp = null; + + for(j=0; j<v0.size(); j++) { + p = (Param)(v0.get(j)); + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + if (adtmp != null) { + adtmp.addNext(adap); + } else { + listB.addCor(adap, tgc); + } + adtmp = adap; + nameTmp = p.getName(); + nameTmp = nameTmp.substring(nameTmp.indexOf("__"), nameTmp.length()); + adap.setActionValue(name1 + nameTmp); + } + + listE.addCor(adtmp, tgc); + } else { + //System.out.println("Unknown param 0 or 1"); + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Action state (2) (" + s + "): \"" + s + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + } + + } else { + //System.out.println("Unknown param"); + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Action state (2) (" + s + "): \"" + s + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + tadas.setStateAction(ErrorHighlight.UNKNOWN_AS); + } + //System.out.println("Bad action state found " + s); + } + + } else if (tgc instanceof TADTimeCapture) { + p = t.getParamByName(tgc.getValue().trim()); + if (p != null){ + System.out.println("Time capture with param " + p.getName()); + adtc = new ADTimeCapture(p); + ad.addElement(adtc); + ((TADTimeCapture)tgc).setStateAction(ErrorHighlight.ATTRIBUTE); + } else { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown variable: " + tgc.getValue()); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ((TADTimeCapture)tgc).setStateAction(ErrorHighlight.UNKNOWN_AS); + } + + // Get element from Array + } else if (tgc instanceof TADArrayGetState) { + TADArrayGetState ags = (TADArrayGetState)tgc; + sTmp = ags.getIndex(); + try { + nbActions = Integer.decode(sTmp).intValue(); + + p = t.getParamByName(ags.getVariable()); + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ags.getVariable() + ": unknown variable"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ags.setStateAction(ErrorHighlight.UNKNOWN); + } else { + adap = new ADActionStateWithParam(p); + p = t.getParamByName(ags.getArray() + "__" + nbActions); + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ags.getArray() + "[" + ags.getIndex() + "]: unknown array or wrong index"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ags.setStateAction(ErrorHighlight.UNKNOWN); + } else { + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, ags.getArray() + "__" + nbActions)); + listE.addCor(adap, tgc); + listB.addCor(adap, tgc); + ags.setStateAction(ErrorHighlight.OK); + } + } + } catch (Exception e) { + // Index is not an absolute value + System.out.println("Index is not an absolute value"); + Gate error = t.addNewGateIfApplicable("arrayOverflow"); + + ADChoice choice1 = new ADChoice(); + ADJunction junc = new ADJunction(); + ADStop stop1 = new ADStop(); + ADActionStateWithGate adag1 = new ADActionStateWithGate(error); + + ad.addElement(choice1); + ad.addElement(junc); + ad.addElement(stop1); + ad.addElement(adag1); + + String basicGuard = "(" + ags.getIndex() + ")"; + + p = t.getParamByName(ags.getArray() + "__size"); + + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ags.getArray() + "[" + ags.getIndex() + "]: unknown array or wrong index"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ags.setStateAction(ErrorHighlight.UNKNOWN); + } else { + int size = 2; + try { + size = Integer.decode(p.getValue()).intValue(); + } catch (Exception e0) { + } + + p = t.getParamByName(ags.getVariable()); + + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ags.getVariable() + ": unknown variable"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ags.setStateAction(ErrorHighlight.UNKNOWN); + } else { + for(int i=0; i<size; i++) { + //System.out.println("Adding guard: [" + basicGuard + "== " + i + "]"); + choice1.addGuard("[" + basicGuard + " == " + i + "]"); + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, ags.getArray() + "__" + i)); + choice1.addNext(adap); + adap.addNext(junc); + ags.setStateAction(ErrorHighlight.OK); + } + + choice1.addGuard("[" + basicGuard + "> (" + ags.getArray() + "__size - 1)]"); + choice1.addNext(adag1); + adag1.addNext(stop1); + + listE.addCor(junc, tgc); + listB.addCor(choice1, tgc); + + } + } + } + + } else if (tgc instanceof TADArraySetState) { + TADArraySetState ass = (TADArraySetState)tgc; + sTmp = ass.getIndex(); + try { + nbActions = Integer.decode(sTmp).intValue(); + p = t.getParamByName(ass.getArray() + "__" + nbActions); + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ass.getArray() + "[" + ass.getIndex() + "]: unknown array or wrong index"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ass.setStateAction(ErrorHighlight.UNKNOWN); + } else { + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, ass.getExpr())); + listE.addCor(adap, tgc); + listB.addCor(adap, tgc); + ass.setStateAction(ErrorHighlight.OK); + } + + } catch (Exception e) { + // Index is not an absolute value + //System.out.println("Set: Index is not an absolute value"); + Gate error = t.addNewGateIfApplicable("arrayOverflow"); + + ADChoice choice1 = new ADChoice(); + ADJunction junc = new ADJunction(); + ADStop stop1 = new ADStop(); + ADActionStateWithGate adag1 = new ADActionStateWithGate(error); + + ad.addElement(choice1); + ad.addElement(junc); + ad.addElement(stop1); + ad.addElement(adag1); + + String basicGuard = "(" + ass.getIndex() + ")"; + + p = t.getParamByName(ass.getArray() + "__size"); + + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ass.getArray() + "[" + ass.getIndex() + "]: unknown array or wrong index"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ass.setStateAction(ErrorHighlight.UNKNOWN); + } else { + int size = 2; + try { + size = Integer.decode(p.getValue()).intValue(); + } catch (Exception e0) { + } + + for(int i=0; i<size; i++) { + //System.out.println("Adding guard: [" + basicGuard + "== " + i + "]"); + p = t.getParamByName(ass.getArray() + "__" + i); + adap = null; + if (p == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Array setting: " + ass.getArray() + "[" + ass.getIndex() + "]: unknown array or wrong index"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ass.setStateAction(ErrorHighlight.UNKNOWN); + } else { + choice1.addGuard("[" + basicGuard + " == " + i + "]"); + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, ass.getExpr())); + choice1.addNext(adap); + adap.addNext(junc); + ass.setStateAction(ErrorHighlight.OK); + } + + choice1.addGuard("[" + basicGuard + "> (" + ass.getArray() + "__size - 1)]"); + choice1.addNext(adag1); + adag1.addNext(stop1); + + listE.addCor(junc, tgc); + listE.addCor(choice1, tgc); + if (adap != null) { + listE.addCor(adap, tgc); + } + listE.addCor(stop1, tgc); + listE.addCor(adag1, tgc); + listB.addCor(choice1, tgc); + + } + } + } + + } else if (tgc instanceof TADChoice) { + adch = new ADChoice(); + ad.addElement(adch); + listE.addCor(adch, tgc); + } else if (tgc instanceof TADDeterministicDelay) { + add = new ADDelay(); + ad.addElement(add); + add.setValue(TURTLEModeling.manageGateDataStructures(t, ((TADDeterministicDelay)tgc).getDelayValue())); + listE.addCor(add, tgc); + } else if (tgc instanceof TADJunction) { + adj = new ADJunction(); + ad.addElement(adj); + listE.addCor(adj, tgc); + } else if (tgc instanceof TADNonDeterministicDelay) { + adl = new ADLatency(); + ad.addElement(adl); + adl.setValue(TURTLEModeling.manageGateDataStructures(t, ((TADNonDeterministicDelay)tgc).getLatencyValue())); + listE.addCor(adl, tgc); + } else if (tgc instanceof TADParallel) { + adp = new ADParallel(); + ad.addElement(adp); + adp.setValueGate(((TADParallel)tgc).getValueGate()); + listE.addCor(adp, tgc); + } else if (tgc instanceof TADSequence) { + adseq = new ADSequence(); + ad.addElement(adseq); + listE.addCor(adseq, tgc); + } else if (tgc instanceof TADPreemption) { + adpre = new ADPreempt(); + ad.addElement(adpre); + listE.addCor(adpre, tgc); + } else if (tgc instanceof TADStopState) { + adst = new ADStop(); + ad.addElement(adst); + listE.addCor(adst, tgc); + } else if (tgc instanceof TADTimeInterval) { + adti = new ADTimeInterval(); + ad.addElement(adti); + adti.setValue(TURTLEModeling.manageGateDataStructures(t, ((TADTimeInterval)tgc).getMinDelayValue()), TURTLEModeling.manageGateDataStructures(t, ((TADTimeInterval)tgc).getMaxDelayValue())); + listE.addCor(adti, tgc); + } else if (tgc instanceof TADTimeLimitedOffer) { + s = ((TADTimeLimitedOffer)tgc).getAction(); + g = t.getGateFromActionState(s); + if (g != null) { + adtlo = new ADTLO(g); + ad.addElement(adtlo); + adtlo.setLatency("0"); + s1 = t.getActionValueFromActionState(s); + //System.out.println("Adding type"); + s1 = TURTLEModeling.manageGateDataStructures(t, s1); + s1 = TURTLEModeling.addTypeToDataReceiving(t, s1); + //System.out.println("Adding type done"); + adtlo.setAction(s1); + adtlo.setDelay(TURTLEModeling.manageGateDataStructures(t, ((TADTimeLimitedOffer)tgc).getDelay())); + listE.addCor(adtlo, tgc); + ((TADTimeLimitedOffer)tgc).setStateAction(ErrorHighlight.GATE); + } else { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Time-limited offer (" + s + ", " + ((TADTimeLimitedOffer)tgc).getDelay() + "): \"" + s + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ((TADTimeLimitedOffer)tgc).setStateAction(ErrorHighlight.UNKNOWN_AS); + //System.out.println("Bad time limited offer found " + s); + } + } else if (tgc instanceof TADTimeLimitedOfferWithLatency) { + s = ((TADTimeLimitedOfferWithLatency)tgc).getAction(); + g = t.getGateFromActionState(s); + if (g != null) { + adtlo = new ADTLO(g); + ad.addElement(adtlo); + adtlo.setLatency(TURTLEModeling.manageGateDataStructures(t, ((TADTimeLimitedOfferWithLatency)tgc).getLatency())); + s1 = t.getActionValueFromActionState(s); + //System.out.println("Adding type"); + s1 = TURTLEModeling.manageGateDataStructures(t, s1); + s1 = TURTLEModeling.addTypeToDataReceiving(t, s1); + //System.out.println("Adding type done"); + adtlo.setAction(s1); + adtlo.setDelay(TURTLEModeling.manageGateDataStructures(t, ((TADTimeLimitedOfferWithLatency)tgc).getDelay())); + listE.addCor(adtlo, tgc); + ((TADTimeLimitedOfferWithLatency)tgc).setStateAction(ErrorHighlight.GATE); + } else { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Time-limited offer (" + s + ", " + ((TADTimeLimitedOfferWithLatency)tgc).getLatency() + ", " + ((TADTimeLimitedOfferWithLatency)tgc).getDelay() + "): \"" + s + "\" is not a correct expression"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + ((TADTimeLimitedOfferWithLatency)tgc).setStateAction(ErrorHighlight.UNKNOWN_AS); + //System.out.println("Bad time limited offer found " + s); + } + + // TURTLE-OS AD + } else if (tgc instanceof TOSADTimeInterval) { + adti = new ADTimeInterval(); + ad.addElement(adti); + adti.setValue(TURTLEModeling.manageGateDataStructures(t, ((TOSADTimeInterval)tgc).getMinDelayValue()), TURTLEModeling.manageGateDataStructures(t, ((TOSADTimeInterval)tgc).getMaxDelayValue())); + listE.addCor(adti, tgc); + } else if (tgc instanceof TOSADIntTimeInterval) { + adti = new ADTimeInterval(); + ad.addElement(adti); + adti.setValue(TURTLEModeling.manageGateDataStructures(t, ((TOSADIntTimeInterval)tgc).getMinDelayValue()), TURTLEModeling.manageGateDataStructures(t, ((TOSADIntTimeInterval)tgc).getMaxDelayValue())); + listE.addCor(adti, tgc); + } else if (tgc instanceof TOSADStopState) { + adst = new ADStop(); + ad.addElement(adst); + listE.addCor(adst, tgc); + } else if (tgc instanceof TOSADJunction) { + adj = new ADJunction(); + ad.addElement(adj); + listE.addCor(adj, tgc); + } else if (tgc instanceof TOSADChoice) { + adch = new ADChoice(); + ad.addElement(adch); + listE.addCor(adch, tgc); + } if (tgc instanceof TOSADActionState) { + s = ((TOSADActionState)tgc).getAction(); + s = s.trim(); + //remove ';' if last character + if (s.substring(s.length()-1, s.length()).compareTo(";") == 0) { + s = s.substring(0, s.length()-1); + } + nbActions = Conversion.nbChar(s, ';') + 1; + + if (nbActions>1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, s + " should not start with a '=='"); + ce.setTClass(t); + ce.setTGComponent(tgc); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + } else { + //s = TURTLEModeling.manageDataStructures(t, s); + g = t.getGateFromActionState(s); + p = t.getParamFromActionState(s); + + if (p != null) { + adap = new ADActionStateWithParam(p); + ad.addElement(adap); + adap.setActionValue(TURTLEModeling.manageDataStructures(t, t.getExprValueFromActionState(s))); + listE.addCor(adap, tgc); + } else { + adag = new ADActionStateWithGate(g); + ad.addElement(adag); + listE.addCor(adag, tgc); + adag.setActionValue(s); + } + } + //System.out.println("Nb Actions in state: " + nbActions); + } + } + + TGConnectingPoint p1, p2; + //TGConnectorFullArrow tgco; + TGComponent tgc1, tgc2, tgc3; + ADComponent ad1, ad2; + + // Managing Java code + iterator = list.listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof PreJavaCode) { + ad1 = listE.getADComponentByIndex(tgc, tdp.count); + if (ad1 != null) { + ad1.setPreJavaCode(tgc.getPreJavaCode()); + } + } + if (tgc instanceof PostJavaCode) { + ad1 = listE.getADComponentByIndex(tgc, tdp.count); + if (ad1 != null) { + ad1.setPostJavaCode(tgc.getPostJavaCode()); + } + } + } + + // Connecting elements + TGConnectorBetweenElementsInterface tgcbei; + iterator = list.listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof TGConnectorBetweenElementsInterface) { + tgcbei = (TGConnectorBetweenElementsInterface)tgc; + p1 = tgcbei.getTGConnectingPointP1(); + p2 = tgcbei.getTGConnectingPointP2(); + + // identification of connected components + tgc1 = null; tgc2 = null; + for(j=0; j<list.size(); j++) { + tgc3 = (TGComponent)(list.get(j)); + if (tgc3.belongsToMe(p1)) { + tgc1 = tgc3; + } + if (tgc3.belongsToMe(p2)) { + tgc2 = tgc3; + } + } + + // connecting turtle modeling components + if ((tgc1 != null) && (tgc2 != null)) { + //ADComponent ad1, ad2; + + //System.out.println("tgc1 = " + tgc1.getValue() + " tgc2= "+ tgc2.getValue()); + + ad1 = listE.getADComponentByIndex(tgc1, tdp.count); + if ((tgc2 instanceof TADArrayGetState) || (tgc2 instanceof TADArraySetState) || (tgc2 instanceof TADActionState)) { + ad2 = listB.getADComponent(tgc2); + } else { + ad2 = listE.getADComponentByIndex(tgc2, tdp.count); + } + + //System.out.println("ad1 = " + ad1 + " ad2= "+ ad2); + + if ((ad1 == null) || (ad2 == null)) { + //System.out.println("Correspondance issue"); + } + int index = 0; + if ((ad1 != null ) && (ad2 != null)) { + if ((tgc1 instanceof TADTimeLimitedOffer) || (tgc1 instanceof TADTimeLimitedOfferWithLatency)) { + index = tgc1.indexOf(p1) - 1; + ad1.addNextAtIndex(ad2, index); + } else if (tgc1 instanceof TADChoice) { + TADChoice tadch = (TADChoice)tgc1; + index = tgc1.indexOf(p1) - 1; + String myguard = TURTLEModeling.manageGateDataStructures(t, tadch.getGuard(index)); + String tmp = Conversion.replaceAllChar(myguard, '[', ""); + tmp = Conversion.replaceAllChar(tmp, ']', "").trim(); + if (tmp.compareTo("else") == 0) { + // Must calculate guard + String realGuard = ""; + int cpt = 0; + for(int k=0; k<tadch.getNbInternalTGComponent(); k++) { + if (k != index) { + if (cpt == 0) { + tmp = TURTLEModeling.manageGateDataStructures(t, tadch.getGuard(k)); + tmp = Conversion.replaceAllChar(tmp, '[', ""); + tmp = Conversion.replaceAllChar(tmp, ']', "").trim(); + if (tmp.length() > 0) { + realGuard = tmp; + cpt ++; + } + } else { + tmp = TURTLEModeling.manageGateDataStructures(t, tadch.getGuard(k)); + tmp = Conversion.replaceAllChar(tmp, '[', ""); + tmp = Conversion.replaceAllChar(tmp, ']', "").trim(); + if (tmp.length() > 0) { + realGuard = "(" + realGuard + ") and (" + tmp + ")"; + cpt ++; + } + } + } + //System.out.println("Real guard=" + realGuard + "k=" + k + " index=" + index); + } + + if (realGuard.length() == 0) { + myguard = "[ ]"; + } else { + myguard = "[not(" + realGuard + ")]"; + } + System.out.println("My guard=" + myguard); + } + ((ADChoice)ad1).addGuard(myguard); + ad1.addNext(ad2); + } else if ((tgc1 instanceof TADSequence) ||(tgc1 instanceof TADPreemption)){ + index = tgc1.indexOf(p1) - 1; + ad1.addNextAtIndex(ad2, index); + } else if (tgc1 instanceof TOSADChoice) { + TOSADChoice tadch = (TOSADChoice)tgc1; + index = tgc1.indexOf(p1) - 1; + ((ADChoice)ad1).addGuard(TURTLEModeling.manageGateDataStructures(t, tadch.getGuard(index))); + ad1.addNext(ad2); + } else { + ad1.addNextAtIndex(ad2, index); + //System.out.println("Adding connector from " + ad1 + " to " + ad2); + } + } + } + } + } + // Increasing count of this panel + tdp.count ++; + + // Remove all elements not reachable from start state + int sizeb = ad.size(); + + System.out.println("Removing non reachable elements in t:" + t.getName()); + ad.removeAllNonReferencedElts(); + + int sizea = ad.size(); + if (sizeb > sizea) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Non reachable elements have been removed in " + t.getName()); + ce.setTClass(t); + ce.setTGComponent(null); + ce.setTDiagramPanel(tdp); + addWarning(ce); + //System.out.println("Non reachable elements have been removed in " + t.getName()); + } + + //ad.replaceAllADActionStatewithMultipleParam(listE); + }*/ + + + public void createRelationsBetweenTClasses(TURTLEModeling tm, LinkedList<AvatarBDBlock> blocks, String preName) { + adp.getAvatarBDPanel().updateAllSignalsOnConnectors(); + Iterator iterator = adp.getAvatarBDPanel().getComponentList().listIterator(); + + TGComponent tgc; + AvatarBDPortConnector port; + AvatarBDBlock block1, block2; + LinkedList<String> l1, l2; + int i; + String name1, name2; + Relation r; + TClass t1, t2; + Gate g1, g2; + + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarBDPortConnector) { + port = (AvatarBDPortConnector)tgc; + block1 = port.getAvatarBDBlock1(); + block2 = port.getAvatarBDBlock2(); + + t1 = tm.getTClassWithName(preName + block1.getBlockName()); + t2 = tm.getTClassWithName(preName + block2.getBlockName()); + r = new Relation(Relation.SYN, t1, t2, true); + // Signals of l1 + l1 = port.getListOfSignalsOrigin(); + l2 = port.getListOfSignalsDestination(); + + for(i=0; i<l1.size(); i++) { + name1 = AvatarSignal.getSignalNameFromFullSignalString(l1.get(i)); + name2 = AvatarSignal.getSignalNameFromFullSignalString(l2.get(i)); + g1 = t1.getGateByName(name1); + g2 = t2.getGateByName(name2); + if ((g1 != null) && (g2 != null)) { + r.addGates(g1, g2); + } else { + TraceManager.addDev("null gates in AVATAR relation: " + name1 + " " + name2); + } + } + tm.addRelation(r); + } + } + } + + +} diff --git a/src/ui/AvatarSignal.java b/src/ui/AvatarSignal.java index c36fed3f18..66234fa72e 100644 --- a/src/ui/AvatarSignal.java +++ b/src/ui/AvatarSignal.java @@ -190,4 +190,19 @@ public class AvatarSignal extends AvatarMethod { return true; } + + public static String getSignalNameFromFullSignalString(String _signal) { + String signal = _signal.trim(); + int index0 = signal.indexOf(" "); + if (index0 != -1) { + signal = signal.substring(index0+1, signal.length()).trim(); + } + + index0 = signal.indexOf("("); + if (index0 != -1) { + signal = signal.substring(0, index0).trim(); + } + + return signal; + } } \ No newline at end of file diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java index 4bbe60b994..57e43a8b87 100755 --- a/src/ui/GTURTLEModeling.java +++ b/src/ui/GTURTLEModeling.java @@ -1543,6 +1543,46 @@ public class GTURTLEModeling { return true; } + + // BUILDING An AVATAR Design AND CHECKING IT + public boolean checkAvatarDesign(Vector blocks, AvatarDesignPanel adp, boolean overideSyntaxChecking) { + // Builds a TURTLE modeling from diagrams + //warnings = new Vector(); + //checkingErrors = null; + mgui.setMode(MainGUI.VIEW_SUGG_DESIGN_KO); + //tm = new TURTLEModeling(); + //listE = new CorrespondanceTGElement(); + mgui.reinitCountOfPanels(); + + AvatarDesignPanelTranslator adpt = new AvatarDesignPanelTranslator(adp); + tm = adpt.generateTURTLEModeling(blocks, ""); + tmState = 0; + + listE = adpt.getCorrespondanceTGElement(); + checkingErrors = adpt.getErrors(); + warnings = adpt.getWarnings(); + if ((checkingErrors != null) && (checkingErrors.size() >0)){ + return false; + } + + // Modeling is built + // Now check it ! + if (!overideSyntaxChecking) { + TURTLEModelChecker tmc = new TURTLEModelChecker(tm, listE); + + checkingErrors = tmc.syntaxAnalysisChecking(); + warnings.addAll(tmc.getWarnings()); + + if ((checkingErrors != null) && (checkingErrors.size() > 0)){ + analyzeErrors(); + return false; + } else { + return true; + } + } + + return true; + } public Vector getCheckingErrors() { return checkingErrors; diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java index 2a5ec315d9..11d47e3f5a 100755 --- a/src/ui/MainGUI.java +++ b/src/ui/MainGUI.java @@ -2565,8 +2565,48 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { } } - // NC - } else if (tp instanceof NCPanel) { + // AVATAR + } else if (tp instanceof AvatarDesignPanel) { + //Design + AvatarDesignPanel adp = (AvatarDesignPanel)tp; + JDialogModelChecking.validated = adp.validated; + JDialogModelChecking.ignored = adp.ignored; + tclassesToValidate = new Vector(); + JDialogSelectAvatarBlock jdmc = new JDialogSelectAvatarBlock(frame, tclassesToValidate, adp.getAvatarBDPanel().getFullBlockList(), "Choosing blocks to validate"); + if (!automatic) { + GraphicLib.centerOnParent(jdmc); + jdmc.setVisible(true); // blocked until dialog has been closed + } else { + jdmc.closeDialog(); + } + boolean optimize = jdmc.getOptimize(); + if (tclassesToValidate.size() > 0) { + adp.validated = JDialogModelChecking.validated; + adp.ignored = JDialogModelChecking.ignored; + b = gtm.checkAvatarDesign(tclassesToValidate, adp, optimize); + if (b) { + ret = true; + setMode(MainGUI.MODEL_OK); + setMode(MainGUI.GEN_DESIGN_OK); + if (!automatic) { + JOptionPane.showMessageDialog(frame, + "0 error, " + getCheckingWarnings().size() + " warning(s). You can now generate a corresponding formal (UPPAAL) specification", + "Syntax analysis successful on avatar design diagrams", + JOptionPane.INFORMATION_MESSAGE); + } + } else { + if (!automatic) { + JOptionPane.showMessageDialog(frame, + "The Avatar modeling contains several errors", + "Syntax analysis failed", + JOptionPane.INFORMATION_MESSAGE); + } + } + } + + + // NC + } else if (tp instanceof NCPanel) { NCPanel ncp = (NCPanel) tp; b = gtm.translateNC(ncp); if (b) { @@ -2869,7 +2909,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { public boolean generateRTLOTOS(boolean automatic) { - if (gtm.getTURTLEModelingState() == 1) { + if (gtm.getTURTLEModelingState() > 0) { if (!generateTURTLEModelingFromState(gtm.getTURTLEModelingState(), automatic, RT_LOTOS)) { return false; } @@ -2900,11 +2940,12 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { if (gtm.getTURTLEModelingState() > 0) { if (!generateTURTLEModelingFromState(gtm.getTURTLEModelingState(), automatic, LOTOS)) { dtree.toBeUpdated(); + TraceManager.addDev("Generate from state failed"); return false; } - if (!automatic) { + /*if (!automatic && (gtm.getTURTLEModelingState() == 1)) { return true; - } + }*/ } //System.out.println("generate LOTOS"); @@ -2931,6 +2972,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { return generateTIFFromMapping(automatic, generator); } if (state == 2) { + TraceManager.addDev("Generating from state 2"); return generateTIFFromTMLModeling(automatic, generator); } return false; @@ -3029,7 +3071,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { public void generateUPPAAL() { //System.out.println("Generate UPPAAL!"); //gtm.mergeChoices(true); - if (gtm.getTURTLEModelingState() == 1) { + if (gtm.getTURTLEModelingState() > 0) { if (!generateTURTLEModelingFromState(gtm.getTURTLEModelingState(), false, UPPAAL)) { return; } diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java index f6402dc494..4b5186a76c 100644 --- a/src/ui/avatarbd/AvatarBDBlock.java +++ b/src/ui/avatarbd/AvatarBDBlock.java @@ -55,6 +55,7 @@ import org.w3c.dom.*; import myutil.*; import ui.*; import ui.window.*; +import ui.avatarsmd.*; public class AvatarBDBlock extends TGCScalableWithInternalComponent implements SwallowTGComponent, SwallowedTGComponent { @@ -841,6 +842,10 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S return null; } + public AvatarSMDPanel getAvatarSMDPanel() { + return ((AvatarDesignPanel)(tdp.tp)).getAvatarSMDPanel(getBlockName()); + } + } diff --git a/src/ui/avatarbd/AvatarBDPortConnector.java b/src/ui/avatarbd/AvatarBDPortConnector.java index d21f6a566f..d70be0b0f4 100644 --- a/src/ui/avatarbd/AvatarBDPortConnector.java +++ b/src/ui/avatarbd/AvatarBDPortConnector.java @@ -352,14 +352,14 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom oldScaleFactor = scaleFactor; } - public LinkedList getListOfSignalsOrigin() { + public LinkedList<String> getListOfSignalsOrigin() { LinkedList<String> list = new LinkedList<String>(); list.addAll(inSignalsAtOrigin); list.addAll(outSignalsAtOrigin); return list; } - public LinkedList getListOfSignalsDestination() { + public LinkedList<String> getListOfSignalsDestination() { LinkedList<String> list = new LinkedList<String>(); list.addAll(inSignalsAtDestination); list.addAll(outSignalsAtDestination); diff --git a/src/ui/avatarsmd/AvatarSMDState.java b/src/ui/avatarsmd/AvatarSMDState.java index 905baa1b92..35cde49339 100644 --- a/src/ui/avatarsmd/AvatarSMDState.java +++ b/src/ui/avatarsmd/AvatarSMDState.java @@ -412,5 +412,28 @@ public class AvatarSMDState extends TGCScalableWithInternalComponent implements return TGComponentManager.AVATARSMD_CONNECTOR; } + public AvatarSMDState checkForStartStateOfCompositeStates() { + AvatarSMDState tgc; + LinkedList<AvatarSMDState> list = getFullStateList(); + for(AvatarSMDState s: list) { + tgc = s.checkForStartStateOfCompositeStates(); + if (tgc != null) { + return tgc; + } + } + + int cpt = 0; + for(int i=0; i<nbInternalTGComponent; i++) { + if (tgcomponent[i] instanceof AvatarSMDStartState) { + cpt ++; + } + } + + if (cpt > 1) { + return this; + } + return null; + } + } diff --git a/src/ui/window/JDialogModelChecking.java b/src/ui/window/JDialogModelChecking.java index 6c4b5e0b88..48a3a67b9e 100755 --- a/src/ui/window/JDialogModelChecking.java +++ b/src/ui/window/JDialogModelChecking.java @@ -151,7 +151,7 @@ public class JDialogModelChecking extends javax.swing.JDialog implements ActionL // ignored list panel1 = new JPanel(); panel1.setLayout(new BorderLayout()); - panel1.setBorder(new javax.swing.border.TitledBorder("TClasses ignored")); + panel1.setBorder(new javax.swing.border.TitledBorder("Ignored")); listIgnored = new JList(ign); //listIgnored.setPreferredSize(new Dimension(200, 250)); listIgnored.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION ); @@ -164,7 +164,7 @@ public class JDialogModelChecking extends javax.swing.JDialog implements ActionL // validated list panel2 = new JPanel(); panel2.setLayout(new BorderLayout()); - panel2.setBorder(new javax.swing.border.TitledBorder("TClasses taken into account")); + panel2.setBorder(new javax.swing.border.TitledBorder("Taken into account")); listValidated = new JList(val); //listValidated.setPreferredSize(new Dimension(200, 250)); listValidated.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION ); diff --git a/src/ui/window/JDialogSelectAvatarBlock.java b/src/ui/window/JDialogSelectAvatarBlock.java new file mode 100755 index 0000000000..5464e1af25 --- /dev/null +++ b/src/ui/window/JDialogSelectAvatarBlock.java @@ -0,0 +1,372 @@ +/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille + +ludovic.apvrille AT enst.fr + +This software is a computer program whose purpose is to allow the +edition of TURTLE analysis, design and deployment diagrams, to +allow the generation of RT-LOTOS or Java code from this diagram, +and at last to allow the analysis of formal validation traces +obtained from external tools, e.g. RTL from LAAS-CNRS and CADP +from INRIA Rhone-Alpes. + +This software is governed by the CeCILL license under French law and +abiding by the rules of distribution of free software. You can use, +modify and/ or redistribute the software under the terms of the CeCILL +license as circulated by CEA, CNRS and INRIA at the following URL +"http://www.cecill.info". + +As a counterpart to the access to the source code and rights to copy, +modify and redistribute granted by the license, users are provided only +with a limited warranty and the software's author, the holder of the +economic rights, and the successive licensors have only limited +liability. + +In this respect, the user's attention is drawn to the risks associated +with loading, using, modifying and/or developing or reproducing the +software by the user in light of its specific status of free software, +that may mean that it is complicated to manipulate, and that also +therefore means that it is reserved for developers and experienced +professionals having in-depth computer knowledge. Users are therefore +encouraged to load and test the software's suitability as regards their +requirements in conditions enabling the security of their systems and/or +data to be ensured and, more generally, to use and operate it in the +same conditions as regards security. + +The fact that you are presently reading this means that you have had +knowledge of the CeCILL license and that you accept its terms. + +/** + * Class JDialogSelectAvatarBlock + * Dialog for managing blocks to be validated + * Creation: 18/05/2010 + * @version 1.0 18/05/2010 + * @author Ludovic APVRILLE + * @see + */ + +package ui.window; + +import java.awt.*; +import java.awt.event.*; +import javax.swing.*; +import javax.swing.event.*; +import java.util.*; + +import ui.*; +import ui.avatarbd.*; + + +public class JDialogSelectAvatarBlock extends javax.swing.JDialog implements ActionListener, ListSelectionListener { + public static Vector validated, ignored; + private static boolean optimized = true; + + private Vector val, ign, back; + + //subpanels + private JPanel panel1, panel2, panel3, panel4, panel5, panel6; + private JList listIgnored; + private JList listValidated; + private JButton allValidated; + private JButton addOneValidated; + private JButton addOneIgnored; + private JButton allIgnored; + protected JCheckBox optimize; + + // Main Panel + private JButton closeButton; + private JButton cancelButton; + + /** Creates new form */ + public JDialogSelectAvatarBlock(Frame f, Vector _back, LinkedList componentList, String title) { + super(f, title, true); + + back = _back; + + if ((validated == null) || (ignored == null)) { + val = makeNewVal(componentList); + ign = new Vector(); + } else { + val = validated; + ign = ignored; + checkTask(val, componentList); + checkTask(ign, componentList); + addNewTask(val, componentList, ign); + } + + initComponents(); + myInitComponents(); + pack(); + } + + private Vector makeNewVal(LinkedList list) { + Vector v = new Vector(); + TGComponent tgc; + + for(int i=0; i<list.size(); i++) { + tgc = (TGComponent)(list.get(i)); + //System.out.println(tgc); + if (tgc instanceof AvatarBDBlock) { + v.addElement(tgc); + } + } + return v; + } + + private void checkTask(Vector tobeChecked, LinkedList source) { + AvatarBDBlock t; + + for(int i=0; i<tobeChecked.size(); i++) { + t = (AvatarBDBlock)(tobeChecked.elementAt(i)); + if (!source.contains(t)) { + tobeChecked.removeElementAt(i); + i--; + } + } + } + + public void addNewTask(Vector added, LinkedList source, Vector notSource) { + TGComponent tgc; + + for(int i=0; i<source.size(); i++) { + tgc = (TGComponent)(source.get(i)); + if ((tgc instanceof AvatarBDBlock) && (!added.contains(tgc)) && (!notSource.contains(tgc))){ + added.addElement(tgc); + //System.out.println("New element"); + } + } + } + + private void myInitComponents() { + setButtons(); + } + + private void initComponents() { + Container c = getContentPane(); + GridBagLayout gridbag1 = new GridBagLayout(); + GridBagConstraints c1 = new GridBagConstraints(); + setFont(new Font("Helvetica", Font.PLAIN, 14)); + c.setLayout(new BorderLayout()); + setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE); + + // ignored list + panel1 = new JPanel(); + panel1.setLayout(new BorderLayout()); + panel1.setBorder(new javax.swing.border.TitledBorder("Blocks ignored")); + listIgnored = new JList(ign); + //listIgnored.setPreferredSize(new Dimension(200, 250)); + listIgnored.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION ); + listIgnored.addListSelectionListener(this); + JScrollPane scrollPane1 = new JScrollPane(listIgnored); + panel1.add(scrollPane1, BorderLayout.CENTER); + panel1.setPreferredSize(new Dimension(200, 250)); + c.add(panel1, BorderLayout.WEST); + + // validated list + panel2 = new JPanel(); + panel2.setLayout(new BorderLayout()); + panel2.setBorder(new javax.swing.border.TitledBorder("Blocks taken into account")); + listValidated = new JList(val); + //listValidated.setPreferredSize(new Dimension(200, 250)); + listValidated.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION ); + listValidated.addListSelectionListener(this); + JScrollPane scrollPane2 = new JScrollPane(listValidated); + panel2.add(scrollPane2, BorderLayout.CENTER); + panel2.setPreferredSize(new Dimension(200, 250)); + c.add(panel2, BorderLayout.EAST); + + // central buttons + panel3 = new JPanel(); + panel3.setLayout(gridbag1); + + c1.weighty = 1.0; + c1.weightx = 1.0; + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + c1.fill = GridBagConstraints.HORIZONTAL; + c1.gridheight = 1; + + allValidated = new JButton(IconManager.imgic50); + allValidated.setPreferredSize(new Dimension(50, 25)); + allValidated.addActionListener(this); + allValidated.setActionCommand("allValidated"); + panel3.add(allValidated, c1); + + addOneValidated = new JButton(IconManager.imgic48); + addOneValidated.setPreferredSize(new Dimension(50, 25)); + addOneValidated.addActionListener(this); + addOneValidated.setActionCommand("addOneValidated"); + panel3.add(addOneValidated, c1); + + panel3.add(new JLabel(" "), c1); + + addOneIgnored = new JButton(IconManager.imgic46); + addOneIgnored.addActionListener(this); + addOneIgnored.setPreferredSize(new Dimension(50, 25)); + addOneIgnored.setActionCommand("addOneIgnored"); + panel3.add(addOneIgnored, c1); + + allIgnored = new JButton(IconManager.imgic44); + allIgnored.addActionListener(this); + allIgnored.setPreferredSize(new Dimension(50, 25)); + allIgnored.setActionCommand("allIgnored"); + panel3.add(allIgnored, c1); + + c.add(panel3, BorderLayout.CENTER); + + // main panel; + panel6 = new JPanel(); + panel6.setLayout(new BorderLayout()); + + panel5 = new JPanel(); + panel5.setLayout(new FlowLayout()); + + optimize = new JCheckBox("Optimize specification"); + optimize.setSelected(optimized); + panel5.add(optimize); + + panel4 = new JPanel(); + panel4.setLayout(new FlowLayout()); + + closeButton = new JButton("Start Syntax Analysis", IconManager.imgic37); + //closeButton.setPreferredSize(new Dimension(600, 50)); + closeButton.addActionListener(this); + closeButton.setPreferredSize(new Dimension(200, 30)); + + cancelButton = new JButton("Cancel", IconManager.imgic27); + cancelButton.addActionListener(this); + cancelButton.setPreferredSize(new Dimension(200, 30)); + panel4.add(cancelButton); + panel4.add(closeButton); + + panel6.add(panel5, BorderLayout.NORTH); + panel6.add(panel4, BorderLayout.SOUTH); + + c.add(panel6, BorderLayout.SOUTH); + + } + + public void actionPerformed(ActionEvent evt) { + String command = evt.getActionCommand(); + + // Compare the action command to the known actions. + if (command.equals("Start Syntax Analysis")) { + closeDialog(); + } else if (command.equals("Cancel")) { + cancelDialog(); + } else if (command.equals("addOneIgnored")) { + addOneIgnored(); + } else if (command.equals("addOneValidated")) { + addOneValidated(); + } else if (command.equals("allValidated")) { + allValidated(); + } else if (command.equals("allIgnored")) { + allIgnored(); + } + } + + + private void addOneIgnored() { + int [] list = listValidated.getSelectedIndices(); + Vector v = new Vector(); + Object o; + for (int i=0; i<list.length; i++){ + o = val.elementAt(list[i]); + ign.addElement(o); + v.addElement(o); + } + + val.removeAll(v); + listIgnored.setListData(ign); + listValidated.setListData(val); + setButtons(); + } + + private void addOneValidated() { + int [] list = listIgnored.getSelectedIndices(); + Vector v = new Vector(); + Object o; + for (int i=0; i<list.length; i++){ + o = ign.elementAt(list[i]); + val.addElement(o); + v.addElement(o); + } + + ign.removeAll(v); + listIgnored.setListData(ign); + listValidated.setListData(val); + setButtons(); + } + + private void allValidated() { + val.addAll(ign); + ign.removeAllElements(); + listIgnored.setListData(ign); + listValidated.setListData(val); + setButtons(); + } + + private void allIgnored() { + ign.addAll(val); + val.removeAllElements(); + listIgnored.setListData(ign); + listValidated.setListData(val); + setButtons(); + } + + + public void closeDialog() { + back.removeAllElements(); + for(int i=0; i<val.size(); i++) { + back.addElement(val.elementAt(i)); + } + validated = val; + ignored = ign; + optimized = optimize.isSelected(); + dispose(); + } + + public void cancelDialog() { + dispose(); + } + + private void setButtons() { + int i1 = listIgnored.getSelectedIndex(); + int i2 = listValidated.getSelectedIndex(); + + if (i1 == -1) { + addOneValidated.setEnabled(false); + } else { + addOneValidated.setEnabled(true); + //listValidated.clearSelection(); + } + + if (i2 == -1) { + addOneIgnored.setEnabled(false); + } else { + addOneIgnored.setEnabled(true); + //listIgnored.clearSelection(); + } + + if (ign.size() ==0) { + allValidated.setEnabled(false); + } else { + allValidated.setEnabled(true); + } + + if (val.size() ==0) { + allIgnored.setEnabled(false); + closeButton.setEnabled(false); + } else { + allIgnored.setEnabled(true); + closeButton.setEnabled(true); + } + } + + + public void valueChanged(ListSelectionEvent e) { + setButtons(); + } + + public boolean getOptimize() { + return optimized; + } +} \ No newline at end of file -- GitLab