Link Search Menu Expand Document

Enterprise Architect gets us started

  1. Introduction
    1. Your bio
    2. Your assignment
  2. Creating the requirements document
    1. Functional requirements
    2. Non-Functional requirements
  3. Requirements summary
  4. Architecture
  5. Creating the Formal Specification Model
    1. The state machine
    2. Data Model
    3. Specification
    4. Stubs
  6. Summary

Introduction

Your bio

You’re the kind of person who uses acronyms like OLTP, OLAP and OAuth in a sentence and knows what they mean. Whenever your company gets together for a game of Whiteboard, you win hands down. It’s been a little while since you’ve coded anything, but it’s like riding a bike: terrifying and dangerous. Modeling languages are fair game though!

Your assignment

  1. Clarify the customers requirements into a requirements document
  2. Distill the requirements document down into a formal specification
  3. Come up with an architecture based on the requirements

By the end of this, coding the solution should be a piece of cake.

Note: The client has only contracted us to build the backend software and expose APIs. A different firm is handling the frontend.

Creating the requirements document

Through conversations with the customers, you have distilled their requirements into a standard format.

Functional requirements

ID Requirement
1 The system SHALL have a Start Subscription endpoint
1.1         that is web accessible as an HTTP endpoint
2 When a request is received by the Start Subscription endpoint
2.1         if the requesting User is Subscribed, the request SHALL return with 409 Conflict
2.2         if the requesting User is In Trial, the trial SHALL end and the requesting User SHALL be Subscribed
2.3         if the requesting User is Not Subscribed the requesting User SHALL be Subscribed
2.4         if the requesting User is scheduled to be Not Subscribed due to cancellation the requesting User SHALL remain Subscribed
3 The system SHALL have a Cancel Subscription endpoint
3.1         that is web accessible as an HTTP endpoint
4 When a request is received by the Cancel Subscription endpoint
4.1         if the requesting User is not Subscribed, the request SHALL return with 409 Conflict
4.2         if the requesting User is Subscribed
4.2.1                 the User SHALL be Not Subscribed at the end of the current month
4.2.2                 if the user is Not Subscribed at the end of the current month they SHALL be Billed a Cancellation Fee
5 The system SHALL have a Start Trial endpoint
5.1         that is web accessible as an HTTP endpoint
6 When a request is received by the Start Trial endpoint
6.1         if the requesting User is Subscribed, or In Trial the request SHALL return with 409 Conflict
6.2         if the requesting User has previously been Subscribed or In Trial the request SHALL return with 409 Conflict
6.3         if the requesting User is has never been Subscribed or In Trial, that User SHALL be In Trial. Justification: we only want new users to be able to start a trial
7 The system SHALL have a Cancel Trial Endpoint endpoint
7.1         that is web accessible as an HTTP endpoint
8 When a request is received by the Cancel Trial endpoint
8.1         if the requesting User is not In Trial the request SHALL return with 409 Conflict
8.2         if the requesting User is In Trial the User SHALL be Not Subscribed
9 The system SHALL have a Watch Video endpoint
9.1         that is web accessible as an HTTP endpoint
10 When a request is received by the Watch Video endpoint
10.1         if the requesting User is not In Trial or Subscribed the request SHALL return with 409 Conflict
10.2         if the requesting User is In Trial or Subscribed the system SHALL allow the User to Watch Video
11 When a User is In Trial at the end of the month that the trial was started they SHALL be Subscribed
12 When a User becomes Subscribed
12.1         they SHALL be Billed the Subscription Fee before the end of the month
12.2         if the requesting User has Post Due Payments they SHALL be Billed in that amount before the end of the month, and Post Due Payments SHALL be zeroed
13 When a User is Subscribed at the start of a month, they SHALL be Billed the Subscription Fee
14 The system SHALL be able to interface with the Payment Processor
14.1         it SHALL be able to call the Bill endpoint of the Payment Processor
14.2         it SHALL have a Payment Failed endpoint that can accept the Payment Processor callback
15 When a User is Billed the system SHALL call the Bill endpoint of the Payment Processor
16 When a callback is received to the Payment Failed endpoint for a User the system SHALL
16.1         mark the User as Not Subscribed
16.2         set Post Due Payments for the User to: (failed payment amount) + Failed Payment Fee

