StatefulContext[S: S, M: M]¶

The system under test and the reference model for the current sample.

In step, the context is ref — both sut and model can be read and written. In invariant and final_check, the context is box — viewpoint adaptation makes ctx.sut and ctx.model read-only.

S and M should be ref or val capability types. iso gives tag through the box view (unusable); trn gives box where mutation was expected.

class ref StatefulContext[S: S, M: M]

Constructors¶

create¶

[Source]

new ref create(
  sut': S^,
  model': M^)
: StatefulContext[S, M] ref^

Parameters¶

sut': S^
model': M^

Returns¶

StatefulContext[S, M] ref^

Public fields¶

var sut: S¶

[Source]

var model: M¶

[Source]