VerificationAssertion

public class VerificationAssertion

An assertion about a Coco file. Assertions are arranged in a tree, the structure of which is: * Root * [Module] (for each module that is known about) * [Port] (for each port defined in this module) * [Component] (for each component defined in this module) Under each [Port]/[Component] there will be further trees of assertions. The lifetime of this object is tied to the lifetime of the context in which this is created: references to a VerificationAssertion must not outlive the reference to the context.

Constructors

VerificationAssertion

protected VerificationAssertion(APIClient client, long objectId)

Internal constructor

Methods

cancelVerify

public void cancelVerify()

May be called during run to cancel verification of this assertion. This will request cancellation of the running assertion, and will return immediately. The cancellation will happen as soon as is possible, depending on the verification backend. For example, whilst this may return immediately, the pending call to run() may only start a few seconds later. If this is called at irrelevant times, this will have no adverse affect. If this is a parent assertion, this will cancel the verification of all child assertions.

childAssertions

public java.util.ArrayList<io.cocotec.coco.platform.coco.VerificationAssertion> childAssertions()

Assertions are arranged into a tree; these are the child assertions of this assertion.

counterexamples

public java.util.ArrayList<io.cocotec.coco.platform.coco.Counterexample> counterexamples()

If this is an assertion and the status of this is FinishedFailed, then any counterexamples that were reported.

description

public String description()

A longer human-readable description of this assertion

finalize

protected void finalize()

getObjectId

public long getObjectId()

Internal method

getOrCreate

public static VerificationAssertion getOrCreate(APIClient client, long objectId)

Internal method

isGroup

public boolean isGroup()

Is this a group of assertions; i.e. an assertion with children?

isLeaf

public boolean isLeaf()

Is this a leaf assertion; i.e. an assertion with no children?

isModuleGroup

public boolean isModuleGroup()

Is this an assertion group?

isRoot

public boolean isRoot()

Is this the root assertion?

name

public String name()

A short human-readable name of this assertion.

node

public io.cocotec.coco.platform.coco.Node node()

The node that this is an assertion about. This may be invalid for some group assertions.

parent

public io.cocotec.coco.platform.coco.VerificationAssertion parent()

The parent assertion of this in the tree.

position

public io.cocotec.coco.platform.coco.SourceRange position()

A position that is associated with this assertion. This may not be valid, but if valid, represents a location that should be navigated to if this assertion is selected in a Coco IDE.

run

public void run()

Verifies this assertion. If this is a parent assertion, this will start verifying all child assertions (in an intelligent order).

statistics

public io.cocotec.coco.platform.coco.VerificationStatistics statistics()

If verification of this check has started or finished, returns statistics about this assertion. If this is a non-leaf assertion, then these statistics will be nullptr.

status

public io.cocotec.coco.platform.coco.VerificationStatus status()

The status of this assertion.