EventuallyCounterexample

public class EventuallyCounterexample extends BehaviourComparisonCounterexample

Constructors

EventuallyCounterexample

protected EventuallyCounterexample(APIClient client)

Internal constructor

Methods

eventuallyAttribute

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

Returns one of the attributes on one of the relevant children of eventually_nondetl

eventuallyNode

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

The EventState or nondet that contains the -labelled branch that was violated.

eventuallyPremiseIndex

public int eventuallyPremiseIndex()

The index at which the premise was true, and thus the was required to be satisfied.

fromProtobuf

public static EventuallyCounterexample fromProtobuf(APIClient client, Out.CocoCounterexample inputValue)

Internal constructor

loopStartIndex

public int loopStartIndex()