此信号如何添加到Alloy中的关系中？

Question

我正在用Alloy建模类似Google Docs的嵌入式评论系统。具体来说，我正在建模用户可以执行的UI交互。用英语约束是：

• 用户可以有任意数量的评论
• 用户可以同时撰写任意数量的评论
• 注释可以是合成的或编辑的，不能同时是两个
• （最终）用户可以一次展开一个评论以查看它，否则文本将被截断。

到目前为止，我仅以添加新评论为模型，或者我认为！当我运行下面的模型时，我希望看到Alloy无法找到任何反例，但它一次找到了同时在composed和composing关系中都带有注释的示例。

我认为我的心理模型在这种情况下可能会有些偏离。我在这里看不到如何向composed关系中添加评论：我认为init会将所有草稿设置为在其中具有空关系，并且Traces中的操作将永远排除评论添加到composed。但！我显然错了，因为Alloy找到了一个示例，其中composed是非空的。有人知道这里到底发生了什么吗？

module inlineComments

open util/ordering [Time] as TimeOrdering

sig Time {}

sig Draft {
  composing: set Comment -> Time,
  composed: set Comment -> Time,
  -- expanded: lone Comment -> Time,
}

sig Comment {}

-- What can we do with these?

pred newComment (t, t': Time, c: Comment, d: Draft) {
  -- comment is not already known to us
  c not in d.composing.t
  c not in d.composed.t

  -- start composing the comment
  d.composing.t' = d.composing.t + c
}

pred init (t: Time) {
  all d: Draft, c: Comment | c not in d.composing.t
  all d: Draft, c: Comment | c not in d.composed.t
}

fact Traces {
  init[TimeOrdering/first]

  all t: Time - TimeOrdering/last |
    let t' = TimeOrdering/next[t] |
      some d: Draft, c: Comment |
        newComment [t, t', c, d]
}

-- Is the world how we expect it to be?

assert validState {
  -- comments cannot be composing and composed at the same time
  all t: Time, d: Draft | d.composing.t & d.composed.t = none
}

check validState for 3 but 1 Draft

Answer 1

这就是所谓的“框架问题”：您已指定可以在composing中添加新注释，但没有其他反应！您必须明确指出，系统更改的唯一方法是via newComment。这是您可以执行此操作的一种方法：

fact Traces {
  init[TimeOrdering/first]

  all t: Time - TimeOrdering/last |
    let t' = TimeOrdering/next[t] |
      some d: Draft, c: Comment {
        newComment [t, t', c, d]
        d.composed.t = d.composed.t' -- d.composed doesn't change
      }
}

请注意，这仅适用于您明确限制了1个草稿的范围。如果使用两个草稿进行测试，则还必须显示所有草稿均未发生任何变化。如果总是只有一个草稿，可以写one sig Draft来强制执行。