diff --git a/src/avatartranslator/AvatarPragma.java b/src/avatartranslator/AvatarPragma.java
index be732314af2c8acebdf1146d46b379a4f7357eb7..ac540dab36fbeef8bb5260efb84c309be6dd0cf0 100644
--- a/src/avatartranslator/AvatarPragma.java
+++ b/src/avatartranslator/AvatarPragma.java
@@ -51,16 +51,26 @@ import myutil.*;
import ui.*;
public abstract class AvatarPragma extends AvatarElement {
- private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public"};
- private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public"};
+ private final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "Constant"};
+ private final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "Constant"};
private LinkedList<AvatarAttribute> arguments;
+
+ private int proofStatus = 0;
+
+
public AvatarPragma(String _name, Object _referenceObject) {
super(_name, _referenceObject);
}
public LinkedList<AvatarAttribute> getArgs(){
return arguments;
}
+ public int getProofStatus(){
+ return proofStatus;
+ }
+ public void setProofStatus(int status){
+ proofStatus = status;
+ }
public static AvatarPragma createFromString(String str, Object obj, LinkedList<AvatarBlock> blocks){
//createFromString takes in a pragma string (with # removed), the containing object, and the list of AvatarBlocks, and returns the corresponding AvatarPragma or null if an error occurred
//The attributes referenced must exist
diff --git a/src/avatartranslator/AvatarPragmaSecret.java b/src/avatartranslator/AvatarPragmaSecret.java
index f060b0abd36e6d03a32582b66ed5d575becb767e..5a8b831f2da285e4e3e19b366decc5b5b1f8e066 100644
--- a/src/avatartranslator/AvatarPragmaSecret.java
+++ b/src/avatartranslator/AvatarPragmaSecret.java
@@ -39,7 +39,7 @@
* Class AvatarPragma
* Creation: 20/05/2010
* @version 1.1 01/07/2014
- * @author Ludovic APVRILLE, Raja GATGOUT
+ * @author Ludovic APVRILLE, Letitia LI
* @see
*/
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index f4c39f7c3258b3e115a5d6fd000fee486617c18a..f4abd6e2f483b2afdfff2441f02f4c2005809414 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -313,7 +313,13 @@ public class AvatarDesignPanel extends TURTLEPanel {
for(AvatarBDBlock block1: abdp.getFullBlockList()) {
block1.resetConfidentialityOfAttributes();
}
-
+ for (Object tgc: abdp.getComponentList()){
+ if (tgc instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) tgc;
+ pragma.authMap.clear();
+
+ }
+ }
// Reset reachable states
for(int i=0; i<panels.size(); i++) {
tdp = (TDiagramPanel)(panels.get(i));
@@ -348,6 +354,12 @@ public class AvatarDesignPanel extends TURTLEPanel {
if (index != -1) {
attr = attr.substring(0, index);
}
+ else {
+ index = attr.indexOf("_");
+ if (index != -1){
+ attr = attr.substring(0, index);
+ }
+ }
//TraceManager.addDev("Analyzing block=" + block + " attr=" + attr);
a = abdp.getAttributeByBlockName(block, attr);
if (a != null) {
@@ -366,6 +378,12 @@ public class AvatarDesignPanel extends TURTLEPanel {
if (index != -1) {
attr = attr.substring(0, index);
}
+ else {
+ index = attr.indexOf("_");
+ if (index != -1){
+ attr = attr.substring(0, index);
+ }
+ }
//TraceManager.addDev("Analyzing block=" + block + " attr=" + attr);
a = abdp.getAttributeByBlockName(block, attr);
if (a != null) {
@@ -428,6 +446,89 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
}
+ //Map Authenticity results to Pragma
+ for (String s: pvoa.getNotProved()){
+ if (s.contains("authenticity")){
+ String[] split = s.split(" ==> ");
+ String[] argA = split[0].split("authenticity__")[1].split("\\(")[0].split("__");
+ String[] argB = split[1].split("authenticity__")[1].split("\\(")[0].split("__");
+ String fstr1 = argA[0]+"."+argA[3]+"."+argA[1];
+ String fstr2 = argB[0]+"."+argB[3]+"."+argB[1];
+ //Find the authenticity pragma
+ for (Object ob: abdp.getComponentList()){
+ if (ob instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) ob;
+ for (String prop: pragma.getProperties()){
+ if (prop.contains("#Authenticity") && prop.contains(fstr1) && prop.contains(fstr2)){
+ pragma.authMap.put(prop, 4);
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ for (String s: pvoa.getSatisfiedAuthenticity()){
+ String[] split = s.split(" ==> ");
+ String[] argA = split[0].split("__");
+ String[] argB = split[1].split("__");
+ String fstr1 = argA[0]+"."+argA[3]+"."+argA[1];
+ String fstr2 = argB[0]+"."+argB[3]+"."+argB[1];
+ System.out.println(fstr1 + " "+ fstr2);
+ //Find the authenticity pragma
+ for (Object ob: abdp.getComponentList()){
+ if (ob instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) ob;
+ for (String prop: pragma.getProperties()){
+ if (prop.contains("#Authenticity") && prop.contains(fstr1) && prop.contains(fstr2)){
+ pragma.authMap.put(prop, 1);
+ }
+ }
+ }
+ }
+
+ }
+ for (String s: pvoa.getSatisfiedWeakAuthenticity()){
+ String[] split = s.split(" ==> ");
+ String[] argA = split[0].split("__");
+ String[] argB = split[1].split("__");
+ String fstr1 = argA[0]+"."+argA[3]+"."+argA[1];
+ String fstr2 = argB[0]+"."+argB[3]+"."+argB[1];
+ //Find the authenticity pragma
+ for (Object ob: abdp.getComponentList()){
+ if (ob instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) ob;
+ for (String prop: pragma.getProperties()){
+ if (prop.contains("#Authenticity") && prop.contains(fstr1) && prop.contains(fstr2)){
+ pragma.authMap.put(prop, 2);
+ }
+ }
+ }
+ }
+
+ }
+ for (String s: pvoa.getNonSatisfiedAuthenticity()){
+ String[] split = s.split(" ==> ");
+ String[] argA = split[0].split("__");
+ String[] argB = split[1].split("__");
+ String fstr1 = argA[0]+"."+argA[3]+"."+argA[1];
+ String fstr2 = argB[0]+"."+argB[3]+"."+argB[1];
+ //Find the authenticity pragma
+ for (Object ob: abdp.getComponentList()){
+ if (ob instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) ob;
+ for (String prop: pragma.getProperties()){
+ if (prop.contains("#Authenticity") && prop.contains(fstr1) && prop.contains(fstr2)){
+ pragma.authMap.put(prop, 3);
+ }
+ }
+ }
+ }
+
+ }
+
+
}
public ArrayList<String> getAllNonMappedAvatarBlockNames(String _name, ADDDiagramPanel _tadp, boolean ref, String name) {
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 8f56bd6b31054c7081f41d1e7b90e440869add63..a1d79e5782f3134a527034eba8784219161b22a3 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -120,14 +120,14 @@ public class AvatarDesignPanelTranslator {
public void createPragmas(AvatarSpecification _as, LinkedList<AvatarBDBlock> _blocks) {
Iterator iterator = adp.getAvatarBDPanel().getComponentList().listIterator();
TGComponent tgc;
- Pragma tgcn;
+ AvatarBDPragma tgcn;
String values [];
String tmp;
AvatarPragma tmpPragma;
while(iterator.hasNext()) {
tgc = (TGComponent)(iterator.next());
- if (tgc instanceof Pragma) {
- tgcn = (Pragma)tgc;
+ if (tgc instanceof AvatarBDPragma) {
+ tgcn = (AvatarBDPragma)tgc;
values = tgcn.getValues();
for(int i=0; i<values.length; i++) {
tmp = values[i].trim();
diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java
index c780bbd3518ce42e80fc27265dce2c37545289cc..0fb19fa859d5b183b620f79b23416eb131fa83b7 100755
--- a/src/ui/TGComponentManager.java
+++ b/src/ui/TGComponentManager.java
@@ -728,7 +728,7 @@ public class TGComponentManager {
tgc = new TGCNote(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
case PRAGMA:
- tgc = new Pragma(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+ tgc = new AvatarBDPragma(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
case IOD_CHOICE:
tgc = new IODChoice(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
diff --git a/src/ui/window/JDialogPragma.java b/src/ui/window/JDialogPragma.java
new file mode 100755
index 0000000000000000000000000000000000000000..8bb53ac74bbb570b72dbbac7c9473dbc9291d561
--- /dev/null
+++ b/src/ui/window/JDialogPragma.java
@@ -0,0 +1,319 @@
+/**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 JDialogPragma
+ * Dialog for entering a note
+ * Creation: 06/12/2003
+ * @version 1.0 06/12/2003
+ * @author Ludovic APVRILLE, Letitia LI
+ * @see
+ */
+
+package ui.window;
+
+import java.awt.*;
+import java.awt.event.*;
+import javax.swing.*;
+import javax.swing.text.*;
+import ui.*;
+import java.util.*;
+
+public class JDialogPragma extends javax.swing.JDialog implements ActionListener {
+
+ protected String text;
+
+
+ //components
+ protected JTextArea textarea;
+ protected JButton close;
+ protected JButton cancel;
+
+ /** Creates new form */
+ public JDialogPragma(Frame f, String title, String _text) {
+ super(f, title, true);
+ text = _text;
+
+ initComponents();
+ pack();
+ }
+//Suggestion Panel code from: http://stackoverflow.com/questions/10873748/how-to-show-autocomplete-as-i-type-in-jtextarea
+
+ public class SuggestionPanel {
+ private final String[] pragma = {"#Constant", "#InitialSystemKnowledge", "#InitialSessionKnowledge", "#PrivatePublicKeys", "#Public", "#Confidentiality", "#Secret", "#SecrecyAssumption", "#Authenticity"};
+ private JList list;
+ private JPopupMenu popupMenu;
+ private String subWord;
+ private final int insertionPosition;
+
+ public SuggestionPanel(JTextArea textarea, int position, String subWord, Point location) {
+ this.insertionPosition = position;
+ this.subWord = subWord;
+ popupMenu = new JPopupMenu();
+ popupMenu.removeAll();
+ popupMenu.setOpaque(false);
+ popupMenu.setBorder(null);
+ popupMenu.add(list = createSuggestionList(position, subWord), BorderLayout.CENTER);
+ popupMenu.show(textarea, location.x, textarea.getBaseline(0, 0) + location.y);
+ }
+
+ public void hide() {
+ popupMenu.setVisible(false);
+ if (suggestion == this) {
+ suggestion = null;
+ }
+ }
+
+ private JList createSuggestionList(final int position, final String subWord) {
+ ArrayList<String> matches = new ArrayList<String>();
+ if (subWord.startsWith("#")){
+ for (String p: pragma) {
+ if (p.startsWith(subWord)){
+ matches.add(p);
+ }
+ }
+ }
+ Object[] data = new Object[matches.size()];
+ data = matches.toArray(data);
+ JList list = new JList(data);
+ list.setBorder(BorderFactory.createLineBorder(Color.DARK_GRAY, 1));
+ list.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+ list.setSelectedIndex(0);
+ list.addMouseListener(new MouseAdapter() {
+ @Override
+ public void mouseClicked(MouseEvent e) {
+ if (e.getClickCount() == 2) {
+ insertSelection();
+ }
+ }
+ });
+
+ return list;
+ }
+
+
+ public boolean insertSelection() {
+ if (list.getSelectedValue() != null) {
+ try {
+ final String selectedSuggestion = ((String) list.getSelectedValue()).substring(subWord.length());
+ textarea.getDocument().insertString(insertionPosition, selectedSuggestion, null);
+ return true;
+ } catch (BadLocationException e1) {
+ e1.printStackTrace();
+ }
+ hideSuggestion();
+ }
+ return false;
+ }
+
+ public void moveUp() {
+ int index = Math.min(list.getSelectedIndex() - 1, 0);
+ selectIndex(index);
+ }
+
+ public void moveDown() {
+ int index = Math.min(list.getSelectedIndex() + 1, list.getModel().getSize() - 1);
+ selectIndex(index);
+ }
+
+ private void selectIndex(int index) {
+ final int position = textarea.getCaretPosition();
+ list.setSelectedIndex(index);
+ SwingUtilities.invokeLater(new Runnable() {
+ @Override
+ public void run() {
+ textarea.setCaretPosition(position);
+ };
+ });
+ }
+ }
+ private SuggestionPanel suggestion;
+ protected void showSuggestionLater() {
+ SwingUtilities.invokeLater(new Runnable() {
+ @Override
+ public void run() {
+ showSuggestion();
+ }
+
+ });
+ }
+
+ protected void showSuggestion() {
+ hideSuggestion();
+ final int position = textarea.getCaretPosition();
+ Point location;
+ try {
+ location = textarea.modelToView(position).getLocation();
+ } catch (BadLocationException e2) {
+ e2.printStackTrace();
+ return;
+ }
+ String text = textarea.getText();
+ int start = Math.max(0, position - 1);
+ while (start > 0) {
+ if (!Character.isWhitespace(text.charAt(start))) {
+ start--;
+ } else {
+ start++;
+ break;
+ }
+ }
+ if (start > position) {
+ return;
+ }
+ final String subWord = text.substring(start, position);
+ if (subWord.length() < 2) {
+ return;
+ }
+ suggestion = new SuggestionPanel(textarea, position, subWord, location);
+ SwingUtilities.invokeLater(new Runnable() {
+ @Override
+ public void run() {
+ textarea.requestFocusInWindow();
+ }
+ });
+ }
+
+ private void hideSuggestion() {
+ if (suggestion != null) {
+ suggestion.hide();
+ }
+ }
+
+ protected void initComponents() {
+
+ Container c = getContentPane();
+ Font f = new Font("Helvetica", Font.PLAIN, 14);
+ setFont(f);
+ c.setLayout(new BorderLayout());
+ //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
+
+ textarea = new JTextArea();
+ textarea.setEditable(true);
+ textarea.setMargin(new Insets(10, 10, 10, 10));
+ textarea.setTabSize(3);
+ textarea.append(text);
+ textarea.setFont(new Font("times", Font.PLAIN, 12));
+ textarea.addKeyListener(new KeyListener() {
+
+ @Override
+ public void keyTyped(KeyEvent e) {
+ if (e.getKeyChar() == KeyEvent.VK_ENTER || e.getKeyChar() == KeyEvent.VK_TAB) {
+ if (suggestion != null) {
+ if (suggestion.insertSelection()) {
+ e.consume();
+ final int position = textarea.getCaretPosition();
+ SwingUtilities.invokeLater(new Runnable() {
+ @Override
+ public void run() {
+ try {
+ textarea.getDocument().remove(position - 1, 1);
+ } catch (BadLocationException e) {
+ e.printStackTrace();
+ }
+ }
+ });
+ }
+ }
+ }
+ }
+
+ @Override
+ public void keyReleased(KeyEvent e) {
+ if (e.getKeyCode() == KeyEvent.VK_DOWN && suggestion != null) {
+ suggestion.moveDown();
+ } else if (e.getKeyCode() == KeyEvent.VK_UP && suggestion != null) {
+ suggestion.moveUp();
+ } else if (Character.isLetterOrDigit(e.getKeyChar())) {
+ showSuggestionLater();
+ } else if (Character.isWhitespace(e.getKeyChar())) {
+ hideSuggestion();
+ }
+ }
+
+ @Override
+ public void keyPressed(KeyEvent e) {
+
+ }
+ });
+
+ JScrollPane jsp = new JScrollPane(textarea, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jsp.setPreferredSize(new Dimension(300, 300));
+ c.add(jsp, BorderLayout.CENTER);
+
+ close = new JButton("Ok", IconManager.imgic25);
+ cancel = new JButton("Cancel", IconManager.imgic27);
+
+ close.setPreferredSize(new Dimension(150, 30));
+ cancel.setPreferredSize(new Dimension(150, 30));
+
+ close.addActionListener(this);
+ cancel.addActionListener(this);
+
+ JPanel jp = new JPanel();
+ jp.add(close);
+ jp.add(cancel);
+
+ c.add(jp, BorderLayout.SOUTH);
+ }
+
+ public void actionPerformed(ActionEvent evt) {
+ String command = evt.getActionCommand();
+
+ // Compare the action command to the known actions.
+ if (command.equals("Cancel")) {
+ cancel();
+ } else if (command.equals("Ok")) {
+ close();
+ }
+ }
+
+ public void cancel() {
+ dispose();
+ }
+
+ public void close() {
+ text = textarea.getText();
+ dispose();
+ }
+
+ public String getText() {
+ return text;
+ }
+
+
+}