Определение факта в сплаве, который ограничивает пропускную способность самолета - PullRequest
Новая
       10

Определение факта в сплаве, который ограничивает пропускную способность самолета

0 голосов
/ 22 марта 2020

В приведенной ниже спецификации я пытаюсь определить Факт сплава, который не позволил бы добавить человека в набор пассажиров самолета, если в нем недостаточно места. Кроме того, я хотел бы добавить еще один факт, который запретил бы удаление человека из пассажирского набора самолета, если бы количество его пассажиров не превышало ноль.

Любая помощь будет принята с благодарностью.

Приветствия,

Фиро c

PS Вот мой первый удар по первоначальному факту: 

a'.onboard <= a'.capacity implies
    no p and add [a,a',p] and del [a',a'',p] implies a.onboard = a''.onboard

... Согласно Даниэлю Джексону, это неверно, потому что условие до того, как ключевое слово подразумевает , потенциально может быть ложным. Кроме того, это не имеет ожидаемого эффекта, препятствующего тому, чтобы число пассажиров превышало вместимость самолета, управляя моделью. Например, иногда вы получаете наборы с количеством элементов 4, хотя емкость равна 2, когда вы выполняете модель ... 

sig Person {}
sig Airplane {onboard: set Person, capacity: Int}

fact {
    some a,a': Airplane | disj [a.onboard, a'.onboard] 
}

pred show(a: Airplane) {
    #a.onboard > 0
    a.capacity = 2
}
run show for 10 but 2 Airplane

pred add (a, a': Airplane, p: Person) {
    a'.onboard = a.onboard + p
}

pred del (a, a': Airplane, p: Person) {
    a'.onboard = a.onboard - p
}

assert delUndoesAdd {
    all a,a',a'': Airplane, p: Person |
        no p and add [a,a',p] and del [a',a'',p] implies a.onboard = a''.onboard
}

assert addIdempotence {
    all a,a',a'': Airplane, p: Person |
        add [a,a',p] and add [a',a'',p] implies a'.onboard = a''.onboard
}

check delUndoesAdd for 10 but 3 Airplane
check addIdempotence for 3

1 Ответ

0 голосов
/ 22 марта 2020

Я думаю, что нашел решение. 

sig Person {}
sig Airplane {onboard: set Person, capacity: Int}

fact {
    some a,a': Airplane | disj [a.onboard, a'.onboard] 
}

fact {
    all a: Airplane | a.capacity = 3 and #a.onboard <= a.capacity
}

pred show(a: Airplane) {
}

run show for 10 but 2 Airplane

pred add (a, a': Airplane, p: Person) {
    a'.onboard = a.onboard + p
}

pred del (a, a': Airplane, p: Person) {
    a'.onboard = a.onboard - p
}

assert delUndoesAdd {
    all a,a',a'': Airplane, p: Person |
        no p and add [a,a',p] and del [a',a'',p] implies a.onboard = a''.onboard
}

assert addIdempotence {
    all a,a',a'': Airplane, p: Person |
        add [a,a',p] and add [a',a'',p] implies a'.onboard = a''.onboard
}

check delUndoesAdd for 10 but 3 Airplane
check addIdempotence for 3
...