Modelling a vehicle locking system

models
1

I’ve started working towards a model of the lock/unlock behaviour of a typical light commercial vehicle. For the sake of having a concrete example, a Ford Transit. I will use only information publicly available in the vehicle Handook.

This is the kind of messy and arbitrary domain wherein I feel that a little bit of modelling has a lot of potential benefit. But it is not the kind of domain that leands itself to a neat, elegant, “clever” solution. At least I don’t think so. Anyway, I’m much more intersted in applying tools like Alloy to this kinds of domain than I am to finding dark corners of distributed consensus finding algorithms or whatever—valuable as I can see those exercises may be, it’s not where I make my living.

The repo is at https://github.com/keithb-b/learning-alloy/

My current sticking point is as decribed in the commit comment at HEAD: how to ensure that each Door is a door on only one Vehicle. Without the fact doorsAreOnOneVehicleOnly I get counterexamples where doors are shared between multiple vans, with the fact in place I get no countrexamples but also no instances. A puzzle. Probably I’m missing something which should be obvious, but I can’t see what.

Any concrete suggestions for improvement gratefully received.

Thanks,
Keith

2

Hi Keith, Assuming this is the same issue you posted on the Alloy forum, I’m pasting in my response here. But let me know if there is something else you’re stuck with. --Daniel

Keith asks: Assuming that I’m correct in thinking that these two facts mean the same thing:

fact doorsAreOnOneVehicleOnly_set_ops{
all disj v, u: Vehicle |
none = v.allDoors & u.allDoors

Daniel responds: I would prefer

no v.allDoors & u.allDoors

It’s more idiomatic Alloy, since the “no” expression quantifier is intended precisely for this, and it reads (to me at least) more naturally.

Note that you could also use a multiplicity declaration constraint

allDoors in Vehicle lone -> Door

Also, a tiny nitpick: I’d put the quantifier vars in alphabetical order:

all dis u, v: ….=

}

