Junior Developer tries their best

Introduction
1. Your bio
2. Your assignment
The first attempt
1. Modeling
2. Verification
The second attempt
1. Modeling
2. Verification
The working attempt
1. Modeling
2. Verification
Next steps

Introduction

Your bio

You recently graduated from a good computer science program. Not only do you have a firm grasp on CS fundamentals, you’ve also taken electives in operating system and compiler design. None of that has been much help here, though. You keep waiting for someone to ask you to traverse a tree or write a new lexer for C, but you’re starting to fear that day will never come.

Your assignment

Try to create a solution that implements the Enterprise Architect’s specification.
Use the model checker to get your solution working.

The first attempt

Modeling

Note: We are assuming the junior programmer is fully competent in TLA+ and code style. Only the architectural and/or requirements knowledge will be lacking.

You start with a simple and clean solution that meets the requirements as you understood them:

------------------------------- MODULE juniorv1 -------------------------------

(***************************************************************************)
(* Redeclaration of specdatamodels variables                               *)
(***************************************************************************)

EXTENDS Sequences, Naturals, FiniteSets

CONSTANT USERS

CONSTANTS
    SubscriptionFee,
    CancellationFee,
    FailedPaymentFee

VARIABLES
    month,
    database,
    events 

vars == <<events, month, database>>

INSTANCE specdatamodels

Now == Len(events)

Months == 0..10

(***************************************************************************)
(* Strong Typing                                                           *)
(***************************************************************************)

Month == Nat

(***************************************************************************)
(* Database Rows                                                           *)
(***************************************************************************)

UserRow == [
    subscribed: BOOLEAN,
    \* Forget canceled
    inTrial: BOOLEAN,
    trialStartTime: Nat,
    billedForMonth: Nat
]

BillQueueItem == [
    user: USERS,
    fee: Fees
]

TypeOk ==
    /\ EventsOk
    /\ month \in Month
    /\ database.users \in [USERS -> UserRow]
    /\ database.billQueue \in Seq(BillQueueItem)

    
(***************************************************************************)
(* API endpoints                                                           *)
(***************************************************************************)


StartSubscription(u) ==
    /\ database.users[u].subscribed = FALSE
    /\ database' = [database EXCEPT
                        !["users"][u].subscribed = TRUE
                   ]
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "startsubscription", user |-> u])
    /\ UNCHANGED month


CancelSubscription(u) ==
    /\ database.users[u].subscribed = TRUE
    /\ database' = 
        [database EXCEPT
            !["users"][u].subscribed = FALSE,
            \* Charge cancellation fee
            !["billQueue"] = 
                Append(database.billQueue, 
                    [user |-> u, fee |-> CancellationFee])
        ]
                   
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "cancelsubscription", user |-> u])
    /\ UNCHANGED <<month>>

    
StartTrial(u) ==
    /\ database.users[u].inTrial = FALSE
    /\ database.users[u].subscribed = FALSE
    /\ database' = [database EXCEPT
                        !["users"][u].inTrial = TRUE]
                        
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "starttrial", user |-> u])
    /\ UNCHANGED <<month>>
    

CancelTrial(u) ==
    /\ database.users[u].inTrial = TRUE
    /\ database' = [database EXCEPT
                        !["users"][u].inTrial = FALSE
                   ]
                   
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "canceltrial", user |-> u])
    /\ UNCHANGED <<month>>


WatchVideo(u) ==
    /\ \/ database.users[u].subscribed = TRUE
       \/ database.users[u].inTrial = TRUE
    
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "watchvideo", user |-> u])
    /\ UNCHANGED <<month, database>>

\* Stub method, do not change
Bill(u, fee) ==
    /\ events' = Append(events, [type |-> "bill", 
                                 user |-> u, 
                                 fee |-> fee])

PaymentFailed(u, fee) ==
    /\ database' = [database EXCEPT
                        !["users"][u].subscribed = FALSE
                   ]
    
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "paymentfailed", 
                                 user |-> u , 
                                 fee |-> fee])
    /\ UNCHANGED <<month>>

(***************************************************************************)
(* Recurring Operations                                                    *)
(***************************************************************************)

\* This the the state that calls the Payment Failed API
ExistingBillFailed == 
    \/ \E i \in 1..Len(events):
        \* Only a past bill can fail
        /\ events[i] \in BillEvent
        /\ PaymentFailed(events[i].user, events[i].fee)


BillSubscribedUsers ==
    \E u \in USERS:
        \* That is subscribed
        /\ \/ database.users[u].subscribed = TRUE
           \* Subscribed from a trial so bill
           \/ /\ database.users[u].inTrial = TRUE
              /\ database.users[u].trialStartTime < month
        \* Ensure users are not double billed
        /\ database.users[u].billedForMonth < month
        /\ database' = 
            [database EXCEPT
                \* Add subscription fee
                !["billQueue"] = 
                    Append(database.billQueue, 
                            [user |-> u, fee |-> SubscriptionFee]),
                !["users"][u].billedForMonth = month
            ]

