|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectSimplifier
Ein Simplifier vereinfacht eine Verifikationsbedingung. Er ist der wesentliche Bestandteil des Beweisers. Es koennen entweder so viele Vereinfachungsschritte wie moeglich oder lediglich ein einzelner Schritt durchgefuehrt werden.
BoolSimp
,
OrdSimp
,
AlgSimp
,
SimpleNode
,
JPV
Field Summary | |
(package private) AlgSimp |
algSimp
Enthält die algebraischen Vereinfachungsregeln. |
(package private) BoolSimp |
boolSimp
Enthält die booleschen Vereinfachungsregeln. |
(package private) OrdSimp |
ordSimp
Enthält die relationalen Vereinfachungsregeln. |
Constructor Summary | |
Simplifier(SimpleNode condition,
BoolSimp boolSimp,
OrdSimp ordSimp,
AlgSimp algSimp,
javax.swing.JTextArea output)
Erzeugt einen Simplifier. |
Method Summary | |
SimpleNode |
applySubsts(SimpleNode simpPattern)
Ersetzt im Muster simpPattern Variablen, zu denen in theta eine Substitution enthalten ist, durch den an die Variable gebundenen Ausdruck. |
SimpleNode |
doWork(boolean output,
int numSteps)
Steuert den Vereinfachungsprozeß. |
SimpleNode[] |
getResults()
Methode, die für alle Regeln prüft, ob sie auf den Teilbaum anwendbar sind. |
boolean |
hasSimplified()
Gibt an, ob in einem kompletten Durchlauf aller Vereinfachungsregeln eine Regel angewandt wurde. |
boolean |
reduce(SimpleNode ccondition,
Rules rules,
boolean output)
Versucht einen einzelnen Vereinfachungsschritt durch Anwendung einer Vereinfachungsregel durchzufuehren. |
boolean |
reduceOne(SimpleNode ccondition,
Rules rules,
int rule,
boolean output)
Versucht, die i-te Regel von rules (OrdSimp, BoolSimp oder AlgSimp) auf ccondition anzuwenden. |
boolean |
simplify(SimpleNode ccondition,
boolean output)
Versucht durch Verwendung der Methode reduce(SimpleNode ccondition, Rules rules,
boolean output) einen einzelnen Vereinfachungsschritt durchzufuehren.
|
java.lang.String |
substitutionsToString()
Konvertiert die Liste aus Verifikationsbedingungen in einen String. |
boolean |
unify(SimpleNode condition,
SimpleNode pattern)
Startet den Unifikationsalgorithmus. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
BoolSimp boolSimp
OrdSimp ordSimp
AlgSimp algSimp
Constructor Detail |
public Simplifier(SimpleNode condition, BoolSimp boolSimp, OrdSimp ordSimp, AlgSimp algSimp, javax.swing.JTextArea output)
condition
- Die zu vereinfachende Verifikationsbedingung.boolSimp
- Die booleschen Vereinfachungsregeln.ordSimp
- Die relationalen Vereinfachungsregeln.algSimp
- Die algebraischen Vereinfachungsregeln.output
- Textfeld zur Ausgabe vereinfachter Regeln.Method Detail |
public boolean hasSimplified()
public SimpleNode applySubsts(SimpleNode simpPattern)
simpPattern
- Das Muster, in dem die Ersetzungen vorgenommen werden.
public boolean unify(SimpleNode condition, SimpleNode pattern)
condition
- Die zu vereinfachende Verifikationsbedingung.pattern
- Das Muster, mit dem die Verifkationsbedingung verglichen werden soll.
public boolean reduceOne(SimpleNode ccondition, Rules rules, int rule, boolean output)
ccondition
- Die zu vereinfachende Bedingung.rules
- Der Regeltyp.rule
- Gibt an, die wievielte Regel von rules angewendet werden soll.output
- Gibt an, ob Zwischenschritte ausgegeben werden sollen.
public boolean reduce(SimpleNode ccondition, Rules rules, boolean output)
ccondition
- Die zu vereinfachende Bedingung.rules
- Der Regeltyp.output
- Gibt an, ob Zwischenschritte ausgegeben werden sollen.
public SimpleNode[] getResults()
public boolean simplify(SimpleNode ccondition, boolean output)
reduce(SimpleNode ccondition, Rules rules,
boolean output)
einen einzelnen Vereinfachungsschritt durchzufuehren.
Die Methode regelt dazu die Reihenfolge der Anwendung der verschiedenen Regeln aus AlgSimp, BoolSimp oder OrdSimp.
ccondition
- Die zu vereinfachende Bedingung.output
- Gibt an, ob Zwischenschritte ausgegeben werden sollen.
AlgSimp
,
BoolSimp
,
OrdSimp
public SimpleNode doWork(boolean output, int numSteps)
simplify(SimpleNode ccondition,
boolean output)
wird die Verifikationsbedingung, die in dem Feld condition enthalten ist, vereinfacht.
output
- Gibt an, ob Zwischenschritte ausgegeben werden sollen.numSteps
- Anzahl der maximal durchzufuehrenden Vereinfachungsschritte.
public java.lang.String substitutionsToString()
|
||||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |