Nusmv states and transitions

Question

I want to formulate this problem in NuSMv :

• A user can be in one of these three states: U-need,U-using,U-sad(representing a user that needs a service, starts using and he/ she is happy with the quality of this service or starts using and he/ she is sad because of the bad quality of his service respectively).

• A service can be in one of these three states: S-offer,S-good,S-bad; ;(representing a service that is not in use, a service offering a good quality or a service offering a bad quality respectively).

• A set of events : look,use,stop,monitor,detect-p,remedy-p , representing looking for a service, start using a service, stop using a service , monitoring the quality, detecting a problem in a service and remedy the problem respectively.

• this is my SMV code:

   MODULE main
   VAR
  
  
   Service: {S-offer,S-good,S-bad};
   User:{U-need,U-using,U-sad};
   Event:{look,use,stop,monitor,detect-p,remedy-p};
  
    ASSIGN
  
        init(Event) := look; 
        init(User) := U-need;
        init(Service) := {S-offer,S-good};
  
  
      next(Event) := case
  
      (Event = look) &  (Service=S-offer) : look;
      (Event = look) &  (Service=S-good) : use;
      (Event = use) &  (Service=S-good) : monitor;
      (Event = monitor) &  (Service=S-good) : {monitor,stop,detect-p};
      (Event = detect-p)  : remedy-p;
      (Event = remedy-p)  : monitor;
  
      TRUE:Event;
  
               esac;
  
  
      next(User) := case
  
      (Event = look) &  next(Event)=look : U-need;
      (Event = look) &  next(Event)=use : U-using;
      (Event = use) &  next(Event)=monitor : U-using;
      (Event = monitor) &  next(Event)=monitor : U-using;
      (Event = monitor) &  next(Event)=stop : U-need;
      (Event = monitor) &  next(Event)=detect-p : U-sad;
      (Event = detect-p ) &  next(Event)=remedy-p :  U-using; 
  
                  TRUE:User;
  
               esac;
        next(Service) := case
  
      (Event = look) &  next(Event)=look : S-offer;
      (Event = look) &  next(Event)=use : S-good;
      (Event = use) &  next(Event)=monitor : S-good;
      (Event = monitor) &  next(Event)=monitor : S-good;
      (Event = monitor) &  next(Event)=stop : S-offer;
      (Event = monitor) &  next(Event)=detect-p : S-bad;
      (Event = detect-p ) &  next(Event)=remedy-p :  S-good; 
  
                  TRUE:Service;
  
               esac;
  

-I want to confirm that this code represents the problem I described above - I represent both the events and the states of services and users as variables, is this correct?