Современная электроника №2/2021

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 41 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 2 2021 перекачивает или газ, или воздух, но не их вместе ( REQ10 ). Теорема Т11 утверждает, что если компрессоры К1 и К2 работают, то кла- пан V2 закрыт – это гарантирует, что компрессоры никогда не перекачивают одно и то же вещество ( REQ11 ). Теорема Т12 утверждает, что снятие сигнала Run отключает компрессоры К1 и К2 ( REQ12 ). Теорема Т13 утверждает, что клапа- ны V7 и V8 никогда не открыты одно- временно – это гарантирует, что эндо- газ не может подаваться в холодильник из двух реторт одновременно ( REQ13 ). Теорема Т14_1 утверждает, что для реторты R1 никогда не открыт ни один из воздушных трактов к коллектору. Существует всего три тракта: тракт 1 – при открытии клапанов V7 и V9, тракт 2 – при открытии клапанов V7 и V4, тракт 3 – при открытии клапанов V7, V3, V2. Теорема Т14_2 содержит аналогич- ное утверждение для реторты R2. Вме- сте теоремы Т14_1 и Т14_2 гарантиру- ют, что в линии Л3 никогда нет воздуха ( REQ14 ). Теорема Т15 утверждает, что при подаче газа (работает компрессор К1 и открыт клапан V1) обязательно открыт газовый тракт через реторту ( REQ15 ). Газовый тракт через реторту R1 возни- кает при открытии клапана V3 вместе с одним из клапанов V7, V9, через ретор- ту R2 – при открытии клапана V5 вме- сте с одним из клапанов V8, V10. Теорема Т16 утверждает, что газ пода- ётся (открыт клапан V1 и работает ком- прессор К1) на две реторты (открыты клапаны V3 и V5) и одна из них рабо- тает на холодильник (открыт клапан V7 или V8) тогда и только тогда, ког- да одна реторта находится в рабочем режиме, а вторая в режиме продувки газом (автомат B находится в состоя- нии B6 или B8). Теорема Т16 гаранти- рует выполнение требования REQ16 . Доказательство теорем Теоремы Т1 … Т16 были доказаны в интерактивном режиме. Дерево дока- зательства теоремы Т16 представле- но на рисунке 1. Основные леммы теоремы Т16 представлены в табли- це 2. Доказательство имеет следую- щую стратегию: эквиваленция теоре- мы разбивается на две импликации lem1 и lem2 (T16 = lem1 ∧ lem2). Левая часть импликации леммы lem1 добав- ляется к гипотезам и доказывает- ся её правая часть: что функция dtb при принятых гипотезах возвраща- ет значение B6 или B8. Лемма lem1.1 используется для доказательства лем- мы lem1 . Лемма lem1.1 утверждает, что функция dtb при принятых гипо- тезах никогда не возвращает значе- ния B1, B2, B3, B4, B5, B7, B9. В итоге из всех возможных значений функ- ции dtb остаётся только два: B6 или B8, что и требовалось доказать в лем- ме lem1 . Левая часть импликации леммы lem2 добавляется к гипотезам, и доказывает- ся её правая часть: что указанные функ- ции выходов при принятых гипотезах имеют значения TRUE. Доказательство леммы lem2 разбивается на доказатель- ство ряда лемм: lem2.1 … lem2.5 . Лемма lem2.1 утверждает, что функ- ция выходов LA_y3 имеет значение TRUE. Лемма lem2.1.1 используется для Листинг 2 axm24: partition(B, {B1},{B2},{B3},{B4},{B5},{B6},{B7},{B8},{B9}) axm25: InB = (A × BOOL × BOOL) axm26: b_1_4 = {x1 ↦ x2 ↦ x3 | x1=A2 ∧ x2=TRUE ∧ x3 ∈ BOOL} axm27: b_9_8 = b_1_4 axm28: b_1_5 = {x1 ↦ x2 ↦ x3 | x1=A2 ∧ x2=FALSE ∧ x3 ∈ BOOL} axm29: b_7_6 = b_1_5 axm30: b_4_7 = {x1 ↦ x2 ↦ x3 | x1=A2 ∧ x2 ∈ BOOL ∧ x3=TRUE} axm31: b_5_9 = b_4_7 axm32: b_6_9 = b_4_7 axm33: b_8_7 = b_4_7 axm34: b_x_1 = {x1 ↦ x2 ↦ x3 | x1=A1 ∧ x2 ∈ BOOL ∧ x3 ∈ BOOL} axm35: b_x_2 = {x1 ↦ x2 ↦ x3 | x1=A3 ∧ x2 ∈ BOOL ∧ x3 ∈ BOOL} axm36: b_x_3 = {x1 ↦ x2 ↦ x3 | x1=A4 ∧ x2 ∈ BOOL ∧ x3 ∈ BOOL} axm37: b_1_1 = InB\(b_1_4 ∪ b_1_5) axm38: b_2_2 = InB\(b_x_1) axm39: b_3_3 = InB\(b_x_1) axm40: b_4_4 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_4_7) axm41: b_5_5 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_5_9) axm42: b_6_6 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_6_9) axm43: b_7_7 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_7_6) axm44: b_8_8 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_8_7) axm45: b_9_9 = InB\(b_x_1 ∪ b_x_2 ∪ b_x_3 ∪ b_9_8) axm46: dtb ∈ (B × InB) → B axm47: ∀ s,i•((s=B1 ∧ i ∈ b_1_1) ∨ (s ∈ B\{B1} ∧ i ∈ b_x_1)) ⇔ dtb(s ↦ i) = B1 axm48: ∀ s,i•((s=B2 ∧ i ∈ b_2_2) ∨ (s ∈ B\{B1,B2,B3} ∧ i ∈ b_x_2)) ⇔ dtb(s ↦ i) = B2 axm49: ∀ s,i•((s=B3 ∧ i ∈ b_3_3) ∨ (s ∈ B\{B1,B2,B3} ∧ i ∈ b_x_3)) ⇔ dtb(s ↦ i) = B3 axm50: ∀ s,i•((s=B4 ∧ i ∈ b_4_4) ∨ (s=B1 ∧ i ∈ b_1_4)) ⇔ dtb(s ↦ i) = B4 axm51: ∀ s,i•((s=B5 ∧ i ∈ b_5_5) ∨ (s=B1 ∧ i ∈ b_1_5)) ⇔ dtb(s ↦ i) = B5 axm52: ∀ s,i•((s=B6 ∧ i ∈ b_6_6) ∨ (s=B7 ∧ i ∈ b_7_6)) ⇔ dtb(s ↦ i) = B6 axm53: ∀ s,i•((s=B7 ∧ i ∈ b_7_7) ∨ (s=B4 ∧ i ∈ b_4_7) ∨ (s=B8 ∧ i ∈ b_8_7)) ⇔ dtb(s ↦ i) = B7 axm54: ∀ s,i•((s=B8 ∧ i ∈ b_8_8) ∨ (s=B9 ∧ i ∈ b_9_8)) ⇔ dtb(s ↦ i) = B8 axm55: ∀ s,i•((s=B9 ∧ i ∈ b_9_9) ∨ (s=B5 ∧ i ∈ b_5_9) ∨ (s=B6 ∧ i ∈ b_6_9)) ⇔ dtb(s ↦ i) = B9 axm56: LB_y1 ∈ B → BOOL axm57: LB_y2 ∈ B → BOOL axm58: LB_y3 ∈ B → BOOL axm59: LB_y4 ∈ B → BOOL axm60: LB_y5 ∈ B → BOOL axm61: LB_y6 ∈ B → BOOL axm62: LB_y7 ∈ B → BOOL axm63: LB_y8 ∈ B → BOOL axm64: LB_y9 ∈ B → BOOL axm65: ∀ s•s ∈ {B2,B4,B6,B7,B8} ⇔ LB_y1(s) = TRUE axm66: ∀ s•s ∈ {B3,B5,B9} ⇔ LB_y2(s) = TRUE axm67: ∀ s•s ∈ {B2,B5,B6,B8,B9} ⇔ LB_y3(s) = TRUE axm68: ∀ s•s ∈ {B3,B4,B7} ⇔ LB_y4(s) = TRUE axm69: ∀ s•s ∈ {B6,B7} ⇔ LB_y5(s) = TRUE axm70: ∀ s•s ∈ {B8,B9} ⇔ LB_y6(s) = TRUE axm71: ∀ s•s ∈ {B2,B3,B4,B5,B8,B9} ⇔ LB_y7(s) = TRUE axm72: ∀ s•s ∈ {B2,B3,B4,B5,B6,B7} ⇔ LB_y8(s) = TRUE axm73: ∀ s•s ∈ {B4,B5,B6,B8} ⇔ LB_y9(s) = TRUE Таблица 1. Назначение аксиом Аксиома Назначение (что определяет аксиома) axm1 А – множество состояний автомата A axm2 InA – множество всех векторов входных сигналов автомата A axm3… axm10 a_i_j – множество векторов входных сигналов автомата A для перехода из состояния i в состояние j axm11 Тип функции переходов автомата А axm12… axm15 dta – функция переходов автомата А axm16… axm19 Тип функции выходов автомата А axm20… axm23 LA – функция выходов автомата А axm24 В – множество состояний автомата В axm25 InВ – множество всех векторов входных сигналов автомата В axm26… axm45 b_i_j – множество векторов входных сигналов автомата В для перехода из состояния i в состояние j axm46 Тип функции переходов автомата В axm47… axm55 dtb – функция переходов автомата В axm56… axm64 Тип функции выходов автомата В axm65… axm73 LВ – функция выходов автомата В