Show simulator's progress on the table in the side panel

Signed-off-by: Federico Ponzi <me@fponzi.me>
tlaplus · Sep 29, 2024 · dde2dfe · dde2dfe
1 parent b042ac5
commit dde2dfe
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/parsers/tlc.ts b/src/parsers/tlc.ts
@@ -347,6 +347,7 @@ class ModelCheckResultBuilder {
                 this.workersCount -= 1;
                 break;
             case msg.TLC_PROGRESS_STATS:
+            case msg.TLC_PROGRESS_SIMU:
                 this.parseProgressStats(message.lines);
                 this.status = CheckStatus.SuccessorStatesComputing;
                 break;

diff --git a/src/parsers/tlcCodes.ts b/src/parsers/tlcCodes.ts
@@ -223,7 +223,7 @@ export const TLC_COVERAGE_END = registerCode(2202, TlcCodeType.Ignore);
 export const TLC_CHECKPOINT_RECOVER_END_DFID = registerCode(2203, TlcCodeType.Ignore);
 export const TLC_PROGRESS_START_STATS_DFID = registerCode(2205, TlcCodeType.Ignore);
 export const TLC_PROGRESS_STATS_DFID = registerCode(2206, TlcCodeType.Ignore);
-export const TLC_PROGRESS_SIMU = registerCode(2209, TlcCodeType.Ignore);
+export const TLC_PROGRESS_SIMU = registerCode(2209, TlcCodeType.Info);
 export const TLC_FP_COMPLETED = registerCode(2211, TlcCodeType.Ignore);
 
 export const TLC_LIVE_IMPLIED = registerCode(2212, TlcCodeType.Ignore);