@@ -211,7 +211,7 @@ instance {-# OVERLAPPING #-} IsPerformResult Void a where
211211instance {-# OVERLAPPABLE #-} (EitherIsh e a ~ Either e a ) => IsPerformResult e a where
212212 performResultToEither = id
213213
214- class (forall a . Show (Action state a ), Monad m ) => RunModel state m where
214+ class (forall a . Show (Action state a ), Show ( Error state m ), Monad m ) => RunModel state m where
215215 -- | The type of errors that actions can throw. If this is defined as anything
216216 -- other than `Void` `perform` is required to return `Either (Error state) a`
217217 -- instead of `a`.
@@ -377,7 +377,7 @@ instance StateModel state => Show (Actions state) where
377377showWithUsed :: StateModel state => VarContext -> Actions state -> String
378378showWithUsed ctx (Actions as) =
379379 let as' = WithUsedVars (combineContexts ctx $ usedVariables (Actions as)) <$> as
380- in intercalate " \n " $ zipWith (++) (" do " : repeat " " ) (map show as' ++ [" pure ()" ])
380+ in intercalate " \n " $ zipWith (++) (" do " : repeat " " ) (map show as' ++ [" pure ()" | null as' ])
381381
382382usedVariables :: forall state . StateModel state => Actions state -> VarContext
383383usedVariables (Actions as) = go initialAnnotatedState as
@@ -683,11 +683,11 @@ commonActions ParallelActions{linearActions = Actions steps, ..} =
683683
684684threadAActions :: ParallelActions state -> [Step state ]
685685threadAActions ParallelActions {linearActions = Actions steps, .. } =
686- [ step | step @ ( v := _) <- steps, elem (unsafeVarIndex v) threadATags ]
686+ [ v := s{polarity = PosPolarity } | v := s <- steps, elem (unsafeVarIndex v) threadATags ]
687687
688688threadBActions :: ParallelActions state -> [Step state ]
689689threadBActions ParallelActions {linearActions = Actions steps, .. } =
690- [ step | step @ ( v := _) <- steps, elem (unsafeVarIndex v) threadBTags ]
690+ [ v := s{polarity = PosPolarity } | v := s <- steps, elem (unsafeVarIndex v) threadBTags ]
691691
692692instance StateModel state => Show (ParallelActions state ) where
693693 show pas =
@@ -793,12 +793,13 @@ runParActions :: ( StateModel state
793793 , ForkYou m
794794 ) => ParallelActions state -> PropertyM m ()
795795runParActions pas = do
796- monitor $ counterexample " -- Monitoring main thread"
797796 (trC, env) <- run $ runTracing mempty $ commonActions pas
798797 joinA <- run $ forkThread $ runTracing env (threadAActions pas)
799798 joinB <- run $ forkThread $ runTracing env (threadBActions pas)
800799 (trA, _) <- run joinA
801800 (trB, _) <- run joinB
801+ monitor $ counterexample " -- Monitoring main thread"
802+ monitorTrace mempty trC
802803 monitor $ counterexample " -- Monitoring thread A"
803804 monitorTrace env trA
804805 monitor $ counterexample " -- Monitoring thread B"
@@ -811,8 +812,11 @@ runParActions pas = do
811812monitorTrace :: forall state m . (StateModel state , RunModelPar state m )
812813 => Env -> Trace state m -> PropertyM m ()
813814monitorTrace _env [] = pure ()
814- monitorTrace env (TraceStep r v step : tr) = do
815- monitor $ monitoringPar @ state @ m (polarAction step) (lookUpVar env) r
815+ monitorTrace env (TraceStep r v act : tr) = do
816+ let showR (Right x) = show x
817+ showR (Left err) = " fail " ++ showsPrec 10 err " "
818+ monitor $ counterexample (showR r ++ " <- " ++ show (polarAction act))
819+ monitor $ monitoringPar @ state @ m (polarAction act) (lookUpVar env) r
816820 monitorTrace env' tr
817821 where
818822 env' | Right val <- r = (v :== val) : env
0 commit comments