Non-Functional requirements

ID Requirement
1 The latency of all endpoints SHOULD be < 1 second
2 Data SHALL be encrypted at rest
3 Data SHALL be encrypted in transit

Requirements summary

You feel confident that you’ve gathered all the necessary requirements to ensure successful delivery on the contract. There are 44 requirements including sub-clauses, which is not that many, but you’re worried some might be forgotten due to the tight deliverable schedule. Formal modeling seems like a good way to ensure that doesn’t happen, but first you need to come up with an architecture.

Architecture

Based on the requirements, it’s safe to chose a simple architecture, with an autoscaling group of Business Logic Servers that access a Database hosted in a replica set. There is also an external Payment Processor that can accept bills, and occasionally provide Payment Failed callbacks.

Payment ProcessorDatabaseDatabase ConnectionBusiness Logic ServersClientsPayment Failed(user)Bill(user, amount)Start Subscription(user)Cancel Subscription(user)Start Trial(user)Cancel Trial(user)Watch Video(user)uses

Now that you’ve come up with the architecture, you’re satisfied that it will work within the requirements and your team won’t have any trouble with it.

Creating the Formal Specification Model

Looking over the requirements, it’s clear that only the Functional Requirements can be modeled. That might not always be true, but in this case they only influence implementation details and not the Business Logic itself. You don’t want to provide the implementation details; after all, that’s not your job. You need to write the spec in an implementation-agnostic way.

The state machine

You create a state machine of the user workflow. The state machine here will not necessarily translate directly to a model, but it’s still useful to have.

NotSubscribedSubscriptionStartedTrialStartedMonthElapsedTrialCanceledSubscriptionCanceledPaymentFailedOnly if not subscribed or had trial

Data Model

The data model is shared between the specification and all the implementations. It lays out all the event types used for observability.

Show Code Show LaTex
--------------------------- MODULE specdatamodels ---------------------------
\* This module will be imported into every implementation

EXTENDS Sequences

