将系统模型转换为转换系统进行模型检查
将系统模型转换为转换系统进行模型检查
提问于 2016-07-13 04:34:40
目前，我正在尝试将系统原型转换为转换系统模型。我有一些LTL属性，我想使用模型检查工具NuSMV来验证这些属性。我只是介绍了如何通过定义原子性质和其他数学方面来开始建模。
模型的图形表示
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-07-13 10:17:08
在该转换系统的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;但是，我认为您提供的模型有点过于简单，无法与您的问题描述相匹配，因此我请您提供有关您打算做什么的更多信息。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/38342731
复制相关文章
相似问题
腾讯云开发者
