Моделирование состояний в Alloy: синтаксис для всех идентичных отношений, кроме следующих - PullRequest
Новая
       7

Моделирование состояний в Alloy: синтаксис для всех идентичных отношений, кроме следующих

0 голосов
/ 21 декабря 2018

Во время моделирования состояний я часто оказываюсь в одной и той же ситуации.

Государственная подпись имеет некоторое (большее) количество отношений внутри нее.В рамках определенного перехода я хочу сказать что-то вроде: «Все в предварительном состоянии совпадает с пост-состоянием, , за исключением следующего» * ​​1005 * 

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

Делает что-нибудькак это существует?

1 Ответ

0 голосов
/ 21 декабря 2018

В книге 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)
    }

, и использовать его в таких условиях фрейма в стиле Рейтера (из примера блокировки книги): 

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)
    }

, но энтузиазма по этому поводу не было много.

...