时间戳

首页 > 解决方案 > 合金中的建模状态：所有关系的语法相同，但以下除外

alloy - 合金中的建模状态：所有关系的语法相同，但以下除外

问题描述

在建模状态下，我发现自己经常处于相同的情况。

国家签名中包含一些（更多）关系。在特定的过渡中，我实际上想说的是：“前状态中的所有内容都与后状态相同，除了以下内容”

pred SampleTransition (s, s': State, f: Foo) {
    s = s' but
        s'.foos = s.foos - f
}

这样的事情存在吗？

标签： alloy

解决方案

Alloy 书讨论了各种选项——在索引中查找“框架条件”。

人们经常在事件范式中定义一个不变的谓词，这使得规范更具可读性：

pred Event.unchanged (field: univ -> Time) {
    field.(this.pre) = field.(this.post)
    }

您还可以像这样定义谓词

pred modifies (es: set Event, field: univ -> Time) {
    all e: Event - es | field.(e.pre) = field.(e.post)
    }

并在像这样的 Reiter 风格的框架条件下使用它（来自 book's hotel locking example）：

sig Room {
    key: Key one -> Time,
    prev:  Key lone -> Time,
    occ: Guest -> Time
    }
    {
    Checkin.modifies [prev]
    (Checkin + Checkout).modifies [occ]
    RecodeEnter.modifies [key]
    }

有一次，我们尝试了一种元功能，允许您定义这样的谓词

pred Event.modifies (fs: set field$) {
    all f: field$ - fs | f.value.(this.pre) = f.value.(this.post)
    }

但并没有多少热情。

推荐阅读