uk.ac.sheffield.vtts.model

Class Proposition

java.lang.Object

uk.ac.sheffield.vtts.model.Element

uk.ac.sheffield.vtts.model.Named

uk.ac.sheffield.vtts.model.Expression

uk.ac.sheffield.vtts.model.Function

uk.ac.sheffield.vtts.model.Predicate

uk.ac.sheffield.vtts.model.Proposition

public class Proposition
extends Predicate

Proposition represents a logical expression with a Boolean operator root node. The operands are expected to be other Predicates, or Boolean valued Parameters. There are five possible Boolean operators, whose names include: or, and, not, implies and equals, although the last two are rarely used. Two of the operators (and, or) are designed to accept two or more operands (to reduce nesting and associativity issues), two further operators (implies, equals) expect exactly two operands, and one operator (not) expects a single operand.

Version:

Broker@Cloud 1.0

Author:

Anthony J H Simons

Field Summary

Fields inherited from class uk.ac.sheffield.vtts.model.Function

expressions, maxOperands

Fields inherited from class uk.ac.sheffield.vtts.model.Expression

factory, type

Fields inherited from class uk.ac.sheffield.vtts.model.Named

name

Constructor Summary

Constructors

Constructor and Description
Proposition() Creates a default logical Proposition.
Proposition(java.lang.String name) Creates a logical Proposition with the given name.

Method Summary

Methods

Modifier and Type	Method and Description
protected boolean	allConjunctsSubsume(Predicate other) Tests whether all of this AND-Proposition's conjuncts subsume the other Predicate.
java.lang.Boolean	evaluate() Executes this Proposition on its operands.
java.util.List<Predicate>	getPredicates() Returns the list of operand Predicates governed by this Proposition.
boolean	isConsistent() Reports whether this Proposition is consistent.
protected void	nameCheck() Validates the name of a logical Proposition and sets the expected number of operands.
Predicate	negate() Returns the complement of this logical Proposition.
Proposition	normalise() Converts this Proposition into a term dominated by AND, OR or NOT.
protected boolean	oneDisjunctSubsumes(Predicate other) Tests whether one of this OR-Proposition's disjuncts subsumes the other Predicate.
Predicate	operand(int index) Returns one of the operand Predicates at an index.
protected void	rebindFalse() Rebinds the unbound operands of this Proposition, so that it yields false.
protected void	rebindTrue() Rebinds the unbound operands of this Proposition, so that it yields true.
java.util.List<Predicate>	refine() Returns a list of refinements of this Proposition.
boolean	subsumes(Predicate other) Tests whether this Proposition subsumes another Predicate.
protected boolean	subsumesAllDisjunctsOf(Proposition other) Tests whether this Proposition subsumes all disjuncts of the other OR-Proposition.
protected boolean	subsumesOneConjunctOf(Proposition other) Tests whether this Proposition subsumes one conjunct of the other AND-Proposition.
protected void	typeCheck() Checks the types of the operands of this Proposition predicate.

Methods inherited from class uk.ac.sheffield.vtts.model.Predicate

isFalseConstant, rebind, rebind, setType, subsumesProposition

Methods inherited from class uk.ac.sheffield.vtts.model.Function

addExpression, assign, equals, getExpressions, getType, hashCode, isAssignable, isBound, resolve, setName, toString, unbind

Methods inherited from class uk.ac.sheffield.vtts.model.Expression

getName, isBottom, isOrdered

Methods inherited from class uk.ac.sheffield.vtts.model.Named

setName

Methods inherited from class uk.ac.sheffield.vtts.model.Element

safeEquals, safeHashCode, semanticError

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

Proposition

public Proposition()

Creates a default logical Proposition. The result type is automatically set to "Boolean".

Proposition

public Proposition(java.lang.String name)

Creates a logical Proposition with the given name. Checks that the name is one of the legal names for a logical Proposition. The result type is automatically set to "Boolean".

Parameters:

name - the name of this Proposition.

Method Detail

nameCheck

protected void nameCheck()

Validates the name of a logical Proposition and sets the expected number of operands. All Boolean operators expect two operands, apart from "not", which expects one operand.

Specified by:

nameCheck in class Function

typeCheck

protected void typeCheck()

Checks the types of the operands of this Proposition predicate. The operands and the result must all have the type Boolean.

Specified by:

typeCheck in class Function

operand

public Predicate operand(int index)

Returns one of the operand Predicates at an index. Converts the Expression to a Predicate, to enable recursive Predicate processing.

Overrides:

operand in class Function

Parameters:

index - the index.

Returns:

the indexed operand, as a Predicate.

getPredicates

public java.util.List<Predicate> getPredicates()

Returns the list of operand Predicates governed by this Proposition. Converts the Expression operands of this Proposition into a list of Predicates. Each operand is either already some kind of Predicate, or it is some kind of Parameter, in which case it is wrapped as an Atomic predicate. This method is used when treating Boolean-valued expressions uniformly as predicates.

Returns:

the list of operands as a list of Predicates.

normalise

public Proposition normalise()

Converts this Proposition into a term dominated by AND, OR or NOT. Eliminates the operators "implies" and "equals" by logical conversion.

Overrides:

normalise in class Predicate

Returns:

the normalised form of this Proposition.

isConsistent

