Attribute value not taken into account

[Pytheas01]

Hello, in the below Alloy specification, the Airplane capacity isn't taken into account. For instance, if you execute the specification, you'll find airplanes with a number of passengers greater than the specified capacity (2).

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 = 2
}

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

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

pred del (a, a': Airplane, p: Person) {
    a.capacity >= 0 implies 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

[dnjackson]

Hi Phiroc,

Can you post queries like this to StackOverflow?

In short, the answer to your question is that

condition implies effect

allows (by standard logic) executions in which condition is false.

Daniel

On Mar 22, 2020, at 10:46 AM, Phiroc notifications@github.com wrote:

Hello, in the below Alloy specification, the Airplane capacity isn't taken into account. For instance, if you execute the specification, you'll find airplanes with a number of passengers greater than the specified capacity (2).

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 = 2 }

pred show(a: Airplane) {

a.onboard > 0

} run show for 10 but 2 Airplane

pred add (a, a': Airplane, p: Person) {

a.onboard =< a.capacity implies a'.onboard = a.onboard + p

}

pred del (a, a': Airplane, p: Person) { a.capacity >= 0 implies 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

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[Pytheas01]

Many thanks, Daniel. Sorry about the logic error.