There may be no cities with rainy weather

Question

Let “Weather” be one of these: Rainy, Sunny, Cloudy.

I can create an Alloy model that says: “weather” is a relation between City and one Weather.

sig Forecast {weather: City -> one Weather}

sig City, Weather {} 

one sig Rainy, Sunny, Cloudy extends Weather {}

Here’s a sample instance:

Boston – Sunny  
Seattle – Cloudy  
Miami – Sunny

Given that model, I should be able to assert: Every City has Weather.

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

I can then ask the Alloy Analyzer to check the assert:

check Every_city_has_weather

The Analyzer returns the expected result: No counterexample found

Excellent.

Now I would like to assert that there may be a Weather for which no City has that weather. In the example above, no City has the value Rainy.

I am having difficulty expressing this. I tried this: There is some w: Weather such that there is no City when joining the weather relation with w. Here’s the Alloy assert:

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

Then I asked the Alloy Analyzer to check my assertion:

check A_weather_may_not_be_in_any_city

The Analyzer responded with a counterexample (it showed an instance where each Weather value is mapped to a City).

Apparently my logic is not right. Can you think of the right logic for expressing this?

Daniel Jackson Daniel Jackson · Accepted Answer · 2016-11-19T22:56:31

If you want to see that some instance exists, you should use a run and not a check statement. An assert says something is true of every instance.
Given that you want to say "There is some w: Weather such that there is no City when joining the weather relation with w", I'd suggest expressing this very directly:

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

There may be no cities with rainy weather

1 Answers