1

我在 Alloy 上做了一些工作，所以我对它有一些了解。然而，很多速记并没有真正涵盖任何地方。我想知道的是在下面的例子中：

open util/relation

abstract sig Proc { prv : lone (Proc - Remove) 
}{
}

fact {acyclic[prv,Proc] // no cycles 
}
sig Remove extends Proc{}
sig Begin extends Proc{}{no prv}
sig Action extends Proc{}

pred show() {} 
run show for 3

我想确保最终的 Proc 始终是 Begin（目前它也可以是 Action）。

有很多方法可以手写。我在下面包含了一个，当包含它时，可以确保最终的 Proc（即不在域中的）始终是 Begin。

fact {
all p : Proc  |   p not in dom[prv] implies p in Begin
}

但是，我喜欢使用 (Proc - Remove) 的简写，例如因为它使事情更容易阅读，这意味着 Remove 不能从另一个 Proc 链接到。我希望我已经解释得很好。我认为会有一个非常明显的答案，但我想不出它是什么。请问有什么想法吗？

4

2 回答 2

1

听起来好像你可以通过写作来实现你的目标

sig Remove extends Proc{}{some prv}
sig Begin extends Proc{}{no prv}
sig Action extends Proc{}{some prv}

这确保没有 Begin 有 prv 节点，所有非 Begin 节点都有。

于 2013-09-16T01:06:07.643 回答
0

这个怎么样

fact { ^prv.Begin = Proc - Begin }

它不是超级短，但至少它不使用量词。我不确定你是否能做得更好。

在图术语中，它基本上说：如果您prv通过尽可能多地跟踪其中的所有边来完全扩展图（即，采用 prv, 的传递闭包^prv），然后选择那些指向 Begin 的边的源节点node ( ^prv.Begin)，该集合必须包含除 Begin 节点之外的所有节点。事实上，您已经知道 Begin 节点没有 prv，这意味着从任何非 Begin 节点开始并仅跟随prv链接，将到达 Begin 节点，并且链将在那里结束。这个事实不允许动作节点和这样的链。

您可以通过断言在合金中检查此声明

check {
  // there is no non-Begin node that does not lead to a Begin node
  no p: Proc-Begin | no (Begin & p.^prv)
} for 6

并检查它没有找到任何反例。

于 2013-09-14T18:15:05.947 回答