diff --git a/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java b/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java
index 2b0efc82a696f484bbd23a777bc82bd88e6a0dba..17966777c1b1e6c9713673a3a100a2fbc95a9dbd 100644
--- a/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java
+++ b/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java
@@ -39,6 +39,8 @@
package avatartranslator;
+import common.CanBeTagged;
+import common.Tags;
import graph.AUTGraph;
import graph.AUTState;
import graph.AUTTransition;
@@ -205,6 +207,7 @@ public class AvatarCompactDependencyGraph {
tr = new AUTTransition(newState.id, "", newStateD.id);
tr.addTag(AUTGraph.COMM_TAG);
+ //TraceManager.addDev("**** Adding COMM Tag to transition " + tr);
transitions.add(tr);
newState.addOutTransition(tr);
newStateD.addInTransition(tr);
@@ -213,6 +216,7 @@ public class AvatarCompactDependencyGraph {
if (!(ar.isAsynchronous())) {
tr = new AUTTransition(newStateD.id, "", newState.id);
tr.addTag(AUTGraph.COMM_TAG);
+ //TraceManager.addDev("**** Adding COMM Tag to transition " + tr);
transitions.add(tr);
newStateD.addOutTransition(tr);
newState.addInTransition(tr);
@@ -418,6 +422,8 @@ public class AvatarCompactDependencyGraph {
// Make the graph
graph = new AUTGraph(states, transitions);
+ TraceManager.addDev("Graph done");
+
}
@@ -568,11 +574,13 @@ public class AvatarCompactDependencyGraph {
}
// Handling all nexts
+ //TraceManager.addDev("Handling all nexts");
//if (!(_elt instanceof AvatarActionOnSignal)) {
for (AvatarStateMachineElement eltN : _elt.getNexts()) {
makeCompactDependencyGraphForAvatarElement(bl, eltN, state, _elt, _states, _transitions, withID, null);
}
//}
+ //TraceManager.addDev("Done.");
return state;
}
@@ -994,5 +1002,131 @@ public class AvatarCompactDependencyGraph {
}*/
}
+ public void reduceGraph(String[] tags) {
+ // print transitions with COMM_TAG
+ /*TraceManager.addDev("Transition with COMM TAG - Total of transitions:" + graph.getTransitions().size());
+ for(AUTTransition tr: graph.getTransitions()) {
+ if (tr.hasTag(AUTGraph.COMM_TAG)) {
+ TraceManager.addDev("\t" + tr.toExtendedString());
+ }
+ }*/
+
+ // 1. We remove all vertices which tags are all in tags
+ ArrayList<AUTState> toBeRemoved = new ArrayList<>();
+ for(AUTState state: graph.getStates()) {
+ if ((state.referenceObject != null)) {
+ if (isTagged(state, tags)) {
+ toBeRemoved.add(state);
+ TraceManager.addDev("Removing first element: " + state + "/" + state.referenceObject);
+ removeCommElements(state, toBeRemoved);
+ }
+ }
+ }
+
+ TraceManager.addDev("Tagged states removed. Working on dependencies");
+
+ // 2. We iteratively remove elements with no backward dependencies that are not a start state, with no incoming edge
+ boolean modified = true;
+
+ while(modified) {
+ // We consider non-removed state. If they have no other dependency than nothing (but not a start state) or a remove state,
+ // they are added to remove
+ modified = false;
+ for(AUTState state: graph.getStates()) {
+ if (! toBeRemoved.contains(state)) {
+ if (!(hasStartStateInReference(state))) {
+ if (hasOnlyTransitionFromRemovedStatesOrComm(state, toBeRemoved)) {
+ toBeRemoved.add(state);
+ TraceManager.addDev("Removing secondary state: " + state + "/" + state.referenceObject + " of class " +
+ state.referenceObject.getClass());
+ // We also need to remove all states leading to the remove state if they are comm elements
+ removeCommElements(state, toBeRemoved);
+ modified = true;
+ }
+ }
+ }
+ }
+ }
+
+
+ // We finally remove the state
+ graph.removeStates(toBeRemoved);
+ removeReferencesOf(toBeRemoved);
+ }
+
+ public boolean hasOnlyTransitionFromRemovedStatesOrComm(AUTState state, ArrayList<AUTState>toBeRemoved) {
+ for(AUTTransition tr: state.inTransitions) {
+ if (!(tr.hasTag(AUTGraph.COMM_TAG))) {
+ AUTState previous = graph.getState(tr.origin);
+ if (!(toBeRemoved.contains(previous))) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
+ public void removeCommElements(AUTState state, ArrayList<AUTState>toBeRemoved) {
+ //TraceManager.addDev("Looking for comm transition starting from state " + state);
+ for(AUTTransition tr: state.outTransitions) {
+ AUTState next = graph.getState(tr.destination);
+ //TraceManager.addDev("Investigating transition " + tr.toExtendedString() + " from " + state + " TO " + next);
+ if (tr.hasTag(AUTGraph.COMM_TAG)) {
+ //TraceManager.addDev("Found comm tag in out transition from state " + state);
+ if (!toBeRemoved.contains(next)) {
+ //TraceManager.addDev("Removing comm state: " + state + "/" + state.referenceObject);
+ toBeRemoved.add(next);
+ }
+ }
+ }
+ }
+
+ public boolean hasStartStateInReference(AUTState state) {
+ if (state.referenceObject == null) {
+ return false;
+ }
+
+ if (!(state.referenceObject instanceof ArrayList)) {
+ return false;
+ }
+
+ ArrayList al = (ArrayList) (state.referenceObject);
+
+ for(Object o: al) {
+ if (o instanceof AvatarStartState) {
+ return true;
+ }
+ }
+
+ return false;
+
+ }
+
+ public boolean isTagged(AUTState state, String[] tags) {
+ if (state.referenceObject == null) {
+ return false;
+ }
+
+ if (!(state.referenceObject instanceof ArrayList)) {
+ return false;
+ }
+
+ ArrayList al = (ArrayList) (state.referenceObject);
+ if (al.size() > 0) {
+ for(Object o: al) {
+ //TraceManager.addDev("Investigating object: " + o.toString() + " for state " + state);
+ if (o instanceof CanBeTagged) {
+ if (Tags.hasAtLeastOneTagOf((CanBeTagged) o, tags)) {
+ //TraceManager.addDev("tagged");
+ return true;
+ }
+ }
+ }
+ }
+
+ return false;
+ }
+
+
}
diff --git a/src/main/java/avatartranslator/AvatarDependencyGraph.java b/src/main/java/avatartranslator/AvatarDependencyGraph.java
index 29152a8b35673610af64a12bb7f50d97ea942452..063d56b29943cee0bfaa783d05211930b41322c6 100644
--- a/src/main/java/avatartranslator/AvatarDependencyGraph.java
+++ b/src/main/java/avatartranslator/AvatarDependencyGraph.java
@@ -612,4 +612,6 @@ public class AvatarDependencyGraph {
}
+
+
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 8e8047808ef9a692202902a056dd09619e2ef5f9..f275dfbccef2b34fe8f70ecca47e624f4503c70b 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -1626,33 +1626,36 @@ public class Action extends Command implements ProVerifOutputListener {
return Interpreter.BAD;
}
- AvatarSpecification spec = interpreter.mgui.gtm.getAvatarSpecification();
+ AvatarSpecification spec = getAvatarSpecification(interpreter);
if (spec == null) {
return "No AVATAR specification";
}
- List<String> mutationList = null;
- try {
- mutationList = Files.readAllLines(new File(command).toPath());
- } catch (IOException e) {
- throw new RuntimeException(e);
- }
+ // 1. Generate Dependency graph from Avatar Spec
+ AvatarCompactDependencyGraph acdg = new AvatarCompactDependencyGraph();
+ acdg.buildGraph(spec, true);
- for (String mutationCommand:mutationList){
- try {
- AvatarMutation am = AvatarMutation.createFromString(mutationCommand);
- if (am != null) {
- am.apply(spec);
- }
- } catch (ParseMutationException e) {
- TraceManager.addDev("Exception in parsing mutation: " + e.getMessage());
- return e.getMessage();
- } catch (ApplyMutationException e) {
- TraceManager.addDev("Exception in applying mutation: " + e.getMessage());
- return e.getMessage();
- }
- }
+ RG rg = new RG("Dependency Graph");
+ rg.graph = acdg.getGraph();
+ rg.nbOfStates = rg.graph.getNbOfStates();
+ rg.nbOfTransitions = rg.graph.getNbOfTransitions();
+
+ interpreter.mgui.addRG(rg);
+
+ // 2. Reduce graph by removing elements with given tags + their dependencies
+ AvatarCompactDependencyGraph acdgReduced = acdg.clone();
+ acdgReduced.reduceGraph(commands);
+
+ rg = new RG("Dependency Graph");
+ rg.graph = acdgReduced.getGraph();
+ rg.nbOfStates = rg.graph.getNbOfStates();
+ rg.nbOfTransitions = rg.graph.getNbOfTransitions();
+
+ interpreter.mgui.addRG(rg);
+
+ // 3. Generate new Avatar spec
+ as = acdg.makeAvatarSpecification();
return null;
}
@@ -2741,6 +2744,7 @@ public class Action extends Command implements ProVerifOutputListener {
addAndSortSubcommand(makeMutationFromAvatar);
addAndSortSubcommand(makeComplexityAction);
addAndSortSubcommand(makeMutationBatchFromAvatar);
+ addAndSortSubcommand(optimizeAvatarSpecRemoveTags);
addAndSortSubcommand(drawAvatarSpec);
addAndSortSubcommand(avatarSimulationToBrk);
addAndSortSubcommand(avatarSimulationSelectTrace);
diff --git a/src/main/java/common/Tags.java b/src/main/java/common/Tags.java
index 8e3584e91f17d8fc3db3ad81dc157f9918cc6f69..0157db22417c45dc869b6cd4c92111fffc0e377f 100644
--- a/src/main/java/common/Tags.java
+++ b/src/main/java/common/Tags.java
@@ -41,6 +41,8 @@
package common;
+import myutil.TraceManager;
+
import java.util.ArrayList;
import java.util.List;
@@ -123,6 +125,33 @@ public class Tags implements CanBeTagged {
return ret.trim();
}
+ public static boolean hasAtLeastOneTagOf(CanBeTagged cbt, String[] tags) {
+ for(String t: tags) {
+ if (cbt.hasTag(t)) {
+ //TraceManager.addDev("Tag found:>" + t + "<");
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public static boolean hasNoExtraTag(CanBeTagged cbt, String[] tags) {
+ for(Tag t: cbt.getAllTags()) {
+ boolean found = false;
+ for(String s: tags) {
+ if (t.getTag().compareTo(s) == 0) {
+
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ return false;
+ }
+ }
+ return true;
+ }
+
diff --git a/src/main/java/graph/AUTGraph.java b/src/main/java/graph/AUTGraph.java
index 46745c872d7d5db70926ac0f6f8a19b9b20661a5..d93bce91e99339e8276ea5a335ded6ef075790fc 100755
--- a/src/main/java/graph/AUTGraph.java
+++ b/src/main/java/graph/AUTGraph.java
@@ -553,6 +553,11 @@ public class AUTGraph implements myutil.Graph {
for (AUTTransition tr : transitions) {
AUTTransition newTr = new AUTTransition(tr.origin, tr.transition, tr.destination);
+ if (tr.tags != null) {
+ for(AUTTag t: tr.tags) {
+ newTr.addTag(t);
+ }
+ }
trN.add(newTr);
// Update receiving and destination states
AUTState s = statesN.get(tr.origin);
diff --git a/src/main/java/graph/AUTTransition.java b/src/main/java/graph/AUTTransition.java
index 5825d7ddd4069db0f25c1e29ab4467bad584e982..f9b0bd0592e4d77a5ce3a1ff4c1b66b71be2869c 100755
--- a/src/main/java/graph/AUTTransition.java
+++ b/src/main/java/graph/AUTTransition.java
@@ -93,6 +93,25 @@ public class AUTTransition implements Comparable<AUTTransition> {
return "(" + origin + " ," + transition + ", " + destination + ")";
}
+ public String toExtendedString() {
+ return "(" + origin + " ," + transition + ", " + destination + ") AUTTag:" + AUTTagsToString();
+ }
+
+
+ public String AUTTagsToString() {
+ if ((tags == null) || tags.size() == 0) {
+ return "";
+ }
+
+ String ret = "";
+ for(AUTTag t: tags) {
+ ret += t.getID() + " ";
+ }
+ return ret.trim();
+
+
+ }
+
public String getLabel() {
int index0 = transition.indexOf("(");
int index1 = transition.indexOf(")");