Математические операции в сплаве

Question

У меня очень простая модель из сплава. Он должен приложить максимум максимум до 5 врачей в клинику, но когда я выполняю модель, она прикрепляет к клинике более 5 врачей. Вот моя модель.

abstract sig Clinic { 
    doctors : set Doctor 
} 
abstract sig Doctor { 
} 
fact ClinicDoctorRestriction { 
    all c:Clinic | #c.doctors <= 5 
} 
pred showresult{ 
} 
run showresult for exactly 1 Clinic, exactly 100 Doctor 

С моей моделью что-то не так?

Answer 1

В вашей модели нет ничего особенно плохого, если это область, которую вы используете для ее анализа.

Обратите внимание, что в вашем случае вы проверяете количество врачей, связанных с клиниками. Теперь вы выполнили в своей команде запуска, что ровно 100 докторов.

Вы должны всегда быть осторожным при игре с числами в сплаве, так как диапазон целых чисел, который вы можете использовать, зависит от ширины бита, назначенной им по их объему.

По умолчанию объем целого числа 4, и поэтому целые числа в диапазоне от -8 до 7.

Возвращаясь к вашему вопросу:

Почему существует более 5 врачей, связанных с клиникой ?

Предположим, что в клинику назначено 8 врачей, как может быть предоставленный вами факт, пусть это произойдет? Сплав не может представлять 8 в диапазоне [-8,7], поэтому происходит «переполнение», что приводит к неожиданному результату, что число врачей, назначенных клинике, составляет -8. Тот факт, что -8 действительно меньше 5, является причиной, по которой ваша модель позволяет, например, 8 врачей, которые будут связаны с одной клиник.

Как исправить:

Два варианта среди других:

• уменьшить количество врача
• увеличить диапазон Целые. Вам понадобится, чтобы представить достаточно целых чисел с шириной бита не менее 8, чтобы «разорвать» этих 100 врачей. run .. для 8 Int даст вам следующий диапазон целого числа: [-128,127]

Answer 2

Будьте осторожны с вашим объемом. Зачем вам 100 врачей?

Обратите внимание, что у 100 врачей и 1 клиники отношение врачей имеет 2^100 = 10^30 значений. Помните, что анализатор сплавов подобен проверке модели, поэтому вам нужно посмотреть пространство состояний. Никакой контролер модели не был бы счастлив с таким пространством состояний.