合金分析仪：如何定义“运行”直到条件成立？答案

【问题标题】：Alloy Analyzer: how to define "run" until a condition holds?合金分析仪：如何定义“运行”直到条件成立？
【发布时间】：2016-01-13 22:12:24
【问题描述】：

我有一个模型来指定任务和任务之间的关系。实际上我有不同类型的关系，但为了简单起见，我们假设只有一种。更简单的代码如下：

open util/ordering[Time]

sig Time {}

abstract sig State {}
lone sig Enabled extends State {}
lone sig Disabled extends State {}

sig Task {
    state : State one -> Time
}

sig Relation {
    relation : Task one -> Task,
}

fact noLoop {
    no a : Task | a not in a.^(Relation.relation)
}

fact trace {
    init[first[]]
    all t : Time - last[] |
        let t' = t.next[] |
            some a : Task |
                execute[a, t, t']
}

pred init [t : Time] {
    Task.state.t = Enabled
}

pred execute[exec : Task, t, t' : Time] {
    exec.state.t = Enabled

    let
        disabledTasks = 
            exec 
            + {a : Task | let r = Relation | a in exec.(r.relation)}
            + {a : Task | a.state.t = Disabled},
        otherTasks = {a : Task | a not in disabledTasks}
    |
        disabledTasks.state.t' = Disabled
        and 
        otherTasks.state.t' = Enabled
}

最初，所有任务都处于启用状态。执行时，该任务以及所有相关任务都进入禁用状态。

我知道我可以找到模型正在运行的实例，例如：

run execute for 6

这将只显示具有 6 个时间步长的实例。有时，在第 6 个时间步结束时，会有启用的任务。我想知道是否存在要求合金分析器运行执行谓词直到所有任务都被禁用的方法。其实我想展示的是，这个模型总能达到所有任务都被禁用的状态（即使我需要定义一个有限的范围）。

感谢大家的帮助。

【问题讨论】：

我也接受对我的模型进行改进的建议。

标签： alloy

【解决方案1】：

run 的唯一参数是要运行的谓词的名称和范围。

所以不，不能按照您描述的方式完成。然而，问题不在于run 对两个参数的句法限制；问题是，Alloy 与您不同，没有内在的时间概念，因此“直到”在向 Alloy 描述事物时不是一个有用的概念。

另一方面，如果您想运行模拟直到达到某种状态，您所要做的就是在命名谓词中描述该状态，然后运行该谓词。所以：定义一个谓词，意思是“所有任务都被禁用”；称之为all_done。然后定义谓词

pred interesting {
  execute and all_done
}
run interesting for ...

祝你好运。

【讨论】：