如何使用形式验证语言创建带有“自由”变量的模8计数器？

如何解决如何使用形式验证语言创建带有“自由”变量的模8计数器？

我要完成的任务如下：

实施一个模拟与环境互动的计数器（模数为8）的系统，作为Xchek和 属性集。 为计数器建立一个模型，计算一次 变量在GCLang中的值为1模8，带有二进制变量。在 换句话说，您的变量之一应该是自由变量，并且 计数器的转换应取决于此free的值 变量。

因此，我尝试在GCLang中以最明显的方式对此进行建模。我的伪代码如下：

NAME Modulo8
VAR
-- For the mod 8 counter
  x    : boolean;
  y    : boolean;
  z    : boolean;

-- The Free Variable
  a    : boolean;

INIT
-- Set everything to false initially
  !x & !y & !z & !a

Rules
  !x & !y & !z & a : x:=0; y:=0; z:=1; a:=0  -- We always reset a to false once we have incremented the counter by 1

  !x & !y & z & a : x:=0; y:=1; z:=0; a:=0

  !x & y & !z & a : x:=0; y:=1; z:=1; a:=0

  !x & y & z & a : x:=1; y:=0; z:=0; a:=0

  x & !y & !z & a : x:=1; y:=0; z:=1; a:=0

  x & !y & z & a : x:=1; y:=1; z:=0; a:=0

  x & y & !z & a : x:=1; y:=1; z:=1; a:=0

  x & y & z & a : x:=1; y:=1; z:=1; a:=0 -- Loop the Counter

因此，乍一看，我的代码似乎符合规范。我有一个自循环的mod 8计数器。 mod8计数器的转换取决于“自由”变量a的值。但是，这是一个大问题。以下CTL公式是正确的：

AX(!x & y & z)
AX(x & y & !z)

两个人怎么可能同时成为真。从初始状态到那两个状态怎么可能？这些应该在以后很久才成立。

我正在尝试在GCLang，Xchek中完成我的解决方案，文档可以在http://www.cs.toronto.edu/~arie/xchek/xchek_user_manual.pdf的第6页中找到。但是对于任何形式的验证语言，该代码都可以被视为通用伪代码。