Как устанавливаются начальные состояния в динамических моделях в Electrum 2?

Я взял пример с дверного замка отеля и придумал этот MWE для автомобильных дверей.

enum LockState {Locked, Unlocked}

sig Door {
    var state: LockState
}

sig Vehicle {
     doors :  disj set Door
}

//actions
pred unlock[d: Door]{
    d.state' = Unlocked
}

pred lock[d: Door]{
    d.state' = Locked
}

//traces
pred init{
    all s: Door.state | s = Locked
}

pred trace{
    init
    always {
        some d: Door | 
            unlock[d] or
            lock[d]
    }
}

//demonstrate
run {} for 4 but exactly 2 Vehicle, 4 Time

Что, к моему удивлению, допускает пример, показанный ниже, в котором некоторые двери заперты, а некоторые нет. Как установить условие, что все двери заперты в самый ранний момент? экземпляр приведенной выше модели, показывающий, что некоторые двери постоянно заперты, а некоторые открыты.


alloy
person keithb_b    schedule 19.08.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Начальные состояния определяются без каких-либо временных ключевых слов, как вы это делали в init.

Проблема в том, что вы определили свой trace как предикат. Если вы определите его как fact, он будет применяться всегда. Однако, если вы сделаете его предикатом (мое предпочтение, поскольку оно кажется менее глобальным), вы должны включить его из команды запуска. Выбери один:

run trace for 4 but exactly 2 Vehicle, 4 Time
run  { trace } for 4 but exactly 2 Vehicle, 4 Time

Однако ваша модель все равно не будет работать хорошо.

  • Вы указываете always, но не ставите цель. Так что после одного состояния Аллой доволен. Вы должны предоставить eventually, чтобы Alloy попытался продолжить, пока не будет удовлетворен.
  • Вы разрешаете транспорт без дверей, я бы использовал some Door вместо set Door
  • Ваш init можно сделать чище, как Door.state = Locked
  • В вашей трассировке каждый шаг устанавливает одну дверь. Однако вы не указываете, в каком состоянии должны быть другие двери. Если вы не укажете значение для следующего состояния, они могут стать чем угодно. Они должны быть явно установлены, чтобы иметь их старое значение.

Поэтому я придумал следующую модель:

enum LockState { Locked, Unlocked }
sig Door       { var state: LockState }
sig Vehicle    { doors :  disj some Door }

pred Door.unlock { this.state' = Unlocked }
pred Door.lock   { this.state' = Locked }

pred trace {
    Door.state = Locked
    always (
        some d: Vehicle.doors {
            (d.unlock or d.lock) 
            unchanged[state,d]

        }
    )
    eventually Door.state = Unlocked
}

run trace for 4 but exactly 2 Vehicle


pred unchanged[ r : univ->univ, x : set univ ] {
    (r - x->univ)' = (r - x->univ)
}

обновлено Добавлен неизменный предикат.

person Peter Kriens    schedule 19.08.2020