Skip to content

Commit

Permalink
Write to stdout when coverage information is written.
Browse files Browse the repository at this point in the history
  • Loading branch information
@lemmy
lemmy committed Mar 27, 2024
1 parent be407a8 commit 26a8462
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion tla/StatsFile.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,8 @@ WriteStatsFile ==
SerialiseCoverageConstraint ==
LET interval == 500000
IN IF TLCGet("distinct") % interval = 0
THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
THEN /\ Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])

Check warning

Code scanning / genaiscript

TLAi-linter Warning

The Serialize function in line 23 is used with options that suggest the creation and appending of data to the CoverageFilename. This is consistent with the comment in line 19 that states the file should be created if it does not exist and that data should be appended.

Check failure

Code scanning / genaiscript

TLAi-linter Error

The Serialize operator's options in line 23 include "WRITE", "CREATE", "APPEND", which are not standard TLA+ operators or strings and may not be understood by the TLA+ toolset without custom definitions or extensions.
/\ PrintT("Writing coverage to file: " \o CoverageFilename)
ELSE TRUE

====

0 comments on commit 26a8462

Please sign in to comment.