fsm - 将系统模型转换为转换系统以进行模型检查

Question

目前我正在尝试将系统原型转换为过渡系统模型。我有一些 LTL 属性，我想使用模型检查工具 NuSMV 验证这些属性。我只是介绍如何通过定义原子属性和其他数学方面来开始建模。

模型的图示

Answer 1

该转换系统的NuSMV中的一个非常简单的编码将是

MODULE main()
VAR
  state : { GETINFO, ACK, SEND };
ASSIGN
  init(state) := GETINFO;
  next(state) := case
    state = GETINFO : SEND;
    state = SEND    : ACK;
    state = ACK     : {GETINFO, SEND};
  esac;

但是，我认为您提供的模型过于简单，无法与您的问题描述相匹配，因此我邀请您提供有关您打算做什么的更多信息。