NuSMV开发：改变案例陈述中"TRUE"的功能

Question

>最近我尝试做一些工作，将一些模型转换为Nusmv模型，但我想尝试更改"TRUE："关键字的功能。 众所周知，"TRUE："中的"案例...esac;" 可以定义一些你想要的动作，当情况条件没有那个特定条件时，但是，我有要求天气 "TRUE"可以执行上次操作，例如：

next(a) := 
case 
a>0 : -10;
a<0 : 10;
TRUE : (do the last time actions);
esac;

换句话说，当"a"=0时，如果上次分配"a"-10，这次它也将被分配-10;如果上次"a"被分配10，这次它也将被分配10。

所以，现在的问题是，是否有可能通过更改NuSMV的源代码来做到这一点，你能告诉我哪个是实现"case"中"TRUE"函数的c语言文件吗？

感谢您的帮助！

Answer 1

可以使用几种方法。

解决方案 1.

此解决方案基于值持久性。请注意，它可以用于您在问题中提供的玩具示例，但它绝不是通用解决方案。

MODULE main
VAR
a : -1..1;
ASSIGN
init(a) := -1;
next(a) := case
a < 0 : 1;
a > 0 : -1;
TRUE  : a;
esac;

值持久性就足够了，因为我们为变量分配了一个常量值。

解决方案 2.

如果分配的值不是常量，则无法使用值持久性。相反，我们用足够的内存来丰富模型，以便跟踪正在执行的操作。

MODULE main
VAR
a : -1..1;
action : { ACTION_1, ACTION_2, NONE };
ASSIGN
init(action) := NONE;
next(action) := case
a < 0 : ACTION_1;
a > 0 : ACTION_2;
TRUE  : action;
esac;
init(a) := -1;
next(a) := case
a < 0 : a + 1;
a > 0 : a - 1;
action = ACTION_1 : a + 1;
action = ACTION_2 : a - 1;
TRUE              : a;
esac;

在此示例中，action跟踪对变量a执行的最后一个选择。每当acase的前提条件不足以确定应该采取哪个操作时，我们依靠保存的action值并重放先前执行的操作。

请注意，设计人员有责任决定在初始状态下应发生什么，以防未触发a的任何前提条件。在这种情况下，我们无法重播以前的操作(它不存在(，因此规范可以以不同的方式处理。就我而言，我决定让a永远保持价值0。