Alloy 能否模拟所有汽车是否都能在道路上急转弯？答案

【问题标题】：Can Alloy model whether all cars can make the sharp turn in the road?Alloy 能否模拟所有汽车是否都能在道路上急转弯？
【发布时间】：2016-12-21 11:43:52
【问题描述】：

路上有个急转弯。

限速40。

BMW 可以轻松转弯。卡车可以转弯，还是会偏离道路？

使用合金创建模型。

断言：所有车辆都可以转弯。

请合金分析器看看是否有反例。

...

这是Alloy可以做到的吗？

如果是，请您提供有关如何创建模型的提示吗？

【问题讨论】：

如何判断车辆是否可以急转弯？请注意，Alloy 并不是最适合对算术表达式进行推理，您可能希望抽象出大部分数字和操作，以限制对简单但具有良好代表性概念的推理。

标签： alloy

【解决方案1】：

一切都可以在 Alloy 中建模，问题只是对于您要解决的问题，这是否是正确的抽象级别。

这是一个示例，您可以如何抽象地模拟急转弯的汽车并检查有关您的模型的各种断言：

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

【讨论】：