NuSMV运行样例解析

  1. short.smv
    1. 代码
      MODULE main # 新建模型,名为main
      VAR # 变量声明
      request : {Tr, Fa}; # 变量request,取值在True或False之中
      state : {ready, busy}; # 变量state,取值在ready或busy之中
      ASSIGN # 指定约束
      init(state) := ready; # state初始值为ready
      next(state) := case # state下一状态为条件选择
      #如果state等于ready并且request等于True,则返回busy作为state的下一状态
      state = ready & (request = Tr): busy;
      TRUE : {ready,busy}; # 如果前面一句未命中,则返回一个ready或busy中的随机值作为state的下一状态
      esac; # 退出case结构
      SPEC
      AG((request = Tr) -> AF state = busy) # 询问是否状态request等于True的下一状态为state等于busy
    2. 运行结果:
      -- specification AG (request = Tr -> AF state = busy) is true
  2. counter.smv
    1. 系统行为模型(状态图):
      • 模拟了一个3bit的进位的模型,每个bit有一个value和一个进位标志carryout,进位标志需要把3个bit看成一个整体。
      • 当这个整体需要进位的时候,carryout将置1.
        image
    2. 代码
      MODULE main                                 # 新建一个模型,名为main
      VAR                                         # 变量声明
          bit0 : counter_cell(TRUE);              # bit0是模型counter_cell的实例
          bit1 : counter_cell(bit0.carry_out);
          bit2 : counter_cell(bit1.carry_out);
      SPEC                                        # CTL说明
          AG AF bit2.carry_out                    # AG(forall globally),AF(forall finally),检测bit2.carry_out的结果
      
      MODULE counter_cell(carry_in)               # 新建一个模型,名为counter_cell
      VAR                                         # 变量声明
          value : boolean;                        # 定义变量value,类型为boolean
      ASSIGN                                      # 指定约束
          init(value) := FALSE;                   # 初始化value为FALSE
          next(value) := value xor carry_in;      # value下一状态为value和carry_in的异或值
      DEFINE                                      # 定义声明
          carry_out := value & carry_in;          # carry_out是value和carry_in的与值
      
    3. 运行结果表明输出结果为true
      -- specification AG (AF bit2.carry_out) is true
  3. ring.smv
    1. 代码
      MODULE main
      VAR
          gate1 : process inverter(gate3.output);
          gate2 : process inverter(gate1.output);
          gate3 : process inverter(gate2.output);
      SPEC
          (AG AF gate1.output) & (AG AF !gate1.output)
      
      MODULE inverter(input)
      VAR
          output : boolean;
      ASSIGN
          init(output) := FALSE;
          next(output) := !input;
      FAIRNESS    # 添加FAIRNESS可强制inverter模块的每个实例得以并发执行
          running
      
    2. 运行结果
      -- specification (AG (AF gate1.output) & AG (AF !gate1.output)) is true
  4. semaphore.smv
    1. 代码
      MODULE main
      VAR
          semaphore : boolean;
          proc1 : process user(semaphore);
          proc2 : process user(semaphore);
      ASSIGN
          init(semaphore) := FALSE;
      SPEC
          # 状态proc1.state等于entering的下一个状态为proc1.state等于critical
          AG (proc1.state = entering -> AF proc1.state = critical)    
      
      MODULE user(semaphore)
      VAR
          state : {idle,entering,critical,exiting};
      ASSIGN
          init(state) := idle;
          next(state) := 
              case 
                  state = idle : {idle,entering};
                  state = entering & !semaphore : critical;
                  state = critical : {critical,exiting};
                  state = exiting : idle;
                  TRUE : state;
              esac;
          next(semaphore) := 
              case
                  state = entering : TRUE;
                  state = exiting : FALSE;
                  TRUE : semaphore;
              esac;
      FAIRNESS
          running
      
    2. 运行结果
      -- specification AG (proc1.state = entering -> AF proc1.state = critical) is false
      -- as demonstrated by the following execution sequence
      Trace Description: CTL Counterexample
      Trace Type: Counterexample
      -> State: 1.1 <- # 状态1.1
      semaphore = FALSE # 各个变量被初始化
      proc1.state = idle
      proc2.state = idle
      -> Input: 1.2 <- # 切换模块
      _process_selector_ = proc1 # 进入模块proc1
      running = FALSE # 改变变量绑定模块的运行状态
      proc2.running = FALSE
      proc1.running = TRUE
      -- Loop starts here # 从这里开始循环
      -> State: 1.2 <- # 状态1.2
      # proc1从状态idle进入entering
      proc1.state = entering
      -> Input: 1.3 <-
      _process_selector_ = proc2 # 进入模块proc2
      proc2.running = TRUE # proc2运行,proc1挂起
      proc1.running = FALSE
      -- Loop starts here # 从这里开始循环
      -> State: 1.3 <-
      -> Input: 1.4 <-
      -> State: 1.4 <-
      proc2.state = entering # proc2从状态idle进入entering
      -> Input: 1.5 <-
      -> State: 1.5 <- # 在此状态中semaphore和proc2.state同时发生变化
      semaphore = TRUE # 信号量semaphore从初始状态FALSE切换到TRUE
      proc2.state = critical # proc2.state从状态entering切换到critical
      -> Input: 1.6 <-
      _process_selector_ = proc1 # 进入模块proc1
      proc2.running = FALSE # proc1运行,proc2挂起
      proc1.running = TRUE
      -> State: 1.6 <- # 进入proc1后由于状态无法发生变化,此处可能省略了此未变化状态
      -> Input: 1.7 <-
      _process_selector_ = proc2 # 进入模块proc2
      proc2.running = TRUE # proc2运行,proc1挂起
      proc1.running = FALSE
      -> State: 1.7 <-
      proc2.state = exiting # proc2.state从状态critical切换到exiting
      -> Input: 1.8 <-
      -> State: 1.8 <- # 在此状态中semaphore和proc2.state同时发生变化
      semaphore = FALSE # 信号量semaphore从状态TRUE切换到FALSE
      proc2.state = idle # proc2.state从状态exiting切换到idle

发表评论