Formal Modeling

1.2.1.1 Model State

1. Model Entity Users
   

   State of entity Users is modeled using tla+ module tla/Timeoff_Users.tla

   \* State variable Timeoff_Users initialized to an empty set
   Timeoff_Users = {};
   

2. Model Entity Companies
   

   State of entity Companies is modeled using tla+ module tla/Timeoff_Companies.tla

   \* State variable Timeoff_Companies initialized to an empty set
   Timeoff_Companies = {};
   

1.2.1.2 Model Service

1. tla/TimeoffRegisterCompany.tla
   

   (*
    * Service entry point for interface /registerCompany(post).
    * Calls service implementation in procedure 
    * proc_TimeoffRegisterCompany
   *)
   macro TimeoffRegisterCompany( input ) {
   
         call proc_TimeoffRegisterCompany( input );
   
   }
   

2. tla/proc_TimeoffRegisterCompany.tla
   

   (*
    * Service implementation for interface /registerCompany(post).
    * Adds user and company entities for valid input and returns status 200 for 
    * valid input. For invalid input return status "400".
   *)
   procedure proc_TimeoffRegisterCompany( input_proc_TimeoffRegisterCompany ) {
   
   proc_TimeoffRegisterCompany_start:
   
     if (      valid_User( input_proc_TimeoffRegisterCompany )  
          /\   valid_Company( input_proc_TimeoffRegisterCompany )  
   
        ) {
         TimeoffAddUser( 
             [ user_name |-> input_proc_TimeoffRegisterCompany.user_name, 
               user_lastname |-> input_proc_TimeoffRegisterCompany.user_lastname,
               user_email |-> input_proc_TimeoffRegisterCompany.user_email
             ] );
         TimeoffAddCompany( 
             [ 
               company_name |-> input_proc_TimeoffRegisterCompany.company_name 
             ] );
   
         InfrastructureServiceReturn( "/registerCompany(post)", "status_200", Nil );
     }
     else {
         InfrastructureServiceReturn( "/registerCompany(post)", "status_400", Nil );
     };
   
   proc_TimeoffRegisterCompany_exit:
     return;
   }
   

1.2.1.3 Actions Modifying Persistent State

1. Action: Add new user
   

   In file tla/TimeoffAddUser.tla

   (*
    * Add new user entry to model state - if it does not exist
   *)
   macro TimeoffAddUser( user ) {
       
       if ( ~ user \in Timeoff_Users ) {
             Timeoff_Users := Timeoff_Users \union { user };
       };
   }
   

2. Action: Add new company
   

   In file tla/TimeoffAddCompany.tla

   (*
    * Add new companry entry to model state - if it does not exist
   *)
   macro TimeoffAddCompany( company ) {
       
       if ( ~ company \in Timeoff_Companies ) {
             Timeoff_Companies := Timeoff_Companies \union { company };
       };
   }
   

1.2.1.4 Validation Operators

1. Operator: validate User entity
   

   Operator tla/valid_User.tla

   (*
    * Validate data model entry user
    *)
   valid_User( user ) ==
                     user # Nil
                /\   user.user_name # Nil
                /\   user.user_lastname # Nil
                /\   user.user_email # Nil
   

2. Operator: Validate Company Entity
   

   Operator tla/valid_Company.tla

   (*
    * Validate data model entry companry
    *)
   valid_Company( co ) ==
                     co # Nil
                /\   co.company_name # Nil
   

1.2.2.1 Invariant: verify formal model state

(*
 * All user and company entries in formal model state are valid
*)
correct_Database == \A user \in Timeoff_Users: valid_User(user)
                 /\ \A co \in Timeoff_Companies: valid_Company(co)

1.2.3.1 Service /registerCompany(post) Executes Successfully

(*
 * Evaluate TRUE whe service /registerCompany(post)
 * succeeds i.e. return status 200.
*)
isCompanyRegistered == InfrastructureServiceGetStatus("/registerCompany(post)") = "status_200"

1.2.3.2 Service /registerCompany(post) Execution Fails

 (*
 * Evaluate TRUE whe service /registerCompany(post)
 * fails  i.e. returns status 400.
 *)
  isCompanyRegisteredFails == InfrastructureServiceGetStatus("/registerCompany(post)") = "status_400"