formal-verification - Nusmv 状态和转换

Question

我想在 NuSMv 中制定这个问题：

• 用户可以处于以下三种状态之一：U-need,U-using,U-sad（表示需要服务、开始使用并且他/她对该服务的质量感到满意或开始使用并且他/她分别因为他的服务质量差而感到难过）。

• 服务可以处于以下三种状态之一：S-offer、S-good、S-bad；;（分别代表未使用的服务、提供优质服务或提供劣质服务的服务）。

• 一组事件：look,use,stop,monitor,detect-p,remedy-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;
  

- 我想确认这段代码代表了我上面描述的问题 - 我将服务和用户的事件和状态都表示为变量，这是否正确？