# Modelling a vehicle locking system

**URL:** <https://alloytools.discourse.group/t/modelling-a-vehicle-locking-system/20>\
**Category:** models\
**Created:** [August 14, 2020, 11:44am UTC](https://alloytools.discourse.group/t/modelling-a-vehicle-locking-system/20 "2020-08-14T11:44:24Z")\
**Posts on this page:** 1\
**Page:** 2

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 5:04pm UTC](https://alloytools.discourse.group/t/modelling-a-vehicle-locking-system/20/21 "2020-09-11T17:04:51Z")

</div>

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?

 ![Screen Shot 2020-09-11 at 18.00.38](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/ea841b68ee786f6c7af3a3a67f3b3c9f0742812e.png)

[Previous page](https://alloytools.discourse.group/t/modelling-a-vehicle-locking-system/20.md?page=1)