jpov.structure
Class Goal

java.lang.Object
  jpov.structure.TreeObject
      jpov.structure.Goal

public class Goal

extends TreeObject

This class implements a goal.

Author:

L. Burdy

Method Summary

Formula	getFormula() Returns the formula.
int	getGoalType() Returns the origin of the goal
int	getNbPo() Returns the number of proof obligations for this node.
int	getNbPoProved() Returns the number of proved proof obligations for this node.
int	getNbPoProved(java.lang.String prover) Returns the number of proved proof obligations for this node.
int	getNumber() Returns the number associated with this goal in the .po file of the Atelier B
Formula	getOriginal()
java.lang.String	getOriginString() Returns a string describing the goal origin.
ProverStatus	getProverStatus(java.lang.String prover)
GoalStatus	getState()
Substitution[]	getSubs()
java.lang.String	getText(int type) Returns the displayed text for this node.
VirtualFormula	getVf() Returns the virtual formula.
boolean	isChecked() Returns whether this node is checked
boolean	isMergeable() Returns whether the goal is proven or checked.
boolean	isProved(java.lang.String prover)
boolean	isSelected()
void	setChecked() Sets the node and its children to checked.
void	setSelected()
void	setStatus(java.lang.String prover, ProverStatus b) Sets the goal status
void	setUnchecked() Sets the node and its children to unchecked
void	setUnselected()

Methods inherited from class jpov.structure.TreeObject

getParent, isProved, percentProved

Methods inherited from class java.lang.Object

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

Method Detail

getText

public java.lang.String getText(int type)

Description copied from class: TreeObject

Returns the displayed text for this node.

Specified by:

getText in class TreeObject

Returns:

Goal xx

getNbPoProved

public int getNbPoProved(java.lang.String prover)

Description copied from class: TreeObject

Returns the number of proved proof obligations for this node.

Specified by:

getNbPoProved in class TreeObject

Returns:

1 if the goal is proved, 0 otherwise

getNbPoProved

public int getNbPoProved()

Description copied from class: TreeObject

Returns the number of proved proof obligations for this node.

Specified by:

getNbPoProved in class TreeObject

Returns:

1 if the goal is proved, 0 otherwise

getNbPo

public int getNbPo()

Description copied from class: TreeObject

Returns the number of proof obligations for this node.

Specified by:

getNbPo in class TreeObject

Returns:

Goal 1

isProved

public boolean isProved(java.lang.String prover)

isChecked

public boolean isChecked()

Description copied from class: TreeObject

Returns whether this node is checked

Overrides:

isChecked in class TreeObject

Returns:

false by default

isMergeable

public boolean isMergeable()

Returns whether the goal is proven or checked.

Returns:

true if the goal is not unproved, false otherwise

getOriginString

public java.lang.String getOriginString()

Returns a string describing the goal origin.

setStatus

public void setStatus(java.lang.String prover,
                      ProverStatus b)

Sets the goal status

Parameters:

b - The goal status to set

setChecked

public void setChecked()

Description copied from class: TreeObject

Sets the node and its children to checked.

Specified by:

setChecked in class TreeObject

setUnchecked

public void setUnchecked()

Description copied from class: TreeObject

Sets the node and its children to unchecked

Specified by:

setUnchecked in class TreeObject

getVf

public VirtualFormula getVf()

Returns the virtual formula.

Returns:

vf

getFormula

public Formula getFormula()

Returns the formula.

getNumber

public int getNumber()

Returns the number associated with this goal in the .po file of the Atelier B

Returns:

number

getGoalType

public int getGoalType()

Returns the origin of the goal

Returns:

origin

getProverStatus

public ProverStatus getProverStatus(java.lang.String prover)

getOriginal

public Formula getOriginal()

Returns:

getSubs

public Substitution[] getSubs()

Returns:

getState

public GoalStatus getState()

Returns:

setSelected

public void setSelected()

setUnselected

public void setUnselected()

isSelected

public boolean isSelected()

Returns: