📄 defaultloopcheckingalgorithm.java
字号:
package org.mandarax.reference;
/*
* Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2 of the License, or (at your option) any later version.
*
* This library is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
*/
import org.mandarax.kernel.LoopCheckingAlgorithm;
import org.mandarax.util.logging.LogCategories;
/**
* Simple implementation of a loop checking algorithm that can be customized
* by setting some parameters. Suitable if one can estimate the recurrence patterns
* causing an infinite loop. (number of recurrences indicating that we are in a loop, max
* number of recuring patterns).
* @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
* @version 3.4 <7 March 05>
* @since 1.3
*/
public class DefaultLoopCheckingAlgorithm
implements LoopCheckingAlgorithm, LogCategories {
// number of proof steps without checks
private int numberOfStepsWithoutCheck = 10;
// we check for sequences of clauses that are repeated. this is the max length of such patterns checked
private int maxPatternLength = 5;
// the min number of recurrences of a pattern needed to regard this sequence as an infinite loop
private int minRecurrenceNumber = 5;
/**
* Constructor.
*/
public DefaultLoopCheckingAlgorithm() {
super ();
}
/**
* Constructor.
* @param par1 we check for sequences of clauses that are repeated. this is the max length of such patterns checked
* @param par2 the min number of recurrences of a pattern needed to regard this sequence as an infinite loop
* @param par3 number of proof steps without checks
*/
public DefaultLoopCheckingAlgorithm(int par1, int par2, int par3) {
super ();
maxPatternLength = par1;
minRecurrenceNumber = par2;
numberOfStepsWithoutCheck = par3;
}
/**
* Check the sequences.
* @return boolean
* @param startSeq1 start index of the first sequence
* @param startSeq2 start index of the second sequence
* @param length the length of the sequences
* @param list the list
* @param index the number of the comparsion
*/
private boolean check(int startSeq1, int startSeq2, int length,
java.util.List list, int index) {
if(index == 0) {
return true;
}
boolean result = compareSequences (startSeq1, startSeq2, length,
list);
if(result && (startSeq1 >= length)) {
return check (startSeq1 - length, startSeq2 - length, length,
list, index - 1);
} else {
return false;
}
}
/**
* Compare two sequences of elements in a list.
* @return boolean if the sequences are equal
* @param startSeq1 the start index of the first index
* @param startSeq2 the start index of the second sequence
* @param length the length of the sequences
* @param list the list of objects
*/
private boolean compareSequences(int startSeq1, int startSeq2,
int length, java.util.List list) {
for(int i = 0; i < length; i++) {
if(list.get (startSeq1 + i) != list.get (startSeq2 + i)) {
return false;
}
}
return true;
}
/**
* Insert the method's description here.
* Creation date: (2/14/2001 8:36:28 AM)
* @return boolean
* @param startSeq1 int
* @param startSeq2 int
* @param length int
* @param list java.util.List
* @param comp int
*/
private boolean compareSequences(int startSeq1, int startSeq2,
int length, java.util.List list,
int comp) {
return false;
}
/**
* Get the max pattern length.
* @return a value
*/
public int getMaxPatternLength() {
return maxPatternLength;
}
/**
* Get the min recurrence number.
* @return a value
*/
public int getMinRecurrenceNumber() {
return minRecurrenceNumber;
}
/**
* Get the number of steps without checks.
* @return a value
*/
public int getNumberOfStepsWithoutCheck() {
return numberOfStepsWithoutCheck;
}
/**
* Indicates whether the list of applied clauses represents an infinite loop.
* No loop checking means return false.
* @return false
* @param appliedClauses a list
*/
public boolean isInfiniteLoop(java.util.List appliedClauses) {
int s = appliedClauses.size ();
if((s == 0) || (s % numberOfStepsWithoutCheck > 0)) {
return false;
}
boolean logOn = LOG_IE_LOOPCHECK.isDebugEnabled ();
// start check
for(int i = 1; i < maxPatternLength + 1; i++) {
if(i * minRecurrenceNumber > s) {
if(logOn) {
LOG_IE_LOOPCHECK.debug ("No loop detected in :"
+ appliedClauses);
}
return false;
}
if(check (s - (2 * i), s - i, i, appliedClauses,
minRecurrenceNumber)) {
if(logOn) {
LOG_IE_LOOPCHECK.debug ("Loop detected in :"
+ appliedClauses);
LOG_IE_LOOPCHECK.debug (
"The length of the recuring pattern is: " + i);
LOG_IE_LOOPCHECK.debug ("The pattern recures "
+ minRecurrenceNumber + " times");
}
return true;
}
}
if(logOn) {
LOG_IE_LOOPCHECK.debug ("No loop detected in :" + appliedClauses);
}
return false;
}
/**
* Set the max pattern length.
* @param value the new value
*/
public void setMaxPatternLength(int value) {
maxPatternLength = value;
}
/**
* Set the min recurrence number.
* @param value the new value
*/
public void setMinRecurrenceNumber(int value) {
minRecurrenceNumber = value;
}
/**
* Set the number of steps without checks.
* @param value the new value
*/
public void setNumberOfStepsWithoutChecks(int value) {
numberOfStepsWithoutCheck = value;
}
}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -