Here is my new, radically simplified model.
abstract sig Location{}
abstract sig Zone{
locations: disj some Location
}
abstract sig Vehicle{
//structural relations
,locations: some Location
,zones: some Zone
,locationsInZone: zones one -> some locations
//state
,var locked: disj set zones
,var unlocked: disj set zones
}{
//facts about derived relations
all z: zones | z.locations = locationsInZone[z]
//facts about state
zones = locked + unlocked
}
one sig DriverFront extends Location{}
one sig PassengerFront extends Location{}
one sig PassengerSide extends Location{}
one sig Rear extends Location{}
one sig People extends Zone{}
abstract sig Cargo extends Zone{}
one sig RearCargo extends Cargo{}
one sig OtherCargo extends Cargo{}
sig Transit extends Vehicle {
}{
zones =
People
+ RearCargo
+ OtherCargo
locations =
Rear
+ PassengerSide
+ DriverFront
+ PassengerFront
locationsInZone =
People -> DriverFront
+ People -> PassengerFront
+ RearCargo -> Rear
+ OtherCargo -> PassengerSide
}
//observations
pred Vehicle::zoneLocked[z: Zone]{
z in this.locked
}
pred Vehicle::zoneUnchanged[z: Zone]{
{z} & this.locked = {z} & this.locked'
{z} & this.unlocked = {z} & this.unlocked'
}
pred Vehicle::zonesOtherThanUnchanged[z: Zone]{
all z: this.zones - z | this.zoneUnchanged[z]
}
//actions
pred Vehicle::unlockAZone[z: Zone]{
this.unlocked' = this.unlocked + {z}
this.locked' = this.locked - {z}
this.zonesOtherThanUnchanged[z]
}
pred Vehicle::lockAZone[z: Zone]{
this.locked' = this.locked + {z}
this.unlocked' = this.unlocked - {z}
this.zonesOtherThanUnchanged[z]
}
//demonstration
pred trace{
//initally -- it would be nice to have a (yes, redundant!) keyword for this
all v:Vehicle |
all z: v.zones | v.zoneLocked[z]
always
one v: Vehicle |
one z: Zone |
v.unlockAZone[z]
eventually
all v:Vehicle |
all z: v.zones | not v.zoneLocked[z]
}
//run {trace} for exactly 1 Transit, 4 Door
run {} for exactly 1 Transit
Incorporating the fruits of various bits of feedback, thanks all.
But! I am missing something, because this now has no meaningful behaviour. It allows the following instance, in which the eventually seems not to be met. Why so?
