可能没有下雨天的城市

Question

让“天气”成为其中之一：Rainy、Sunny、Cloudy。

我可以创建一个合金模型，上面写着：“天气”是城市和一个天气之间的关系。

sig Forecast {weather: City -> one Weather}

sig City, Weather {} 

one sig Rainy, Sunny, Cloudy extends Weather {}

这是一个示例实例：

Boston – Sunny  
Seattle – Cloudy  
Miami – Sunny

鉴于该模型，我应该能够断言：每个城市都有天气。

assert Every_city_has_weather {
   all forecast: Forecast | all city: City | one forecast.weather[city]
}             

然后我可以让合金分析仪检查断言：

check Every_city_has_weather

分析器返回预期结果：没有找到反例

非常好。

现在我想断言，可能有一个天气，没有哪个城市有这种天气。在上面的示例中，没有任何 City 具有 Rainy 值。

我很难表达这一点。我试过这个：有一些w：天气，当加入与w的天气关系时没有城市。这是合金断言：

assert A_weather_may_not_be_in_any_city {
   all forecast: Forecast | some w: Weather | no forecast.weather.w
}

然后我让合金分析仪检查我的断言：

check A_weather_may_not_be_in_any_city

分析器给出了一个反例（它显示了一个实例，其中每个天气值都映射到一个城市）。

显然我的逻辑不对。你能想出表达这一点的正确逻辑吗？

Answer 1

1. 如果您想查看某个实例是否存在，您应该使用 run 而不是 check 语句。断言表明 每个 实例都是正确的。

2. 鉴于你想说“有一些 w: Weather 这样在加入与 w 的天气关系时没有 City”，我建议非常直接地表达：

   some w: Weather | no c: City | ...