ProcessBills ==
    /\ Len(database.billQueue) > 0
    /\ LET bill == Head(database.billQueue) IN
        \* Bills user
        /\ Bill(bill.user, bill.fee)
        /\ database' = 
            [database EXCEPT
                \* Removes head of queue
                !["billQueue"] = 
                    SubSeq(database.billQueue, 
                    2, Len(database.billQueue))
            ]

(***************************************************************************)
(* Stub method that prevents the month from passing until all operations   *)
(* are complete. Represent worker methods, etc.                            *)
(***************************************************************************)
HandledMonth ==
    /\ ~ENABLED BillSubscribedUsers
    /\ ~ENABLED ProcessBills

\* DO NOT MODIFY
MonthPasses ==
    /\ HandledMonth
    /\ month' = month + 1
    /\ events' = Append(events, [type |-> "monthpass"])
    /\ UNCHANGED <<database>>

(***************************************************************************)
(* Specification                                                           *)
(***************************************************************************)
Init ==
    /\ events = <<>> \* Events must be initialized empty, per stub
    /\ month = 0
    /\ database = [
            \* Users start with everything unset
            users |-> 
                [u \in USERS |-> 
                   [
                    subscribed |-> FALSE,
                    inTrial |-> FALSE,
                    trialStartTime |-> 0,
                    billedForMonth |-> 0
                   ]
                ],
            \* Bill queue starts empty
            billQueue |-> <<>>
       ]


(*
Next ==
    \* Required by stub
    \/ MonthPasses
    \* State modified below
    \/ \E u \in USERS:
            \/ StartSubscription(u)
            \/ CancelSubscription(u)
            \/ StartTrial(u)
            \/ CancelTrial(u)
            \/ WatchVideo(u)
            \* Add more user based states
    \* Payment failing behavior is part of spec not implementation
    \/ ExistingBillFailed
    \/ BillSubscribedUsers
*)

=============================================================================
\* Modification History
\* Last modified Sun Jun 19 17:39:21 MST 2022 by elliotswart
\* Created Fri Jun 17 00:43:20 MST 2022 by elliotswart

Verification

Your solution does not hold up under test.

Next Section

Download Configuration

Invariant StartSubscriptionAccessControl is violated.

1. Initial predicate
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0}
  - billQueue :
- events :
- month : 0
2. StartTrial A trial starts, but user can still subscribe.
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>true, "trialStartTime"=>0, "billedForMonth"=>0}
  - billQueue :
- events
  1. - user : u1
    - type : starttrial
- month : 0
3. MonthPasses A month passes, converting trial into a full subscription. Now you shouldn't be able to start a subscription, but you still can.
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>true, "trialStartTime"=>0, "billedForMonth"=>0}
  - billQueue :
- events
  1. - user : u1
    - type : starttrial
  2. - type : monthpass
- month : 1

There are basic logical errors that need to be fixed.

The second attempt

Modeling

For this next attempt you work through all the standard logical errors around access control.

------------------------------ MODULE juniorv2 ------------------------------

(***************************************************************************)
(* Database Rows                                                           *)
(***************************************************************************)

UserRow == [
    subscribed: BOOLEAN,
    \* Forget canceled
    inTrial: BOOLEAN,
    trialStartTime: Nat,
    billedForMonth: Nat,
    hasHadTrialOrSubscription: BOOLEAN,
    hasCancelled: BOOLEAN,
    cancelMonth: Nat
]

StartSubscription(u) ==
    \* Not subscribed
    /\ /\ database.users[u].subscribed = FALSE
       /\ \/ database.users[u].inTrial = FALSE
          \/ database.users[u].trialStartTime = month
          
    /\ database' = 
        [database EXCEPT
              !["users"][u].subscribed = TRUE,
              !["users"][u].hasHadTrialOrSubscription = TRUE,
              !["users"][u].hasCancelled = FALSE
        ]
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "startsubscription", user |-> u])
    /\ UNCHANGED month


CancelSubscription(u) ==
    \* Subscribed
    /\ \/ database.users[u].subscribed = TRUE
       \/ /\ database.users[u].inTrial = TRUE
          /\ database.users[u].trialStartTime < month
    /\ database' = 
        [database EXCEPT
            !["users"][u].subscribed = FALSE,
            !["users"][u].inTrial = FALSE,
            !["users"][u].hasCancelled = TRUE,
            !["users"][u].cancelMonth = month,
            \* Charge cancellation fee
            !["billQueue"] = 
                Append(database.billQueue, 
                    [user |-> u, fee |-> CancellationFee])
        ]
                   
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "cancelsubscription", user |-> u])
    /\ UNCHANGED <<month>>

