@@ -31,48 +31,48 @@ p_correctAgencies :: ProtocolDescription (TestCodec ()) -> Property
3131p_correctAgencies d =
3232 counterexample (show stateAgencyMap) .
3333 once $
34- counterexample " EndState" (lookup " EndState" stateAgencyMap === Just NobodyAgencyID )
34+ counterexample " EndState" (lookup ( State " EndState" ) stateAgencyMap === Just NobodyAgencyID )
3535 .&&.
36- counterexample " InitialState" (lookup " InitialState" stateAgencyMap === Just ServerAgencyID )
36+ counterexample " InitialState" (lookup ( State " InitialState" ) stateAgencyMap === Just ServerAgencyID )
3737 .&&.
38- counterexample " IdleState" (lookup " IdleState" stateAgencyMap === Just ServerAgencyID )
38+ counterexample " IdleState" (lookup ( State " IdleState" ) stateAgencyMap === Just ServerAgencyID )
3939 .&&.
40- counterexample " WaitForConfirmationState" (lookup " WaitForConfirmationState" stateAgencyMap === Just ClientAgencyID )
40+ counterexample " WaitForConfirmationState" (lookup ( State " WaitForConfirmationState" ) stateAgencyMap === Just ClientAgencyID )
4141 .&&.
42- counterexample " WaitForInfoState" (lookup " WaitForInfoState" stateAgencyMap === Just ClientAgencyID )
42+ counterexample " WaitForInfoState" (lookup ( State " WaitForInfoState" ) stateAgencyMap === Just ClientAgencyID )
4343 .&&.
44- counterexample " WaitForPublicKeyState" (lookup " WaitForPublicKeyState" stateAgencyMap === Just ClientAgencyID )
44+ counterexample " WaitForPublicKeyState" (lookup ( State " WaitForPublicKeyState" ) stateAgencyMap === Just ClientAgencyID )
4545 where
4646 stateAgencyMap = [(state, agency) | (state, _, agency) <- protocolStates d]
4747
4848p_correctStateTransitions :: ProtocolDescription (TestCodec () ) -> Property
4949p_correctStateTransitions d =
5050 once $
51- checkMessage " VersionMessage" " InitialState" " IdleState"
51+ checkMessage " VersionMessage" ( State " InitialState" ) ( State " IdleState" )
5252 .&&.
53- checkMessage " GenStagedKeyMessage" " IdleState" " WaitForPublicKeyState"
53+ checkMessage " GenStagedKeyMessage" ( State " IdleState" ) ( State " WaitForPublicKeyState" )
5454 .&&.
55- checkMessage " QueryStagedKeyMessage" " IdleState" " WaitForPublicKeyState"
55+ checkMessage " QueryStagedKeyMessage" ( State " IdleState" ) ( State " WaitForPublicKeyState" )
5656 .&&.
57- checkMessage " DropStagedKeyMessage" " IdleState" " WaitForPublicKeyState"
57+ checkMessage " DropStagedKeyMessage" ( State " IdleState" ) ( State " WaitForPublicKeyState" )
5858 .&&.
59- checkMessage " PublicKeyMessage" " WaitForPublicKeyState" " IdleState"
59+ checkMessage " PublicKeyMessage" ( State " WaitForPublicKeyState" ) ( State " IdleState" )
6060 .&&.
61- checkMessage " InstallKeyMessage" " IdleState" " WaitForConfirmationState"
61+ checkMessage " InstallKeyMessage" ( State " IdleState" ) ( State " WaitForConfirmationState" )
6262 .&&.
63- checkMessage " InstallResultMessage" " WaitForConfirmationState" " IdleState"
63+ checkMessage " InstallResultMessage" ( State " WaitForConfirmationState" ) ( State " IdleState" )
6464 .&&.
65- checkMessage " RequestInfoMessage" " IdleState" " WaitForInfoState"
65+ checkMessage " RequestInfoMessage" ( State " IdleState" ) ( State " WaitForInfoState" )
6666 .&&.
67- checkMessage " InfoMessage" " WaitForInfoState" " IdleState"
67+ checkMessage " InfoMessage" ( State " WaitForInfoState" ) ( State " IdleState" )
6868 .&&.
69- checkMessage " AbortMessage" " InitialState" " EndState"
69+ checkMessage " AbortMessage" ( State " InitialState" ) ( State " EndState" )
7070 .&&.
71- checkMessage " EndMessage" " IdleState" " EndState"
71+ checkMessage " EndMessage" ( State " IdleState" ) ( State " EndState" )
7272 .&&.
73- checkMessage " ProtocolErrorMessage" " st " " EndState"
73+ checkMessage " ProtocolErrorMessage" AnyState ( State " EndState" )
7474 where
75- checkMessage :: String -> String -> String -> Property
75+ checkMessage :: String -> StateRef -> StateRef -> Property
7676 checkMessage msgName fromState toState =
7777 counterexample msgName $ do
7878 msg <- findMessage msgName
0 commit comments