@@ -103,13 +103,20 @@ instance Show a => Show (Variable a) where
103103 show (Value x) = show x
104104 show (Variable u) = "<<" ++ show (hashUnique u) ++ ">>"
105105
106−type BundleId = Int
106+-- | In the implementation "bundles" are purely a conceptual idea, but in the
107+-- verifier we need to concretize this notion
108+--
109+-- Invariant: first endpoint address < second endpoint address
110+type BundleId = (EndPointAddress, EndPointAddress, Int)
111+
112+incrementBundleId :: BundleId -> BundleId
113+incrementBundleId (a, b, i) = (a, b, i + 1)
107114
108115data ConnectionInfo = ConnectionInfo {
109− source :: EndPointAddress
110− , target :: EndPointAddress
111− , connectionId :: Variable ConnectionId
112− , bundleId :: BundleId
116+ source :: EndPointAddress
117+ , target :: EndPointAddress
118+ , connectionId :: Variable ConnectionId
119+ , connectionBundle :: BundleId
113120 }
114121 deriving Show
115122
@@ -125,9 +132,10 @@ data RunState = RunState {
125132 , _connections :: [(Connection, ConnectionInfo)]
126133 , _expectedEvents :: Map EndPointAddress [ExpEvent]
127134 , _forwardingThreads :: [ThreadId]
135+ -- | Invariant: not mayBreak && broken
128136 , _mayBreak :: Set BundleId
129137 , _broken :: Set BundleId
130− , _currentBundle :: BundleId
138+ , _currentBundle :: Map (EndPointAddress, EndPointAddress) BundleId
131139 }
132140
133141initialRunState :: RunState
@@ -138,7 +146,7 @@ initialRunState = RunState {
138146 , _forwardingThreads = []
139147 , _mayBreak = Set.empty
140148 , _broken = Set.empty
141− , _currentBundle = 0
149+ , _currentBundle = Map.empty
142150 }
143151
144152verify :: (Transport, TransportInternals) -> Script -> IO (Either String ())
@@ -153,8 +161,8 @@ verify (transport, transportInternals) script = do
153161 mEndPoint <- liftIO $ newEndPoint transport
154162 case mEndPoint of
155163 Right endPoint -> do
156− modify endPoints (snoc endPoint)
157164 tid <- liftIO $ forkIO (forward endPoint)
165+ modify endPoints (snoc endPoint)
158166 modify forwardingThreads (tid :)
159167 Left err ->
160168 liftIO $ throwIO err
@@ -162,23 +170,24 @@ verify (transport, transportInternals) script = do
162170 endPointA <- get (endPointAtIx i)
163171 endPointB <- address <$> get (endPointAtIx j)
164172 mConn <- liftIO $ connect endPointA endPointB ReliableOrdered defaultConnectHints
173+ let bundleId = currentBundle (address endPointA) endPointB
165174 case mConn of
166175 Right conn -> do
167− bundleBroken <- get currentBundle >>= get . broken
176+ bundleBroken <- get bundleId >>= get . broken
168177 currentBundleId <- if bundleBroken
169− then modify currentBundle (+ 1) >> get currentBundle
170− else get currentBundle
178+ then modify bundleId incrementBundleId >> get bundleId
179+ else get bundleId
171180 connId <- Variable <$> liftIO newUnique
172181 let connInfo = ConnectionInfo {
173− source = address endPointA
174− , target = endPointB
175− , connectionId = connId
176− , bundleId = currentBundleId
182+ source = address endPointA
183+ , target = endPointB
184+ , connectionId = connId
185+ , connectionBundle = currentBundleId
177186 }
178187 modify connections (snoc (conn, connInfo))
179188 modify (expectedEventsAt endPointB) (snoc (ExpConnectionOpened connInfo))
180189 Left err -> do
181− currentBundleId <- get currentBundle
190+ currentBundleId <- get bundleId
182191 expectingBreak <- get $ mayBreak currentBundleId
183192 if expectingBreak
184193 then do
@@ -196,12 +205,12 @@ verify (transport, transportInternals) script = do
196205 case mResult of
197206 Right () -> return ()
198207 Left err -> do
199− expectingBreak <- get $ mayBreak (bundleId connInfo)
200− isBroken <- get $ broken (bundleId connInfo)
208+ expectingBreak <- get $ mayBreak (connectionBundle connInfo)
209+ isBroken <- get $ broken (connectionBundle connInfo)
201210 if expectingBreak || isBroken
202211 then do
203− set (mayBreak (bundleId connInfo)) False
204− set (broken (bundleId connInfo)) True
212+ set (mayBreak (connectionBundle connInfo)) False
213+ set (broken (connectionBundle connInfo)) True
205214 else
206215 liftIO $ throwIO err
207216 modify (expectedEventsAt (target connInfo)) (snoc (ExpReceived connInfo payload))
@@ -211,7 +220,7 @@ verify (transport, transportInternals) script = do
211220 liftIO $ do
212221 sock <- socketBetween transportInternals endPointA endPointB
213222 scheduleReadAction sock n (sClose sock)
214− currentBundleId <- get currentBundle
223+ currentBundleId <- get (currentBundle endPointA endPointB)
215224 set (mayBreak currentBundleId) True
216225 modify (expectedEventsAt endPointA) (snoc (ExpConnectionLost currentBundleId endPointB))
217226 modify (expectedEventsAt endPointB) (snoc (ExpConnectionLost currentBundleId endPointA))
@@ -291,9 +300,9 @@ possibleTraces = go
291300 removeBundle bid = filter ((/= bid) . eventBundleId)
292301
293302 eventBundleId :: ExpEvent -> BundleId
294− eventBundleId (ExpConnectionOpened connInfo) = bundleId connInfo
295− eventBundleId (ExpConnectionClosed connInfo) = bundleId connInfo
296− eventBundleId (ExpReceived connInfo _) = bundleId connInfo
303+ eventBundleId (ExpConnectionOpened connInfo) = connectionBundle connInfo
304+ eventBundleId (ExpConnectionClosed connInfo) = connectionBundle connInfo
305+ eventBundleId (ExpReceived connInfo _) = connectionBundle connInfo
297306 eventBundleId (ExpConnectionLost bid _) = bid
298307
299308 eventConnId :: ExpEvent -> Maybe (Variable ConnectionId)
@@ -543,6 +552,18 @@ script_BreakConnect = [
543552 , Connect 0 1
544553 ]
545554
555+-- | Simulate broken send, then reconnect
556+script_BreakSendReconnect :: Script
557+script_BreakSendReconnect = [
558+ NewEndPoint
559+ , NewEndPoint
560+ , Connect 0 1
561+ , BreakAfterReads 1 1 0
562+ , Send 0 ["ping1"]
563+ , Connect 0 1
564+ , Send 1 ["ping2"]
565+ ]
566+
546567--------------------------------------------------------------------------------
547568-- Main application driver --
548569--------------------------------------------------------------------------------
@@ -558,9 +579,10 @@ basicTests transport numEndPoints trans = [
558579tests :: (Transport, TransportInternals) -> [Test]
559580tests transport = [
560581 testGroup "Specific scripts" [
561− testOne "Bug1" transport script_Bug1
562− , testOne "BreakSend" transport script_BreakSend
563− , testOne "BreakConnect" transport script_BreakConnect
582+ testOne "Bug1" transport script_Bug1
583+ , testOne "BreakSend" transport script_BreakSend
584+ , testOne "BreakConnect" transport script_BreakConnect
585+ , testOne "BreakSendReconnect" transport script_BreakSendReconnect
564586 ]
565587 , testGroup "One endpoint, with delays" (basicTests transport 1 id)
566588 , testGroup "Two endpoints, with delays" (basicTests transport 2 id)
@@ -651,8 +673,12 @@ broken bid = aux >>> DAC.set bid
651673 aux :: Accessor RunState (Set BundleId)
652674 aux = accessor _broken (\bs st -> st { _broken = bs })
653675
654−currentBundle :: Accessor RunState BundleId
655−currentBundle = accessor _currentBundle (\bid st -> st { _currentBundle = bid })
676+currentBundle :: EndPointAddress -> EndPointAddress -> Accessor RunState BundleId
677+currentBundle i j = aux >>> if i < j then DAC.mapDefault (i, j, 0) (i, j)
678+ else DAC.mapDefault (j, i, 0) (j, i)
679+ where
680+ aux :: Accessor RunState (Map (EndPointAddress, EndPointAddress) BundleId)
681+ aux = accessor _currentBundle (\mp st -> st { _currentBundle = mp })
656682
657683--------------------------------------------------------------------------------
658684-- Pretty-printing --