可能没有城市会下雨

Question

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

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

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]
}

然后我可以让 Alloy 分析器检查断言：

check Every_city_has_weather

分析器returns预期结果：未找到反例

优秀。

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

我很难表达这一点。我试过这个：有一些 w: Weather 使得在加入与 w 的天气关系时没有城市。这是 Alloy 断言：

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

然后我让 Alloy 分析器检查我的断言：

check A_weather_may_not_be_in_any_city

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

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

Answer 1

如果您想查看某个实例是否存在，您应该使用运行而不是检查语句。一个断言说每个实例都是真的。
鉴于你想说"There is some w: Weather such that there is no City when joining the weather relation with w"，我建议直接表达：

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

There may be no cities with rainy weather