An expression file can be generated from the counter-example selection, but nothing in the file says so. Reading such a file back therefore adds the sentences to the model as ordinary, valid facts - the exact opposite of what they are. The same holds for unconfirmed tuples: the distinction is lost the moment the expressions leave the model.

There is also no way for a user to state it by hand. When someone writes or edits an expression file - the usual way to collect examples with a domain expert - every sentence in it is a fact that holds. A counter example is a normal part of that conversation ('and this one must NOT be possible'), and it should be possible to write one down as such, per sentence, and have CaseTalk understand it when the file is processed.

Finally, the expression file window shows every line the same way, so even when the state is known there is nothing to see. Counter examples and unconfirmed tuples are already recognisable at a glance in the diagrams and in the expression viewer; the expression file window should follow the same convention.