Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 10

Каждое отдельноеописание этого раздела cодержит перечисление имен каналов с указанием типапередаваемых посредством них значений и имеет вид:id1, … ,idn : type_expr, где n ≥ 1.Например:channel a : Nat,c, b : IntФункции с доступом к каналамФункции, имеющие доступ к каналам, в RSL называются также процессами. Всигнатуре таких функций доступ к каналам описывается в форме:in id1, ..., idn, n ≥ 1,где перечисляются каналы ввода, из которых функция может получать значения,или в форме:out id1, ..., idn, n ≥ 1,где указываются каналы вывода, по которым функция может выводить значения.В качестве примера рассмотрим следующий фрагмент спецификации:channel a ,b: Natvalue p : Unit -> in a out b UnitЗдесь функция p может вводить значения типа Nat по каналу a и выводить значениятого же типа по каналу b.51Выражения взаимодействияВ RSL предусмотрено два примитива взаимодействия: один для вводазначения из канала, другой для вывода значения в канал.

Если имеется следующееобъявление канала:channel id: Tто ввод значения из этого канала специфицируется выражением ввода вида:id?Вычисление данного выражения приостанавливается до тех пор, пока в указанныйканал не будет выведено значение каким-либо другим процессом. В этом случаевычисление выражения ввода завершается, и принятое по каналу значениевозвращается как результат вычисления выражения ввода.

Таким образом, длязавершения вычисления выражения ввода должно произойти взаимодействиепроцессов посредством указанного в выражении канала. Тип выражения вводасовпадает с типом канала.Например, выражение:a := c?специфицирует факт присваивания переменной a значения, введенного по каналу c.Вывод значения в канал специфицируется выражением вывода вида:id! value_exprВычисление такого выражения начинается с вычисления выражения value_expr,значение которого выводится в канал id. На этом вычисление выражения выводаприостанавливается до тех пор, пока выведенное значение не будет потреблено изканала каким-либо другим процессом. Таким образом, для завершения вычислениявыражения вывода также должно произойти взаимодействие процессовпосредством указанного в выражении канала.

Тип выражения value_expr долженсовпадать с типом канала id. Типом выражения вывода является тип Unit.В качестве примера рассмотрим спецификацию процесса opb, моделирующегоодноместный буфер, взаимодействующий с окружением посредством каналов add иget. Значения типа Elem вводятся из канала add и затем выводятся в канал get.scheme ONE_PLACE_BUFFER =classtype Elemchannel add, get : Elemvalue opb : Unit -> in add out get Unitaxiom opb() is let v = add? in get!v end; opb()endДанный процесс циклически выполняет указанное действие, цикличностьобеспечивается рекурсивным вызовом процесса.52Композиция параллельных выраженийВ RSL предусмотрено четыре вида композиции параллельных выражений:• параллельная композиция,• внешний выбор,• внутренний выбор,• взаимная блокировка (interlock).Параллельная композицияПараллельная композиция двух выражений задается выражением вида:value_expr1 || value_expr2Указанные выражения вычисляются параллельно до тех пор, пока одно из них незавершится, в то время как другое продолжит свое вычисление.

Оба выражениядолжны иметь тип Unit, этот же тип имеет и всё выражение. Символ || обозначаеткомбинатор параллельной композиции.Например, пусть имеются следующие объявления:channel c : Intvariable x : IntТогда параллельная композиция выражений x := c? и c!5 задается выражением:x := c? || c!5Вычисление этого выражения может привести к потенциальному взаимодействиювходящих в него выражений. В этом случае эффект вычисления параллельнойкомпозиции определяется выражением:x := 5Однако параллельные попытки записи в канал и чтения из каналанеобязательно приводят к взаимодействию. Это зависит от внутреннего выборавыражений.

В частности, выражения могут вообще не осуществить никакоговзаимодействия или осуществить взаимодействие с каким-либо другимпараллельно вычисляющимся выражением. Так, вычисление выражения:(x := c? || c!5) || c!7может привести к одному из следующих эффектов:••x := 7; c!5x := 5; c!7• взаимодействие не происходитКомбинатор параллельной композиции обладает свойствами коммутативностии ассоциативности.Внешний выборВнешний выбор задается выражением вида:value_expr1 |=| value_expr253Выражения value_expr1 и value_expr2 должны иметь одинаковый тип, которыйсчитается также и типом всего выражения внешнего выбора.

В результатевнешнего выбора из двух указанных выражений для вычисления выбираетсятолько одно, причем на выбор может оказать влияние окружение, т.е. другиевыражения, вычисляющиеся параллельно с данным. Именно поэтому в названииданной композиции фигурирует термин «внешний». Символ |=| обозначаеткомбинатор внешнего выбора.Внешний выбор служит для спецификации выбора между различными видамивзаимодействия. Например, в области видимости объявлений:channel c , d: Intvariable x : Intрассмотрим выражение внешнего выбора:x := c? |=| d!5Это выражение предлагает два вида взаимодействия: ввод из канала c или вывод вканал d.

Предположим, данное выражение вычисляется в следующем окружении:(x := c? |=| d!5) || c!1Тогда возможный эффект вычисления такого выражения состоит в выполнениивзаимодействия посредством канала c, в результате чего получается выражение:x := 1В данном случае выбор в пользу первого выражения диктуется окружением ( c!1).Комбинатор внешнего выбора обладает свойствами коммутативности иассоциативности.Внутренний выборВнутренний (недетерминированный) выбор задается выражением вида:value_expr1 |^| value_expr2 ,где выражения value_expr1 и value_expr2 должны иметь одинаковый тип, которыйсовпадает с типом всего выражения. В результате внутреннего выбора из двухвыражений для вычисления выбирается только одно, причем в отличие отпредыдущего случая окружение не оказывает никакого влияния на этот выбор.Символ |^| обозначает комбинатор внутреннего выбора.Например, в выражении:(x := c? |^| d!5) || c!1выражение c!1 не влияет на то, какое из выражений x := c? или d!5 выбирается.

Есливнутренний выбор выпадает на x:=c?, то результатом является выражение:x:= c? || c!1,потенциально приводящее к взаимодействию через канал c. Если выбор выпадаетна d!5, то результатом оказывается выражение:d!5 || c!1,54препятствующее внутренним взаимодействиям.Комбинаторвнутреннеговыборатакжекоммутативности и ассоциативности.обладаетсвойствамиВзаимная блокировка (interlock)Взаимная блокировка (interlock) задается выражением вида:value_expr1 ++ value_expr2 ,где ++ обозначает комбинатор взаимной блокировки. Указанные выражениявычисляются параллельно, блокируя друг друга по отношению к внешнимвзаимодействиям, до тех пор, пока одно из них не завершится, в то время какдругое продолжит свое вычисление. Оба выражения должны иметь тип Unit, этотже тип имеет и всё выражение. Отличие взаимной блокировки от параллельнойкомпозиции (||) состоит в том, что в течение параллельного вычисления непроисходит взаимодействия с окружением, оно становится возможным толькопосле снятия взаимной блокировки в результате завершения вычисления одного извыражений.

Таким образом, взаимная блокировка вынуждает выражениявзаимодействовать друг с другом.Комбинатор взаимной блокировки обладает свойством коммутативности, ноне является ассоциативным.Рассмотрим несколько примеров в области видимости объявлений:value e, e1, e2 : Tchannel c , c1, c2: Tvariable x : TОтличие взаимной блокировки от параллельной композиции иллюстрируютдве следующие эквивалентности:x := c? ++ c!e is x := ex := c? || c!e is (x := e) |^| ((x := c?; c!e)|=|(c!e; x := c?)|=|(x := e))В первом случае наличие взаимной блокировки вынуждает выражения выполнитьвзаимодействие.

Во втором случае в зависимости от внутреннего выборавыражений взаимодействие между ними либо происходит, либо окружение делаетвнешний выбор в пользу одного из указанных взаимодействий.Взаимная блокировка наглядно иллюстрирует также различие между внешними внутренним выбором:(x := c1? |=| c2!e2) ++ c1!e1 is x := e1(x := c1? |^| c2!e2) ++ c1!e1 is x := e1 |^| stopПри внутреннем выборе может произойти останов из-за невозможности выполнитьвзаимодействие (c2!e2 ++ c1!e1). Такая тупиковая ситуация специфицируется в RSLпредопределенным выражением stop.Другим примером того, как невозможность взаимодействия с окружениемприводит к останову, является эквивалентность:x := c1? ++ c2!e is stop55Для параллельной композиции соответствующая эквивалентность принимает вид:x := c1? || c2!e is (x := c1?; c2!e) |=| (c2!e; x := c1?)и выражает тот факт, что поскольку данные выражения не могутвзаимодействовать друг с другом, для них возможно только взаимодействие сокружением.Упрощение параллельных выраженийПри упрощении параллельных выражений кроме указанных свойств полезноиметь в виду следующие эквивалентности:value_expr1 || (value_expr2 |^| value_expr3) is(value_expr1 || value_expr2) |^| (value_expr1 || value_expr3)value_expr1 ++ (value_expr2 |^| value_expr3) is(value_expr1 ++ value_expr2) |^| (value_expr1 ++ value_expr3)Кроме того, если выражения value_expr, value_expr1 и value_expr2 не вызываютвзаимодействия и c1 ~= c2, то справедливы свойства:x := c1? || c2! value_expr is (x := c1?; c2! value_expr) |=| (c2! value_expr; x := c1?)x := c? || c! value_expr is (x := value_expr) |^|((x := c?; c! value_expr)|=|(c! value_expr; x := c?)|=|(x := value_expr))x := c1? ++ c2! value_expr is stopx := c? ++ c! value_expr is x := value_expr(x := c1? |=| c2! value_expr2) ++ c1! value_expr1 is x := value_expr1(x := c1? |^| c2! value_expr2) ++ c1! value_expr1 is (x := value_expr1) |^| stopУпражненияУпростить следующие параллельные выражения в предположении, чтопроизошли все возможные взаимодействия:1.

(b!2) || (y := a?) || if (x := 1); (a!x); (true |^| false) then a!(b?) else a!(1 + b?) end2. (b!2) || (x := a?) || if (a!3; true) |^| ((a!b? + 5); false) then a!(b?)else a!(1 + b?) end || (a!0)3. (if (a?) > 0 then b!1 else b!2 end ++( a!1; x := b?; b!4)) ||(y := if (b?) = 1 then a? else (0 - a?) end) || (a!0)4. a!(5 + b?) || ((x := (if true |^| false then x := b?; 1 else b!3; x := 2; 6 end) + x) ++(b!4 || y := b?))5. a!(5 + a?) || ((x := (if true |^| false then x := b?; 1 else x := b?; 6 end)) ++(b!4 || x := a? || a!3 || y := b?))566. case (1 |^| b?) of1 -> x := a? + 1,2 -> x := b?,3 -> y := a? + 3,4 -> y := b? + a?,5 -> x := y := a?; yend || a!1 || b!(a? + 2) || a!37. case (1 |^| b?) of1 -> x := a? + 1,2 -> x := b? |^| a?,3 -> y := a? + 3,4 -> y := b? + a?,5 -> x := y: = a?; yend || a!0 || b!(a? + a?) || a!2 || a!38.

case (a?) of0, 1 -> x := a? + 1,2 -> x := b?,3 -> y := a? + 3,4 -> y := b? + a?end || (x := a?; a!0 |=| b!(a?)) || a!457ГЛАВА 10. НЕДЕТЕРМИНИЗМ И НЕПОЛНЫЕ СПЕЦИФИКАЦИИПонятие недетерминизма и неполной спецификации. Источники недетерминизма вспецификациях. Недетерминизм в case- и let-выражениях. Упражнения.Понятие недетерминизма и неполной спецификацииПонятия недетерминизма и неполной спецификации имеют разную природу,но, вместе с тем, в спецификациях часто встречаются в похожих ситуациях,поэтому имеет смысл рассмотреть эти понятия совместно.Сначала остановимся на недетерминизме, а потом перейдем к неполнымспецификациям или, как говорят для краткости - недоспецификациям.Недетерминированным поведением мы называем такое поведение системы, когдадве попытки выполнения одной и той же операции, в случае RSL одного и того жевыражения, дают (могут дать) два разных результата.

Сразу же сделаем одноважное замечание. В принципе, можно рассматривать недетерминизм реальнойсистемы и недетерминизм ее модели, которая представлена некоторойспецификацией. В данной главе мы рассматриваем недетерминированныеспецификации, при этом в общем случае возможны следующие сочетанияреальных систем и их моделей:• ДсДм - детерминированная система и детерминированная модель - этопростейший случай;• НсДм - недетерминированная система и детерминированная модель• НсНм - недетерминированная система и недетерминированная модель• ДсНм - детерминированная система и недетерминированная модель.Пропуская случай ДсДм как достаточно простой, начнем сразу со второгослучая.