specman - 如何解决 IntelliGen 中的无尽回溯

Question

我写了以下代码：

struct packet {
    x:int;
    y:int;

    x >= 0 => y==1;
    x < 0 => y==2;
};

虽然它在 Specman 中解决得非常快，但对于某些种子，Gen 调试器显示生成器尝试将 y 分配给不同于 1 和 2 的值，甚至是“y：回滚集”。我做错了什么？

score 3 · Accepted Answer

由于生成引擎不知道 y 值的有效空间，它可能会尝试通过在 [MIN_INT..MAX_INT] 中为 y 分配一个随机值，然后才为 x 分配一个随机值，从而导致无限循环。您可以通过选项解决它：

score 0 · Accepted Answer

在这种情况下，生成引擎需要从 2 个不同的约束中推断出关于 y 的信息，这很昂贵。尝试将约束合并为一个约束和/或添加您已经知道的信息来帮助它。

score 0 · Accepted Answer

0

在这种情况下使用三元结构，生成器可以轻松解决约束。

于 2014-05-13T08:26:47.267 回答

score 0 · Accepted Answer

您可以根据您的意图通过减少解决方案的状态空间来帮助生成器。可以通过两种方式完成 1. 将 y 保留在 [1..2] 中；2. 巩固约束保持 y == (x>0) ? 1：2；

4 回答 4