1+ module TicketTests
2+
3+ open FsCheck.Xunit
4+ open Swensen.Unquote
5+ open Ticket
6+ open Ticket.Folds
7+
8+ /// We want to generate Allocate requests with and without the same listId in some cases
9+ let (| MaybeSameCommands |) = function
10+ | Allocate _ as x, Allocate _, cmd3, Choice1Of2 () -> x, x, cmd3
11+ | cmd1, ( Allocate _ as x), Allocate _, Choice1Of2 () -> cmd1, x, x
12+ | cmd1, cmd2, cmd3, ( Choice1Of2 ()| Choice2Of2 ()) -> cmd1, cmd2, cmd3
13+
14+ /// Explicitly generate sequences with the same allocator running twice or three times
15+ let (| MaybeSameIds |) = function
16+ | Choice1Of4 a -> a, a, a
17+ | Choice2Of4 ( a, b) -> a, a, b
18+ | Choice3Of4 ( a, b) -> a, b, b
19+ | Choice4Of4 ( a, b, c) -> a, b, c
20+
21+ let (| Invariants |) = function
22+ // Revokes always succeed iff Unallocated
23+ | Unallocated, Revoke, true , [], Unallocated ->
24+ ()
25+ // Everything else fails
26+ | _, _, res, e, _ ->
27+ test <@ not res && List.isEmpty e @>
28+
29+ let (| ReservedCases | _ |) allocator = function
30+ // Reserve given unallocated
31+ | Unallocated, Reserve, true , [ Events.Reserved { allocatorId = a }], state ->
32+ test <@ a = allocator && state = Reserved a @>
33+ Some ()
34+ // Idempotent reserve request
35+ | Reserved a, Reserve, true , [], _ ->
36+ test <@ a = allocator @>
37+ Some ()
38+ // Revokes not by the owner are reported as successful, but we force the real owner to do the real relinquish
39+ | ( Reserved by | Allocated( by,_)), Revoke, true , [], _ ->
40+ test <@ by <> allocator @>
41+ Some ()
42+ // Revokes succeed iff by the owner
43+ | ( Reserved by | Allocated( by,_)), Revoke, true , [ Events.Revoked], Unallocated ->
44+ test <@ by = allocator @>
45+ Some ()
46+ // Reservations can transition to Allocations as long as it's the same Allocator requesting
47+ | Reserved a, Allocate l, true , [ Events.Allocated { allocatorId = ea; listId = el }], Allocated ( sa, sl) ->
48+ test <@ a = allocator && a = ea && a = sa && l = el && l = sl @>
49+ Some()
50+ | _ -> None
51+
52+ let [<Property>] properties ( MaybeSameIds ( a1 , a2 , a3 )) ( MaybeSameCommands ( c1 , c2 , c3 )) =
53+ let res , events = decide a1 c1 Folds.initial
54+ let state1 = Folds.fold Folds.initial events
55+
56+ match Folds.initial, c1, res, events, state1 with
57+ | _, Reserve, true , [ Events.Reserved { allocatorId = a }], Reserved sa ->
58+ test <@ a = a1 && sa = a1 @>
59+ | Invariants -> ()
60+
61+ let res , events = decide a2 c2 state1
62+ let state2 = Folds.fold state1 events
63+ match state1, c2, res, events, state2 with
64+ | ReservedCases a2 -> ()
65+ | Invariants -> ()
66+
67+ let res , events = decide a3 c3 state2
68+ let state3 = Folds.fold state2 events
69+ match state2, c3, res, events, state3 with
70+ // Idempotent allocate ignore
71+ | Allocated ( a, l), Allocate l3, true , [], _ ->
72+ test <@ a = a3 && l = l3 @>
73+ // Allocated -> Revoked
74+ | Allocated ( a,_), Revoke, true , [ Events.Revoked], Unallocated ->
75+ test <@ a = a3 @>
76+ | ReservedCases a3 -> ()
77+ | Invariants -> ()
78+
79+ let [<Property>] ``codec can roundtrip`` event =
80+ let ee = Events.codec.Encode( None, event)
81+ let ie = FsCodec.Core.TimelineEvent.Create( 0 L, ee.EventType, ee.Data)
82+ test <@ Some event = Events.codec.TryDecode ie @>
0 commit comments