diff --git a/modeling/AVATAR/CoffeeMachine_Avatar.xml b/modeling/AVATAR/CoffeeMachine_Avatar.xml
index 51ca9525ae2b0f2756ff9b5eac0e3cc11b43ee8e..f53a42fdc1e481bab2a7c6e89f2f0b7aa2bd2d42 100644
--- a/modeling/AVATAR/CoffeeMachine_Avatar.xml
+++ b/modeling/AVATAR/CoffeeMachine_Avatar.xml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
-<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="false" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="1" LAST_SELECTED_SUB_TAB="3">
+<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="false" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="1" LAST_SELECTED_SUB_TAB="0">
<Modeling type="Avatar Requirement" nameTab="AVATAR Requirements" >
<AvatarRDPanel name="AVATAR RD" minX="10" maxX="1900" minY="10" maxY="1400" zoom="1.0" >
diff --git a/src/main/java/avatartranslator/AvatarDependencyGraph.java b/src/main/java/avatartranslator/AvatarDependencyGraph.java
index ec5343dd640b2deebc4bb67a13ee7aac313b8794..7bbab65b2872a975fecdc680b386cb8a9b42c77b 100644
--- a/src/main/java/avatartranslator/AvatarDependencyGraph.java
+++ b/src/main/java/avatartranslator/AvatarDependencyGraph.java
@@ -43,9 +43,11 @@ import graph.AUTGraph;
import graph.AUTState;
import graph.AUTTransition;
import myutil.TraceManager;
+import ui.TGComponent;
import java.util.ArrayList;
import java.util.HashMap;
+import java.util.HashSet;
public class AvatarDependencyGraph {
private AUTGraph graph;
@@ -96,7 +98,7 @@ public class AvatarDependencyGraph {
if (signal.isOut()) {
// Write operation
AvatarSignal correspondingSig = _avspec.getCorrespondingSignal(signal);
- TraceManager.addDev("Corresponding signal=" + correspondingSig);
+ //TraceManager.addDev("Corresponding signal=" + correspondingSig);
if (correspondingSig != null) {
for(AUTState stateDestination: states) {
if (stateDestination.referenceObject instanceof AvatarActionOnSignal) {
@@ -106,10 +108,14 @@ public class AvatarDependencyGraph {
//TraceManager.addDev("Found relation!");
AUTTransition tr = new AUTTransition(state.id, "", stateDestination.id);
transitions.add(tr);
+ state.addOutTransition(tr);
+ stateDestination.addInTransition(tr);
AvatarRelation ar = _avspec.getAvatarRelationWithSignal(correspondingSig);
if (!(ar.isAsynchronous())) {
tr = new AUTTransition(stateDestination.id, "", state.id);
transitions.add(tr);
+ stateDestination.addOutTransition(tr);
+ state.addInTransition(tr);
}
}
}
@@ -190,6 +196,83 @@ public class AvatarDependencyGraph {
return adg;
}
+ public AvatarDependencyGraph reduceGraphBefore(ArrayList<AvatarElement> eltsOfInterest) {
+ AvatarDependencyGraph result = clone();
+
+ /*TraceManager.addDev("Size of original graph: s" + graph.getNbOfStates() + " t" + graph.getNbOfTransitions());
+ TraceManager.addDev("Size of graph after clone: s" + result.graph.getNbOfStates() + " t" + result.graph.getNbOfTransitions());
+
+ TraceManager.addDev("old graph:\n" + graph.toStringAll() + "\n");
+
+ TraceManager.addDev("Cloned graph:\n" + result.graph.toStringAll() + "\n");*/
+
+ /*TraceManager.addDev("Size of original graph toStates:" + toStates.size());
+ TraceManager.addDev("Size of original graph fromStates:" + fromStates.size());
+ TraceManager.addDev("Size of cloned graph toStates:" + result.toStates.size());
+ TraceManager.addDev("Size of cloned graph fromStates:" + result.fromStates.size());*/
+
+ // For each state, we figure out whether if it is linked to go to the elt states
+ // or if they are after the elts.
+
+ HashSet<AUTState> beforeStates = new HashSet<>();
+
+
+ // We take each elt one after the other and we complete the after or before states
+ for(AvatarElement ae: eltsOfInterest) {
+ //TraceManager.addDev("Condering elt:" + ae.getName());
+ Object ref = ae.getReferenceObject();
+ if (ref != null) {
+ // Finding the state referencing o
+ AUTState stateOfInterest = null;
+ for(AUTState s: graph.getStates()) {
+ AvatarElement elt = fromStates.get(s);
+ if (elt.getReferenceObject() == ref) {
+ stateOfInterest = s;
+ break;
+ }
+ }
+
+ if (stateOfInterest != null) {
+ //TraceManager.addDev("Has a state of interest: " + stateOfInterest.id);
+ for (AUTState state : graph.getStates()) {
+ if (state == stateOfInterest) {
+ beforeStates.add(result.graph.getState(state.id));
+ } else {
+ /*if (graph.hasPathFromTo(state.id, stateOfInterest.id)) {
+ beforeStates.add(result.graph.getState(state.id));
+ }*/
+ if (graph.canGoFromTo(state.id, stateOfInterest.id)) {
+ beforeStates.add(result.graph.getState(state.id));
+ }
+ }
+ }
+ }
+ }
+ }
+
+ //TraceManager.addDev("Size of before: " + beforeStates.size());
+
+ // We now have to figure out which states have to be removed
+ ArrayList<AUTState> toRemoveStates = new ArrayList<>();
+ for(AUTState st: result.graph.getStates()) {
+ if (!beforeStates.contains(st)) {
+ toRemoveStates.add(st);
+ }
+ }
+
+ //TraceManager.addDev("Size of remove: " + toRemoveStates.size());
+
+ result.graph.removeStates(toRemoveStates);
+
+ /*TraceManager.addDev("Size of graph after remove: s" + result.graph.getNbOfStates() + " t" + result.graph.getNbOfTransitions());
+ TraceManager.addDev("New graph:\n" +result.graph.toStringAll() + "\n");*/
+
+
+
+ return result;
+
+ }
+
}
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 4bf9c9edea12d0d09016acf594644fd8357f267a..d00d075f1bb5de184645fce3fe424ee2930fa8ed 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -823,11 +823,32 @@ public class AvatarSpecification extends AvatarElement {
return adg;
}
+
+ public AvatarSpecification simplifyFromDependencies(ArrayList<AvatarElement> eltsOfInterest) {
+ AvatarSpecification clonedSpec = advancedClone();
+ AvatarDependencyGraph adg = clonedSpec.makeDependencyGraph();
+ AvatarDependencyGraph reducedGraph = adg.reduceGraphBefore(eltsOfInterest);
+ clonedSpec.reduceFromDependencyGraph(reducedGraph);
+ return clonedSpec;
+
+ }
+
+
+
+
+
// TO BE COMPLETED
- AvatarSpecification reduceFromDependencyGraph(AvatarDependencyGraph _adg) {
- AvatarSpecification avspec = advancedClone();
+ // We assume the graph has been reduced already to what is necessary:
+ // We now need to reduce the avatarspec accordingly
+ public void reduceFromDependencyGraph(AvatarDependencyGraph _adg) {
+
+ // We have to update the state machines according to the graph
+
+
+ // then we can remove useless variables and signals
+
+
- return avspec;
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
index c075ce10f999755c49d1b8337b353d7e60205310..4958e3cb6398cacc9b8c7485caf4d26b83bcba2b 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
@@ -1,26 +1,26 @@
/* 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,
@@ -31,95 +31,93 @@
* 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.
*/
-
-
-
package avatartranslator.modelchecker;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarStateMachineElement;
/**
- * Class SpecificationReachability
- * Reachability of an element
- * Creation: 07/06/2016
- * @version 1.0 07/06/2016
- * @author Ludovic APVRILLE
+ * Class SpecificationReachability
+ * Reachability of an element
+ * Creation: 07/06/2016
+ *
+ * @author Ludovic APVRILLE
+ * @version 1.0 07/06/2016
*/
-public class SpecificationReachability {
+public class SpecificationReachability {
public Object ref1, ref2; // ref1 must be provided, ref2 might be null
public SpecificationPropertyPhase result;
public SpecificationState state;
-
+
public SpecificationReachability(Object _ref1, Object _ref2) {
- ref1 = _ref1;
- ref2 = _ref2;
- result = SpecificationPropertyPhase.NOTCOMPUTED;
- state = null;
+ ref1 = _ref1;
+ ref2 = _ref2;
+ result = SpecificationPropertyPhase.NOTCOMPUTED;
+ state = null;
}
public String toString() {
- String name;
- if (ref1 instanceof AvatarStateMachineElement) {
- name = "Element " + ((AvatarStateMachineElement)ref1).getExtendedName();
- } else {
- name = ref1.toString();
- }
-
- if (ref2 != null) {
- if (ref2 instanceof AvatarBlock) {
- name += " of block " + ((AvatarBlock)ref2).getName();
- } else {
- name += ref2.toString();
- }
- }
-
-
- if (result == SpecificationPropertyPhase.NOTCOMPUTED) {
- return name + " -> not computed";
- }
-
- if (result == SpecificationPropertyPhase.SATISFIED) {
- return name + " -> reachable in RG state " + state.id;
- }
-
- return name + " -> NOT reachable";
-
+ String name;
+ if (ref1 instanceof AvatarStateMachineElement) {
+ name = "Element " + ((AvatarStateMachineElement) ref1).getExtendedName();
+ } else {
+ name = ref1.toString();
+ }
+
+ if (ref2 != null) {
+ if (ref2 instanceof AvatarBlock) {
+ name += " of block " + ((AvatarBlock) ref2).getName();
+ } else {
+ name += ref2.toString();
+ }
+ }
+
+
+ if (result == SpecificationPropertyPhase.NOTCOMPUTED) {
+ return name + " -> not computed";
+ }
+
+ if (result == SpecificationPropertyPhase.SATISFIED) {
+ return name + " -> reachable in RG state " + state.id;
+ }
+
+ return name + " -> NOT reachable";
+
}
-
+
public String toStringGeneric() {
String name;
if (ref1 instanceof AvatarStateMachineElement) {
- name = "Element " + ((AvatarStateMachineElement)ref1).getExtendedName();
+ name = "Element " + ((AvatarStateMachineElement) ref1).getExtendedName();
} else {
name = ref1.toString();
}
if (ref2 != null) {
if (ref2 instanceof AvatarBlock) {
- name += " of block " + ((AvatarBlock)ref2).getName();
+ name += " of block " + ((AvatarBlock) ref2).getName();
} else {
- name += ref2.toString();
+ name += ref2.toString();
}
}
-
+
if (result == SpecificationPropertyPhase.NOTCOMPUTED) {
- return name + " -> not computed";
+ return name + " -> not computed";
}
-
+
if (result == SpecificationPropertyPhase.SATISFIED) {
return name + " -> reachable";
}
return name + " -> NOT reachable";
-
+
}
}
diff --git a/src/main/java/graph/AUTGraph.java b/src/main/java/graph/AUTGraph.java
index afe4e0c69c7f845ee3dd618547fa0e5170452268..d4cb4f8b203decb19c050efb403f6b83f6b01294 100755
--- a/src/main/java/graph/AUTGraph.java
+++ b/src/main/java/graph/AUTGraph.java
@@ -1,26 +1,26 @@
/* 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,
@@ -31,7 +31,7 @@
* 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.
*/
@@ -43,14 +43,13 @@ import myutil.Conversion;
import myutil.DijkstraState;
import myutil.GraphAlgorithms;
import myutil.TraceManager;
+import rationals.*;
+import rationals.transformations.Reducer;
import java.io.BufferedReader;
import java.io.StringReader;
import java.util.*;
-import rationals.*;
-import rationals.transformations.*;
-
/**
* Class AUTGraph
* Creation : 16/09/2004
@@ -87,6 +86,104 @@ public class AUTGraph implements myutil.Graph {
statesComputed = true;
}
+ public static String[] decodeLine(String s) {
+ int index1, index2;
+ String s1, s2, s3;
+
+ index1 = s.indexOf("(");
+ index2 = s.indexOf(",");
+ s1 = s.substring(index1 + 1, index2);
+ s = s.substring(index2 + 1, s.length());
+ s = Conversion.removeFirstSpaces(s);
+
+ // for of the action
+ // , action,
+ // "i(action<1,2,4>)",
+ // "action<1,2,4>",
+
+ // guillemets ?
+ index1 = s.indexOf("\"");
+ if (index1 > -1) {
+ //TraceManager.addDev("Guillemets on " + s);
+ s2 = s.substring(index1 + 1, s.length());
+ s2 = s2.substring(0, s2.indexOf("\""));
+ //TraceManager.addDev("Guillemets on " + s2);
+ /*index2 = s2.indexOf("(");
+ if (index2 > -1) {
+ s2 = s2.substring(index2+1, s2.indexOf(")"));
+ }*/
+ //TraceManager.addDev("Guillemets on " + s2);
+
+ } else {
+ //TraceManager.addDev("No Guillemets on " + s);
+ index1 = s.indexOf(",");
+ if ((index2 = s.indexOf("(")) >= 0) {
+ s2 = s.substring(index2 + 1, index1 - 2);
+ } else {
+ if ((index2 = s.indexOf("\"t\"")) >= 0) {
+ s2 = "t";
+ } else {
+ s2 = s.substring(0, index1);
+ }
+ }
+ }
+
+ s = s.substring(s.indexOf(s2) + s2.length(), s.length());
+ //TraceManager.addDev("s=" + s);
+ index1 = s.indexOf(",");
+ //index2 = s.indexOf(")");
+ //s2 = s.substring(0, index1-1);
+ s3 = s.substring(index1 + 1, s.length() - 1);
+ s3 = Conversion.removeFirstSpaces(s3);
+ //TraceManager.addDev("s1=" + s1 + " s2=" + s2 + " s3=" + s3);
+
+ String[] array = new String[3];
+ array[0] = s1;
+ array[1] = s2;
+ array[2] = s3;
+ return array;
+ }
+
+ public static String removeSameSignal(String input) {
+ int indexE = input.indexOf("!");
+ int indexQ = input.indexOf("?");
+ int indexP = input.indexOf("(");
+
+ if ((indexE == -1) || (indexQ == -1) || (indexP == -1)) {
+ return input;
+ }
+
+ if (indexQ < indexE) {
+ return input;
+ }
+
+ if (indexP < indexQ) {
+ return input;
+ }
+
+ String tmpE = input.substring(indexE + 1, indexQ - 1);
+ String tmpQ = input.substring(indexQ + 1, indexP);
+
+ TraceManager.addDev("tmpE=" + tmpE + " tmpQ=" + tmpQ);
+
+ if (tmpE.compareTo(tmpQ) != 0) {
+ return input;
+ }
+
+
+ return "!" + input.substring(indexQ, input.length());
+ }
+
+ public static String removeOTime(String input) {
+ if (input.endsWith("[0...0]")) {
+ return input.substring(0, input.length() - 7);
+ } else {
+ return input;
+ }
+
+
+ }
+
public void stopBuildGraph() {
br = null;
}
@@ -170,64 +267,6 @@ public class AUTGraph implements myutil.Graph {
}
}
- public static String[] decodeLine(String s) {
- int index1, index2;
- String s1, s2, s3;
-
- index1 = s.indexOf("(");
- index2 = s.indexOf(",");
- s1 = s.substring(index1 + 1, index2);
- s = s.substring(index2 + 1, s.length());
- s = Conversion.removeFirstSpaces(s);
-
- // for of the action
- // , action,
- // "i(action<1,2,4>)",
- // "action<1,2,4>",
-
- // guillemets ?
- index1 = s.indexOf("\"");
- if (index1 > -1) {
- //TraceManager.addDev("Guillemets on " + s);
- s2 = s.substring(index1 + 1, s.length());
- s2 = s2.substring(0, s2.indexOf("\""));
- //TraceManager.addDev("Guillemets on " + s2);
- /*index2 = s2.indexOf("(");
- if (index2 > -1) {
- s2 = s2.substring(index2+1, s2.indexOf(")"));
- }*/
- //TraceManager.addDev("Guillemets on " + s2);
-
- } else {
- //TraceManager.addDev("No Guillemets on " + s);
- index1 = s.indexOf(",");
- if ((index2 = s.indexOf("(")) >= 0) {
- s2 = s.substring(index2 + 1, index1 - 2);
- } else {
- if ((index2 = s.indexOf("\"t\"")) >= 0) {
- s2 = "t";
- } else {
- s2 = s.substring(0, index1);
- }
- }
- }
-
- s = s.substring(s.indexOf(s2) + s2.length(), s.length());
- //TraceManager.addDev("s=" + s);
- index1 = s.indexOf(",");
- //index2 = s.indexOf(")");
- //s2 = s.substring(0, index1-1);
- s3 = s.substring(index1 + 1, s.length() - 1);
- s3 = Conversion.removeFirstSpaces(s3);
- //TraceManager.addDev("s1=" + s1 + " s2=" + s2 + " s3=" + s3);
-
- String[] array = new String[3];
- array[0] = s1;
- array[1] = s2;
- array[2] = s3;
- return array;
- }
-
public int getNbOfStates() {
return nbState;
}
@@ -249,6 +288,12 @@ public class AUTGraph implements myutil.Graph {
return states;
}
+ public void setStates(ArrayList<AUTState> _states) {
+ states = _states;
+ nbState = states.size();
+ statesComputed = true;
+ }
+
public ArrayList<AUTTransition> getTransitions() {
return transitions;
}
@@ -262,7 +307,6 @@ public class AUTGraph implements myutil.Graph {
states.add(_st);
}
-
public int getNbPotentialDeadlocks() {
int nb = 0;
@@ -287,6 +331,9 @@ public class AUTGraph implements myutil.Graph {
return "";
}
+ /* State numbers are return under the form of int */
+ /* Should be rewritten: not of high performance at all */
+
public boolean hasEntryTransition(int state) {
if (hasEntryTransition == null) {
computeEntryExitTransitions();
@@ -316,8 +363,7 @@ public class AUTGraph implements myutil.Graph {
}
- /* State numbers are return under the form of int */
- /* Should be rewritten: not of high performance at all */
+ // For Graph interface
public int[] getVectorPotentialDeadlocks() {
int nbPotentialDeadlock = getNbPotentialDeadlocks();
@@ -341,7 +387,6 @@ public class AUTGraph implements myutil.Graph {
return GraphAlgorithms.ShortestPathFrom(this, fromState)[targetState].path;
}
-
public boolean hasTransitionWithAction(String action) {
for (AUTTransition aut1 : transitions) {
@@ -352,8 +397,6 @@ public class AUTGraph implements myutil.Graph {
return false;
}
- // For Graph interface
-
public int getWeightOfTransition(int originState, int destinationState) {
if (statesComputed) {
if (states.get(originState).hasTransitionTo(destinationState)) {
@@ -376,7 +419,6 @@ public class AUTGraph implements myutil.Graph {
return graph.toString();
}
-
public String toFullString() {
StringBuffer graph = new StringBuffer("Transitions:");
for (AUTTransition aut1 : transitions) {
@@ -416,12 +458,6 @@ public class AUTGraph implements myutil.Graph {
return statesComputed;
}
- public void setStates(ArrayList<AUTState> _states) {
- states = _states;
- nbState = states.size();
- statesComputed = true;
- }
-
public HashSet<String> getAllActions() {
HashSet<String> hs = new HashSet<String>();
for (AUTTransition tr : transitions) {
@@ -430,7 +466,6 @@ public class AUTGraph implements myutil.Graph {
return hs;
}
-
public void reinitMet() {
for (AUTState state : states) {
state.met = false;
@@ -475,23 +510,34 @@ public class AUTGraph implements myutil.Graph {
display.display();
}
-
public AUTGraph cloneMe() {
- AUTGraph newGraph = new AUTGraph();
- newGraph.setNbOfStates(getNbOfStates());
+ ArrayList<AUTState> statesN = new ArrayList<>();
+ ArrayList<AUTTransition> trN = new ArrayList<>();
+
+ //newGraph.computeStates();
+ for (AUTState st : getStates()) {
+ AUTState newSt = st.clone();
+ statesN.add(newSt);
+ }
+
for (AUTTransition tr : transitions) {
AUTTransition newTr = new AUTTransition(tr.origin, tr.transition, tr.destination);
- newGraph.addTransition(newTr);
+ trN.add(newTr);
+ // Update receiving and destination states
+ AUTState s = statesN.get(tr.origin);
+ s.addOutTransition(newTr);
+ s = statesN.get(tr.destination);
+ s.addInTransition(newTr);
}
- newGraph.computeStates();
- return newGraph;
- }
+ return new AUTGraph(statesN, trN);
+ }
+
public String getCompoundString(AUTTransition t, HashSet<AUTTransition> set) {
String ret = "";
int cpt = 0;
- for(AUTTransition tr: transitions) {
+ for (AUTTransition tr : transitions) {
if ((tr.origin == t.origin) && (tr.destination == t.destination)) {
set.add(tr);
if (cpt > 0) {
@@ -505,46 +551,6 @@ public class AUTGraph implements myutil.Graph {
return ret;
}
- public static String removeSameSignal(String input) {
- int indexE = input.indexOf("!");
- int indexQ = input.indexOf("?");
- int indexP = input.indexOf("(");
-
- if ((indexE == -1) || (indexQ == -1) || (indexP == -1) ) {
- return input;
- }
-
- if (indexQ < indexE) {
- return input;
- }
-
- if (indexP < indexQ) {
- return input;
- }
-
- String tmpE = input.substring(indexE+1, indexQ-1);
- String tmpQ = input.substring(indexQ+1, indexP);
-
- TraceManager.addDev("tmpE=" + tmpE + " tmpQ=" + tmpQ);
-
- if (tmpE.compareTo(tmpQ) != 0) {
- return input;
- }
-
-
- return "!" + input.substring(indexQ, input.length());
- }
-
- public static String removeOTime(String input) {
- if (input.endsWith("[0...0]")) {
- return input.substring(0, input.length()-7);
- } else {
- return input;
- }
-
-
- }
-
public String[] getInternalActions() {
HashSet<String> list = new HashSet<>();
for (AUTTransition tr : transitions) {
@@ -598,13 +604,63 @@ public class AUTGraph implements myutil.Graph {
}
-
//minimizeTau(tauOnly);
//return this;
return reduceGraph();
}
+
+ public boolean canGoFromTo(int from, int to) {
+ //TraceManager.addDev("Can go from " + from + " to " + to);
+
+ if (from == to) {
+ return true;
+ }
+
+ HashSet<AUTState> alreadyAnalyzed = new HashSet<>();
+ AUTState s = states.get(from);
+
+ // We assume pending states are not the "to" state
+ ArrayList<AUTState> pending = new ArrayList<>();
+ pending.add(s);
+
+ while(pending.size() > 0) {
+ /*String str = "Pending ";
+ for(AUTState sp : pending) {
+ str += sp.id + " ";
+ }
+ TraceManager.addDev(str + "\n");*/
+ AUTState currentS = pending.get(0);
+ pending.remove(0);
+ if (!alreadyAnalyzed.contains(currentS)) {
+ alreadyAnalyzed.add(currentS);
+
+ // We consider all outgoing transitions
+ //TraceManager.addDev("Nb of outgoing transitions:" + currentS.outTransitions.size() + ":" + currentS.outTransitions);
+ for (AUTTransition tr : currentS.outTransitions) {
+ if (tr.destination == to) {
+ return true;
+ } else {
+ pending.add(states.get(tr.destination));
+ }
+ }
+ }
+ }
+
+ //TraceManager.addDev("False ...");
+ return false;
+ }
+
+
+ public boolean hasPathFromTo(int idInit, int idEnd) {
+ DijkstraState[] dss;
+ dss = GraphAlgorithms.ShortestPathFrom(this, idInit);
+ int size = dss[idEnd].path.length;
+ return size > 0;
+ }
+
+
public void minimizeTau(boolean tauOnly) {
boolean modif = true;
@@ -654,7 +710,7 @@ public class AUTGraph implements myutil.Graph {
for (AUTTransition trM : st1.outTransitions) {
st.outTransitions.add(trM);
trM.origin = st.id;
- // TraceManager.addDev("New out transitions " + trM);
+ // TraceManager.addDev("New out transitions " + trM);
}
st1.outTransitions.clear();
break;
@@ -801,7 +857,7 @@ public class AUTGraph implements myutil.Graph {
}
- private void removeStates(ArrayList<AUTState> toRemoveStates) {
+ public void removeStates(ArrayList<AUTState> toRemoveStates) {
if (toRemoveStates.size() > 0) {
hasExitTransition = null;
@@ -814,6 +870,10 @@ public class AUTGraph implements myutil.Graph {
for (AUTState str : toRemoveStates) {
// We need to remove all transitions of the removed state
//TraceManager.addDev("Removing transitions of state:" + str.id + "\n" + toFullString());
+
+ //TraceManager.addDev("Transition size before:" + transitions.size());
+
+
for (AUTTransition trin : str.inTransitions) {
transitions.remove(trin);
}
@@ -821,6 +881,8 @@ public class AUTGraph implements myutil.Graph {
transitions.remove(trout);
}
+ //TraceManager.addDev("Transition size after:" + transitions.size());
+
for (AUTState state : states) {
state.removeAllTransitionsWithId(str.id);
}
@@ -839,8 +901,9 @@ public class AUTGraph implements myutil.Graph {
AUTState moved = states.get(nbState - 1);
//TraceManager.addDev("Moving state " + moved.id + " to index " + str.id);
+ states.remove(moved);
states.set(str.id, moved);
- states.remove(nbState - 1);
+ states.remove(str);
nbState--;
//TraceManager.addDev("nbState=" + nbState + " states size = " + states.size());
/*AUTTransition tt = findTransitionWithId(nbState);
@@ -849,6 +912,10 @@ public class AUTGraph implements myutil.Graph {
}*/
//TraceManager.addDev("Update id\n" + toAUTStringFormat());
moved.updateID(str.id);
+
+
+
+
/*tt = findTransitionWithId(nbState);
if (tt != null) {
TraceManager.addDev("2) Transition with id not normal" + tt);
@@ -1046,14 +1113,14 @@ public class AUTGraph implements myutil.Graph {
long startTime = System.nanoTime();
- AUTState[] statesToConsider = new AUTState[1];
+ AUTState[] statesToConsider = new AUTState[1];
LinkedList<AUTState> nextStatesToConsider = new LinkedList<AUTState>();
statesToConsider[0] = states.get(0);
states.get(0).met = true;
- for(int cpt=0; cpt<statesToConsider.length; cpt++){
+ for (int cpt = 0; cpt < statesToConsider.length; cpt++) {
nextStatesToConsider.clear();
- for (AUTState st: statesToConsider) {
+ for (AUTState st : statesToConsider) {
//st.met = true;
//cpt++;
for (AUTTransition tr : st.outTransitions) {
@@ -1087,8 +1154,8 @@ public class AUTGraph implements myutil.Graph {
long endTime = System.nanoTime();
- TraceManager.addDev("First part: " + (time1-startTime)/1000000000 +
- " Second part: " + (endTime - time1)/1000000000);
+ TraceManager.addDev("First part: " + (time1 - startTime) / 1000000000 +
+ " Second part: " + (endTime - time1) / 1000000000);
//statesComputed = false;
@@ -1118,11 +1185,11 @@ public class AUTGraph implements myutil.Graph {
Set<Transition<String>> trs = (Set<Transition<String>>) a.delta();
//Set<?> trs = a.delta();
@SuppressWarnings("unchecked")
- Set<State> sts = (Set<State>)(a.states());
+ Set<State> sts = (Set<State>) (a.states());
Map<State, Integer> mapOfStates = new HashMap<>();
int cpt = 1;
- for(State st: sts) {
+ for (State st : sts) {
if (st.isInitial()) {
//@SuppressWarnings("unchecked")
@@ -1131,13 +1198,13 @@ public class AUTGraph implements myutil.Graph {
//@SuppressWarnings("unchecked")
mapOfStates.put(st, new Integer(cpt));
- cpt ++;
+ cpt++;
}
}
graph.setNbOfStates(mapOfStates.size());
- for(Transition<String> tr: trs) {
+ for (Transition<String> tr : trs) {
State s1 = tr.start();
State s2 = tr.end();
String label = tr.label();
@@ -1161,12 +1228,12 @@ public class AUTGraph implements myutil.Graph {
computeStates();
boolean initial = true;
- for(AUTState s: states) {
+ for (AUTState s : states) {
State as = a.addState(initial, s.isTerminationState());
s.referenceObject = as;
initial = false;
}
- for(AUTTransition t: transitions) {
+ for (AUTTransition t : transitions) {
try {
String label = t.transition;
if (t.isTau) {
@@ -1175,7 +1242,8 @@ public class AUTGraph implements myutil.Graph {
a.addTransition(new Transition<String>((State) (states.get(t.origin).referenceObject), label, (State) (states.get(t
.destination)
.referenceObject)));
- } catch (NoSuchStateException nsse) { }
+ } catch (NoSuchStateException nsse) {
+ }
}
return a;
@@ -1226,8 +1294,8 @@ public class AUTGraph implements myutil.Graph {
Collections.sort(sortedAlphabet);
TraceManager.addDev("Alphabet size:" + sortedAlphabet.size());
- for (int i=0; i<alphabet.size(); i++) {
- TraceManager.addDev("Letter #" + i + ": " + sortedAlphabet.get(i).toString());
+ for (int i = 0; i < alphabet.size(); i++) {
+ TraceManager.addDev("Letter #" + i + ": " + sortedAlphabet.get(i).toString());
}
@@ -1358,7 +1426,7 @@ public class AUTGraph implements myutil.Graph {
bii = currentP.blocks.get(1);
}
- TraceManager.addDev("B= " + b + " bi=" + bi + " bii=" + bii);
+ TraceManager.addDev("B= " + b + " bi=" + bi + " bii=" + bii);
for (AUTElement elt : sortedAlphabet) {
//TraceManager.addDev("\n*** Considering alphabet element = " + elt.value);
@@ -1640,10 +1708,10 @@ public class AUTGraph implements myutil.Graph {
public int getMinValue(String nameOfTransition) {
int minValue = Integer.MAX_VALUE;
//System.out.println("executing. min value");
- for (AUTTransition tr: transitions) {
+ for (AUTTransition tr : transitions) {
//System.out.println("executing. Dealing with " + tr.transition);
if (tr.transition.length() > 3) {
- String trans = tr.transition.substring(2, tr.transition.length()-1);
+ String trans = tr.transition.substring(2, tr.transition.length() - 1);
//System.out.println("executing. trans " + trans);
int index = trans.indexOf("<");
if (index > 0) {
@@ -1671,10 +1739,10 @@ public class AUTGraph implements myutil.Graph {
public int getMaxValue(String nameOfTransition) {
int maxValue = -1;
//System.out.println("executing. min value");
- for (AUTTransition tr: transitions) {
+ for (AUTTransition tr : transitions) {
//System.out.println("executing. Dealing with " + tr.transition);
if (tr.transition.length() > 3) {
- String trans = tr.transition.substring(2, tr.transition.length()-1);
+ String trans = tr.transition.substring(2, tr.transition.length() - 1);
//System.out.println("executing. trans " + trans);
int index = trans.indexOf("<");
if (index > 0) {
@@ -1699,5 +1767,27 @@ public class AUTGraph implements myutil.Graph {
return maxValue;
}
+ public String toStringStates() {
+ StringBuffer sb = new StringBuffer();
+ sb.append("nb of states: " + nbState + "\n");
+ for(AUTState s: states) {
+ sb.append(s.toString());
+ }
+ return sb.toString();
+ }
+
+ public String toStringAll() {
+ StringBuffer sb = new StringBuffer();
+ sb.append("nb of states: " + nbState + "\n");
+ for(AUTState s: states) {
+ sb.append(s.toString());
+ }
+ for(AUTTransition t: transitions) {
+ sb.append(t.toString() + "\n");
+ }
+
+ return sb.toString();
+ }
+
}
diff --git a/src/main/java/graph/AUTState.java b/src/main/java/graph/AUTState.java
index 15a648e28a5311e3a18a18e3c0bbb5992b2689d4..fb5f720453a1dd9caa2f6bc06d4cef5c76308338 100755
--- a/src/main/java/graph/AUTState.java
+++ b/src/main/java/graph/AUTState.java
@@ -1,26 +1,26 @@
/* 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,
@@ -31,14 +31,12 @@
* 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.
*/
-
-
package graph;
import java.util.ArrayList;
@@ -46,14 +44,15 @@ import java.util.LinkedList;
import java.util.Random;
/**
- * Class AUTState
- * Creation : 05/03/2008
- ** @version 1.0 05/03/2008
- * @author Ludovic APVRILLE
+ * Class AUTState
+ * Creation : 05/03/2008
+ * * @version 1.0 05/03/2008
+ *
+ * @author Ludovic APVRILLE
*/
public class AUTState implements Comparable<AUTState> {
- public String info;
+ public String info;
public int id;
public ArrayList<AUTTransition> inTransitions; // Arriving to that state
public ArrayList<AUTTransition> outTransitions; // Departing from that state
@@ -61,14 +60,15 @@ public class AUTState implements Comparable<AUTState> {
public Object referenceObject;
public boolean isOrigin = false;
+
public AUTState(int _id) {
id = _id;
inTransitions = new ArrayList<AUTTransition>();
outTransitions = new ArrayList<AUTTransition>();
}
- public int compareTo( AUTState _s ) {
- return id - _s.id;
+ public int compareTo(AUTState _s) {
+ return id - _s.id;
}
public void addInTransition(AUTTransition tr) {
@@ -88,11 +88,11 @@ public class AUTState implements Comparable<AUTState> {
}
public boolean isTerminationState() {
- return (outTransitions.size() == 0);
+ return (outTransitions.size() == 0);
}
public AUTTransition getTransitionTo(int destination) {
- for(AUTTransition tr: outTransitions) {
+ for (AUTTransition tr : outTransitions) {
if (tr.destination == destination) {
return tr;
}
@@ -101,7 +101,7 @@ public class AUTState implements Comparable<AUTState> {
}
public boolean hasTransitionTo(int destination) {
- for(AUTTransition aut1 : outTransitions) {
+ for (AUTTransition aut1 : outTransitions) {
if (aut1.destination == destination) {
return true;
}
@@ -126,136 +126,148 @@ public class AUTState implements Comparable<AUTState> {
}
public void updateID(int _newID) {
- id = _newID;
- for(AUTTransition inT: inTransitions) {
- inT.destination = id;
- }
-
- for(AUTTransition outT: outTransitions) {
- outT.origin = id;
- }
+ id = _newID;
+ for (AUTTransition inT : inTransitions) {
+ inT.destination = id;
+ }
+
+ for (AUTTransition outT : outTransitions) {
+ outT.origin = id;
+ }
}
public AUTTransition[] getAtLeastTwoOutTauTransitions() {
- if (outTransitions == null) {
- return null;
- }
+ if (outTransitions == null) {
+ return null;
+ }
- int cpt = 0;
- AUTTransition[] trans = new AUTTransition[2];
- for(AUTTransition tr: outTransitions) {
- if (tr.isTau) {
- trans[cpt] = tr;
- cpt ++;
- if (cpt == 2) {
- return trans;
- }
- }
- }
- return null;
+ int cpt = 0;
+ AUTTransition[] trans = new AUTTransition[2];
+ for (AUTTransition tr : outTransitions) {
+ if (tr.isTau) {
+ trans[cpt] = tr;
+ cpt++;
+ if (cpt == 2) {
+ return trans;
+ }
+ }
+ }
+ return null;
}
public boolean hasOneIncomingTauAndOneFollower() {
- if (outTransitions.size() != 1) {
- return false;
- }
+ if (outTransitions.size() != 1) {
+ return false;
+ }
- if (inTransitions.size() != 1) {
- return false;
- }
+ if (inTransitions.size() != 1) {
+ return false;
+ }
- return inTransitions.get(0).isTau;
+ return inTransitions.get(0).isTau;
}
public boolean hasOutputTauTransition() {
- if (outTransitions.size() < 1) {
- return false;
- }
+ if (outTransitions.size() < 1) {
+ return false;
+ }
- for(AUTTransition outT: outTransitions) {
- if (outT.isTau) {
- return true;
- }
- }
+ for (AUTTransition outT : outTransitions) {
+ if (outT.isTau) {
+ return true;
+ }
+ }
- return false;
+ return false;
}
public boolean hasSimilarTransition(AUTTransition _tr) {
- if (outTransitions.size() == 0) {
- return false;
- }
- for(AUTTransition tr: outTransitions) {
- if ((tr.origin == _tr.origin) && (tr.destination == _tr.destination) && (tr.transition.compareTo(_tr.transition) == 0)) {
- return true;
- }
- }
-
- return false;
+ if (outTransitions.size() == 0) {
+ return false;
+ }
+ for (AUTTransition tr : outTransitions) {
+ if ((tr.origin == _tr.origin) && (tr.destination == _tr.destination) && (tr.transition.compareTo(_tr.transition) == 0)) {
+ return true;
+ }
+ }
+
+ return false;
}
public void removeAllOutTauTransitions(ArrayList<AUTTransition> _transitions, ArrayList<AUTState> _states) {
- ArrayList<AUTTransition> outTransitions2 = new ArrayList<AUTTransition>();
- for(AUTTransition tr: outTransitions) {
- if (!(tr.isTau)) {
- outTransitions2.add(tr);
- } else {
- _transitions.remove(tr);
- _states.get(tr.destination).removeInTransition(tr);
- }
- }
- outTransitions = outTransitions2;
+ ArrayList<AUTTransition> outTransitions2 = new ArrayList<AUTTransition>();
+ for (AUTTransition tr : outTransitions) {
+ if (!(tr.isTau)) {
+ outTransitions2.add(tr);
+ } else {
+ _transitions.remove(tr);
+ _states.get(tr.destination).removeInTransition(tr);
+ }
+ }
+ outTransitions = outTransitions2;
}
public void removeInTransition(AUTTransition _tr) {
- inTransitions.remove(_tr);
+ inTransitions.remove(_tr);
}
public void createTransitionsButNotDuplicate(LinkedList<AUTTransition> _newTransitions, ArrayList<AUTState> _states, ArrayList<AUTTransition> _transitions) {
- for(AUTTransition tr: _newTransitions) {
- if (!(hasSimilarTransition(tr))) {
- AUTTransition ntr = tr.basicClone();
- ntr.origin = id;
- outTransitions.add(ntr);
- _states.get(ntr.destination).addInTransition(ntr);
- _transitions.add(ntr);
- }
- }
+ for (AUTTransition tr : _newTransitions) {
+ if (!(hasSimilarTransition(tr))) {
+ AUTTransition ntr = tr.basicClone();
+ ntr.origin = id;
+ outTransitions.add(ntr);
+ _states.get(ntr.destination).addInTransition(ntr);
+ _transitions.add(ntr);
+ }
+ }
}
public void removeAllTransitionsWithId(int id) {
- ArrayList<AUTTransition> toBeRemoved = new ArrayList<AUTTransition>();
- for(AUTTransition tr: outTransitions) {
- if (tr.destination == id) {
- toBeRemoved.add(tr);
- }
- }
- for(AUTTransition tr: toBeRemoved) {
- outTransitions.remove(tr);
- }
- toBeRemoved.clear();
-
- for(AUTTransition tr: inTransitions) {
- if (tr.origin == id) {
- toBeRemoved.add(tr);
- }
- }
- for(AUTTransition tr: toBeRemoved) {
- inTransitions.remove(tr);
- }
+ ArrayList<AUTTransition> toBeRemoved = new ArrayList<AUTTransition>();
+ for (AUTTransition tr : outTransitions) {
+ if (tr.destination == id) {
+ toBeRemoved.add(tr);
+ }
+ }
+ for (AUTTransition tr : toBeRemoved) {
+ outTransitions.remove(tr);
+ }
+ toBeRemoved.clear();
+
+ for (AUTTransition tr : inTransitions) {
+ if (tr.origin == id) {
+ toBeRemoved.add(tr);
+ }
+ }
+ for (AUTTransition tr : toBeRemoved) {
+ inTransitions.remove(tr);
+ }
}
public String toString() {
- String s = "" + id + "\n";
- for(AUTTransition tr: inTransitions) {
- s += "\t in: " + tr.toString() + "\n";
- }
- for(AUTTransition tr: outTransitions) {
- s += "\tout: " + tr.toString() + "\n";
- }
- return s;
+ String s = "" + id + " ";
+ if (info != null) {
+ s += "\"" + info + "\"";
+ }
+ s += "\n";
+ for (AUTTransition tr : inTransitions) {
+ s += "\t in: " + tr.toString() + "\n";
+ }
+ for (AUTTransition tr : outTransitions) {
+ s += "\tout: " + tr.toString() + "\n";
+ }
+ return s;
}
+ public AUTState clone() {
+ AUTState s = new AUTState(id);
+ s.info = info;
+ s.referenceObject = referenceObject;
+ s.isOrigin = isOrigin;
+ return s;
+ }
+
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 8d8f02e79ce2d3bbe3fc45129c4a833e84d4620a..3e50e3855e52d3d3e2fa51e5565a0fcc730dee93 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -40,6 +40,7 @@
package ui.window;
import avatartranslator.AvatarDependencyGraph;
+import avatartranslator.AvatarElement;
import avatartranslator.AvatarSpecification;
import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
@@ -64,13 +65,8 @@ import java.awt.event.ActionListener;
import java.io.File;
import java.text.DateFormat;
import java.text.SimpleDateFormat;
-import java.util.ArrayList;
-import java.util.Date;
-import java.util.HashMap;
+import java.util.*;
import java.util.List;
-import java.util.LinkedList;
-import java.util.Map;
-import java.util.TimerTask;
import java.util.concurrent.TimeUnit;
/**
@@ -108,6 +104,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean ignoreInternalStatesSelected = true;
protected static boolean generateDesignSelected = false;
protected static boolean generateDependencyGraphSelected = false;
+ protected static boolean generateDependencyGraphEltSelected = false;
protected static int reachabilitySelected = REACHABILITY_NONE;
protected static int livenessSelected = LIVENESS_NONE;
protected static boolean safetySelected = false;
@@ -184,7 +181,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JCheckBox saveGraphAUT, saveGraphDot, ignoreEmptyTransitions, ignoreInternalStates,
- ignoreConcurrenceBetweenInternalActions, generateDesign, generateDependencyGraph;
+ ignoreConcurrenceBetweenInternalActions, generateDesign, generateDependencyGraph, generateDependencyGraphElt;
protected JButton graphDirButton, graphPathDotButton;
protected JTextField graphPath, graphPathDot;
protected JTabbedPane jp1;
@@ -202,6 +199,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
//protected boolean startProcess = false;
protected Map<String, Integer> verifMap;
+ private HashSet<TGComponent> hasDependencyGraph;
+
+
/*
* Creates new form
*/
@@ -233,6 +233,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
verifMap = new HashMap<String, Integer>();
+ hasDependencyGraph = new HashSet<>();
+
/*if ((mgui != null) && (spec != null)) {
mgui.drawAvatarSpecification(spec);
}*/
@@ -296,6 +298,13 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jp01.add(generateDependencyGraph, c01);
}
+ if (TraceManager.devPolicy == TraceManager.TO_CONSOLE) {
+ generateDependencyGraphElt = new JCheckBox("[For testing purpose only] Generate dependency graph for Reachability / liveness",
+ generateDependencyGraphEltSelected);
+ generateDependencyGraphElt.addActionListener(this);
+ jp01.add(generateDependencyGraphElt, c01);
+ }
+
c01.gridwidth = 1;
ignoreEmptyTransitions = new JCheckBox("Do not display empty transitions as internal actions", ignoreEmptyTransitionsSelected);
@@ -1167,6 +1176,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
Object o = ((AvatarStateMachineElement) _o).getReferenceObject();
if (o instanceof TGComponent) {
TGComponent tgc = (TGComponent) (o);
+
+ handleDependencyGraph(_o, tgc);
+
//TraceManager.addDev("Reachability of tgc=" + tgc + " value=" + tgc.getValue() + " class=" + tgc.getClass());
switch (_res) {
case NOTCOMPUTED:
@@ -1184,12 +1196,34 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
}
+
+ protected void handleDependencyGraph(Object _o, TGComponent _tgc) {
+ if (hasDependencyGraph.contains(_tgc)) {
+ return;
+ }
+ hasDependencyGraph.add(_tgc);
+ if (generateDependencyGraphEltSelected) {
+ TraceManager.addDev("Generating dependency graph for component:" + _tgc.toString());
+ AvatarDependencyGraph adg = spec.makeDependencyGraph();
+ ArrayList<AvatarElement> elts = new ArrayList<>();
+ elts.add((AvatarElement)_o);
+ AvatarDependencyGraph clonedG = adg.reduceGraphBefore(elts);
+ RG rg = new RG("Dependency Graph of " + _tgc.toString() + "/" + _tgc.getAVATARID() + ".");
+ rg.graph = clonedG.getGraph();
+ rg.nbOfStates = rg.graph.getNbOfStates();
+ rg.nbOfTransitions = rg.graph.getNbOfTransitions();
+ mgui.addRG(rg);
+ }
+ }
protected void handleLiveness(Object _o, SpecificationPropertyPhase _res) {
if (_o instanceof AvatarStateMachineElement) {
Object o = ((AvatarStateMachineElement) _o).getReferenceObject();
if (o instanceof TGComponent) {
TGComponent tgc = (TGComponent) (o);
+
+ handleDependencyGraph(_o, tgc);
+
//TraceManager.addDev("Reachability of tgc=" + tgc + " value=" + tgc.getValue() + " class=" + tgc.getClass());
switch (_res) {
case NOTCOMPUTED:
@@ -1247,6 +1281,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (generateDependencyGraph != null) {
generateDependencyGraphSelected = generateDependencyGraph.isSelected();
}
+ if (generateDependencyGraph != null) {
+ generateDependencyGraphEltSelected = generateDependencyGraphElt.isSelected();
+ }
ignoreEmptyTransitionsSelected = ignoreEmptyTransitions.isSelected();
ignoreConcurrenceBetweenInternalActionsSelected = ignoreConcurrenceBetweenInternalActions.isSelected();
ignoreInternalStatesSelected = ignoreInternalStates.isSelected();