@@ -103,13 +103,20 @@ instance Show a => Show (Variable a) where
103 show (Value x) = show x
103 show (Value x) = show x
104 show (Variable u) = "<<" ++ show (hashUnique u) ++ ">>"
104 show (Variable u) = "<<" ++ show (hashUnique u) ++ ">>"
106+-- | In the implementation "bundles" are purely a conceptual idea, but in the
107+-- verifier we need to concretize this notion
109+-- Invariant: first endpoint address < second endpoint address
106−type BundleId = Int
110+type BundleId = (EndPointAddress, EndPointAddress, Int)
112+incrementBundleId :: BundleId -> BundleId
113+incrementBundleId (a, b, i) = (a, b, i + 1)
108data ConnectionInfo = ConnectionInfo {
115data ConnectionInfo = ConnectionInfo {
109− source :: EndPointAddress
116+ source :: EndPointAddress
110− , target :: EndPointAddress
117+ , target :: EndPointAddress
111− , connectionId :: Variable ConnectionId
118+ , connectionId :: Variable ConnectionId
112− , bundleId :: BundleId
119+ , connectionBundle :: BundleId
114 deriving Show
121 deriving Show
@@ -125,9 +132,10 @@ data RunState = RunState {
125 , _connections :: [(Connection, ConnectionInfo)]
132 , _connections :: [(Connection, ConnectionInfo)]
126 , _expectedEvents :: Map EndPointAddress [ExpEvent]
133 , _expectedEvents :: Map EndPointAddress [ExpEvent]
127 , _forwardingThreads :: [ThreadId]
134 , _forwardingThreads :: [ThreadId]
135+ -- | Invariant: not mayBreak && broken
128 , _mayBreak :: Set BundleId
136 , _mayBreak :: Set BundleId
129 , _broken :: Set BundleId
137 , _broken :: Set BundleId
130− , _currentBundle :: BundleId
138+ , _currentBundle :: Map (EndPointAddress, EndPointAddress) BundleId
133initialRunState :: RunState
141initialRunState :: RunState
@@ -138,7 +146,7 @@ initialRunState = RunState {
138 , _forwardingThreads = []
146 , _forwardingThreads = []
139 , _mayBreak = Set.empty
147 , _mayBreak = Set.empty
140 , _broken = Set.empty
148 , _broken = Set.empty
141− , _currentBundle = 0
149+ , _currentBundle = Map.empty
144verify :: (Transport, TransportInternals) -> Script -> IO (Either String ())
152verify :: (Transport, TransportInternals) -> Script -> IO (Either String ())
@@ -153,8 +161,8 @@ verify (transport, transportInternals) script = do
153 mEndPoint <- liftIO $ newEndPoint transport
161 mEndPoint <- liftIO $ newEndPoint transport
154 case mEndPoint of
162 case mEndPoint of
155 Right endPoint -> do
163 Right endPoint -> do
156− modify endPoints (snoc endPoint)
157 tid <- liftIO $ forkIO (forward endPoint)
164 tid <- liftIO $ forkIO (forward endPoint)
165+ modify endPoints (snoc endPoint)
158 modify forwardingThreads (tid :)
166 modify forwardingThreads (tid :)
159 Left err ->
167 Left err ->
160 liftIO $ throwIO err
168 liftIO $ throwIO err
@@ -162,23 +170,24 @@ verify (transport, transportInternals) script = do
162 endPointA <- get (endPointAtIx i)
170 endPointA <- get (endPointAtIx i)
163 endPointB <- address <$> get (endPointAtIx j)
171 endPointB <- address <$> get (endPointAtIx j)
164 mConn <- liftIO $ connect endPointA endPointB ReliableOrdered defaultConnectHints
172 mConn <- liftIO $ connect endPointA endPointB ReliableOrdered defaultConnectHints
173+ let bundleId = currentBundle (address endPointA) endPointB
165 case mConn of
174 case mConn of
166 Right conn -> do
175 Right conn -> do
167− bundleBroken <- get currentBundle >>= get . broken
176+ bundleBroken <- get bundleId >>= get . broken
168 currentBundleId <- if bundleBroken
177 currentBundleId <- if bundleBroken
169− then modify currentBundle (+ 1) >> get currentBundle
178+ then modify bundleId incrementBundleId >> get bundleId
170− else get currentBundle
179+ else get bundleId
171 connId <- Variable <$> liftIO newUnique
180 connId <- Variable <$> liftIO newUnique
172 let connInfo = ConnectionInfo {
181 let connInfo = ConnectionInfo {
173− source = address endPointA
182+ source = address endPointA
174− , target = endPointB
183+ , target = endPointB
175− , connectionId = connId
184+ , connectionId = connId
176− , bundleId = currentBundleId
185+ , connectionBundle = currentBundleId
178 modify connections (snoc (conn, connInfo))
187 modify connections (snoc (conn, connInfo))
179 modify (expectedEventsAt endPointB) (snoc (ExpConnectionOpened connInfo))
188 modify (expectedEventsAt endPointB) (snoc (ExpConnectionOpened connInfo))
180 Left err -> do
189 Left err -> do
181− currentBundleId <- get currentBundle
190+ currentBundleId <- get bundleId
182 expectingBreak <- get $ mayBreak currentBundleId
191 expectingBreak <- get $ mayBreak currentBundleId
183 if expectingBreak
192 if expectingBreak
@@ -196,12 +205,12 @@ verify (transport, transportInternals) script = do
196 case mResult of
205 case mResult of
197 Right () -> return ()
206 Right () -> return ()
198 Left err -> do
207 Left err -> do
199− expectingBreak <- get $ mayBreak (bundleId connInfo)
208+ expectingBreak <- get $ mayBreak (connectionBundle connInfo)
200− isBroken <- get $ broken (bundleId connInfo)
209+ isBroken <- get $ broken (connectionBundle connInfo)
201 if expectingBreak || isBroken
210 if expectingBreak || isBroken
203− set (mayBreak (bundleId connInfo)) False
212+ set (mayBreak (connectionBundle connInfo)) False
204− set (broken (bundleId connInfo)) True
213+ set (broken (connectionBundle connInfo)) True
206 liftIO $ throwIO err
215 liftIO $ throwIO err
207 modify (expectedEventsAt (target connInfo)) (snoc (ExpReceived connInfo payload))
216 modify (expectedEventsAt (target connInfo)) (snoc (ExpReceived connInfo payload))
@@ -211,7 +220,7 @@ verify (transport, transportInternals) script = do
211 liftIO $ do
220 liftIO $ do
212 sock <- socketBetween transportInternals endPointA endPointB
221 sock <- socketBetween transportInternals endPointA endPointB
213 scheduleReadAction sock n (sClose sock)
222 scheduleReadAction sock n (sClose sock)
214− currentBundleId <- get currentBundle
223+ currentBundleId <- get (currentBundle endPointA endPointB)
215 set (mayBreak currentBundleId) True
224 set (mayBreak currentBundleId) True
216 modify (expectedEventsAt endPointA) (snoc (ExpConnectionLost currentBundleId endPointB))
225 modify (expectedEventsAt endPointA) (snoc (ExpConnectionLost currentBundleId endPointB))
217 modify (expectedEventsAt endPointB) (snoc (ExpConnectionLost currentBundleId endPointA))
226 modify (expectedEventsAt endPointB) (snoc (ExpConnectionLost currentBundleId endPointA))
@@ -291,9 +300,9 @@ possibleTraces = go
291 removeBundle bid = filter ((/= bid) . eventBundleId)
300 removeBundle bid = filter ((/= bid) . eventBundleId)
293 eventBundleId :: ExpEvent -> BundleId
302 eventBundleId :: ExpEvent -> BundleId
294− eventBundleId (ExpConnectionOpened connInfo) = bundleId connInfo
303+ eventBundleId (ExpConnectionOpened connInfo) = connectionBundle connInfo
295− eventBundleId (ExpConnectionClosed connInfo) = bundleId connInfo
304+ eventBundleId (ExpConnectionClosed connInfo) = connectionBundle connInfo
296− eventBundleId (ExpReceived connInfo _) = bundleId connInfo
305+ eventBundleId (ExpReceived connInfo _) = connectionBundle connInfo
297 eventBundleId (ExpConnectionLost bid _) = bid
306 eventBundleId (ExpConnectionLost bid _) = bid
299 eventConnId :: ExpEvent -> Maybe (Variable ConnectionId)
308 eventConnId :: ExpEvent -> Maybe (Variable ConnectionId)
@@ -543,6 +552,18 @@ script_BreakConnect = [
543 , Connect 0 1
552 , Connect 0 1
555+-- | Simulate broken send, then reconnect
556+script_BreakSendReconnect :: Script
557+script_BreakSendReconnect = [
561+ , BreakAfterReads 1 1 0
546--------------------------------------------------------------------------------
567--------------------------------------------------------------------------------
547-- Main application driver --
568-- Main application driver --
548--------------------------------------------------------------------------------
569--------------------------------------------------------------------------------
@@ -558,9 +579,10 @@ basicTests transport numEndPoints trans = [
558tests :: (Transport, TransportInternals) -> [Test]
579tests :: (Transport, TransportInternals) -> [Test]
559tests transport = [
580tests transport = [
560 testGroup "Specific scripts" [
581 testGroup "Specific scripts" [
561− testOne "Bug1" transport script_Bug1
582+ testOne "Bug1" transport script_Bug1
562− , testOne "BreakSend" transport script_BreakSend
583+ , testOne "BreakSend" transport script_BreakSend
563− , testOne "BreakConnect" transport script_BreakConnect
584+ , testOne "BreakConnect" transport script_BreakConnect
585+ , testOne "BreakSendReconnect" transport script_BreakSendReconnect
565 , testGroup "One endpoint, with delays" (basicTests transport 1 id)
587 , testGroup "One endpoint, with delays" (basicTests transport 1 id)
566 , testGroup "Two endpoints, with delays" (basicTests transport 2 id)
588 , testGroup "Two endpoints, with delays" (basicTests transport 2 id)
@@ -651,8 +673,12 @@ broken bid = aux >>> DAC.set bid
651 aux :: Accessor RunState (Set BundleId)
673 aux :: Accessor RunState (Set BundleId)
652 aux = accessor _broken (\bs st -> st { _broken = bs })
674 aux = accessor _broken (\bs st -> st { _broken = bs })
654−currentBundle :: Accessor RunState BundleId
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)
680+ aux :: Accessor RunState (Map (EndPointAddress, EndPointAddress) BundleId)
655−currentBundle = accessor _currentBundle (\bid st -> st { _currentBundle = bid })
681+ aux = accessor _currentBundle (\mp st -> st { _currentBundle = mp })
657--------------------------------------------------------------------------------
683--------------------------------------------------------------------------------
658-- Pretty-printing --
684-- Pretty-printing --