EventuallyCounterexample¶

class Cocotec.CocoPlatform.Coco.EventuallyCounterexample : public Cocotec.CocoPlatform.Coco.BehaviourComparisonCounterexample¶

Public Functions

uint LoopStartIndex ()¶

uint EventuallyPremiseIndex ()¶

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

Cocotec.CocoPlatform.Coco.Node EventuallyNode ()¶

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

Cocotec.CocoPlatform.Coco.Node EventuallyAttribute ()¶

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