0
没有城市
让“天气”是其中之一：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
分析仪返回预期的结果：没有发现反例
优秀。
现在我想断言，有可能是对于没有城市有天气天气。在上面的示例中，没有城市具有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
分析器报以反（这表明其中每个天气值映射到一个城市一个实例）。
显然我的逻辑是不正确的。你能想出表达这一点的正确逻辑吗？