@@ -149,26 +149,29 @@ runParActions pas = do
149149 joinB <- run $ forkThread $ runTracing env (threadBActions pas)
150150 (trA, _) <- run joinA
151151 (trB, _) <- run joinB
152- monitor $ counterexample " -- Monitoring main thread"
153- monitorTrace mempty trC
154- monitor $ counterexample " -- Monitoring thread A"
155- monitorTrace env trA
156- monitor $ counterexample " -- Monitoring thread B"
157- monitorTrace env trB
152+ let used = varsUsedInActions $ linearActions pas
153+ monitor $ counterexample " -- Main thread:"
154+ monitorTrace used mempty trC
155+ monitor $ counterexample " \n -- Thread A:"
156+ monitorTrace used env trA
157+ monitor $ counterexample " \n -- Thread B:"
158+ monitorTrace used env trB
158159 let ilvs = prepend trC $ interleavings trA trB
159160 monitor $ tabulate " TraceTree size" (map (bucket . length ) ilvs)
160161 assert $ null ilvs || any (checkTrace initialAnnotatedState mempty ) ilvs
161162 -- TODO: stats collection and cleanup
162163
163164monitorTrace :: forall state m . (StateModel state , RunModelPar state m )
164- => Env -> Trace state m -> PropertyM m ()
165- monitorTrace _env [] = pure ()
166- monitorTrace env (TraceStep r v act : tr) = do
165+ => VarContext -> Env -> Trace state m -> PropertyM m ()
166+ monitorTrace _used _env [] = pure ()
167+ monitorTrace used env (TraceStep r v act : tr) = do
167168 let showR (Right x) = show x
168169 showR (Left err) = " fail " ++ showsPrec 10 err " "
169- monitor $ counterexample (showR r ++ " <- " ++ show (polarAction act))
170+ pre | v `wellTypedIn` used = show v ++ " @ "
171+ | otherwise = " "
172+ monitor $ counterexample (pre ++ showR r ++ " <- " ++ show (polarAction act))
170173 monitor $ monitoringPar @ state @ m (polarAction act) (lookUpVar env) r
171- monitorTrace env' tr
174+ monitorTrace used env' tr
172175 where
173176 env' | Right val <- r = (v :== val) : env
174177 | otherwise = env
0 commit comments