StartTrial(u) ==
    /\ database.users[u].inTrial = FALSE
    /\ database.users[u].subscribed = FALSE
    /\ database.users[u].hasHadTrialOrSubscription = FALSE
    /\ database' = [database EXCEPT
                        !["users"][u].inTrial = TRUE,
                        !["users"][u].trialStartTime = month,
                        !["users"][u].hasHadTrialOrSubscription = TRUE
                   ]
                        
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "starttrial", user |-> u])
    /\ UNCHANGED <<month>>
    

CancelTrial(u) ==
    \* In active trial
    /\ database.users[u].inTrial = TRUE
    /\ database.users[u].trialStartTime = month
    \* And not subscribed 
    /\ database.users[u].subscribed = FALSE
    /\ database' = [database EXCEPT
                        !["users"][u].inTrial = FALSE
                   ]
                   
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "canceltrial", user |-> u])
    /\ UNCHANGED <<month>>


WatchVideo(u) ==
    /\ \/ database.users[u].subscribed = TRUE
       \/ database.users[u].inTrial = TRUE
       \* Remove video access at the end of canceled month
       \/ /\ database.users[u].hasCancelled = TRUE
          /\ database.users[u].cancelMonth = month
    
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "watchvideo", user |-> u])
    /\ UNCHANGED <<month, database>>

(***************************************************************************)
(* Recurring Operations                                                    *)
(***************************************************************************)

BillSubscribedUsers ==
    /\ \E u \in USERS:
        \* That is subscribed
        /\ \/ database.users[u].subscribed = TRUE
           \* Subscribed from a trial so bill
           \/ /\ database.users[u].inTrial = TRUE
              /\ database.users[u].trialStartTime < month
        \* Ensure users are not double billed
        /\ database.users[u].billedForMonth < month
        /\ database' = 
            [database EXCEPT
                \* Add subscription fee
                !["billQueue"] = 
                    Append(database.billQueue, 
                            [user |-> u, fee |-> SubscriptionFee]),
                !["users"][u].billedForMonth = month
            ]
    /\ UNCHANGED <<events, month>>


=============================================================================
\* Modification History
\* Last modified Sun Jun 19 17:44:01 MST 2022 by elliotswart
\* Created Sun Jun 19 16:56:29 MST 2022 by elliotswart

Verification

You test again, running into a billing issue.

Next Section

Download Configuration

Invariant SubscribedUsersBilledStartOfMonth is violated.

1. Initial predicate
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>false, "hasCancelled"=>false, "cancelMonth"=>0}
  - billQueue :
- events :
- month : 0
2. StartSubscription Subscription states.
- database
  - users
    - u1: {"subscribed"=>true, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>true, "hasCancelled"=>false, "cancelMonth"=>0}
  - billQueue :
- events
  1. - user : u1
    - type : startsubscription
- month : 0
3. MonthPasses Month passes, and you assume user should be billed.
- database
  - users
    - u1: {"subscribed"=>true, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>true, "hasCancelled"=>false, "cancelMonth"=>0}
  - billQueue :
- events
  1. - user : u1
    - type : startsubscription
  2. - type : monthpass
- month : 1
4. CancelSubscription User cancels subscription before monthly billing could take place.
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>true, "hasCancelled"=>true, "cancelMonth"=>1}
  - billQueue
    1. : {"user"=>"u1", "fee"=>"CancellationFee"}
- events
  1. - user : u1
    - type : startsubscription
  2. - type : monthpass
  3. - user : u1
    - type : cancelsubscription
- month : 1
5. ProcessBills User is not billed.
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>true, "hasCancelled"=>true, "cancelMonth"=>1}
  - billQueue :
- events
  1. - user : u1
    - type : startsubscription
  2. - type : monthpass
  3. - user : u1
    - type : cancelsubscription
  4. - user : u1
    - fee : CancellationFee
    - type : bill
- month : 1
6. MonthPasses A month passes, and our system hasn't billed. Out of compliance.
- database
  - users
    - u1: {"subscribed"=>false, "inTrial"=>false, "trialStartTime"=>0, "billedForMonth"=>0, "hasHadTrialOrSubscription"=>true, "hasCancelled"=>true, "cancelMonth"=>1}
  - billQueue :
- events
  1. - user : u1
    - type : startsubscription
  2. - type : monthpass
  3. - user : u1
    - type : cancelsubscription
  4. - user : u1
    - fee : CancellationFee
    - type : bill
  5. - type : monthpass
- month : 2

This is a much more complex business logic error, and it’s of the sort that conventional testing may not catch.

The working attempt

Modeling

In the final attempt there you add significantly more billing logic.

------------------------------ MODULE juniorv3 ------------------------------

(***************************************************************************)
(* Database Rows                                                           *)
(***************************************************************************)

