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 26, 2024
1 parent be407a8 commit 33c3f18
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 notice

Code scanning / genaiscript

TLAi-linter

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.
/\ PrintT("Writing stats to file: " \o CoverageFilename)

Check warning

Code scanning / genaiscript

TLAi-linter Warning

The print statement in the SerialiseCoverageConstraint definition incorrectly states "Writing stats to file" instead of "Writing coverage to file", which would be more accurate given the context of appending coverage information.
ELSE TRUE

====

0 comments on commit 33c3f18

Please sign in to comment.