问题标签 [nuxmv]

现在客户有两种选择，电话和短信到诊所预约医生。电话或短信需要发送给话务员或接待处，然后进行下一步....众所周知，电话和短信可以发送成功或发送失败，发送失败的解决方案将继续重试相同的用户选择方式或另一种方式。

基于以上背景，我写了一些做模型检查行为的代码来实现它。我是班上的新手，任何人都可以帮助找出我的代码有什么问题。

它总是给我留下语法错误，并使用 nuXmv 在终端中运行。

问题 给定两个布尔函数f1(a,b)以及f2(a,b,c)a,b 和 c 布尔值，我想知道是否存在 c 的值，这样对于 a et b 的任何组合f1(a,b)=f2(a,b,c)。

例如 iff1(a,b)=a AND b和f2(a,b,c)=a AND b AND c，我们可以看到f1=f2when c=1。但是，如果f1(a,b)=a OR b和f2(a,b,c)=a AND b AND c，则 c 的值不成立f1=f2。

失败的方法 我尝试使用模型检查，在 nuXmv 中实现一个简单的模型，用 CTL 规范回答这个问题，EF ( AG ( (a & b) = (a & b & c)))但它失败了。显然，它适用于规范AG ( c=true -> (a & b = a & b & c))，但它需要有 2^n 规范（其中 n 是两个函数之间的变量数之差）。

您认为解决该问题的最佳方式/工具/方法是什么。

感谢您指出正确的方向。

我正在使用 nuXmv 开发一个模型，我想将其中的 3 个变量初始化为整数范围，而不是固定的整数值。值为 - 1..100、20..100 和 0..200

一组固定初始值的模型模拟按预期工作，并且可以验证属性。

但是，当我输入一系列随机选择的初始值时，模型会无限期地挂起。

有谁知道可能是什么原因以及如何解决这个问题？

I have a model in muXmv, where I initialize with a range of values like -

this works perfectly fine.

However, when I use variable instead of values,

it throw syntax error -

line 14: at token "..": syntax error

line 14: Parser error

Not sure where I am going wrong?

Also is there a better way to declare constants in nuxmv?

我正在尝试在 NuSMV 中创建一个 4 in a row 实现。不幸的是，我是 NuSMV 的新手，我很难创建它。我尝试为玩家 1 定义所有获胜案例，并使用 2D 数组来表示网格。现在我从 NUSMV 编译器收到一个错误，它在下一个（移动）块中显示：“非法操作数类型的“=”：整数和布尔值”。使用 seq1 到 seq6 定义玩家可以做的所有未来动作（例如，在游戏开始时，玩家只能在前 7 个空格中放置石头）。

有人有用 smv（nusmv 或 nuxmv）编写的四骑士拼图的代码吗？我用网格描述了问题，但是当我尝试编写约束/移动时，出现如下错误：

第 35 行：递归定义：S1

在第 43 行的 next(S3) 的定义中

在第 35 行的 next(S1) 的定义中

我理解这个问题，但不知道如何实现这个问题并递归地避免这个问题。

谢谢！

1. 有什么方法可以对 CTL 使用同情心吗？
2. 是否可以选择在同情表达上使用 next(state) 编写表达式？谢谢

我试图在 Visual Studio 中以交互方式运行 nuXmv 程序，但总是收到错误

“nuXmv：‘nuXmv’一词未被识别为 cmdlet、函数、脚本文件或可运行程序的名称。”

从互联网上安装 nuXmv 文件后，我应该尝试做些什么来将其移动到正确的文件夹路径？

我通常输入 nuXmv -int NAME.smv

谢谢！

我是学习 nuXMV 的新手，希望有人能帮助我。我正在尝试从 UPAAL 实现灯示例，只是为了学习如何使用这个工具。

所以我想做的是这个例子：

我知道下面的代码不起作用，但这就是我走了多远。我不知道如何模拟例如用户的按钮按下。

如果有人知道如何对其进行编码 - 有一个示例可以指导它会很好:)