public boolean isConsistent()

Reports whether this Proposition is consistent. Chiefly checks large conjunctions to determine whether their conjuncts are satisfiable with any value assignments. Disjunctions are checked to see if any disjunct is satisfiable. Negations are checked to see if their single sub-term is satisfiable. Other logical connectives are normalised first.

Overrides:

isConsistent in class Predicate

Returns:

true if this Predicate is consistent.

subsumes

public boolean subsumes(Predicate other)

Tests whether this Proposition subsumes another Predicate. Checks whether this Proposition is in normal form, dominated by AND, OR, or NOT; otherwise first converts this Proposition, which is dominated by IMPLIES or EQUALS, to normal form, before recursively checking for subsumption. If the other Predicate is also a Proposition, dispatches to a subroutine dealing with this special case. If this Proposition is dominated by AND, checks whether all of its conjuncts subsume the other. If it is dominated by OR, checks whether one of its disjuncts subsumes the other. Otherwise, this is dominated by NOT; so reverses polarity and checks whether the negation of the other subsumes the negation of this. Returns false if this would lead to infinite regression.

Specified by:

subsumes in class Predicate

Parameters:

other - the other Predicate.

Returns:

true, if this Proposition subsumes the other Predicate.

oneDisjunctSubsumes

protected boolean oneDisjunctSubsumes(Predicate other)

Tests whether one of this OR-Proposition's disjuncts subsumes the other Predicate. The other Predicate is not a compound Proposition, but an atomic Comparison or Membership predicate.

Parameters:

other - the other Predicate.

Returns:

true if any of this Proposition's disjuncts subsumes the other.

allConjunctsSubsume

protected boolean allConjunctsSubsume(Predicate other)

Tests whether all of this AND-Proposition's conjuncts subsume the other Predicate. The other Predicate is not a compound Proposition, but an atomic Comparison or Membership predicate.

Parameters:

other - the other Predicate.

Returns:

true if all of this Proposition's conjuncts subsume the other.

subsumesOneConjunctOf

protected boolean subsumesOneConjunctOf(Proposition other)

Tests whether this Proposition subsumes one conjunct of the other AND-Proposition. If this is also an AND-Proposition, all of this Proposition's conjuncts must subsume at least one of the other Proposition's conjuncts. If this is an OR-Proposition, at least one of this Proposition's disjuncts must subsume at least one of the other Proposition's conjuncts. Special version for Propositions, overrides version in Predicate.

Overrides:

subsumesOneConjunctOf in class Predicate

Parameters:

other - an AND-Proposition.

Returns:

true if this Predicate subsumes one conjunct.

subsumesAllDisjunctsOf

protected boolean subsumesAllDisjunctsOf(Proposition other)

Tests whether this Proposition subsumes all disjuncts of the other OR-Proposition. If this is also an OR-Proposition, some of this Proposition's disjuncts must subsume all of the other's disjuncts. If this is an AND-Proposition, all of this Proposition's conjuncts must subsume all of the other's disjuncts. Special version for Propositions, overrides version in Predicate.

Overrides:

subsumesAllDisjunctsOf in class Predicate

Parameters:

other - an OR-Proposition.

Returns:

true if this Predicate subsumes all disjuncts.

negate

public Predicate negate()

Returns the complement of this logical Proposition. The complement of NOT(X) is X; the complement of AND(X, Y) is OR(NOT(X), NOT(Y)). The complement of OR(X, Y) is AND(NOT(X), NOT(Y)). The complement of IMPLIES(X, Y) is determined by first normalising this to OR(NOT(X), Y) subsequently negating to yield AND(X, NOT(Y)). The complement of EQUALS(X, Y) is determined by first normalising this to AND(OR(NOT(X), Y), OR(NOT(Y), X)) and subsequently negating to yield OR(AND(X, NOT(Y)), AND(Y, NOT(X))).

Overrides:

negate in class Predicate

Returns:

the negation, or complement of this logical Proposition.

refine

public java.util.List<Predicate> refine()

Returns a list of refinements of this Proposition. If this Proposition is a logical-AND or logical-OR, we want to collect the atomic Predicates under this Proposition. Refines each of the operands, and returns a list of all of these refinements. If this Proposition is logical-NOT, collects the negation of each of the refinements of this Proposition's (negated) operand.

Overrides:

refine in class Predicate

Returns:

the refinements of this Predicate.

evaluate

public java.lang.Boolean evaluate()

Executes this Proposition on its operands. Expects one operand for a negation, two operands for implies or equals, and two or more operands otherwise (for and, or). Branches according to the name of the operation, and evaluates operands AND, OR lazily.

Specified by:

evaluate in class Predicate

Returns:

true or false.

rebindTrue

protected void rebindTrue()

Rebinds the unbound operands of this Proposition, so that it yields true. This is a heuristic approach that works most of the time, but not universally. For example: if operand[0] is already bound to false, no binding of operand[1] will make AND true.

Specified by:

rebindTrue in class Predicate

rebindFalse

protected void rebindFalse()

Rebinds the unbound operands of this Proposition, so that it yields false. This is a heuristic approach that works most of the time, but not universally. For example: if operand[0] is already bound to false, no binding of operand[1] will make IMPLIES false.

Specified by:

rebindFalse in class Predicate