Свойство, доказывающее с недопустимым свойством
В этом примере показано, как найти недопустимое свойство с помощью анализа доказательства свойства Simulink Design Verifier. Это пытается доказать, что, когда сумма тока и шести предыдущих входных значений больше 6, выход равняется 2. В этом случае свойство недопустимо потому что одно большое входное значение (e.g. 255), заставляет сумму быть больше 6. Simulink Design Verifier производит контрпример, который демонстрирует нарушение.
open_system('sldvdemo_debounce_falseprop');
