Блог

Я позаимствовал пример дверного замка отеля и придумал этот 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
  

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

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

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

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

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

• Вы предоставляете always но не цель. Итак, после одного состояния Alloy счастлив. Вы должны предоставить, 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)
}
  

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