(***************************************************************************)
(* An ordered event stream of every event that occurs in the system.       *)
(* All the specifications will be written based on it.                     *)
(* This is an observability value that you wouldn't have access to in the  *)
(* implementation. We'll only have the API method stubs write to it; no    *)
(* implementation may read from it. This will be enforced with code review *)
(***************************************************************************)
VARIABLE events

\* Represents every potential user in the system
CONSTANT USERS

\* Constants that should be set to single model values to allow comparisons.
\* Only equality comparisons will be made.
CONSTANTS
    SubscriptionFee,
    CancellationFee,
    FailedPaymentFee

Fees == {SubscriptionFee, CancellationFee, FailedPaymentFee}

(***************************************************************************)
(* Event Types: Describes everything that can happen in the system         *)
(***************************************************************************)

MonthPassEvent == [type : {"monthpass"}]

StartSubscriptionEvent == [type : {"startsubscription"}, user: USERS]
CancelSubscriptionEvent == [type : {"cancelsubscription"}, user: USERS]

StartTrialEvent == [type : {"starttrial"}, user: USERS]
CancelTrialEvent == [type : {"canceltrial"}, user: USERS]

WatchVideoEvent == [type : {"watchvideo"}, user: USERS]

BillEvent == [type : {"bill"}, user: USERS, fee: Fees]
PaymentFailedEvent == [type : {"paymentfailed"}, user: USERS, fee: Fees]

Event ==
    MonthPassEvent \union
    StartSubscriptionEvent \union
    CancelSubscriptionEvent \union
    StartTrialEvent \union
    CancelTrialEvent \union
    WatchVideoEvent \union
    BillEvent \union
    PaymentFailedEvent

EventsOk ==
    events \in Seq(Event)
    
    
    
=============================================================================
\* Modification History
\* Last modified Fri Jun 17 00:07:38 MST 2022 by elliotswart
\* Created Thu Jun 16 20:19:00 MST 2022 by elliotswart

Specification

You trace every requirement above to the specification. This is to ensure that every requirement is either represented formally or deliberately excluded.

Show Code Show LaTex
-------------------------------- MODULE speccannonical --------------------------------

EXTENDS Naturals, Sequences, FiniteSets

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

VARIABLE events

CONSTANT USERS

CONSTANTS
    SubscriptionFee,
    CancellationFee,
    FailedPaymentFee

(***************************************************************************)
(* Logic to Test                                                           *)
(* Replace stubs below with implementation. Because there is no forward    *)
(* declaration, we invert what we'd ideally like to do, which is to import *)
(* the requirements into each implementation. Our logic testing relies on  *)
(* determining if a given state is enabled or not.                         *)
(***************************************************************************)

VARIABLE database, month
INSTANCE stubs

Spec == Init /\ [][Next]_vars

(***************************************************************************)
(* Trace requirements to specification                                     *)
(*                                                                         *)
(*  Not Traceable                                                          *)  
(*      Functional: 1,2,3,6,7,9,14                                         *)
(*      NonFunctional: 1,2,3                                               *)
(***************************************************************************)

(***************************************************************************)
(* Definitions                                                             *)
(***************************************************************************)

InTrial(u, end) ==
    \E i \in 1..end:
        /\ events[i] \in StartTrialEvent \* Has started trial
        /\ events[i].user = u
        (*******************************************************************)
        (* 6. Start Trial endpoint request                                 *)
        (* 6.3 If the requesting User has never been Subscribed or In      *)
        (*     Trial, that User SHALL be In Trial                          *)
        (*******************************************************************)
        /\ ~\E j \in i..end: \* And not canceled
            /\ events[j] \in
                (************************************************************)
                (* 8 Cancel Trial endpoint request                          *)
                (* 8.2 [Partial] If the requesting User is In Trial, the    *)
                (*      User SHALL be Not Subscribed                        *)
                (************************************************************)
                CancelTrialEvent \union
                (************************************************************)
                (* 2. Start Subscription endpoint request                   *)
                (* 2.2 If the requesting User is In Trial, the trial SHALL  *)
                (*     end and the requesting User SHALL be Subscribed      *)
                (************************************************************)
                StartSubscriptionEvent
            /\ events[j].user = u

                
        (*******************************************************************)
        (* 11 [Partial] When a User is In Trial at the end of the month    *)
        (*    that the trial was started, they SHALL be Subscribed         *)
        (*******************************************************************)
        /\ ~\E j \in i..end:
            /\ events[j] \in MonthPassEvent



UnsubscribedAfterEvent(u, i, end) ==
    \E j \in i..end: \* And not unsubscribed after
        /\ events[j] \notin MonthPassEvent
        /\ events[j].user = u
        (************************************************************)
        (* Cancel Subscription endpoint request                     *)
        (* 4.2.1 User SHALL be Not Subscribed at the end of the     *)
        (*       current month                                      *)
        (************************************************************)
        /\ \/ /\ events[j] \in CancelSubscriptionEvent
              /\ \E k \in j..end: events[k] \in MonthPassEvent
           (************************************************************)
           (* 16. User has payment failed                              *)
           (* 16.1 mark the User as Not Subscribed                     *)
           (************************************************************)
           \/ events[j] \in PaymentFailedEvent



SubscribedFromStartSubscription(u, end) ==
    (*******************************************************************)
    (* 2.4 If the requesting User is scheduled to be Not Subscribed    *)
    (*     due to cancellation, the requesting User SHALL remain       *)
    (*     Subscribed                                                  *)
    (* Implemented because a StartSubscriptionEvent after Cancel       *)
    (* undoes the cancel.                                              *)
    (*******************************************************************)
    \E i \in 1..end:
        /\ events[i] \in StartSubscriptionEvent \* Has subscribed
        /\ events[i].user = u
        /\ ~UnsubscribedAfterEvent(u, i, end)

AboutToCancel(u, end) ==
    \E i \in 1..end:
        /\ events[i] \in CancelSubscriptionEvent
        /\ ~\E j \in i..end:
            events[j] \in MonthPassEvent \union
                          StartSubscriptionEvent

SubscribedFromTrial(u, end) ==
    (*******************************************************************)
    (* 11 [Partial] When a User is In Trial at the end of the month    *)
    (*    that the trial was started, they SHALL be Subscribed         *)
    (*******************************************************************)
    \E i \in 1..end:
        /\ events[i] \in StartTrialEvent \* Has started trial
        /\ events[i].user = u
        /\ ~InTrial(u, end) \* Requirement fulfilled through InTrial
        /\ ~UnsubscribedAfterEvent(u, i, end)
        (************************************************************)
        (* Cancel Trial endpoint request                            *)
        (* 8.2 [Partial] If the requesting User is In Trial, the    *)
        (*     User SHALL be Not Subscribed                         *)
        (************************************************************)
        /\ ~\E j \in i..end: \* And not canceled
            /\ events[j] \in CancelTrialEvent
            /\ events[j].user = u
            


                
Subscribed(u, end) == 
    \/ SubscribedFromStartSubscription(u, end)
    \/ SubscribedFromTrial(u, end)




(***************************************************************************)
(* Invariants                                                              *)
(***************************************************************************)


(***************************************************************************)
(* 2 When a request is received by the Start Subscription endpoint         *)
(***************************************************************************)
StartSubscriptionAccessControl ==
    \A u \in USERS:
        LET authorized == ~Subscribed(u, Now) \/ AboutToCancel(u, Now) IN
        (*******************************************************************)
        (* 2.1: If the requesting User is Subscribed, the request SHALL    *)  
        (*      return with 409 Conflict                                   *)
        (*******************************************************************)
        \/ /\ ~authorized
           /\ ~ENABLED StartSubscription(u)

        (*******************************************************************)
        (* 2.2 [Partial]: If the requesting User is In Trial, the trial    *)
        (*      SHALL end and the requesting User SHALL be Subscribed      *)
        (*******************************************************************)
        (*******************************************************************)
        (* 2.3: If the requesting User is Not Subscribed, the requesting   *)
        (*        User SHALL be Subscribed                                 *)
        (*******************************************************************)
        \/ /\ authorized
           /\ ENABLED StartSubscription(u)

(***************************************************************************)
(* 4 When a request is received by the Cancel Subscription endpoint        *)
(***************************************************************************)
CancelSubscriptionAccessControl ==
    \A u \in USERS:
        LET authorized == Subscribed(u, Now) /\ ~AboutToCancel(u, Now) IN
        (*******************************************************************)
        (* 4.1 If the requesting User is not Subscribed, the request SHALL *)
        (*     return with 409 Conflict                                    *)
        (*******************************************************************)
        \/ /\ ~authorized
           /\ ~ENABLED CancelSubscription(u)
        (*******************************************************************)
        (* 4.2 [Partial]: If the requesting User is Subscribed, the User   *)  
        (*      SHALL ... [Cancellation Requirements]                      *)
        (*******************************************************************)
        \/ /\ authorized
           /\ ENABLED CancelSubscription(u)


(***************************************************************************)
(* 6.3 [Partial] If the requesting User is has never been Subscribed,      *)
(*      or is In Trial                                                     *)
(***************************************************************************)
EligibleForTrial(u) ==
    ~\E i \in 1..Len(events):
        /\ events[i] \in
            StartSubscriptionEvent \union
            StartTrialEvent
        /\ events[i].user = u

(***************************************************************************)
(* 6 When a request is received by the Start Trial endpoint                *)
(***************************************************************************)
StartTrialAccessControl ==
    \A u \in USERS:
        (*******************************************************************)
        (* 6.1 If the requesting User is Subscribed or In Trial, the       *)
        (*     request SHALL return with 409 Conflict                      *)
        (*******************************************************************)
        (*******************************************************************)
        (* 6.2 If the requesting User has previously been Subscribed or    *)
        (*     In Trial, the request SHALL return with 409 Conflict        *)
        (*******************************************************************)   
        \/ /\ ~EligibleForTrial(u)
           /\ ~ENABLED StartTrial(u)
        (*******************************************************************)
        (* 6.3 If the requesting User has never been Subscribed or         *)
        (*     In Trial, that User SHALL be In Trial                       *)
        (*******************************************************************) 
        \/ /\ EligibleForTrial(u)
           /\ ENABLED StartTrial(u)


(***************************************************************************)
(* 8 When a request is received by the Cancel Trial endpoint               *)
(***************************************************************************)
CancelTrialAccessControl == 
    \A u \in USERS:
                 
        (*******************************************************************)
        (* 8.1 If the requesting User is not In Trial, the request SHALL   *)
        (*     return with 409 Conflict                                    *)
        (*******************************************************************) 
        \/ /\ ~InTrial(u, Now)
           /\ ~ENABLED CancelTrial(u)
                       
        (*******************************************************************)
        (* 8.2 [Partial] If the requesting User is In Trial, the User      *)
        (*     SHALL be Not Subscribed                                     *)
        (*******************************************************************) 
        \/ /\ InTrial(u, Now)
           /\ ENABLED CancelTrial(u)

(***************************************************************************)
(* 10 When a request is received by the Watch Video endpoint               *)
(***************************************************************************)
WatchVideoAccessControl ==
    \A u \in USERS:
        (*******************************************************************)
        (* 10.1 If the requesting User is not In Trial or Subscribed, the  *)
        (*      request SHALL return with 409 Conflict                     *)
        (*******************************************************************)
        \/ /\ ~InTrial(u, Now) /\ ~Subscribed(u, Now)
           /\ ~ENABLED WatchVideo(u)
        (*******************************************************************)
        (* 10.2 If the requesting User is In Trial or Subscribed, the      *) 
        (*      system SHALL allow the User to Watch Video                 *)
        (*******************************************************************)
        \/ /\ InTrial(u, Now) \/ Subscribed(u, Now)
           /\ ENABLED WatchVideo(u)

(***************************************************************************)
(* Runs a given operation between: 1 - first month for the first month,    *) 
(* and month i - month i + 1                                               *)
(***************************************************************************)
TrueForEveryUserMonth(op(_,_,_), checkFirstMonth) ==
    LET numMonthPass == Cardinality({i \in 1..Len(events): events[i]
                                                 \in MonthPassEvent}) 
    IN
    \* If checking the first month
    /\ \/ ~checkFirstMonth
       \/ /\ checkFirstMonth
        \* There does not exist 
          /\ ~\E i \in 1..Len(events):
            \* a first month
            /\ events[i] \in MonthPassEvent
            /\ ~\E j \in 1..i: events[j] \in MonthPassEvent
            \* Where the op is false for any user
            /\ \E u \in USERS: 
                ~op(u,1,i)

    \* There does not exist a pair of consecutive months
    /\ ~\E i \in 1..Len(events):
        /\ events[i] \in MonthPassEvent
        /\ \E j \in i+1..Len(events):
            /\ events[j] \in MonthPassEvent
            /\ ~\E k \in (i + 2)..(j-1):
                events[k] \in MonthPassEvent
            \* where op is not true for all users
            /\ \E u \in USERS:
                ~op(u,i,j)

(***************************************************************************)
(* 15 When a User is Billed the system SHALL call the Bill endpoint        *)
(*    of the Payment Processor.                                            *)
(* This requirement is satisfied by how requirements 4.2.2, 12 and 13      *)
(* are tested. They test that appropriate Bill message was dispatched      *)
(***************************************************************************)

(***************************************************************************)
(* 12 When a User becomes Subscribed                                       *)
(***************************************************************************)

(***************************************************************************)
(* 12.1 they shall be Billed the Subscription Fee before the end of the    *)
(*      month                                                              *)
(***************************************************************************)

SubscribedThisMonth(u, start, end) ==
    /\ ~Subscribed(u, start) 
    /\ Subscribed(u, end-1)

UserSubscribedThisMonthBilledSubscriptionFee(u, start, end) ==
    LET shouldBill == SubscribedThisMonth(u, start, end) IN
    \* Only applies if subscribed this month
    \/ ~shouldBill
    \/ /\ shouldBill
       /\ \E i \in start..end:
            /\ events[i] \in BillEvent
            /\ events[i].user = u
            /\ events[i].fee = SubscriptionFee
    
 
SubscribedNewUsersBilledSubscriptionFee ==
    TrueForEveryUserMonth(UserSubscribedThisMonthBilledSubscriptionFee, TRUE)

(***************************************************************************)
(* 13 When a User is Subscribed at the start of a month, they shall be     *)
(*    Billed the Subscription Fee                                          *)
(***************************************************************************)
SubscribedUserBilledThisMonth(u, start, end) ==
    LET subscribed == Subscribed(u, start) IN
    \* Only applies if subscribed at start of month
    \/ ~subscribed
    \/ /\ subscribed
       /\ \/ \E i \in start..end:
                /\ events[i] \in BillEvent
                /\ events[i].user = u
                /\ events[i].fee = SubscriptionFee
         \* If the user failed a payment this is a separate workflow
          \/ \E i \in start..end: 
                /\ events[i] \in PaymentFailedEvent
                /\ events[i].user = u


SubscribedUsersBilledStartOfMonth == 
    TrueForEveryUserMonth(SubscribedUserBilledThisMonth, FALSE)

(***************************************************************************)
(* 12.2     If the requesting User has Post Due Payments they SHALL be     *)
(*          Billed in that amount before the end of the month, and         *)
(*          Post Due Payments shall be zeroed                              *)
(***************************************************************************)
(***************************************************************************)
(* 16  When a callback is received to the Payment Failed endpoint for a    *)
(*     User, the system SHALL                                              *)
(*     16.2 set Post Due Payment for the User to:                          *)
(*          (failed payment amount) + CancellationFee                      *)
(***************************************************************************)

PotentialStartingEvent(u, event) == 
    /\ event \in StartSubscriptionEvent \union
                 StartTrialEvent
    /\ event.user = u

IsPaymentFailedEvent(u, event) ==
    /\ event \in PaymentFailedEvent
    /\ event.user = u
    
UserBilledForFailureBetweenRange(u, start, end, fee) ==
    \E i \in start..end:
        /\ events[i] \in BillEvent
        /\ events[i].user = u
        /\ events[i].fee = FailedPaymentFee

UserBilledForPostDuePaymentsIfSubscribed(u, start, end) ==
    LET starts == {i \in 1..start: PotentialStartingEvent(u, events[i])} IN
    LET paymentFailed == {i \in 1..start:IsPaymentFailedEvent(u, events[i])} IN
    
    \A p \in paymentFailed:

        LET resubscribedAfterFailedPayment ==
            \E i \in p..end:
                /\ i \in starts
        IN

        \/ ~resubscribedAfterFailedPayment
        \/ /\ resubscribedAfterFailedPayment
            \* There doesn't exist a failed payment
           /\ ~\E i \in p..end:
                \* That has a subscription directly after it
                /\ i \in starts
                /\ ~\E j \in p..i:
                    j \in starts
                \* Where the user was not billed for the failed payment
                /\ ~UserBilledForFailureBetweenRange(u, i, end, events[p].fee)                               

SubscribedUsersBilledPostDuePayements ==
    TrueForEveryUserMonth(UserBilledForPostDuePaymentsIfSubscribed, TRUE)


(***************************************************************************)
(* 4 Cancel Subscription endpoint                                          *)
(* 4.2.2  if the user is Not Subscribed at the end of the current month,   *)
(* they SHALL be Billed a Cancellation Fee                                 *)
(***************************************************************************)
UserCancelledLastMonth(u, start, end) ==
    \* start - 1 because it doesn't count cancellations that take effect
    \* at start
    /\ Subscribed(u, start-1) 
    /\ ~Subscribed(u, start)

UserCancelledLastMonthBilled(u, start, end) ==
    \* Only applies if user cancelled this month
    \/ ~UserCancelledLastMonth(u, start, end)
    \/ /\ UserCancelledLastMonth(u, start, end)
       /\ \/ \E i \in start..end:
                /\ events[i] \in BillEvent
                /\ events[i].user = u
                /\ events[i].fee = CancellationFee
          \* If the user failed a payment this is a separate workflow
          \/ \E i \in start..end: 
                /\ events[i] \in PaymentFailedEvent
                /\ events[i].user = u

CancelingUsersBilledCancelationFees ==
    TrueForEveryUserMonth(UserCancelledLastMonthBilled, FALSE)


(***************************************************************************)
(* State Constraints                                                       *)
(***************************************************************************)

EventLengthLimit ==
    Len(events) < 10


MonthLimit ==
    LET monthPassEvents == SelectSeq(events, LAMBDA x: x.type = "monthpass") 
    IN
    Len(monthPassEvents) < 5

StateLimit ==
    /\ EventLengthLimit
    /\ MonthLimit

=============================================================================
\* Modification History
\* Last modified Sun Jun 19 17:43:11 MST 2022 by elliotswart
\* Created Thu Jun 16 19:34:18 MST 2022 by elliotswart

Stubs

You write initial stubs for all the API calls such that you can add appropriate observability. You also provide the basic architecture of the spec to keep the assignment bounded.

Show Code Show LaTex
------------------------------- MODULE stubs -------------------------------
(***************************************************************************)
(* Redeclaration of specdatamodels variables                               *)
(***************************************************************************)

EXTENDS Sequences, Naturals, FiniteSets

CONSTANT USERS

CONSTANTS
    SubscriptionFee,
    CancellationFee,
    FailedPaymentFee

VARIABLES
    \* Represents the current month
    month,
    \* Represents the status of the database. Design requirements require
    \* that all persistant application state be stored here
    database,
    \* Required by spec
    events 

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

\* Provides all the data models required by the spec
INSTANCE specdatamodels

Now == Len(events)

Months == 0..10

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

Month == Nat

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


TypeOk ==
    /\ EventsOk
    /\ month \in Month
    \* Additional type definitions

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


StartSubscription(u) ==
    \* Add logic here
    
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "startsubscription", user |-> u])
    /\ UNCHANGED month


CancelSubscription(u) ==
    \* Add logic here
     
    \* Observability required by stub
    /\ events' = Append(events, [type |-> "cancelsubscription", user |-> u])
    /\ UNCHANGED <<month>>

    
StartTrial(u) ==
    \* Add logic here

    \* Observability required by stub
    /\ events' = Append(events, [type |-> "starttrial", user |-> u])
    /\ UNCHANGED <<month>>
    

CancelTrial(u) ==
    \* Add logic here

    \* Observability required by stub
    /\ events' = Append(events, [type |-> "canceltrial", user |-> u])
    /\ UNCHANGED <<month>>


WatchVideo(u) ==
    \* Add logic here
    
    \* 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) ==
    \* Add logic here
    
    \* 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)


(***************************************************************************)
(* Stub method that prevents the month from passing until all operations   *)
(* are complete. Represent worker methods, etc                             *)
(***************************************************************************)
HandledMonth ==
    \* Replace logic here
    /\ True


\* 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 = [] \* Add record here

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
    \* Add more global states

=============================================================================
\* Modification History
\* Last modified Sun Jun 19 15:35:00 MST 2022 by elliotswart
\* Created Thu Jun 16 19:34:32 MST 2022 by elliotswart

Note: Generally you expect the first formal spec you write won’t be perfect. If failures are being reported when they shouldn’t, the spec may need to be revised. There’s a collaborative process as the spec gets refined and becomes accurate. We’ve removed that from this narrative for simplicity. Assume there was a back-and-forth and you’re seeing the 3rd revision of the spec above.

Summary

Satisfied that you have specified and architected the system about as well as you can, you pass it off to a junior developer to implement. You work for a contracting firm. How else are you supposed to pay the bills?