Atomkraft fails on trace test assertions

[andrey-kuprianov]

Apparently, Modelator (and by transitivity Atomkraft) doesn't negate test assertions represented as trace invariants properly.

For the following command:

atomkraft model sample --model-path models/bank/BankSendTests.tla --examples TestThreeOutcomes --traces-dir traces/bank --max_error=10 --view=ActionView

I get

Sampling TestThreeOutcomes... 
Results:
Parsing error 💥
    Parse error at BankSendTests__negated.tla:
None

Here TestThreeOutcomes is the following:

\* @type: Seq(STATE) => Bool;
TestThreeOutcomes(trace) ==
  LET outcomes == { trace[s].outcome : s \in DOMAIN trace } IN 
  Cardinality(outcomes) >= 3

Most probably we don't expect test assertions to have parameters.