1

最近我尝试将一些模型转换为 Nusmv 模型，但我想尝试更改“TRUE：”关键字的功能。众所周知，“case ... 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 语言文件吗？

感谢您的帮助！

4

1 回答 1

0

可以使用几种方法。

解决方案 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。每当a's的先决条件case不足以确定应采取的行动时，我们依靠我们保存的action值并重播先前执行的行动。

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

于 2018-05-25T07:37:14.003 回答