UserRow == [
    subscribed: BOOLEAN,
    \* Forget canceled
    inTrial: BOOLEAN,
    trialStartTime: Nat,
    billedForMonth: Nat,
    hasHadTrialOrSubscription: BOOLEAN,
    hasCancelled: BOOLEAN,
    cancelMonth: Nat,
    subscribeMonth: Nat
]
    
(***************************************************************************)
(* API endpoints                                                           *)
(***************************************************************************)


StartSubscription(u) ==
    \* Not subscribed
    /\ /\ database.users[u].subscribed = FALSE
       /\ \/ database.users[u].inTrial = FALSE
          \/ database.users[u].trialStartTime = month
          
    /\ database' = 
        [database EXCEPT
              !["users"][u].subscribed = TRUE,
              !["users"][u].hasHadTrialOrSubscription = TRUE,
              !["users"][u].hasCancelled = FALSE,
              !["users"][u].inTrial = FALSE,
              !["users"][u].subscribeMonth = month,
              !["billQueue"] = 
                    Append(database.billQueue, 
                        [user |-> u, 
                        fee |-> SubscriptionFee,
                        when |-> month])
        ]
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "startsubscription", user |-> u])
    /\ UNCHANGED month


CancelSubscription(u) ==
    LET updatedBillQueue == 
        IF \E i \in 1..Len(database.billQueue):
            /\ database.billQueue[i].user = u
            /\ database.billQueue[i].fee = SubscriptionFee
        THEN database.billQueue
        ELSE Append(database.billQueue, 
                [user |-> u, fee |-> SubscriptionFee, when |-> month])
    IN
    
    \* Subscribed
    /\ \/ database.users[u].subscribed = TRUE
       \/ /\ database.users[u].inTrial = TRUE
          /\ database.users[u].trialStartTime < month
    /\ database' = 
        [database EXCEPT
            !["users"][u].subscribed = FALSE,
            !["users"][u].inTrial = FALSE,
            !["users"][u].hasCancelled = TRUE,
            !["users"][u].cancelMonth = month,

            \* Charge cancellation fee
            !["billQueue"] = 
                Append(updatedBillQueue, 
                    [user |-> u, 
                     fee |-> CancellationFee,
                     when |-> month + 1])
        ]
                   
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "cancelsubscription", user |-> u])
    /\ UNCHANGED <<month>>


(***************************************************************************)
(* Recurring Operations                                                    *)
(***************************************************************************)

BillSubscribedUsers ==
    /\ \E u \in USERS:
        \* That is subscribed
        /\ \/ database.users[u].subscribed = TRUE
           \* Subscribed from a trial so bill
           \/ /\ database.users[u].inTrial = TRUE
              /\ database.users[u].trialStartTime < month
        \* Ensure users are not double billed
        /\ database.users[u].billedForMonth < month
        /\ database' = 
            [database EXCEPT
                \* Add subscription fee
                !["billQueue"] = 
                    Append(database.billQueue, 
                            [user |-> u, 
                            fee |-> SubscriptionFee,
                            when |-> month]),
                !["users"][u].billedForMonth = month
            ]
    /\ UNCHANGED <<events, month>>

ProcessBills ==
    /\ Len(database.billQueue) > 0
    /\ \E i \in 1..Len(database.billQueue):
        LET bill == database.billQueue[i] IN
        /\ bill.when = month
        \* Charge cancellation fees only a month after canceled
        \* and still canceled
        /\  \/ bill.fee # CancellationFee
            \/ /\ bill.fee = CancellationFee
               /\ \/ database.users[bill.user].subscribed = FALSE
                  \* Subscribed too late to cancel cancellation fee
                  \/database.users[bill.user].subscribeMonth >= bill.when
               
        /\ Bill(bill.user, bill.fee)
        /\ database' = 
            [database EXCEPT
                \* Removes head of queue
                !["billQueue"] = 
                    SubSeq(database.billQueue, 1, i-1) \o 
                    SubSeq(database.billQueue, i+1, Len(database.billQueue))
            ]
    /\ UNCHANGED <<month>>

=============================================================================
\* Modification History
\* Last modified Sun Jun 19 17:55:27 MST 2022 by elliotswart
\* Created Sun Jun 19 16:56:29 MST 2022 by elliotswart

The code is starting to look like a nightmare, but hopefully it will work.

Verification

Testing it leads to success!

Next Section

Download Configuration

State Name	Total States	Distinct States
All States	772157	153504

Next steps

So you’ve gotten a solution working, but frankly, it looks like it’ll be a nightmare to implement. Nested if statements all over the place. The database schema is sloppy. It’s time to ask for help.

Note: A valid criticism of the above would be that no one would model business logic like that. And it’s true, no one would model something that badly. But people push solutions much worse than this one to production every day. Maybe if they took the time to model, they wouldn’t.

Next: Principal Engineer saves the day