Skip to content

Commit

Permalink
verifyAbstracTransition: transitions from TerminatedSt
Browse files Browse the repository at this point in the history
Allow transitions from `TermiantedSt` to `ReservedOutboundSt` or
`UnnegotiatedSt Inbound` state.
  • Loading branch information
coot committed Oct 20, 2021
1 parent 61ceee2 commit 0227860
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -1721,6 +1721,7 @@ verifyAbstractTransition Transition { fromState, toState } =
--

-- @Reserve@
(TerminatedSt, ReservedOutboundSt) -> True
(UnknownConnectionSt, ReservedOutboundSt) -> True
-- @Connected@
(ReservedOutboundSt, UnnegotiatedSt Outbound) -> True
Expand Down Expand Up @@ -1759,6 +1760,7 @@ verifyAbstractTransition Transition { fromState, toState } =
--

-- @Accepted@
(TerminatedSt, UnnegotiatedSt Inbound) -> True
(UnknownConnectionSt, UnnegotiatedSt Inbound) -> True
-- @Overwritten@
(ReservedOutboundSt, UnnegotiatedSt Inbound) -> True
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1605,7 +1605,7 @@ prop_multinode_Sim serverAcc (ArbDataFlow dataFlow) script =
-> AllProperty
. (counterexample $!
( "\nUnexpected transition: "
++ ppTransition tr)
++ show tr)
)
. verifyAbstractTransition
$ tr
Expand Down

0 comments on commit 0227860

Please sign in to comment.