首页 文章

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

提问于
浏览 次
1

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

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

为什么不能得到一个实例？我已经跟踪了代码，基本跟踪应该如下：init - > towards - > unlockopen - > getin .

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

非常感谢对此的一些指导 .

alloy

1 回答

  • 6

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

    以下是有关调试不一致性的一些常规提示：

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

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

    • 尝试增加范围 . 但请注意，当您使用 util/ordering 时，这有点棘手，因为它使得有序类型的范围完全正确（例如，如果您有签名操作并且正在订购签名状态，如果您为State设置了范围对于Action，您可能没有足够的动作来填充跟踪） .

    回复于

相关问题