Class Simplifier

java.lang.Object
  extended bySimplifier

class Simplifier
extends java.lang.Object

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.

See Also:
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 boolSimp
Enthält die booleschen Vereinfachungsregeln.


ordSimp

OrdSimp ordSimp
Enthält die relationalen Vereinfachungsregeln.


algSimp

AlgSimp algSimp
Enthält die algebraischen Vereinfachungsregeln.

Constructor Detail

Simplifier

public Simplifier(SimpleNode condition,
                  BoolSimp boolSimp,
                  OrdSimp ordSimp,
                  AlgSimp algSimp,
                  javax.swing.JTextArea output)
Erzeugt einen Simplifier.

Parameters:
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

hasSimplified

public boolean hasSimplified()
Gibt an, ob in einem kompletten Durchlauf aller Vereinfachungsregeln eine Regel angewandt wurde.


applySubsts

public SimpleNode applySubsts(SimpleNode simpPattern)
Ersetzt im Muster simpPattern Variablen, zu denen in theta eine Substitution enthalten ist, durch den an die Variable gebundenen Ausdruck.

Parameters:
simpPattern - Das Muster, in dem die Ersetzungen vorgenommen werden.
Returns:
Das modifizierte simpPattern.

unify

public boolean unify(SimpleNode condition,
                     SimpleNode pattern)
Startet den Unifikationsalgorithmus. Bei dieser Unifikation wird eine Bedingung oder allgemeiner ein Ausdruck mit einem Muster verglichen. Gegebenenfalls werden Bindungen von Variablen an bestimmte Ausdruecke erzeugt und dann in der Liste theta gespeichert.

Parameters:
condition - Die zu vereinfachende Verifikationsbedingung.
pattern - Das Muster, mit dem die Verifkationsbedingung verglichen werden soll.
Returns:
true, falls die Unifikation erfolgreich war, das heißt, ob irgendwelche Bindungen von Variablen erzeugt wurden,
false sonst.

reduceOne

public boolean reduceOne(SimpleNode ccondition,
                         Rules rules,
                         int rule,
                         boolean output)
Versucht, die i-te Regel von rules (OrdSimp, BoolSimp oder AlgSimp) auf
ccondition anzuwenden.

Parameters:
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.
Returns:
true, falls die Regel angewendet werden konnte,
false sonst.

reduce

public boolean reduce(SimpleNode ccondition,
                      Rules rules,
                      boolean output)
Versucht einen einzelnen Vereinfachungsschritt durch Anwendung einer
Vereinfachungsregel durchzufuehren. Dies kann jeweils eine Regel
vom Typ OrdSimp, BoolSimp oder AlgSimp sein.

Parameters:
ccondition - Die zu vereinfachende Bedingung.
rules - Der Regeltyp.
output - Gibt an, ob Zwischenschritte ausgegeben werden sollen.
Returns:
true, falls eine Regel angewendet wurde,
false sonst.

getResults

public SimpleNode[] getResults()
Methode, die für alle Regeln prüft, ob sie auf den Teilbaum anwendbar sind. Die Regeln können aus AlgSinp, BoolSimp oder Ord Simp stammen. Die Ergebnisse werden in einer Liste zwischengespeichert.

Returns:
Das Ergebnis-Array, in dem die anwendbaren Regeln gespeichert sind.

simplify

public boolean simplify(SimpleNode ccondition,
                        boolean output)
Versucht durch Verwendung der Methode 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.

Parameters:
ccondition - Die zu vereinfachende Bedingung.
output - Gibt an, ob Zwischenschritte ausgegeben werden sollen.
Returns:
true, falls eine Regel angewendet wurde,
false sonst.
See Also:
AlgSimp, BoolSimp, OrdSimp

doWork

public SimpleNode doWork(boolean output,
                         int numSteps)
Steuert den Vereinfachungsprozeß. Durch Verwendung der Methode simplify(SimpleNode ccondition, boolean output) wird die Verifikationsbedingung, die in dem Feld condition enthalten ist, vereinfacht.
Diese Methode kann so benutzt werden, daß sie nur einen Umformungsschritt durchfuehrt oder die Bedingung so weit wie moeglich vereinfacht.

Parameters:
output - Gibt an, ob Zwischenschritte ausgegeben werden sollen.
numSteps - Anzahl der maximal durchzufuehrenden Vereinfachungsschritte.
Returns:
Die vereinfachte Bedingung.

substitutionsToString

public java.lang.String substitutionsToString()
Konvertiert die Liste aus Verifikationsbedingungen in einen String.