fact doorsAreOnOneVehicleOnly_quantifiers_and_implication{
all d: Door |
all v, u: Vehicle |
d in v.allDoors and d in u.allDoors <=> v = u

This seems much harder to read to me. If you want to write something like this, I’d write it as

all u, v: Vehicle, d: Door | d in (u.allDoors & v.allDoors) implies u = v

Note that the reverse implication is obvious, so it’s better to omit it. This is a general principle in Alloy: only say as much as you need. Another example, suppose I have a relation liveIn: Person -> House and I want to say every house is lived in. Rather than saying

Person.liveIn = House

I’d say

House in Person.liveIn

because the first adds, gratuitously

Person.liveIn in House

which is already in the decl. Back to your spec…

Or you could write

all u, v: Vehicle | some (u.allDoors & v.allDoors) implies u = v

using this theorem (which I checked following Tim’s advice):

sig A {r: set B}
sig B {}
check {
(all b: B | all a, a’: A | b in a.r & a’.r implies a = a’)
iff
(all a, a’: A | (some b: B | b in a.r & a’.r) implies a = a’)

}

Finally, regarding this

pred doorsOnOneVehicle{
all d: Door |
1 = #{v: Vehicle | d in v.allDoors}
}

This strikes me as very un-Alloy like for the following reasons:

  1. It introduces integers without any need for them; “#R=1” should be written "one R”. This (a) makes it harder to read; (b) slows down the analysis (since it introduces bitwise ops); © might break if you change the scope of integers.

  2. It adds the gratuitous constraint I mentioned above; it should be “lone R” not "one R”.

  3. It introduces a comprehension that is more complicated than a simple relational expression (which would be allDoors.d); once you can read these expressions they save a lot of thinking, are clearer, and can be interpreted easily in diagrammatic form (“go back through allDoors from d”)

  4. Placing the constant on the LHS and the expression on the RHS doesn’t match the natural way to write constraints. I’d say “ the distance of my house from MIT is 10 miles” not “10 miles is the distance of my house from MIT” (which would only make sense in natural language in response to an explicit question). I wonder if this style is a remnant of C programming in which you want to avoid an unintentional assignment to a variable.

3

Hi Daniel,
Thanks, but no, this is not the same question. Aplogies if that was not clear. Over on the Google group I’m asking about style (and thanks for your compendious reply, which I will get back to). Here I am asking about substance. I have not so far managed to produce a model with the constraint that a door belongs only to one vehicle in place, of which Electrum 2 will find any instance. No counter examples, “theModelAsChecked may be valid, as expected”, which is good. But “No instance found. theModelAsRun may be inconsistent.” which isn’t.

4

OK – sorry for not getting that. Looked at the commit messages but still confused. Can you extract a small part of your model and pose the question inline here?

5

No worries, I appreciate you taking the time to look at it.

The core is this:

abstract sig Vehicle{
     doorAt:  Location one -> one Door
    ,locations: set Location
}

fun Vehicle::allDoors: set Door{
    ran[this.doorAt] 
} 

sig Door{
   ,var lockState: one LockState
}{ 
}

sig Transit extends Vehicle {
}{
   locations = //this works, but I can't wite a predicate which fails if this is "in" rather than "="
      Rear
    + PassengerSide
    + DriverFront
    + PassengerFront
}

fact doorsAreInOneLocationOnly{
    all v: Vehicle |
        all l, m: v.locations | 
                v.doorAt[l] = v.doorAt[m] <=> l = m 
}

fact doorsAreOnOneVehicleOnly{
    all disj v, u: Vehicle |
        none = v.allDoors & u.allDoors
}

fact noUnneededLocations{
    all l: Location |
        some v: Vehicle |
            l in v.locations
}

which doesn’t produce any instaces. If I remoive the fact doorsAreInOneLocationOnly then I do get instances, but they have two vans with the same four doors shared between them. I want to see an instance with two vans and eight doors, one door in each place on each van.

Hope that’s clear now.

6

I think the problem may be this declaration constraint

 doorAt:  Location one -> one Door

which says that every door (whichever vehicle it belongs to) is in exactly one of the locations of this vehicle.

Here’s a simplified version of your model as I would write it, which now has the instance you’re expecting:

abstract sig Location, Door {}
one sig Rear, PassengerSide, DriverFront, PassengerFront extends Location {}

abstract sig Vehicle {
     locations: set Location,
     doors: set Door,
     doorAt:  locations one -> one doors
} {
  doors = Location.doorAt
}

fact {
  -- each door belongs to exactly one vehicle
  doors in Vehicle one -> Door
  }

run {
  -- every vehicle has 4 doors
    all v: Vehicle | #v.doors = 4
  -- there are 2 vehicles
    #Vehicle = 2
} for 2 Vehicle, 4 Location, 8 Door
7

Thanks Daniel,
I have incorporated your feedback into my model, which is much improved.

Yes, I do have a C accent. My first three programming jobs were in C and pre-ISO C++. That leaves a mark. Probably why I prefer // and /**/ comments to – comments.

There seem to be some Alloy idioms that make me, as a programmer, quite uncomfortable. For example, in fact { doors in Vehicle one -> Door } it feels very odd to me to see doors, which is declared in sig Vehicle {…} referenced in a free-floating fact without any reference to the sig where it is declared. I find the lack of any hints to scope or name resolution quite worrying.

I’ll get used to it.

Thanks again,
Keith

8

Hi Keith,

Your point about the way in which Alloy allows you to reference a relation without its sig is a good one. This is a very intentional design decision in Alloy. We wanted to make it very easy to write short and succinct models in which you could use a field as a relation without having to qualify it in any way, so that models felt much less hierarchical and structured than code in languages that are designed for big programs and thus impose a big overhead when writing small programs.

At the same time, we wanted to make sure that signatures provided a local namespace, and that you could introduce a field name without worrying about clashes with fields in other signatures. So we devised a type system that would automatically resolve ambiguities. In concert with this, we ensured that the expression signame <: fieldname would always resolve correctly to the field with name fieldname in the signature named signame, using the domain restriction operator taken from the Z language, thereby not introducing any new syntax (and maintaining the property that Alloy is essentially an untyped language).

In short then, you can write Vehicle <: doors if you prefer to be explicit about the signature, but the meaning of that expression can still be explained in pure relational logic without introducing complicated notions of namespace.

Daniel

9

Daniel,
Thanks for that. I might wish that more PL designers were so intentional in thier choices and willing to be clear about the tradeoffs they’ve made.

I have to keep reminding myself that a sig is not a type, howver much it looks like one.

Best,
Keith

10

I had a hard time getting used to this as well until I realized that it naturally enabled two-way navigation. Instead of having to specify the parents and the children … you specify a relation. After that ‘insight’ it became quite natural for me.

11

I think you can simplify the model a bit using enum and disj?

enum Location { Rear, PassengerSide, DriverFront, PassengerFront }
sig Door {}

abstract sig Vehicle {
     doors :  disj set Door,
     doorAt:  Location one -> one doors
}
run {} for 10 but exactly 2 Vehicle
12

That’s what my very first version looked like, but I moved away from it for reasons that I now struggle to recall.

13

Well, Daniel’s technique to set a local ‘doors’ set is quite clever, the ‘disj’ builds on that. I like the conquer and divide approach it represents.

14

So, I’ve extended the model at https://github.com/keithb-b/learning-alloy to try to reflect the “zonal locking” that the vehicle suports. There are both counterexamples and instances that I don’t understand, as described in the README. Any explanatory comments welcome.

15

Which file? The Door.md file does not compile and the VehicleLocking.md tried to open files but cannot open the included modules.

It would help to review if you could keep it in one file? By using different modules you make it a lot harder to try it out in Alloy. The splitting makes it a lot harder to get an overview, which is the primary reason I use Alloy. With relatively little code you can show the essence of a problem. If the essence is splattered over lots of files I might as well go directly go to code … :slight_smile:

16

Thanks for taking a look.

It is one model. VehicleLocking.md is the entry point. I don’t understand why Doorg.md would not compile for you. The whole thing compiles and has instances on my machine when I “execute all” in VehicleLocking. I have Electrum Analyzer 2.0.0.201910111016 running from the .jar on java 14.0.2

I’ll post a synoptic version here.

17

Behaviour of a vehicle locking system

Doors and Locations on the Vehicle, Locks

sig Door{
   var lockState: LockState
}{
}

//actions
pred Door::unlockCommanded{
    this.lockState' = Unlocked
}

pred Door::lockCommanded{
    this.lockState' = Locked
}

pred Door::unchanged{
    this.lockState' = this.lockState
}

//observations
pred  Door::locked{
    this.lockState = Locked
}

pred Door::unlocked{
    this.lockState = Unlocked
}

enum Purpose {ForPeople, ForCargo} 
abstract sig Location {
    ,purpose: one Purpose
}

enum Side {Driver, Passenger}
enum Place {Front, Sliding}
abstract sig PositionalLocation extends Location{
    ,side: one Side
    ,position: one Place
}

one sig DriverFront extends PositionalLocation{}{
    side = Driver
    position = Front
    purpose = ForPeople
}

one sig PassengerFront extends PositionalLocation{}{
    side = Passenger
    position = Front
    purpose = ForPeople
}

one sig PassengerSide extends PositionalLocation{}{
   side = Passenger
   position = Sliding
   purpose = ForCargo
}


one sig Rear extends Location{}{
   purpose = ForCargo
}


abstract sig LockState{}

This could have been an enum, but that doesn’t allow for Locked and Unlocked to have different styling on the visualiser. Which I’d like.

one sig Locked extends LockState{}
one sig Unlocked extends LockState{}

Vehicles and Remote Control Fobs

Vehicles

This sig models the structure of vehicles in general. A specific kind of vehicle should extend this and constrain:

  • locations
  • zones
  • locationsByZones
  • unlockEffects

appropriately for the behaviour of that kind of vehicle.

abstract sig Vehicle{
    ,locations: some Location
    ,doors: some Door
    ,doorAt: locations one -> one doors
    ,fob: disj one RemoteFob
    ,zones: some Zone
    ,locationsByZones: zones one -> some locations
    ,doorsInZone: zones one -> some doors
    ,unlockEffects: set Zone
}{
    doors = Location.doorAt
    doors.lockState = {Locked} or doors.lockState = {Unlocked}
    doorsInZone = locationsByZones.doorAt
}

Actions

pred Vehicle::lockCommanded{
    all d: this.doors |
        d.lockCommanded
}

pred Vehicle::unlockCommanded{
    all d: this.doors | 
        d in this.doorsInZone[this.unlockEffects] implies 
            d.unlockCommanded 
        else
            d.unchanged
}

pred Vehicle::unchanged{
    all d: this.doors |
        d.unchanged
}

Concrete example drawn from 2019 Ford Transit users handbook.

sig Transit extends Vehicle {
}{
   locations = //this works, but I can't wite a predicate which fails if this is "in" rather than "="
      Rear
    + PassengerSide
    + DriverFront
    + PassengerFront

   zones = 
      People +
      RearCargo +
      OtherCargo

   locationsByZones = 
      People -> DriverFront +
      People -> PassengerFront +
      RearCargo -> Rear +
      OtherCargo -> PassengerSide

    unlockEffects = People or unlockEffects = People + Cargo
}

Observations

pred Vehicle::allDoorsLocked{
    no {Unlocked} & this.doors.lockState
} 

pred Vehicle::allDoorsUnlocked{
    no {Locked} & this.doors.lockState
}

pred Vehicle::peopleDoorsUnlockedOnly{
    let peopleDoors = this.doorsInZone[People] | {
        peopleDoors.lockState' = {Unlocked}
        all d: this.doors - peopleDoors | d.unchanged
    }
}

Remote Fobs

Vehicles are locked and unlocked using their paired wireless fob.

sig RemoteFob{
    vehicle: disj one Vehicle
}

Facts

Slightly tricky stuff here: we say that the fob relation (Vehicle -> RemoteFob) joined with the vehicle relation (RemoteFob -> Vehicle) is a subset of the identity relation.

fact FobVehiclePairing{
    fob.vehicle in iden   
}

Actions

pred RemoteFob::unlockCommanded{
   this.vehicle.unlockCommanded
}


pred RemoteFob::lockCommanded{
   this.vehicle.lockCommanded
}

Zonal Locking

   
abstract sig Zone{}

one sig People extends Zone{}

abstract sig Cargo extends Zone{}

one sig RearCargo extends Cargo{}

one sig OtherCargo extends Cargo{}


fact doorsAreOnOneVehicleOnly{
    doors in Vehicle one -> Door
}

fact noUnneededLocations{
    all l: Location |
        some v: Vehicle |
            l in v.locations
}

Checks

The below claims should be true of the above model:

Structure

pred aVehicleHasLocationsForDoors{
    all v: Vehicle |  v.locations != none
}

pred aDoorBelongsToAVehicle{
    all d: Door |
        one v: Vehicle |
            d in v.doors
}

pred aDoorIsInALocationOnAVehicle{
    all d: Door |
        one v: Vehicle |
            one l: v.locations |
                d = v.doorAt[l]
}

pred aDoorIsOnOneVehicleOnly{
    all disj u, v: Vehicle |
        no v.doors & u.doors
} 

pred aDoorIsInOneLocationOnly{
    all v: Vehicle |
        all d: v.doors |
            one v.doorAt :> d
}

pred aDoorIsInAZone{
   all d: Door |
      one z: Zone |
          one v: Vehicle |
             d in v.doorsInZone[z]
}
   
pred aPeopleZoneContainsTheDoorsForPeople{
   all v: Vehicle |
      all l: v.locations |
          l.purpose in ForPeople => some z: v.zones | z in People and l in v.locationsByZones[z]
}

pred aCargoZoneContainsTheDoorsForCargo{
   all v: Vehicle |
      all l: v.locations |
          l.purpose in ForCargo => some z: v.zones | z in Cargo and l in v.locationsByZones[z]
}

collecting all that together for convenience:

pred validStructure{
    aVehicleHasLocationsForDoors
    aDoorBelongsToAVehicle
    aDoorIsInOneLocationOnly
    aDoorIsInAZone 
    aPeopleZoneContainsTheDoorsForPeople
    aCargoZoneContainsTheDoorsForCargo
}

Behaviour


pred doorsInAZoneHaveTheSameLockState{
    all v: Vehicle |
        all z: v.zones | 
           no v.doorsInZone[z].lockState :> Locked or
           no v.doorsInZone[z].lockState :> Unlocked
}

pred doorsChangeStateOnlyOnFobCommands{
    all f: RemoteFob |
        let v = f.vehicle |
            all d: v.doors |
               d.unchanged until f.unlockCommanded or f.lockCommanded        
}

collecting all that together for convenience:

pred consistentBehaviour{
    doorsInAZoneHaveTheSameLockState
    doorsChangeStateOnlyOnFobCommands
}

Checking structure and behaviour together for convenience:

pred vehicleLockingModel{
    validStructure
    consistentBehaviour
}

check theModelAsChecked{vehicleLockingModel} for exactly 2 Transit, 2 RemoteFob, 8 Door, 4 Location, 4 Time expect 0 //counterexamples

Demonstration


pred begin{
    all d: Door |
            d.locked
}

pred someValidChanges{
    always {
         some f: RemoteFob |
            let v = f.vehicle |
                 v.unlockEffects = People + Cargo => (
                     (f.lockCommanded   and v.allDoorsLocked   and allVehiclesUnchagedExcept[v]) or
                     (f.unlockCommanded and v.allDoorsUnlocked and allVehiclesUnchagedExcept[v]) or
                     f.vehicle.unchanged)
                 or 
                 v.unlockEffects = People => (
                     (f.lockCommanded   and v.allDoorsLocked          and allVehiclesUnchagedExcept[v]) or
                     (f.unlockCommanded and v.peopleDoorsUnlockedOnly and allVehiclesUnchagedExcept[v]) or
                     f.vehicle.unchanged)
    }
}

pred targetState{
    eventually {
        all d: Door | d.unlocked
    }
}

pred trace{
    begin
    someValidChanges
    targetState
}

//As  we should see demonstrated thus:
//run singleVanBehaviour{trace} for exactly 1 Transit, 1 RemoteFob, 4 Door, 4 Location, 4 Time
run multipleVanBehaviour{trace} for exactly 2 Transit, 2 RemoteFob, 8 Door, 4 Location, 4 Time

Utilities

let allVehiclesUnchagedExcept[v] = all vv: Vehicle - v | vv.unchanged
18

I was in the wrong Alloy :frowning: I got several open at the same time because I am working on the code. I then looked on Doorg.md and it used :: which I did not know was allowed :slight_smile:

I think it is hard for me to review because I really dislike the verbose and scattered style you’ve selected :frowning: I think I already indicated several times why. Clearly that is your choice but it makes it hard to review for me.

So I’ll follow this thread if there are any questions about details but it is tricky to formulate more feedback without falling in repetition.

19

I think there’s an interesting question here. It’s not whether the “verbose” style is better or worse, but that Keith believes it’s easier to explain to his domain experts.

Does anyone have any actual experience of exploring specs with non-modellers that could help us here? Otherwise, we’ll have to wait until Keith has done the experiment.

20

Well, I’ve got half an hour with them tomorrow, and then I’m on leave for couple of weeks. They can play with it in the meantime and we’ll see if they can make any sense of it. We’ll see which bits they find difficult—I don’t anticipate that it will be insufficient terseness.

Speaking of the folks at work, I’ve been playing with this on my own time. If my client do decide to start paying me to work on a model then there will be a version of this which belongs to them that I will struggle to share, unless I can negotiate a licencing scenario (GPL 2, I guess, to head off anyone else using it commercially).