Nusmv состояния и переходы

Я хочу сформулировать эту проблему в NuSMv:

• Пользователь может находиться в одном из этих трех состояний: U-потребность, U-использование, U-грусть (представляющий собой пользователя, который нуждается в услуге, начинает пользоваться и он/она доволен качеством этой услуги или начинает пользоваться и он /она грустит из-за плохого качества его обслуживания соответственно).

• Услуга может находиться в одном из следующих трех состояний: S-предложение, S-хорошее, S-плохое; ;(обозначает услугу, которая не используется, услугу, предлагающую хорошее качество, или услугу, предлагающую плохое качество соответственно).

• Набор событий: просмотр, использование, остановка, мониторинг, обнаружение-p, устранение-p, представляющих поиск службы, начало использования службы, прекращение использования службы, мониторинг качества, обнаружение проблемы в службе и устранение неполадок. проблема соответственно.

• это мой код SMV:

   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;
  

-Я хочу подтвердить, что этот код представляет проблему, которую я описал выше - я представляю как события, так и состояния сервисов и пользователей как переменные, это правильно?