lection 9 (Электронные лекции)

1Лекция № 9КоннекторыnameвыходнойконнекторnameНельзя вставлять в местах:МакроMacrodefinition < имя > [ fpar < имя > { [ < имя > … ] } ]Mycheck fpar OK, FailТипыnewtype MyStruct CountryInfostructcode Integer;name Charstring;endnewtype CountryInfo;Входнойконнекто2operatorscode Extract!: CountryInfo Æ Integer;name Extract!: CountryInfo Æ Charstring;code Modify!: CountryInfo, Integer Æ CountryInfo;name Modify!: CountryInfo, Integer Æ CountryInfo;dcl myInfo CountryInfo;q Integer;q:= myInfo! Code;myInfo ! name := ‘Russia’;myInfo := ( 7,’Russia’ ) // неявно вызывает makemake!: Integer, Charstring Æ CountryInfo;Синтипы ( syntypes )syntype< name > = < old_name >[ constants < range > ]endsyntype;syntypeNatural = Integer // определение натуральных чиселConstatnts > 0endsyntype;Для Digits constants 1; 9any( Real) // значение – любое значение данного типаerror // ошибка, можно продолжать работу но сотояние не определено error !Определение операторовaxioms ‘perfoms logical xor’уравненияалгоритмическийуравнение: a and b = = b and aДля того чтобы это уравнение стало аксиомой, нужно3for all a, b in Booleanfor all d in Integer( d/0 = = error ! )Упорядочение( ordering )упорядочение – это :axiomsa = b = = True = => a< b = = False;a< b = = True = => a> b == False;a<= b = = a < b or a = b ;a>= b = = a > b or a = b ;a < b and b= c and c<d = => a<d = = True;Алгоритмическийoperator referenced// определение будет на отдельной диаграммеreferencedМОСТ MSC в SDL.

Алгоритм синтеза.Входные данные: набор MSC, HMSC диаграммалгоритм:• построение НКА по исходным данным• построение ДКА по НКА• минимизация ДКА• построение SDL-модели по набору ДКА4Узел на MSC :••••••Отправление ( out )Прием ( in )УстановкаСбросСрабатывание таймераПорождение сущности ( create )5StartStartεemptym1 m2εn2n1out( a,q )c1εin( b,q )n4in( c,q )endНКА(Q, F , Ev, ndgoto)F ⊆Qndgoto : Q × Ev → 2 Q∀q ∈ Q, ∀l ∈ Ev∀q ∈ Qn3c1m3ndgoto(q, l ) ≤ 1ndgoto(q, ε ) = 06ДетерминизацияНаблюд.

эквивалентности(Q, F , Ev, ndgoto)(Q ′, F ′, Ev ′, ndgoto′)Если ДКА ведет себя как НКА – наблюдаются состояния эквивалентностиQQ′ ⊆ 2Qq ∈Q[q ]q ∈ [q]εε∀q ′ : q ′ →q, q →q′⇒ q ′ ∈ [q ]Start, c1, n1, n2, n4endc1, n4n3Минимизация∀q1 , q 2 ∈ Fq1 ~ q 2∀q1 , q 2∀l ∈ Evgoto(q1 , l ) → q1′goto(q 2 , l ) → q 2′q1′ ~ q 2′ ⇒ q1 ~ q 2∀q1 , q 2∀l ∈ Evgoto(q1′ , l ) → q1goto(q ′2 , l ) → q 2q1′ ~ q 2′ ⇒ q1 ~ q 2.