为什么没有找到该谓词的实例？

Question

我有一个非常令人费解的问题。我似乎找不到这个谓词的实例。下面是代码。

module keyless
open util/ordering[state] as trace

abstract sig ownerpostype{}

//owner is out and far away from the car
//this set should be mapped to person
one sig far extends ownerpostype{} //{(far)}
one sig near extends ownerpostype{} //{(near)}
one sig insidecar extends ownerpostype{} //{(insidecar)}

//engine status
abstract sig enginetype{}
one sig on extends enginetype{} //engine is on
one sig off extends enginetype{}

//car door status
abstract sig dooroptype{}
one sig unlock extends dooroptype{}
one sig lock extends dooroptype{}
one sig opened extends dooroptype{}

//car status
abstract sig motortype{}
one sig moving extends motortype{}
one sig still extends motortype{}

//key fob position
abstract sig keypostype{}
one sig incar extends keypostype{} //key fob in car
one sig faralone extends keypostype{}
one sig pocket extends keypostype{}

sig state{
  owner: ownerpostype,  //(s, far) or (s,near) or (s, insideCar)
  //engine: enginetype,  
  door: dooroptype,
  //motor: motortype,
  //key: keypostype
}

//initial state
pred init (s: state){
  //engine intially off
  s.door in lock and s.owner in far
}

//operations on the owners position
pred towards (s, s' : state){
 s.owner in far and s'.owner in near and s.door = s'.door
}

//operations on key position
pred getin (s, s' : state){
 s.owner in near 
 s.door in opened
 s'.door = s.door
 s'.owner in insidecar
}

//operations on door status
pred unlockopen (s, s' : state){
  s.owner in near and s.door in lock
  s'.door in opened 
  s'.owner = s.owner
}

pred close (s, s' : state){
  s.door in opened and s'.door in unlock
  s'.owner = s.owner
}

fact {
  first.init
  all t : state - last | let t' = t.next |
     towards[t, t'] or getin[t, t'] or unlockopen[t, t'] 
}

run getin

为什么 getin 没有实例？我已经跟踪了代码，基本的跟踪应该是这样的：init -> away -> unlockopen -> getin。

这些前面的谓词中的每一个都应该满足后续谓词中的约束。那么，为什么我可以获得除 getin 之外的其余谓词的实例？

非常感谢您对此提供一些指导。

Answer 1

默认范围是 3。您无法执行 3 个具有 3 个状态的操作 - 您需要 4 个！

以下是一些关于调试不一致的一般提示：

1. 如果您的命令没有实例，请松开它，看看会发生什么。在这种情况下，您可以将run getin 更改为run {}。

2. 点击“核心”链接查看未饱和核心。在这种情况下，它显示了所有的动作谓词，表明问题不仅仅是 getin 本身。

3. 尝试扩大范围。但是请注意，当您使用 util/ordering 时，这有点棘手，因为它使有序类型的范围精确（例如，如果您有一个签名动作并且正在订购一个签名状态，如果您设置了一个范围对于状态和较小的操作，您可能没有足够的操作来填充跟踪）。