Raptor.NDRules
Class ForallTick

java.lang.Object
  Raptor.NDRules.NDRule
      Raptor.NDRules.ForallTick

public class ForallTick
extends NDRule

Implements the For All Tick rule.
Extends abstract class NDRule.

Constructor Summary

ForallTick(ProofBox pProof)
Constructs a ForallTick.

Method Summary

void	addInputLine(ProofLine pClickedLine) Adds the input line to the rule. The line is checked to ensure it is a goal line.
void	addLine(ProofLine pClickedLine) Adds the extra lines to the rule once the input line has been added.
void	apply() Called by the RuleController to apply the rule.
void	check() Called by the RuleController to check the input lines to the rule.
boolean	checkVarSub(Formula pFormula1, Formula pFormula2) Only used when the rule is applied backwards to check if the passed formula can be reached by applying For All Tick backwards on the selected line's formula.
boolean	haveAll() Returns true if the rule has all of the required input lines.

Methods inherited from class Raptor.NDRules.NDRule

checkSignature, getNewFormula

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ForallTick

public ForallTick(ProofBox pProof)

Constructs a ForallTick.

Parameters:

pProof - ProofBox representing in which box the rule is being applied

Method Detail

addInputLine

public void addInputLine(ProofLine pClickedLine)
                  throws java.lang.Exception

Adds the input line to the rule.
The line is checked to ensure it is a goal line.

Overrides:

addInputLine in class NDRule

Parameters:

pClickedLine - ProofLine which is the first line selected

Throws:

java.lang.Exception

addLine

public void addLine(ProofLine pClickedLine)
             throws java.lang.Exception

Adds the extra lines to the rule once the input line has been added.

Specified by:

addLine in class NDRule

Parameters:

pClickedLine - ProofLine which has been selected

Throws:

java.lang.Exception

haveAll

public boolean haveAll()

Returns true if the rule has all of the required input lines.

Specified by:

haveAll in class NDRule

check

public void check()
           throws java.lang.Exception

Called by the RuleController to check the input lines to the rule.

Specified by:

check in class NDRule

Throws:

java.lang.Exception

apply

public void apply()
           throws java.lang.Exception

Called by the RuleController to apply the rule.

Specified by:

apply in class NDRule

Throws:

java.lang.Exception

checkVarSub

public boolean checkVarSub(Formula pFormula1,
                           Formula pFormula2)
                    throws java.lang.Exception

Only used when the rule is applied backwards to check if the passed formula can be reached by applying For All Tick backwards on the selected line's formula.

Throws:

java.lang.Exception