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
分析器報以反（這表明其中每個天氣值映射到一個城市一個實例）。
顯然我的邏輯是不正確的。你能想出表達這一點的正確邏輯嗎？