Source Code Cross Referenced for BackTrackingManager.java in  » Testing » KeY » de » uka » ilkd » key » strategy » feature » instantiator » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.strategy.feature.instantiator 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


001:        // This file is part of KeY - Integrated Deductive Software Design
002:        // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003:        //                         Universitaet Koblenz-Landau, Germany
004:        //                         Chalmers University of Technology, Sweden
005:        //
006:        // The KeY system is protected by the GNU General Public License. 
007:        // See LICENSE.TXT for details.
008:        //
009:        //
010:
011:        package de.uka.ilkd.key.strategy.feature.instantiator;
012:
013:        import java.util.ArrayList;
014:        import java.util.Stack;
015:
016:        import de.uka.ilkd.key.rule.RuleApp;
017:
018:        /**
019:         * Manager for the <code>ChoicePoint</code>s that can occur during the
020:         * evaluation of a feature term, taking care of the different branches offered
021:         * by the points, and that is able to systematically explore the resulting
022:         * search space and enumerate all resulting rule applications.
023:         * <code>ChoicePoint</code>s have to register themselves (using method
024:         * <code>passChoicePoint</code>) each time they are invoked during evaluation
025:         * of the feature term, and are asked by the manager for their branches. The
026:         * manager simulates a backtracking behaviour by repeated evaluation of the
027:         * feature term.
028:         */
029:        public class BackTrackingManager {
030:
031:            /**
032:             * The original rule application in question, i.e., the application without
033:             * the changes that can possibly be applied by <code>ChoicePoint</code>s
034:             */
035:            private RuleApp initialApp = null;
036:
037:            /**
038:             * Stack of <code>IteratorOfCPBranch</code>: the branches of
039:             * <code>ChoicePoint</code>s that have not yet been taken, the branches
040:             * of later points being further up in the stack
041:             */
042:            private final Stack choices = new Stack();
043:
044:            /**
045:             * List of <code>CPBranch</code>: the branches that are taken in the
046:             * current evaluation run
047:             */
048:            private final ArrayList chosenBranches = new ArrayList();
049:
050:            /**
051:             * The position within <code>choices</code> during the current evaluation
052:             * run (the number of <code>ChoicePoint</code>s that occured so far
053:             * during the current evaluation)
054:             */
055:            private int position = 0;
056:
057:            /**
058:             * Method that has to be invoked by each feature that represents a choice
059:             * point, each time the feature is invoked during evaluation of the feature
060:             * term
061:             * 
062:             * @param cp
063:             *            the <code>ChoicePoint</code> in question (which does not
064:             *            have to be the same object as the feature, and which does not
065:             *            have to be the same object over different evaluations of the
066:             *            feature term)
067:             * @param ticket
068:             *            a unique object (as unique as possible) that has to be
069:             *            provided by the feature in order to ensure that the same
070:             *            sequence of choice points occurs during the next evaluation
071:             *            run (after backtracking). The <code>ticket</code> must not
072:             *            change between two evaluation runs of the feature term
073:             */
074:            public void passChoicePoint(ChoicePoint cp, Object ticket) {
075:                assert initialApp != null;
076:                assertValidTicket(ticket);
077:                assert chosenBranches.size() == choices.size();
078:
079:                if (position == choices.size()) {
080:                    // phase where we have to ask the choice-points for possibilities
081:                    addChoicePoint(cp);
082:                } else {
083:                    assert choices.size() > position;
084:                    // phase where we have to "replay" choices that have already
085:                    // been made
086:                    ((CPBranch) chosenBranches.get(position)).choose();
087:                }
088:
089:                ++position;
090:
091:            }
092:
093:            /**
094:             * Method that has to be called before a sequence of evaluation runs of a
095:             * feature term.
096:             * 
097:             * @param initialApp
098:             *            the original rule application in question
099:             */
100:            public void setup(RuleApp initialApp) {
101:                this .initialApp = initialApp;
102:                choices.clear();
103:                chosenBranches.clear();
104:                tickets.clear();
105:                position = 0;
106:            }
107:
108:            /**
109:             * In the end of an evaluation run of a feature term, this method has to be
110:             * called for checking whether it is possible to backtrack and whether a
111:             * further evaluation run is necessary
112:             * 
113:             * @return <code>true</code> iff there are paths left to explore, i.e., if
114:             *         evaluation should run a further time
115:             */
116:            public boolean backtrack() {
117:                position = 0;
118:
119:                while (!choices.isEmpty()) {
120:                    final IteratorOfCPBranch chs = (IteratorOfCPBranch) choices
121:                            .pop();
122:                    chosenBranches.remove(chosenBranches.size() - 1);
123:
124:                    if (chs.hasNext()) {
125:                        pushChoices(chs, chs.next());
126:                        return true;
127:                    }
128:
129:                    tickets.remove(tickets.size() - 1);
130:                }
131:
132:                // make sure that no further choicepoints occur until <code>setup</code>
133:                // is invoked the next time
134:                setup(null);
135:
136:                return false;
137:            }
138:
139:            /**
140:             * @return the resulting rule application when all choice points have
141:             *         applied their modifications
142:             */
143:            public RuleApp getResultingapp() {
144:                return getOldRuleApp();
145:            }
146:
147:            private void pushChoices(IteratorOfCPBranch remainingChoices,
148:                    CPBranch chosen) {
149:                choices.push(remainingChoices);
150:                chosenBranches.add(chosen);
151:            }
152:
153:            private void addChoicePoint(ChoicePoint cp) {
154:                final RuleApp oldApp = getOldRuleApp();
155:                if (oldApp == null) {
156:                    // This means that an earlier <code>ChoicePoint</code> did not have
157:                    // any branches. It is necessary to backtrack and to choose a
158:                    // different branch for one of the <code>ChoicePoint</code>s before
159:                    // the failing <code>ChoicePoint</code>, but first we have to finish
160:                    // the current evaluation run of the feature term
161:                    cancelChoicePoint();
162:                    return;
163:                }
164:
165:                final IteratorOfCPBranch chs = cp.getBranches(oldApp);
166:                if (!chs.hasNext()) {
167:                    // This <code>ChoicePoint</code> does not have any branches
168:                    cancelChoicePoint();
169:                    return;
170:                }
171:
172:                final CPBranch chosen = chs.next();
173:                pushChoices(chs, chosen);
174:                chosen.choose();
175:            }
176:
177:            private void cancelChoicePoint() {
178:                pushChoices(SLListOfCPBranch.EMPTY_LIST.iterator(), null);
179:            }
180:
181:            /**
182:             * List of <code>Object</code>: each <code>ChoicePoint</code> has to
183:             * install a ticket, which is used as a sanity check when the evaluation of
184:             * a feature term is repeated. This is a simple runtime measure for ensuring
185:             * that the feature evaluation is deterministic
186:             */
187:            private final ArrayList tickets = new ArrayList();
188:
189:            private void assertValidTicket(Object ticket) {
190:                if (tickets.size() > position) {
191:                    assert tickets.get(position) == ticket;
192:                } else {
193:                    assert tickets.size() == position;
194:                    tickets.add(ticket);
195:                }
196:            }
197:
198:            private RuleApp getOldRuleApp() {
199:                if (chosenBranches.isEmpty())
200:                    return initialApp;
201:                final CPBranch branch = (CPBranch) chosenBranches
202:                        .get(position - 1);
203:                if (branch == null)
204:                    return null;
205:                return branch.getRuleAppForBranch();
206:            }
207:
208:        }
w_w_w_.___j___a__v_a_2_s__._c_om__ | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.