Can Alloy model whether all cars can make the sharp turn in the road?

Question

There is a sharp turn in the road.

The speed limit is 40.

A BMW can easily make the turn. Can trucks make the turn, or will they go off the road?

Use Alloy to create a model.

Assert: all vehicles can make the turn.

Invite the Alloy Analyzer to see if there counterexamples to the assertion.

...

Is this something that Alloy can do?

If yes, would you provide hints on how to create the model, please?

Answer 1

Everything can be modeled in Alloy, the question is just whether that's the right level of abstraction for the problem you're trying to solve.

Here is an example how you could abstractly model cars making sharp turns and checking various assertions about your model:

enum Angle { a45, a90, a135 }

sig Turn {
  angle: one Angle
}

sig Speed in Int {}

abstract sig Car {
  canMake: Turn -> Speed
}
sig SportsCar extends Car {}
sig Truck extends Car {}

pred isSharpTurn[t: Turn] {
  t.angle = a45
}

fun speedsUnder[limit: Int]: set Speed {
  {s: Speed | s <= limit}
}  

fact {
  // speeds must be non-negative
  Speed in {i: Int | i >= 0}

  // sports cars can make any turn if going below 40
  SportsCar -> Turn -> speedsUnder[40] in canMake

  // any car can make any non-sharp turn if going below 40
  Car -> {t: Turn | !isSharpTurn[t]} -> speedsUnder[40] in canMake

  // any car can make any turn if going below 20
  Car -> Turn -> speedsUnder[20] in canMake
}

pred allCarsCanMakeAllTurnsAtAllSpeeds {
  all c: Car, t: Turn, s: Speed | c -> t -> s in canMake
} 

// counterexample: car = Truck1, turn.angle = 45, speed = 127
check AllCarsCanMakeAllTurnsAtAllSpeeds {
  allCarsCanMakeAllTurnsAtAllSpeeds  
} for 3 but 8 Int

// counterexample: car = SportsCar1, turn.angle = 45, speed = 127
check GivenNoTrucks_AllCarsCanMakeAllTurnsAtAllSpeeds {
  no Truck 
    implies allCarsCanMakeAllTurnsAtAllSpeeds
} for 3 but 8 Int

// counterexample: car = Truck1, turn.angle = 45, speed = 32
check GivenSpeedLimit40_AllCarsCanMakeAllTurnsAtAllSpeeds {
  (all s: Speed | s <= 40) 
    implies allCarsCanMakeAllTurnsAtAllSpeeds
} for 3 but 8 Int

// no counterexample found
check GivenNoTrucksAndSpeedLimit40_AllCarsCanMakeAllTurnsAtAllSpeeds {
  (no Truck and (all s: Speed | s <= 40)) 
    implies allCarsCanMakeAllTurnsAtAllSpeeds
} for 3 but 8 Int

// no counterexample found
check GivenNoSharpTurnsAndSpeedLimit40_AllCarsCanMakeAllTurnsAtAllSpeeds {
  ((no t: Turn | isSharpTurn[t]) and (all s: Speed | s <= 40)) 
    implies allCarsCanMakeAllTurnsAtAllSpeeds
} for 3 but 8 Int