В этом примере показано, как проверить модель проекта о ремне безопасности, на которую ссылается верхний блок выше. Блок Свойства ниже содержит свойство, заданное в MATLAB Truth Table, которое указывает, когда выход SeatBeltIcon должен быть активен. Simulink Design Verifier анализирует свойство модели проекта и безопасности, чтобы доказать правильность или идентифицировать контрпримеры. В этой модели свойство доказано при явном предположении, что вход KEY начинается с 0 и изменяется с шагами 1.
open_system('sldvexSBRVerificationTruthTableFixedExample');
