Commit 8d2a6080 authored by Ludovic Apvrille's avatar Ludovic Apvrille

Adding minimization alfos debugged

parent 41780b51
......@@ -23,6 +23,7 @@ BUILD_TO_MODIFY = src/ui/DefaultText.java
TTOOL_BINARY = ttool.jar
LAUNCHER_BINARY = launcher.jar
GRAPHSHOW_BINARY = graphshow.jar
GRAPHMINIMIZE_BINARY = graphminimize.jar
TIFTRANSLATOR_BINARY = tiftranslator.jar
TMLTRANSLATOR_BINARY = tmltranslator.jar
GSCORE_BINARY = gs-core-1.3.jar
......@@ -36,6 +37,7 @@ RUNDSE_JAR_TXT = rundse.txt
TTOOL_JAR_TXT = ttool.txt
LAUNCHER_JAR_TXT = launcher.txt
GRAPHSHOW_JAR_TXT = graphshow.txt
GRAPHMINIMIZE_JAR_TXT = graphminimize.txt
TIFTRANSLATOR_JAR_TXT = tiftranslator.txt
TMLTRANSLATOR_JAR_TXT = tmltranslator.txt
WEBCRAWLER_SERVER_JAR_TXT = webcrawler.txt
......@@ -98,7 +100,7 @@ RELEASE_STD_FILES_WINDIWS_EXE = ttool_windows.bat
RELEASE_STD_FILES_XML = TURTLE/manual-HW.xml AVATAR/DrinkMachineV10.xml TURTLE/WebV01.xml TURTLE/Protocol_example1.xml TURTLE/BasicExchange.xml DIPLODOCUS/SmartCardProtocol.xml TURTLE/ProtocolPatterns.xml CTTool/COCOME_V50.xml AVATAR/CoffeeMachine_Avatar.xml AVATAR/Network_Avatar.xml AVATAR/MicroWaveOven_SafetySecurity_fullMethodo.xml
RELEASE_STD_FILES_LIB = TURTLE/TClock1.lib TURTLE/TTimerv01.lib
RELEASE_STD_FILES_BIN = $(LAUNCHER_BINARY) $(TTOOL_BINARY) $(TIFTRANSLATOR_BINARY) $(TMLTRANSLATOR_BINARY) $(REMOTESIMULATOR_BINARY) $(RUNDSE_BINARY) $(WEBCRAWLER_SERVER_BINARY) $(WEBCRAWLER_CLIENT_BINARY) $(GRAPHSHOW_BINARY)
RELEASE_STD_FILES_BIN = $(LAUNCHER_BINARY) $(TTOOL_BINARY) $(TIFTRANSLATOR_BINARY) $(TMLTRANSLATOR_BINARY) $(REMOTESIMULATOR_BINARY) $(RUNDSE_BINARY) $(WEBCRAWLER_SERVER_BINARY) $(WEBCRAWLER_CLIENT_BINARY) $(GRAPHSHOW_BINARY) $(GRAPHMINIMIZE_BINARY)
RELEASE_STD_FILES_LICENSES = LICENSE LICENSE_CECILL_ENG LICENSE_CECILL_FR
TEST_DIR = $(TTOOL_PATH)/tests
......@@ -165,7 +167,7 @@ basic:
jarttool: launcher ttooljar
jar: launcher ttooljar tiftranslator tmltranslator rundse remotesimulator webcrawler graphshow
jar: launcher ttooljar tiftranslator tmltranslator rundse remotesimulator webcrawler graphshow graphminimize
ttooljar:
rm -f $(TTOOL_BIN)/$(TTOOL_BINARY)
......@@ -176,8 +178,12 @@ launcher:
rm -f $(TTOOL_BIN)/$(LAUNCHER_BINARY)
cd $(TTOOL_SRC);$(JAR) cmf $(LAUNCHER_JAR_TXT) $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class myutil/*.class
graphminimize:
rm -f $(TTOOL_BIN)/$(GRAPHMINIMIZE_BINARY)
cd $(TTOOL_SRC);$(JAR) cmf $(GRAPHMINIMIZE_JAR_TXT) $(TTOOL_BIN)/$(GRAPHMINIMIZE_BINARY) GraphMinimize.class myutil/*.class ui/graph/*.class
graphshow:
rm -f $(TTOOL_BIN)/$(TIFTRANSLATOR_BINARY)
rm -f $(TTOOL_BIN)/$(GRAPHSHOW_BINARY)
cd $(TTOOL_SRC);$(JAR) cmf $(GRAPHSHOW_JAR_TXT) $(TTOOL_BIN)/$(GRAPHSHOW_BINARY) GraphShow.class myutil/*.class ui/graph/*.class ui/IconManager.class ui/file/PNGFilter.class
tiftranslator:
......
This diff is collapsed.
Main-Class: GraphShow
Class-Path: ./gs-core-1.3.jar ./gs-ui-1.3.jar
......@@ -489,7 +489,7 @@ public class AUTGraph implements myutil.Graph {
}
public void minimizeRemoveInternal() {
public void minimizeRemoveInternal(boolean tauOnly) {
String s = "tau";
// mark all transitions as non tau
......@@ -507,11 +507,11 @@ public class AUTGraph implements myutil.Graph {
}
minimizeTau();
minimizeTau(tauOnly);
}
public void minimize(String [] tauTransitions) {
public void minimize(String [] tauTransitions, boolean tauOnly) {
String s = "tau";
// mark all transitions as non tau
......@@ -529,17 +529,21 @@ public class AUTGraph implements myutil.Graph {
}
}
minimizeTau();
minimizeTau(tauOnly);
}
public void minimizeTau() {
public void minimizeTau(boolean tauOnly) {
boolean modif = true;
//TraceManager.addDev(toFullString());
factorizeNonTauTransitions();
if (tauOnly) {
return;
}
/*while(modif) {
modif = removeOnlyOneTauTr();
......@@ -556,7 +560,6 @@ public class AUTGraph implements myutil.Graph {
partitionGraph();
statesComputed = false;
}
// Remove transition going from one state with only one tau transition as output
......@@ -792,13 +795,12 @@ public class AUTGraph implements myutil.Graph {
TraceManager.addDev("2) Transition with id not normal" + tt);
}*/
}
//TraceManager.addDev(toFullString());
}
}
// Removes all tau transition of a state, replacing them with reachable non tau transitions
// A tau transition reaching a end state cannot be removed but can be replaced with a unique transition
// A tau transition reaching an end state cannot be removed but can be replaced with a unique transition
private void factorizeNonTauTransitions() {
boolean modif = false;
boolean endState = false;
......@@ -807,10 +809,7 @@ public class AUTGraph implements myutil.Graph {
st1.met = false;
}
// Remove tr if it is duplicated
for(AUTState st: states) {
// We ignore states with no input tr apart from the start state (id 0)
//TraceManager.addDev("0. state " + st.id);
for (AUTState st: states) {
if ((st.id == 0) || (st.getNbInTransitions() > 0)) {
//TraceManager.addDev(" 1. state " + st.id);
if (st.hasOutputTauTransition()) {
......@@ -823,8 +822,23 @@ public class AUTGraph implements myutil.Graph {
TraceManager.addDev("\t" + tr);
}*/
//TraceManager.addDev("State " + st.id + " can reach an end state with tau tr only?" + canReachAnEndStateWithTau);
st.met = canReachAnEndStateWithTau;
endState = endState || canReachAnEndStateWithTau;
}
}
}
// Remove tr if it is duplicated
for(AUTState st: states) {
// We ignore states with no input tr apart from the start state (id 0)
//TraceManager.addDev("0. state " + st.id);
if ((st.id == 0) || (st.getNbInTransitions() > 0)) {
//TraceManager.addDev(" 1. state " + st.id);
if (st.hasOutputTauTransition()) {
//TraceManager.addDev(" 2. state " + st.id);
LinkedList<AUTTransition> nonTauTransitions = new LinkedList<AUTTransition>();
getAllNonTauTransitionsFrom(st, nonTauTransitions);
// Create these transitions in st if not yet existing
//TraceManager.addDev("Remove tau\n" + toFullString());
......@@ -836,22 +850,41 @@ public class AUTGraph implements myutil.Graph {
}
}
// Remove all non reachable state
//removeAllNonReachableStates();
// If end state: we must create a new end state, and all "met" states should have a tau transition
// to this state
if (endState) {
// We must see if at least one met state has output transitions
boolean hasEndState = false;
for(AUTState st: states) {
if (st.met) {
if (st.outTransitions.size() > 0) {
hasEndState = true;
break;
}
}
}
if (hasEndState) {
int newId = states.size();
AUTState endSt = new AUTState(newId);
states.add(endSt);
nbState = states.size();
for(AUTState st: states) {
if (st.met) {
AUTTransition tr = new AUTTransition(st.id, "tau", endSt.id);
for(AUTState st1: states) {
if (st1.met) {
if (st1.outTransitions.size() > 0) {
TraceManager.addDev("Adding an end tau to state " + st1.id);
AUTTransition tr = new AUTTransition(st1.id, "tau", endSt.id);
tr.isTau = true;
transitions.add(tr);
st.addOutTransition(tr);
st1.addOutTransition(tr);
endSt.addInTransition(tr);
}
st.met = false;
}
st1.met = false;
}
}
}
//TraceManager.addDev(toFullString());
......@@ -970,7 +1003,7 @@ public class AUTGraph implements myutil.Graph {
statesToConsider.addAll(nextStatesToConsider);
}
//TraceManager.addDev("Found " + cpt + " reachable states");
TraceManager.addDev("Found " + cpt + " reachable states");
ArrayList<AUTState> toRemoveStates = new ArrayList<AUTState>();
for(AUTState st2: states) {
if (!(st2.met)) {
......@@ -979,7 +1012,13 @@ public class AUTGraph implements myutil.Graph {
}
}
//TraceManager.addDev(toFullString());
removeStates(toRemoveStates);
//TraceManager.addDev(toFullString());
//statesComputed = false;
//states = null;
//computeStates();
}
......@@ -1111,10 +1150,7 @@ public class AUTGraph implements myutil.Graph {
}
}
<<<<<<< Upstream, based on aa363fe017f226394c627b60189e75002e6b1199
=======
TraceManager.addDev("-----------------\n");
>>>>>>> d0df681 Update on algo management
}
......@@ -1232,7 +1268,7 @@ public class AUTGraph implements myutil.Graph {
}
// Assumes AUTElement have been added to transitions
public AUTGraph generateGraph(AUTPartition partition, HashMap<String, AUTElement> _alphabet) {
public void generateGraph(AUTPartition partition, HashMap<String, AUTElement> _alphabet) {
ArrayList<AUTState> sts = new ArrayList<AUTState>();
ArrayList<AUTTransition> trs = new ArrayList<AUTTransition>();
HashMap<AUTBlock, AUTState> blockToNewStates = new HashMap<AUTBlock, AUTState>();
......@@ -1280,9 +1316,11 @@ public class AUTGraph implements myutil.Graph {
}
}
AUTGraph newGraph = new AUTGraph(sts, trs);
TraceManager.addDev("New graph: " + newGraph.toFullString());
return newGraph;
states = sts;
transitions = trs;
nbState = sts.size();
TraceManager.addDev("New graph: " + toFullString());
}
......
......@@ -178,7 +178,7 @@ public class AUTState implements Comparable<AUTState> {
ArrayList<AUTTransition> outTransitions2 = new ArrayList<AUTTransition>();
for(AUTTransition tr: outTransitions) {
if (!(tr.isTau)) {
outTransitions.add(tr);
outTransitions2.add(tr);
} else {
_transitions.remove(tr);
_states.get(tr.destination).removeInTransition(tr);
......@@ -215,6 +215,7 @@ public class AUTState implements Comparable<AUTState> {
outTransitions.remove(tr);
}
toBeRemoved.clear();
for(AUTTransition tr: inTransitions) {
if (tr.origin == id) {
toBeRemoved.add(tr);
......
......@@ -93,7 +93,8 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
protected JTextArea jta;
private JCheckBox removeInternalActions;
private JRadioButton tauOnly;
private JRadioButton allMinimization;
// Main Panel
......@@ -168,7 +169,14 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
panel4.setBorder(new javax.swing.border.TitledBorder("Minimization: tools and options"));
removeInternalActions = new JCheckBox("Remove internal actions");
removeInternalActions.setEnabled(true);
tauOnly = new JRadioButton("Only remove tau transitions");
tauOnly.setEnabled(true);
allMinimization = new JRadioButton("Complete minimization [Experimental]");
allMinimization.setEnabled(true);
ButtonGroup bt = new ButtonGroup();
bt.add(tauOnly);
bt.add(allMinimization);
allMinimization.setSelected(true);
//c4.anchor = GridBagConstraints.EAST;
c4.weighty = 1.0;
......@@ -177,6 +185,8 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
c4.fill = GridBagConstraints.HORIZONTAL;
c4.gridheight = 1;
panel4.add(removeInternalActions, c4);
panel4.add(tauOnly, c4);
panel4.add(allMinimization, c4);
panelTop.add(panel4, BorderLayout.SOUTH);
......@@ -365,7 +375,7 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
listProjected.setEnabled(true);
listIgnored.setEnabled(true);
setButtonsList();
start.setEnabled(sortedListIgnored.size() > 0);
start.setEnabled(true);
stop.setEnabled(false);
close.setEnabled(true);
getGlassPane().setVisible(false);
......@@ -508,7 +518,31 @@ public class JFrameMinimize extends javax.swing.JFrame implements ActionListener
jta.append("\nMinimizing graph...\n");
String[] strarray = new String[sortedListIgnored.size()];
sortedListIgnored.toArray(strarray );
newRG.graph.minimize(strarray);
if (removeInternalActions.isSelected()) {
int toBeRemoved = 0;
for(String s: sortedListProjected) {
if (s.startsWith("i(")) {
toBeRemoved ++;
}
}
if (toBeRemoved > 0) {
String[] allstr = new String[strarray.length + toBeRemoved];
for(int i=0; i<strarray.length; i++) {
allstr[i] = strarray[i];
}
int index = strarray.length;
for(String s: sortedListProjected) {
if (s.startsWith("i(")) {
allstr[index] = s;
index++;
}
}
strarray = allstr;
}
}
newRG.graph.minimize(strarray, tauOnly.isSelected());
newRG.nbOfStates = newRG.graph.getNbOfStates();
newRG.nbOfTransitions = newRG.graph.getTransitions().size();
mgui.addRG(newRG);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment