uk.ac.sheffield.vtts.model

Class Atomic

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.Atomic

public class Atomic
extends Predicate

Atomic is a degenerate predicate representing an atomic Boolean value. Atomic is a special adapter that allows a Parameter to be treated like a Predicate, when testing for logical subsumption. Atomic objects are only created internally by the verification tool, and are not intended for end user models, which instead should use Parameters (Input, Output, Variable, Constant) with Boolean types directly.

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
Atomic() Creates a default Atomic predicate.
Atomic(boolean value) Creates an Atomic predicate standing for a boolean constant value.
Atomic(Parameter parameter) Creates an Atomic predicate by wrapping a Parameter.

Method Summary

Methods

Modifier and Type	Method and Description
Atomic	addExpression(Expression expression) Adds an expression as an operand to this Assignment expression.
java.lang.Boolean	evaluate() Evaluates this Atomic predicate.
boolean	isFalseConstant() Returns true if this Atomic predicate wraps the boolean Constant false.
boolean	isTrueConstant() Returns true if this Atomic predicate wraps the boolean Constant true.
protected void	nameCheck() Checks the name of an Atomic predicate and sets the number of operands.
Predicate	negate() Negates this Atomic predicate.
protected void	rebindFalse() Rebinds this Atomic predicate so that it yields false.
protected void	rebindTrue() Rebinds this Atomic predicate so that it yields true.
boolean	subsumes(Predicate other) Tests whether this Atomic predicate subsumes the other Predicate.
java.lang.String	toString() Converts this Atomic predicate to a printable string.
protected void	typeCheck() Checks the type of this Atomic predicate.

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

isConsistent, normalise, rebind, rebind, refine, setType, subsumesAllDisjunctsOf, subsumesOneConjunctOf, subsumesProposition

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

assign, equals, getExpressions, getType, hashCode, isAssignable, isBound, operand, resolve, setName, 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

Atomic

public Atomic()

Creates a default Atomic predicate. The result type is automatically set to "Boolean".

Atomic

public Atomic(Parameter parameter)

Creates an Atomic predicate by wrapping a Parameter. The name of this Atomic predicate is taken from the name of the Parameter, and the type is automatically set to "Boolean". Adds the Parameter as the wrapped sub-expression.

Parameters:

parameter - the parameter to wrap.

Atomic

public Atomic(boolean value)

Creates an Atomic predicate standing for a boolean constant value. This constructor is used exclusively during negation of a constant Atomic predicate.

Parameters:

value - the constant true or false.

Method Detail

nameCheck

protected void nameCheck()
                  throws SemanticError

Checks the name of an Atomic predicate and sets the number of operands. There is always only a single operand. The name of this Atomic predicate is the same as the name of the wrapped operand.

Specified by:

nameCheck in class Function

Throws:

SemanticError - if the name is illegal.

typeCheck

protected void typeCheck()
                  throws SemanticError

Checks the type of this Atomic predicate.

Specified by:

typeCheck in class Function

Throws:

SemanticError - if a type inconsistency is detected.

addExpression

public Atomic addExpression(Expression expression)

Adds an expression as an operand to this Assignment expression.

Overrides:

addExpression in class Function

Parameters:

expression - the operand expression.

Returns:

this functional expression.

negate

public Predicate negate()

Negates this Atomic predicate. If this Atomic predicate wraps a Constant, returns an Atomic predicate wrapping the complementary Constant. Otherwise, constructs a Proposition negating the value of this Atomic predicate (which wraps a variable kind of Parameter).

Overrides:

negate in class Predicate

Returns:

the complement of this Predicate.

isTrueConstant

public boolean isTrueConstant()

Returns true if this Atomic predicate wraps the boolean Constant true.

Returns:

true, if this represents the true constant.

isFalseConstant

public boolean isFalseConstant()

Returns true if this Atomic predicate wraps the boolean Constant false.

Overrides:

isFalseConstant in class Predicate

Returns:

true, if this represents the false constant.

evaluate

public java.lang.Boolean evaluate()

Evaluates this Atomic predicate. Evaluates the wrapped Parameter, which has a Boolean value.

Specified by:

evaluate in class Predicate

Returns:

true or false.

subsumes

public boolean subsumes(Predicate other)

Tests whether this Atomic predicate subsumes the other Predicate. The Constant "true" subsumes everything; whereas the Constant "false" only subsumes "false". Any variable Parameter only subsumes the same-named parameter. If the other is a Proposition, applies the subsumption rules for conjunction, disjunction and negation. Otherwise, returns false.

Specified by:

subsumes in class Predicate

Parameters:

other - the other Predicate.

Returns:

true, if this Atomic predicate subsumes the other predicate.

rebindTrue

protected void rebindTrue()

Rebinds this Atomic predicate so that it yields true. Propagates the request to the wrapped Parameter.

Specified by:

rebindTrue in class Predicate

rebindFalse

protected void rebindFalse()

Rebinds this Atomic predicate so that it yields false. Propagates the request to the wrapped Parameter.

Specified by:

rebindFalse in class Predicate

toString

public java.lang.String toString()

Converts this Atomic predicate to a printable string. The output is a string of the form: varName, where this is the name of the wrapped Parameter.

Overrides:

toString in class Function

Returns:

the String representation of this Named element.