Pandora.NDRules
Class ForallTick

java.lang.Object
  extended by Pandora.NDRules.NDRule
      extended by Pandora.NDRules.ForallTick

public class ForallTick
extends NDRule

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


Field Summary
 
Fields inherited from class Pandora.NDRules.NDRule
firstLine
 
Constructor Summary
ForallTick(ProofBox proof)
          Constructs a ForallTick.
 
Method Summary
 void addInputLine(ProofLine clickedLine)
          Adds the input line to the rule.
The line is checked to ensure it is a goal line.
 void addLine(ProofLine clickedLine)
          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 f, Formula f2)
          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 Pandora.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 proof)
Constructs a ForallTick.

Parameters:
proof - ProofBox representing in which box the rule is being applied
Method Detail

addInputLine

public void addInputLine(ProofLine clickedLine)
                  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:
line - ProofLine which is the first line selected
Throws:
java.lang.Exception

addLine

public void addLine(ProofLine clickedLine)
             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:
clickedLine - 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 f,
                           Formula f2)
                    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