diff --git a/src/main/java/automata/State.java b/src/main/java/automata/State.java index 5e72f9b54fff137c0805f93d6ee1125d99a0b08f..56d6b19a5aaaf3703ee6d9ac3258ebbc9df5c861 100755 --- a/src/main/java/automata/State.java +++ b/src/main/java/automata/State.java @@ -54,6 +54,7 @@ import java.util.ListIterator; public class State { private String name; private LinkedList<Transition> transitions; + public Object referenceObject; public State(String _name) { transitions = new LinkedList<Transition>(); diff --git a/src/main/java/tmltranslator/HwLink.java b/src/main/java/tmltranslator/HwLink.java index 3664381f64cde843a5ae15c7c7333605f3d5d5e2..ca2c23259ccbc0c3b1f02088c2e77604e1cea2d6 100755 --- a/src/main/java/tmltranslator/HwLink.java +++ b/src/main/java/tmltranslator/HwLink.java @@ -84,6 +84,4 @@ public class HwLink implements Comparable<HwLink> { return s; } - - } diff --git a/src/main/java/tmltranslator/TMLMapping.java b/src/main/java/tmltranslator/TMLMapping.java index 52bd2927ff596077f904e083ec58daf48edbe497..1476572ee5041a3bc92d5c96d25537af5e8424a8 100755 --- a/src/main/java/tmltranslator/TMLMapping.java +++ b/src/main/java/tmltranslator/TMLMapping.java @@ -48,6 +48,7 @@ import tmltranslator.toproverif.TML2ProVerif; import ui.TMLArchiPanel; import ui.TMLComponentDesignPanel; import ui.CorrespondanceTGElement; +import automata.*; import java.util.*; @@ -88,6 +89,12 @@ public class TMLMapping<E> { private int hashCode; private boolean hashCodeComputed = false; + // Automata to verify the mapping of channels + // and make minimal hardware + private Automata aut; + private HashMap<HwNode, State> nodesToStates; + + // REFERENCES TO BE REMOVED!!!! :( @@ -1615,4 +1622,31 @@ public class TMLMapping<E> { //s = myutil.Conversion.transformToXMLString(s); return s; } + + + public void makeAutomata() { + aut = new Automata(); + nodesToStates = new HashMap<HwNode, State>(); + + // Make a state for each hardware node + for(HwNode node: tmla.getHwNodes()) { + State st = new State(node.getName()); + st.referenceObject = node; + nodesToStates.put(node, st); + } + + // Making links + for(HwLink link: tmla.getHwLinks()) { + HwNode node1 = link.bus; + HwNode node2 = link.hwnode; + + State st1 = nodesToStates.get(node1); + State st2 = nodesToStates.get(node2); + + if ((st1 != null) && (st2 != null)) { + Transition t = new Transition(link.getName(), st2); + st1.addTransition(t); + } + } + } }