Возможно, нет городов с дождливой погодой

Question

Пусть «Погода» будет одним из следующих: Rainy, , 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] 
}    

Затем я могу попросить анализатор сплава проверить Assert:

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 
} 

Затем я спросил анализатор Alloy, чтобы проверить мое утверждение:

check A_weather_may_not_be_in_any_city 

Анализатор ответил контрпример (это показал экземпляр, где каждое значение Погода сопоставляется в городе).

Видимо, моя логика неправильная. Можете ли вы представить себе правильную логику для выражения этого?

Answer 1

1. Если вы хотите увидеть, что какой-либо экземпляр существует, вы должны использовать пробег, а не инструкцию проверки. Утверждение говорит, что что-то верно для каждый экземпляр.

2. Учитывая, что вы хотите сказать, «Существует несколько ш: Погода такая, что нет города, вступая в связь погоды с ш», я предложил бы выразить это очень прямо:

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