@@ -103,7 +103,7 @@ callSUT RunState{hReader, hWriter} req =
103103type Runtime = StateT RunState IO
104104
105105instance Realized IO ([InputBlock ], [EndorserBlock ], [[Vote ]]) ~ ([InputBlock ], [EndorserBlock ], [[Vote ]]) => RunModel NetworkModel Runtime where
106- perform net @ NetworkModel {nodeModel = LeiosState {.. }} (Step a) _ = case a of
106+ perform NetworkModel {nodeModel = LeiosState {.. }} (Step a) _ = case a of
107107 Tick -> do
108108 rs@ RunState {.. } <- get
109109 modify $ \ rs' -> rs'{unfetchedIBs = mempty , unfetchedEBs = mempty , unfetchedVotes = mempty }
@@ -125,15 +125,15 @@ instance Realized IO ([InputBlock], [EndorserBlock], [[Vote]]) ~ ([InputBlock],
125125 NewEB eb -> do
126126 modify $ \ rs -> rs{unfetchedEBs = unfetchedEBs rs ++ pure eb}
127127 pure (mempty , mempty , mempty )
128- NewVote v -> do
129- modify $ \ rs -> rs{unfetchedVotes = unfetchedVotes rs ++ pure [v ]}
128+ NewVote x -> do
129+ modify $ \ rs -> rs{unfetchedVotes = unfetchedVotes rs ++ pure [x ]}
130130 pure (mempty , mempty , mempty )
131131
132- postcondition (net @ NetworkModel {nodeModel = s}, NetworkModel {nodeModel = s'}) (Step a) _ (ibs, ebs, votes) = do
132+ postcondition (NetworkModel {nodeModel = s}, NetworkModel {nodeModel = s'}) (Step a) _ (ibs, ebs, votes) = do
133133 let (expectedIBs, expectedEBs, expectedVotes) = maybe (mempty , mempty , mempty ) fst $ transition s a
134134 let ok = (ibs, ebs) == (expectedIBs, expectedEBs)
135135 monitorPost . counterexample . show $ " action $" <+> pPrint a
136- when (a == Tick && slot s == slot s' + 1 ) $
136+ when (a == Tick && slot s + 1 /= slot s') $
137137 monitorPost . counterexample $
138138 " -- new slot: " ++ show (slot s')
139139 unless (null ibs) $
0 commit comments