Нусмв состояния и переходы

Question

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

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

• Услуга может находиться в одном из следующих трех состояний: 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;
  

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