001: package org.mandarax.reference;
002:
003: /*
004: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
005: *
006: * This library is free software; you can redistribute it and/or
007: * modify it under the terms of the GNU Lesser General Public
008: * License as published by the Free Software Foundation; either
009: * version 2 of the License, or (at your option) any later version.
010: *
011: * This library is distributed in the hope that it will be useful,
012: * but WITHOUT ANY WARRANTY; without even the implied warranty of
013: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
014: * Lesser General Public License for more details.
015: *
016: * You should have received a copy of the GNU Lesser General Public
017: * License along with this library; if not, write to the Free Software
018: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
019: */
020: import org.mandarax.kernel.LoopCheckingAlgorithm;
021: import org.mandarax.util.logging.LogCategories;
022:
023: /**
024: * Simple implementation of a loop checking algorithm that can be customized
025: * by setting some parameters. Suitable if one can estimate the recurrence patterns
026: * causing an infinite loop. (number of recurrences indicating that we are in a loop, max
027: * number of recuring patterns).
028: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
029: * @version 3.4 <7 March 05>
030: * @since 1.3
031: */
032: public class DefaultLoopCheckingAlgorithm implements
033: LoopCheckingAlgorithm, LogCategories {
034:
035: // number of proof steps without checks
036: private int numberOfStepsWithoutCheck = 10;
037:
038: // we check for sequences of clauses that are repeated. this is the max length of such patterns checked
039: private int maxPatternLength = 5;
040:
041: // the min number of recurrences of a pattern needed to regard this sequence as an infinite loop
042: private int minRecurrenceNumber = 5;
043:
044: /**
045: * Constructor.
046: */
047: public DefaultLoopCheckingAlgorithm() {
048: super ();
049: }
050:
051: /**
052: * Constructor.
053: * @param par1 we check for sequences of clauses that are repeated. this is the max length of such patterns checked
054: * @param par2 the min number of recurrences of a pattern needed to regard this sequence as an infinite loop
055: * @param par3 number of proof steps without checks
056: */
057: public DefaultLoopCheckingAlgorithm(int par1, int par2, int par3) {
058: super ();
059: maxPatternLength = par1;
060: minRecurrenceNumber = par2;
061: numberOfStepsWithoutCheck = par3;
062: }
063:
064: /**
065: * Check the sequences.
066: * @return boolean
067: * @param startSeq1 start index of the first sequence
068: * @param startSeq2 start index of the second sequence
069: * @param length the length of the sequences
070: * @param list the list
071: * @param index the number of the comparsion
072: */
073: private boolean check(int startSeq1, int startSeq2, int length,
074: java.util.List list, int index) {
075: if (index == 0) {
076: return true;
077: }
078:
079: boolean result = compareSequences(startSeq1, startSeq2, length,
080: list);
081:
082: if (result && (startSeq1 >= length)) {
083: return check(startSeq1 - length, startSeq2 - length,
084: length, list, index - 1);
085: } else {
086: return false;
087: }
088: }
089:
090: /**
091: * Compare two sequences of elements in a list.
092: * @return boolean if the sequences are equal
093: * @param startSeq1 the start index of the first index
094: * @param startSeq2 the start index of the second sequence
095: * @param length the length of the sequences
096: * @param list the list of objects
097: */
098: private boolean compareSequences(int startSeq1, int startSeq2,
099: int length, java.util.List list) {
100: for (int i = 0; i < length; i++) {
101: if (list.get(startSeq1 + i) != list.get(startSeq2 + i)) {
102: return false;
103: }
104: }
105:
106: return true;
107: }
108:
109: /**
110: * Insert the method's description here.
111: * Creation date: (2/14/2001 8:36:28 AM)
112: * @return boolean
113: * @param startSeq1 int
114: * @param startSeq2 int
115: * @param length int
116: * @param list java.util.List
117: * @param comp int
118: */
119: private boolean compareSequences(int startSeq1, int startSeq2,
120: int length, java.util.List list, int comp) {
121: return false;
122: }
123:
124: /**
125: * Get the max pattern length.
126: * @return a value
127: */
128: public int getMaxPatternLength() {
129: return maxPatternLength;
130: }
131:
132: /**
133: * Get the min recurrence number.
134: * @return a value
135: */
136: public int getMinRecurrenceNumber() {
137: return minRecurrenceNumber;
138: }
139:
140: /**
141: * Get the number of steps without checks.
142: * @return a value
143: */
144: public int getNumberOfStepsWithoutCheck() {
145: return numberOfStepsWithoutCheck;
146: }
147:
148: /**
149: * Indicates whether the list of applied clauses represents an infinite loop.
150: * No loop checking means return false.
151: * @return false
152: * @param appliedClauses a list
153: */
154: public boolean isInfiniteLoop(java.util.List appliedClauses) {
155: int s = appliedClauses.size();
156:
157: if ((s == 0) || (s % numberOfStepsWithoutCheck > 0)) {
158: return false;
159: }
160:
161: boolean logOn = LOG_IE_LOOPCHECK.isDebugEnabled();
162:
163: // start check
164: for (int i = 1; i < maxPatternLength + 1; i++) {
165: if (i * minRecurrenceNumber > s) {
166: if (logOn) {
167: LOG_IE_LOOPCHECK.debug("No loop detected in :"
168: + appliedClauses);
169: }
170:
171: return false;
172: }
173:
174: if (check(s - (2 * i), s - i, i, appliedClauses,
175: minRecurrenceNumber)) {
176: if (logOn) {
177: LOG_IE_LOOPCHECK.debug("Loop detected in :"
178: + appliedClauses);
179: LOG_IE_LOOPCHECK
180: .debug("The length of the recuring pattern is: "
181: + i);
182: LOG_IE_LOOPCHECK.debug("The pattern recures "
183: + minRecurrenceNumber + " times");
184: }
185:
186: return true;
187: }
188: }
189:
190: if (logOn) {
191: LOG_IE_LOOPCHECK.debug("No loop detected in :"
192: + appliedClauses);
193: }
194:
195: return false;
196: }
197:
198: /**
199: * Set the max pattern length.
200: * @param value the new value
201: */
202: public void setMaxPatternLength(int value) {
203: maxPatternLength = value;
204: }
205:
206: /**
207: * Set the min recurrence number.
208: * @param value the new value
209: */
210: public void setMinRecurrenceNumber(int value) {
211: minRecurrenceNumber = value;
212: }
213:
214: /**
215: * Set the number of steps without checks.
216: * @param value the new value
217: */
218: public void setNumberOfStepsWithoutChecks(int value) {
219: numberOfStepsWithoutCheck = value;
220: }
221: }
|