0
「天気」をRainy,Sunny,Cloudyのいずれかにします。雨天の都市はありません
「天気」は、都市と天気の関係です。そのモデルを考える
Boston – Sunny
Seattle – Cloudy
Miami – Sunny
、私は主張することができるはずです：：
sig Forecast {weather: City -> one Weather}
sig City, Weather {}
one sig Rainy, Sunny, Cloudy extends Weather {}
は、ここでのサンプルインスタンスのすべての都市天気を持っています。
assert Every_city_has_weather {
all forecast: Forecast | all city: City | one forecast.weather[city]
}
私は、アサートをチェックするために合金アナライザを求めることができます：ない反例が
が優れた：
check Every_city_has_weather
Analyzerが期待される結果を返します。
ここでは天気があり、その天気がない都市はないと主張したいと思います。上記の例では、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
ザ・アナライザは、（それが各天気値はシティにマッピングされているインスタンスを示した反例と答え）。
明らかに私の論理は正しくありません。あなたはこれを表現するための正しい論理を考えることができますか？