范围的合金简写始终包含特定值答案

【问题标题】：Alloy shorthand for range to always contain certain value范围的合金简写始终包含特定值
【发布时间】：2013-09-14 13:07:47
【问题描述】：

我在 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 链接到。我希望我已经解释得很好。我认为会有一个非常明显的答案，但我想不出它是什么。请问有什么想法吗？

【问题讨论】：

我真的不明白你想要达到什么目的。你能把你的断言写长一点，然后我们看看它是否可以缩短？
抱歉问题措辞不当，我希望现在这有助于理解。

标签： alloy

【解决方案1】：

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

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

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

【讨论】：

【解决方案2】：

这个怎么样

fact { ^prv.Begin = Proc - Begin }

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

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

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

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

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

【讨论】：