GistController.java
Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025 package org.gecode.gist;
00026
00027 import org.gecode.*;
00028 import org.gecode.gist.postscript.*;
00029 import java.util.Hashtable;
00030 import java.util.Enumeration;
00031 import java.io.File;
00032
00033 public class GistController
00034 implements StatisticsListener {
00035
00036 private Space _rootSpace;
00037 private boolean _bab;
00038
00039 private SpaceNode _root;
00040 private SpaceNode _currentNode;
00041
00042 private GistUIInterface _ui;
00043
00044 private Statistics _stats;
00045 private int breakAfterSolutions = 0;
00046 private int solutionsSinceBreak = 0;
00047 private int breakAfterNodes = 0;
00048 private int nodesSinceBreak = 0;
00049 private boolean cancelSearch = false;
00050
00051 private Hashtable<String, GistEventListener> _actionTable;
00052 private String _selectedAction;
00053
00054 public GistController(Space rootSpace, boolean bab) {
00055 _rootSpace = rootSpace;
00056 _bab = bab;
00057 _stats = new Statistics();
00058 _stats.registerSolutionListener(this);
00059 _actionTable = new Hashtable<String, GistEventListener>();
00060 _selectedAction = "default";
00061 if (rootSpace instanceof GistEventListener) {
00062 GistEventListener e = (GistEventListener) rootSpace;
00063 _actionTable.put(e.getName(), e);
00064 _selectedAction=e.getName();
00065 }
00066 }
00067
00068 public void selectInspectionAction(String action) {
00069 _selectedAction = action;
00070 }
00071 public String getSelectedAction() {
00072 return _selectedAction;
00073 }
00074 public Enumeration<String> getListeners() {
00075 return _actionTable.keys();
00076 }
00077
00078 public void registerUI(GistUIInterface ui) {
00079 _ui = ui;
00080 _rootSpace.status(new long[1]);
00081 if (_rootSpace.failed()) {
00082 _root = ui.createRoot(_rootSpace, _bab, _stats);
00083 } else {
00084 _root = ui.createRoot(_rootSpace.cloneSpace(), _bab, _stats);
00085 }
00086 _currentNode = _root;
00087 _root.layout();
00088 }
00089
00090 public void exploreOne() {
00091 breakAfterSolutions = 1;
00092 solutionsSinceBreak = 0;
00093 breakAfterNodes = Config.searchCutoff();
00094 nodesSinceBreak = 0;
00095 cancelSearch = false;
00096 DFS dfs = new DFS();
00097 dfs.setup(_currentNode);
00098 while ( (!dfs.step()) && (!cancelSearch) );
00099 searchDone();
00100 }
00101
00102 public void exploreAll() {
00103 breakAfterSolutions = 0;
00104 breakAfterNodes = Config.searchCutoff();
00105 nodesSinceBreak = 0;
00106 cancelSearch = false;
00107 DFS dfs = new DFS();
00108 dfs.setup(_currentNode);
00109 while ( (!dfs.step()) && (!cancelSearch) );
00110 searchDone();
00111 }
00112
00113 public void exploreN() {
00114 breakAfterSolutions = Config.n();
00115 solutionsSinceBreak = 0;
00116 breakAfterNodes = Config.searchCutoff();
00117 nodesSinceBreak = 0;
00118 cancelSearch = false;
00119 DFS dfs = new DFS();
00120 dfs.setup(_currentNode);
00121 while ( (!dfs.step()) && (!cancelSearch) );
00122 searchDone();
00123 }
00124
00125 public void reset() {
00126 _stats.reset();
00127 if (_rootSpace.failed()) {
00128 _root = _ui.createRoot(_rootSpace, _bab, _stats);
00129 } else {
00130 _root = _ui.createRoot(_rootSpace.cloneSpace(), _bab, _stats);
00131 }
00132 _currentNode = _root;
00133 _root.dirtyUp();
00134 stateChanged();
00135 }
00136
00137 public void saveAs() {
00138 File file = _ui.saveFilename();
00139 if (file != null) {
00140 String fn = file.getName().toLowerCase();
00141 if (! (fn.endsWith(".eps") || fn.endsWith(".ps") ) ) {
00142 file = new File(file.getParentFile(), fn+".eps");
00143 }
00144 if (file.exists() && ! _ui.overwriteDialog() ) {
00145 return;
00146 }
00147 try {
00148 Postscript.saveAs(_root,file);
00149 } catch (java.io.IOException e) {
00150 _ui.reportError("Error",
00151 "Error while saving postscript file:\n"
00152 +e.getMessage());
00153 }
00154 }
00155 }
00156
00157 public void addEventListener(GistEventListener e) {
00158 _actionTable.put(e.getName(), e);
00159 _selectedAction=e.getName();
00160 _ui.updateEventListeners();
00161 }
00162
00163 public void setCurrentNode(SpaceNode c) {
00164 _currentNode = c;
00165 _ui.setCurrentNode(c);
00166 switch (_currentNode.getStatus()) {
00167 case FAILED :
00168 _ui.menuInspectActive(false, _currentNode.isRoot(), true);
00169 _ui.menuSearchActive(false);
00170 _ui.menuHideNodeActive(false, false);
00171 _ui.menuUnhideAllActive(false);
00172 _ui.menuHideFailedActive(false);
00173 break;
00174 case SOLVED:
00175 _ui.menuInspectActive(true, _currentNode.isRoot(), true);
00176 _ui.menuSearchActive(false);
00177 _ui.menuHideNodeActive(false, false);
00178 _ui.menuUnhideAllActive(false);
00179 _ui.menuHideFailedActive(false);
00180 break;
00181 case UNDETERMINED :
00182 _ui.menuInspectActive(true, _currentNode.isRoot(), false);
00183 _ui.menuSearchActive(true);
00184 _ui.menuHideNodeActive(false, false);
00185 _ui.menuUnhideAllActive(false);
00186 _ui.menuHideFailedActive(false);
00187 break;
00188 default:
00189 _ui.menuInspectActive(!_currentNode.isHidden(),
00190 _currentNode.isRoot(), false);
00191 _ui.menuSearchActive(!_currentNode.isHidden() &&
00192 _currentNode.isOpen());
00193 _ui.menuHideNodeActive(true, _currentNode.isHidden());
00194 _ui.menuUnhideAllActive(true);
00195 _ui.menuHideFailedActive(!_currentNode.isHidden());
00196 break;
00197 }
00198 }
00199
00200 public SpaceNode getCurrentNode() {
00201 return _currentNode;
00202 }
00203
00204 private void invokeAction(SpaceNode node) {
00205 if (_selectedAction.equals("default")) {
00206 _ui.inspect(node.getSpace().toString());
00207 } else {
00208 GistEventListener el = _actionTable.get(_selectedAction);
00209 if (el != null) {
00210 el.nodeClickEvent(_ui, node);
00211 }
00212 }
00213 }
00214
00215 public void inspect() {
00216 if (_currentNode.isHidden()) {
00217 toggleHidden();
00218 return;
00219 }
00220 switch (_currentNode.getStatus()) {
00221 case UNDETERMINED:
00222 {
00223 DFS dfs = new DFS();
00224 dfs.setup(_currentNode);
00225 dfs.step();
00226 stateChanged();
00227 break;
00228 }
00229 case FAILED:
00230 break;
00231 default:
00232 invokeAction(_currentNode);
00233 break;
00234 }
00235
00236 }
00237
00238 public void inspectBranches() {
00239 if (_currentNode.isHidden()) {
00240 toggleHidden();
00241 return;
00242 }
00243 switch (_currentNode.getStatus()) {
00244 case FAILED :
00245 break;
00246 case SOLVED:
00247 inspect();
00248 break;
00249 case UNDETERMINED:
00250 {
00251 DFS dfs = new DFS();
00252 dfs.setup(_currentNode);
00253 dfs.step();
00254 stateChanged();
00255 inspectBranches();
00256 break;
00257 }
00258 default:
00259 {
00260 String out = "";
00261 Space s = _currentNode.getSpace();
00262 s.status(new long[1]);
00263 long alt = s.description().alternatives();
00264 out += "There are " + alt + " branches available:\n";
00265 for (int i = 0; i < alt; ++i) {
00266 out += "Branch " + i + "\n";
00267 Space v = s.cloneSpace();
00268 v.status(new long[1]);
00269 BranchingDesc desc = v.description();
00270 v.commit(desc, i);
00271 out += "\t" + v.toString().replaceAll("\n", "\n\t").trim() + "\n";
00272 }
00273 _ui.inspect(out);
00274 break;
00275 }
00276 }
00277 }
00278
00279 public void inspectBeforePropagation() {
00280 if (_currentNode == _root) return;
00281 if (_currentNode.isHidden()) {
00282 toggleHidden();
00283 return;
00284 }
00285 switch (_currentNode.getStatus()) {
00286 case UNDETERMINED:
00287 {
00288 DFS dfs = new DFS();
00289 dfs.setup(_currentNode);
00290 dfs.step();
00291 stateChanged();
00292 inspectBeforePropagation();
00293 break;
00294 }
00295 default:
00296 {
00297 String out = "Before propagation:\n";
00298 Space s = ((SpaceNode)_currentNode.getParent()).getSpace();
00299 s.status(new long[1]);
00300 BranchingDesc desc = s.description();
00301 s.commit(desc, _currentNode.getAlternative());
00302 out += "\t" + s.toString().replaceAll("\n", "\n\t").trim() + "\n";
00303 _ui.inspect(out);
00304 break;
00305 }
00306 }
00307 }
00308
00313 public int[] getStatistics() {
00314 int[] res = new int[5];
00315
00316 res[0] = _stats.getSolutions();
00317 res[1] = _stats.getFailures();
00318 res[2] = _stats.getChoices();
00319 res[3] = _stats.getUndetermined();
00320 res[4] = _stats.getDepth();
00321
00322 return res;
00323 }
00324
00325 public SpaceNode getRoot() {
00326 return _root;
00327 }
00328
00329 public void toggleHidden() {
00330 _currentNode.toggleHidden();
00331 stateChanged();
00332 }
00333 public void hideFailed() {
00334 _currentNode.hideFailed();
00335 stateChanged();
00336 }
00337 public void unhideAll() {
00338 _currentNode.unhideAll();
00339 stateChanged();
00340 }
00341
00342 public void newSolution(int solutions) {
00343 solutionsSinceBreak++;
00344 if (breakAfterSolutions != 0 &&
00345 solutionsSinceBreak>=breakAfterSolutions)
00346 cancelSearch = true;
00347 }
00348
00349 public void newNode() {
00350 nodesSinceBreak++;
00351 if (breakAfterNodes != 0 &&
00352 nodesSinceBreak>=breakAfterNodes)
00353 cancelSearch = true;
00354 }
00355
00356 public void scaleToFit() {
00357 _ui.scaleToFit();
00358 }
00359
00360 public void searchDone() {
00361 if (Config.hide())
00362 _currentNode.hideFailed();
00363 stateChanged();
00364 }
00365
00366 private void stateChanged() {
00367 _root.layout();
00368 if (Config.zoom())
00369 _ui.scaleToFit();
00370 _ui.update();
00371 setCurrentNode(_currentNode);
00372 }
00373
00374
00375 public void navUp() {
00376 SpaceNode p = (SpaceNode) _currentNode.getParent();
00377 if (p != null)
00378 setCurrentNode(p);
00379 }
00380 public void navDown() {
00381 if (_currentNode.getStatus() == NodeStatus.BRANCH &&
00382 !_currentNode.isHidden())
00383 setCurrentNode((SpaceNode)_currentNode.getChild(0));
00384 }
00385 public void navLeft() {
00386 SpaceNode p = (SpaceNode) _currentNode.getParent();
00387 if (p != null) {
00388 int alt = _currentNode.getAlternative();
00389 if (alt > 0)
00390 setCurrentNode((SpaceNode) p.getChild(alt-1));
00391 }
00392 }
00393 public void navRight() {
00394 SpaceNode p = (SpaceNode) _currentNode.getParent();
00395 if (p != null) {
00396 int alt = _currentNode.getAlternative();
00397 if (alt + 1 < p.getNumberOfChildren())
00398 setCurrentNode((SpaceNode) p.getChild(alt+1));
00399 }
00400 }
00401
00402 private void findNextSolution(SpaceNode current) {
00403 SpaceNode p = current;
00404 int alt;
00405 while (true) {
00406 if (p.getStatus() == NodeStatus.SOLVED) {
00407 setCurrentNode(p);
00408 return;
00409 } else if (p.hasSolvedChildren()) {
00410 p = (SpaceNode) p.getChild(0);
00411 } else if (p.getParent() != null) {
00412 SpaceNode pp = (SpaceNode)p.getParent();
00413 alt = p.getAlternative();
00414 if (alt + 1 < pp.getNumberOfChildren()) {
00415 p = (SpaceNode)pp.getChild(alt+1);
00416 } else {
00417 return;
00418 }
00419 } else {
00420 return;
00421 }
00422 }
00423 }
00424
00425 public void jumpNextSol() {
00426
00427 if (_currentNode.getStatus() != NodeStatus.SOLVED &&
00428 _currentNode.hasSolvedChildren()) {
00429 findNextSolution(_currentNode);
00430 return;
00431 }
00432
00433 SpaceNode p = (SpaceNode) _currentNode.getParent();
00434 int alt = _currentNode.getAlternative();
00435 while (p != null) {
00436 if (alt + 1 < p.getNumberOfChildren() &&
00437 ((SpaceNode)p.getChild(alt+1)).hasSolvedChildren() ) {
00438 p = (SpaceNode) p.getChild(alt+1);
00439 findNextSolution(p);
00440 return;
00441 } else {
00442 alt = p.getAlternative();
00443 p = (SpaceNode) p.getParent();
00444 }
00445 }
00446 }
00447 public void jumpPrevSol() {
00448 SpaceNode p = (SpaceNode) _currentNode.getParent();
00449 int alt = _currentNode.getAlternative();
00450 while (p != null) {
00451 if (alt > 0 &&
00452 ((SpaceNode)p.getChild(alt-1)).hasSolvedChildren() ) {
00453
00454 p = (SpaceNode) p.getChild(alt-1);
00455
00456 while (true) {
00457 if (p.getStatus() == NodeStatus.SOLVED) {
00458 setCurrentNode(p);
00459 return;
00460 } else if (p.hasSolvedChildren()) {
00461 p = (SpaceNode) p.getChild(p.getNumberOfChildren()-1);
00462 } else if (p.getParent() != null) {
00463 SpaceNode pp = (SpaceNode)p.getParent();
00464 alt = p.getAlternative();
00465 if (alt > 0) {
00466 p = (SpaceNode)pp.getChild(alt-1);
00467 } else {
00468 return;
00469 }
00470 } else {
00471 return;
00472 }
00473 }
00474 } else {
00475 alt = p.getAlternative();
00476 p = (SpaceNode) p.getParent();
00477 }
00478 }
00479
00480 }
00481
00482 public void jumpRoot() {
00483 setCurrentNode(_root);
00484 }
00485 public void jumpLeftmost() {
00486 SpaceNode p = _root;
00487 while (p.getNumberOfChildren() > 0) {
00488 p = (SpaceNode) p.getChild(0);
00489 }
00490 setCurrentNode(p);
00491 }
00492 public void jumpRightmost() {
00493 SpaceNode p = _root;
00494 while (p.getNumberOfChildren() > 0) {
00495 p = (SpaceNode) p.getChild(p.getNumberOfChildren()-1);
00496 }
00497 setCurrentNode(p);
00498 }
00499
00500 public void centerCursor() {
00501 _ui.centerCursor();
00502 }
00503 }