Skip to content
Snippets Groups Projects
Commit 1e295b11 authored by apvrille's avatar apvrille
Browse files

Update on minimization

parent 3849d056
No related branches found
No related tags found
No related merge requests found
......@@ -501,6 +501,7 @@ public class AUTGraph implements myutil.Graph {
while(modif) {
modif = removeTauTr();
}
statesComputed = false;
}
// Remove transition going from one state with only one tau transition as output
......@@ -513,15 +514,31 @@ public class AUTGraph implements myutil.Graph {
tr = st.outTransitions.get(0);
if (tr.isTau) {
transitions.remove(tr);
st.outTransitions.clear();
AUTState st1 = states.get(tr.destination);
if (st1 != st) {
toRemoveStates.add(st1);
// Must put all incoming transition to the new state
for(AUTTransition trM :st.inTransitions) {
trM.destination = tr.destination;
TraceManager.addDev("Removing state " + st1.id);
// Must put all incoming transition to the first state
st1.inTransitions.remove(tr);
for(AUTTransition trM: st1.inTransitions) {
trM.destination = st.id;
st.inTransitions.add(trM);
TraceManager.addDev("New in transitions " + trM);
}
st1.inTransitions = st.inTransitions;
st1.inTransitions.clear();
// Out transitions
st.outTransitions.clear();
for(AUTTransition trM: st1.outTransitions) {
st.outTransitions.add(trM);
trM.origin = st.id;
TraceManager.addDev("New out transitions " + trM);
}
st1.outTransitions.clear();
}
}
}
......@@ -529,27 +546,49 @@ public class AUTGraph implements myutil.Graph {
// Remove all states and adapt the id in the graph
for(AUTState str: toRemoveStates) {
TraceManager.addDev("Removing really state " + str.id);
// Last state of the array?
if (str.id == nbState - 1) {
if (str.id == (nbState - 1)) {
TraceManager.addDev("Last state " + str.id);
nbState --;
states.remove(str.id);
// str not at the end: we replace it with the last state
// We need to accordingly update
} else {
AUTState moved = states.get(nbState-1);
TraceManager.addDev("Moving state " + moved.id + " to index " + str.id);
states.set(str.id, moved);
states.remove(nbState-1);
nbState --;
moved.updateID(str.id);
}
states.remove(nbState-1);
nbState --;
AUTTransition tt = findTransitionWithId(nbState);
if (tt != null) {
TraceManager.addDev("1) Transition with id not normal" + tt);
}
moved.updateID(str.id);
tt = findTransitionWithId(nbState);
if (tt != null) {
TraceManager.addDev("2) Transition with id not normal" + tt);
}
}
return true;
}
return false;
}
return false;
}
private AUTTransition findTransitionWithId(int id) {
for (AUTTransition tr: transitions) {
if ((tr.origin == id) || (tr.destination == id)) {
return tr;
}
}
return null;
}
}
......@@ -365,7 +365,7 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
listProjected.setEnabled(true);
listIgnored.setEnabled(true);
setButtonsList();
start.setEnabled(sortedListProjected.size() > 0);
start.setEnabled(sortedListIgnored.size() > 0);
stop.setEnabled(false);
close.setEnabled(true);
getGlassPane().setVisible(false);
......@@ -504,14 +504,13 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
computeListOfActions();
return;
}
jta.append("\nMinimizing graph...\n");
String[] strarray = new String[sortedListProjected.size()];
sortedListProjected.toArray(strarray );
String[] strarray = new String[sortedListIgnored.size()];
sortedListIgnored.toArray(strarray );
newRG.graph.minimize(strarray);
newRG.nbOfStates = rg.graph.getNbOfStates();
newRG.nbOfTransitions = rg.graph.getTransitions().size();
newRG.nbOfStates = newRG.graph.getNbOfStates();
newRG.nbOfTransitions = newRG.graph.getTransitions().size();
mgui.addRG(newRG);
jta.append("\nGraph minimized: " + newRG.nbOfStates + " states, " + newRG.nbOfTransitions + " transitions\n");
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment