将系统模型转换为转换系统以进行模型检查答案

【问题标题】：Converting a system model into transition system for model checking将系统模型转换为转换系统以进行模型检查
【发布时间】：2016-07-13 04:34:40
【问题描述】：

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

Pictorial Representation of Model

【问题讨论】：

标签： fsm model-checking nusmv transition-systems

【解决方案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;

但是，我认为您提供的 model 有点过于简单，无法与您的问题描述 相匹配，因此我邀请您提供有关您的意图的更多信息去做。

【讨论】：

谢谢，实际上这是我的系统模型，我必须检查一些 LTL 属性。这是基于A和B两方之间的通信以及一些要验证的属性是AF（A无法向B发送信息）（此问题图片基于系统的sender-model）
哦，好的。我习惯了更复杂的模型
嘿帕特里克！我想知道如何在上面提到的 NuSMV 源代码中合并接收系统模型。在接收器模型中，我们有 {receive information, Deliver information 和 ack} 之类的状态。我想将两个模型合并在一起，使系统模型看起来很复杂
您好，请编辑您的问题并完整描述您的问题，或者打开一个新问题，然后我会看看是否可以更新我的答案。