Теоретическое исследование моделей программы, решающей заданную задачу

Министерство Российской Федерации По связи и информатизации Сибирский государственный университет Телекоммуникации и информатики ПОЯСНИТЕЛЬНАЯ ЗАПИСКА К курсовой работе По дисциплине Теория вычислительных процессов На тему Теоретическое исследование моделей программы, решающей заданную задачу Новосибирск 2012

Задание к курсовой работ

Задачи к курсовой работе

Реферат

Краткая теория

Программная реализация

Вывод результатов

Стандартные схемы программ

Базис класса стандартных схем программ

Линейная форма стандартной схемы

Графовая форма стандартной схемы

Интерпретация стандартных схем программ

Сети Петри

Введение

в сети Петри

Основные определения

Анализ сетей Петри

ЛИНЕЙНАЯ СХЕМА ПРОГРАММ

ССП в графовой форме

Интерпретация

Инварианты и ограничения циклов

Доказательство частичной и полной правильности программы

Анализ сетей Петри на основе дерева достижимости

Сеть Петри

Дерево достижимости

Выводы по работе

Задание к курсовой работе

1. Написать программу решения задачи, номер которой совпадает с Вашим номеров в журнале.

2. Составить и исследовать ССП в линейной и графовой форме.

3. Указать интерпретацию ССП и составить протокол выполнения программы.

4. Построить и исследовать инварианты и ограничения цикла (ов).

5. Доказать частичную и полную правильность программы.

6. Представить схему программы в виде сети Петри и осуществить анализ ее свойств на основе дерева достижимости.

Задачи к курсовой работе

Вариант 2

Для заданной целочисленной матрицы найти максимум среди сумм элементов диагоналей, параллельных главной диагонали матрицы.

Реферат

Данная пояснительная записка содержит 23 листа, 5 схем, образец выполнения программы, текст программы.

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

Краткая теория

Главная диагональ — диагональ квадратной матрицы, идущая из верхнего левого угла матрицы в правый нижний.

Программная реализация

Код программы:

//—————————————————————————————————————;

#include

#pragma hdrstop

#include «Unit1.h»

#include «Unit2.h»

#include

//—————————————————————————————————————;

#pragma package (smart_init)

#pragma resource «*.dfm»

TForm1 *Form1;

int n, maxindex=-10;

//—————————————————————————————————————;

__fastcall TForm1: TForm1(TComponent* Owner)

: TForm (Owner)

{

}

//—————————————————————————————————————;

void __fastcall TForm1: Edit1Change (TObject *Sender)

{

StringGrid1->RowCount = 0;

StringGrid1->ColCount = 0;

StringGrid2->RowCount = 0;

StringGrid2->ColCount = 0;

if (CompareText (Form1->Edit1->Text," «) == 0){}

else

{

if (StrToInt (Form1->Edit1->Text) > 1000)

{

Application->MessageBoxA;

return;

}

try { n = StrToInt (Form1->Edit1->Text); }

catch (…)

{

Application->MessageBox;

return;

}

}

for (int i=0; i < StringGrid1->RowCount; i++) Form1->StringGrid1->Rows[i]->Clear ();

for (int i=0; i < StringGrid2->RowCount; i++) Form1->StringGrid2->Rows[i]->Clear ();

Form1->Edit2->Clear ();

Form1->Edit3->Clear ();

Form1->Button1->Enabled = false;

maxindex = -10;

}

//—————————————————————————————————————;

void __fastcall TForm1: Button2Click (TObject *Sender)

{

randomize ();

Form1->StringGrid1->Visible = true;

int i, j;

if (CompareText (Form1->Edit1->Text," «) == 0) {Application->MessageBoxA}

else

{

Form1->StringGrid1->ColCount = n;

Form1->StringGrid1->RowCount = n;

Form1->StringGrid2->ColCount = 2*n — 1;

Form1->StringGrid2->RowCount = 2;

for (i=0; i

{

for (j=0; jStringGrid1->Cells[i][j]=n — random (2*n);

}

Form1->Button1->Enabled = true;

}

Form1->Edit2->Clear ();

Form1->Edit3->Clear ();

if (n == 0)

{

Form1->Button1->Enabled = false;

Form1->StringGrid2->Visible = false;

}

if (n == 1)

{

Form1->Button1->Enabled = false;

Form1->Edit2->Text = Form1->StringGrid1->Cells[0][0];

Form1->Edit3->Text = 0;

Form1->StringGrid2->Visible = true;

Form1->StringGrid2->Cells[0][0]=0;

Form1->StringGrid2->Cells[0][1]=Form1->StringGrid1->Cells[0][0];

}

}

//—————————————————————————————————————;

void __fastcall TForm1: CheckBox1Click (TObject *Sender)

{

//if (Form1->CheckBox1->Checked) Form1->StringGrid1->Options = Form1->StringGrid1->Options << goEditing;

//else Form1->StringGrid1->Options = Form1->StringGrid1->Options >> goEditing;

}

//—————————————————————————————————————;

void __fastcall TForm1: StringGrid1SetEditText (TObject *Sender, int ACol,

int ARow, const AnsiString Value)

{

int v;

AnsiString s = Form1->StringGrid1->Cells[ACol][ARow];

if ((CompareText (s," «) == 0) || (CompareText (s,» -") == 0)){}

else

{

try { v = StrToInt (s); }

catch (…)

{

Application->MessageBox («Iaaa?iua aoiaiua aaiiua», «Ioeaea», 0);

return;

}

}

}

//—————————————————————————————————————;

void __fastcall TForm1: Button3Click (TObject *Sender)

{

int Row_Count, Col_Count;

TStringList **Result;

if (!Form1->OpenDialog1->Execute ()) return;

if (FileOpen (OpenDialog1->FileName, Result, Row_Count, Col_Count))

{

Form1->Edit1->Clear ();

Form1->StringGrid1->RowCount = Row_Count-1;

Form1->StringGrid1->ColCount = Col_Count-1;

Form1->StringGrid2->ColCount = 2*Row_Count — 1;

Form1->StringGrid2->RowCount = 2;

for (int i = 0; i < Row_Count-1; ++i)

{

for (int j = 0; j < Col_Count-1; ++j) Form1->StringGrid1->Cells[j][i] = Result[i]->Strings[j];

}

Form1->Button1->Enabled = true;

Form1->Edit2->Clear ();

Form1->Edit3->Clear ();

}

n = Row_Count-1;

Form1->StringGrid1->Visible = true;

}

//—————————————————————————————————————;

void __fastcall TForm1: Button1Click (TObject *Sender)

{

StringGrid2->Visible = true;

int i, j, index=0, sum, max=0, t;

for (i=0; i

{

sum = 0;

for (j=0; jStringGrid1->Cells[j][j+n-1-i]);

Form1->StringGrid2->Cells[index][0] = index;

Form1->StringGrid2->Cells[index][1] = sum;

if (sum>max)

{

max=sum;

maxindex=index;

}

index++;

}

sum = 0;

for (j=0; jStringGrid1->Cells[j][j]);

Form1->StringGrid2->Cells[index][0] = index;

Form1->StringGrid2->Cells[index][1] = sum;

if (sum>max)

{

max=sum;

maxindex=index;

}

index++;

for (i=n-2; i>=0; i—)

{

sum = 0;

for (j=0; jStringGrid1->Cells[j+n-1-i][j]);

Form1->StringGrid2->Cells[index][0] = index;

Form1->StringGrid2->Cells[index][1] = sum;

if (sum>max)

{

max=sum;

maxindex=index;

}

index++;

}

StringGrid1->Refresh ();

Form1->Edit3->Text = maxindex;

Form1->Edit2->Text = max;

}

//—————————————————————————————————————-

void __fastcall TForm1: StringGrid2DrawCell (TObject *Sender, int ACol,

int ARow, TRect &Rect, TGridDrawState State)

{

if (ACol == maxindex)

{

StringGrid2->Canvas->Brush->Color = clAqua;

StringGrid2->Canvas->FillRect (Rect);

StringGrid2->Canvas->TextOut (Rect.Left, Rect. Top, StringGrid2->Cells[ACol][ARow]);

}

}

//—————————————————————————————————————-

void __fastcall TForm1: StringGrid1DrawCell (TObject *Sender, int ACol,

int ARow, TRect &Rect, TGridDrawState State)

{

if (n — ARow + ACol — 1 == maxindex)

{

StringGrid1->Canvas->Brush->Color = clAqua;

StringGrid1->Canvas->FillRect (Rect);

StringGrid1->Canvas->TextOut (Rect.Left, Rect. Top, StringGrid1->Cells[ACol][ARow]);

}

}

//—————————————————————————————————————-

void __fastcall TForm1: N2Click (TObject *Sender)

{

Application-> 0);

}

//—————————————————————————————————————-

void __fastcall TForm1: N3Click (TObject *Sender)

{

Application->MessageBoxA;

}

//—————————————————————————————————————-

void __fastcall TForm1: N4Click (TObject *Sender)

{

Application->MessageBoxA («Eo?niaie i? iaeo ii OAI, aa? eaio ?2», «I i? ia?aiia», 0);

}

//—————————————————————————————————————-

void __fastcall TForm1: Button4Click (TObject *Sender)

{

StringGrid1->RowCount = 0;

StringGrid1->ColCount = 0;

StringGrid2->RowCount = 0;

StringGrid2->ColCount = 0;

for (int i=0; i < StringGrid1->RowCount; i++) Form1->StringGrid1->Rows[i]->Clear ();

for (int i=0; i < StringGrid2->RowCount; i++) Form1->StringGrid2->Rows[i]->Clear ();

Form1->Edit2->Clear ();

Form1->Edit3->Clear ();

Form1->Button1->Enabled = false;

maxindex = -10;

Form1->CheckBox1->Checked = false;

}

//—————————————————————————————————————-

void __fastcall TForm1: StringGrid1SelectCell (TObject *Sender, int ACol,

int ARow, bool &CanSelect)

{

AnsiString str = Form1->StringGrid1->Cells[ACol][ARow];

if (Form1->CheckBox1->Checked == true)

{

Form2->Edit1->Text = Form1->StringGrid1->Cells[ACol][ARow];

Form2->ShowModal ();

if (Form2->Edit1->Text == «») Form1->StringGrid1->Cells[ACol][ARow] = str;

else Form1->StringGrid1->Cells[ACol][ARow] = Form2->Edit1->Text;

}

}

//—————————————————————————————————————-

Вывод результатов

Стандартные схемы программ

Базис класса стандартных схем программ

Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы.

Базис класса фиксирует символы, из которых строятся схемы, указывает их роль (переменные, функциональные символы и др.), задает вид выражений и операторов схем.

Полный базис В класса стандартных схем состоит из 4-х непересекающихся, счетных множеств символов и множества операторов — слов, построенных из этих символов.

Множества символов полного базиса:

1. Х = x, х1, х2…, у, у1 у2…, z, z1, z2… — множество символов, называемых переменными;

2. F = f (0), f (1), f (2)…, g (0), g (1), g (2)…, h (0), h (1), h (2)… — множество функциональных символов; верхний символ задает местность символа; нульместные символы называют константами и обозначают начальными буквами латинского алфавита a, b, c…;

3. Р = р (0), р (1), р (2)…; q (0), q (1), q (2)…; - множество предикатных символов; р (0), q (0) —; нульместные символы называют логическими константами;

4. start, stop, …:= и т. д. — множество специальных символов.

Термами (функциональными выражениями) называются слова, построенные из переменных, функциональных и специальных символов по следующим правилам:

1. односимвольные слова, состоящие из переменных или констант, являются термами;

2. слово? вида f (n)(?1, ?2???n), где ?1, ?2???n — термы, является термом;

3. те и только те слова, о которых говорится в п.п. 1,2, являются термами.

Примеры термов: х, f (0), а, f (1)(х), g (2)(x, h (3)(y, a)).

Тестами (логическими выражениями) называются логические константы и слова вида р (n)(?1, ?2,…,?n). Допускается в функциональных и логических выражениях опускать индексы местности, если это не приводит к двусмысленности или противоречию.

Множество операторов включает пять типов:

1. начальный оператор — слово вида start (х1, х2… хк), где k ?0, а х1, х2… хк — переменные, называемые результатом этого оператора;

2. заключительный оператор — слово вида stop (?1, ?2???n), где n ?0, а ?1, ?2???n — термы; вхождения переменных в термы? называются аргументами этого оператора;

3. оператор присваивания — слово вида х := ?, где х — переменная (результат оператора), а? — терм; вхождения переменных в термы называются аргументами этого оператора;

4. условный оператор (тест) — логическое выражение; вхождения переменных в логическое выражение называются аргументами этого оператора;

5. оператор петли — односимвольное слово loop.

Среди операторов присваивания выделим случаи: когда? — переменная, то оператор называется пересылкой (х:=у) и когда? -константа, то оператор называется засылкой (х:=а).

Подклассы используют ограниченные базисы. Так, например, подкласс У1 имеет базис:

х1, х2, а, f (1), p (1), start, stop, (,):=,, и множество операторов start (х1, х2); х1:= f (x1), x2=f (x2), x1:=а, х2:= а, р (х1), р (х2), stop (х1,х2), т. е. схемы из этого подкласса используют две переменные, константу а, один одноместный функциональный символ, один предикатный символ и операторы указанного вида.

Линейная форма стандартной схемы

Для использования линейной формы СПП множество специальных символов расширим дополнительными символами, goto, if, then, else. СПП в линейной форме представляет собой последовательность инструкций, которая строится следующим образом:

1. если выходная дуга начальной вершины с оператором start (х1,…, хn) ведет к вершине с меткой L, то начальной вершине соответствует инструкция:

0: start (х1,…, хn) goto L;

2. если вершина схемы S с меткой L — преобразователь с оператором присваивания х:=?, выходная дуга которого ведет к вершине с меткой L1, то этому преобразователю соответствует инструкция:

L: x: =? goto L1;

3. если вершина с меткой L — заключительная вершина с оператором stop (?1,???m), то ей соответствует инструкция

L: stop (?1,…, ?m);

4. если вершина с меткой L — распознаватель с условием р (?1,???k), причем 1-дуга ведет к вершине с меткой L1, а 0-дуга — к вершине с меткой L0, то этому распознавателю соответствует инструкция

L: if р (?1,???k) then L1 else L0;

5. если вершина с меткой L — петля, то ей соответствует инструкция

L: loop.

Графовая форма стандартной схемы

Представим стандартную схему программ как размеченный граф, вершинам которого приписаны операторы из некоторого базиса В.

Стандартной схемой в базисе В называется конечный (размеченный ориентированный) граф без свободных дуг и с вершинами следующих пяти видов:

1. Начальная вершина (ровно одна) помечена начальным о1ператором. Из нее выходит ровно одна дуга. Нет дуг, ведущих к начальной вершине.

2. Заключительная вершина (может быть несколько). Помечена заключительным оператором. Из нее не выходит ни одной дуги.

3. Вершина-преобразователь. Помечена оператором присваивания. Из нее выходит ровно одна дуга.

4. Вершина-распознаватель. Помечена условным оператором (называемым условием данной вершины). Из нее выходит ровно две дуги, помеченные 1 (левая) и 0 (правая).

5. Вершина-петля. Помечена оператором петли. Из нее не выходит ни одной дуги.

Конечное множество переменных схемы S составляют ее память ХS.

Из определения следует, что один и тот же оператор может помечать несколько вершин схемы.

Вершины именуются (метки вершины) целым неотрицательным числом (0, 1, 2…). Начальная вершина всегда помечается меткой 0.

Схема S называется правильной, если на каждой дуге заданы все переменные.

Интерпретация стандартных схем программ

ССП не является записью алгоритма, поэтому позволяет исследовать только структурные свойства программ, но не семантику вычислений. При построении «семантической» теории схем программ вводится понятие интерпретация ССП. Определим это понятие.

Пусть в некотором базисе В определен класс ССП. Интерпретацией базиса В в области интерпретации D называется функция I, которая сопоставляет:

1. каждой переменной х из базиса В — некоторый элемент d = I (x) из области интерпретации D;

2. каждой константе, а из базиса В — некоторый элемент d = I (а) из области интерпретации D;

3. каждому функциональному символу f (n) — всюду определенную функцию F (n)=I (f (n));

4. каждой логической константе р (0) — один символ множества 0,1 ;

5. каждому предикатному символу р (n) — всюду определенный предикат P (n) = I (p (n)).

Пара (S, I) называется интерпретированной стандартной схемой (ИСС), или стандартной программой (СП).

Определим понятие выполнения программы

Состоянием памяти программы (S, I) называют функцию W: XS D, которая каждой переменной x из памяти схемы S сопоставляет элемент W (x) из области интерпретации D.

Значение терма? при интерпретации I и состоянии памяти W (обозначим ?I (W)) определяется следующим образом:

1) если ?=х, x — переменная, то? I (W) = W (x);

2) если ?=a, a — константа, то? I (W) = I (a);

3) если ?=f (n)(?1, ?2…, ?n), то? I (W)= I (f (n))(?1I (W), ?2I (W),…, ?nI (W)).

Аналогично определяется значение теста при интерпретации I и состоянии памяти W или I (W):

если =р (n)(?1, ?2…, ?n), то I (W)= I (p (n))(?1I (W), ?2I (W),… ?nI (W)), n ?0.

Конфигурацией программы называют пару U=(L, W), где L — метка вершины схемы S, а W — состояние ее памяти. Выполнение программы описывается конечной или бесконечной последовательностей конфигураций, которую называют протоколом выполнения программы (ПВП).

Протокол (U0, U1,…, Ui, Ui+1,…) выполнения программы (S, I) определяем следующим образом (ниже ki означает метку вершины, а Wi — состояние памяти в i-й конфигурации протокола, Ui=(ki, Wi)):

U0=(0, W0), W0 — начальное состояние памяти схемы S при интерпретации I.

Пусть Ui=(ki, Wi) — i-я конфигурация ПВП, а О — оператор схемы S в вершине с меткой ki. Если О — заключительный оператор stop (?1, ?2… ?n), то Ui — последняя конфигурация, так что протокол конечен. В этом случае считают, что, программа (S, I) останавливается, а последовательность значений ?1I (W), ?2I (W),…, ?nI (W) объявляют результатом val (S, I) выполнения программы (S, I). В противном случае, т. е. когда О — не заключительный оператор, в протоколе имеется следующая, (i+1)-я конфигурация Ui+1 = (ki+1, Wi+1), причем

а) если О — начальный оператор, а выходящая из него дуга ведет к вершине с меткой L, то ki+1 = L и Wi+1 = Wi;

б) если О — оператор присваивания х:=?, а выходящая из него дуга ведет к вершине с меткой L, то ki+1 = L, Wi+1 = Wi, Wi+1(х) = ?1(Wi);

в) если О — условный оператор и I (Wi) = ?, где? 0,1, а выходящая из него дуга ведет к вершине с меткой L, то ki+1 = L и Wi+1 = Wi;

г) если О — оператор петли, то ki+1 = L и Wi+1 = Wi, так что протокол бесконечен.

Таким образом, программа останавливается тогда и только тогда, когда протокол ее выполнения конечен. В противном случае программа зацикливается и результат ее выполнения не определен.

Сети Петри

Введение

в сети Петри

Сети Петри это инструмент для математического моделирования и исследования сложных систем. Цель представления системы в виде сети Петри и последующего анализа этой сети состоит в получении важной информации о структуре и динамическом поведении моделируемой системы. Эта информация может использоваться для оценки моделируемой системы и выработки предложений по ее усовершенствованию. Впервые сети Петри предложил немецкий математик Карл Адам Петри.

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

В одном из подходов к проектированию и анализу систем сети Петри используются, как вспомогательный инструмент анализа. Здесь для построения системы используются общепринятые методы проектирования. Затем построенная система моделируется сетью Петри, и модель анализируется. Если в ходе анализа в проекте найдены изъяны, то с целью их устранения проект модифицируется. Модифицированный проект затем снова моделируется и анализируется. Этот цикл повторяется до тех пор, пока проводимый анализ не приведет к успеху.

Другой подход предполагает построение проекта сразу в виде сети Петри. Методы анализа применяются только для создания проекта, не содержащего ошибок. Затем сеть Петри преобразуется в реальную рабочую систему.

В первом случае необходима разработка методов моделирования систем сетями Петри, а во втором случае должны быть разработаны методы реализации сетей Петри системами.

Основные определения

Теоретико-множественное определение сетей Петри

Пусть мультимножество это множество, допускающее вхождение нескольких экземпляров одного и того же элемента.

Сеть Петри N является четверкой N=(P, Т, I, O), где

P = {p1, p2,…, pn} — конечное множество позиций, n 0;

T = {t1, t2,…, tm} — конечное множество переходов, m 0;

I: T P* — входная функция, сопоставляющая переходу мультимножество его входных позиций;

О: T P* - выходная функция, сопоставляющая переходу мультимножество его выходных позиций.

Позиция pP называется входом для перехода tT, если pI (t). Позиция pP называется выходом для перехода tT, если pO (t). Структура сети Петри определяется ее позициями, переходами, входной и выходной функциями.

Графы сетей Петри

Наиболее наглядным представлением сети Петри является её графическое представление, которое представляет собой двудольный, ориентированный мультиграф.

Граф сети Петри обладает двумя типами узлов: кружок, представляющий позицию сети Петри; и планка, представляющая переход сети Петри. Ориентированные дуги этого графа (стрелки) соединяют переход с его входными и выходными позициями. При этом дуги направлены от входных позиций к переходу и от перехода к выходным позициям. Кратным входным и выходным позициям перехода соответствуют кратные входные и выходные дуги. Граф сети Петри примера 4.1.

Правила выполнения сетей Петри

Сеть Петри выполняется посредством запусков переходов. Запуск перехода управляется фишками в его входных позициях и сопровождается удалением фишек из этих позиций и добавлением новых фишек в его выходные позиции.

Переход может запускаться только в том случае, когда он разрешен. Переход называется разрешенным, если каждая из его входных позиций содержит число фишек, не меньшее, чем число дуг, ведущих из этой позиции в переход (или кратности входной дуги).

Пусть функция ^#: PT Nat для произвольных позиции pP и перехода tТ задает значение ^#(p, t), которое совпадает с кратностью дуги, ведущей из p в t, если такая дуга существует, и с нулем, в противном случае.

Пусть функция #^: TP Nat для произвольных и перехода tT позиции pP задает значение #^(t, p), которое совпадает с кратностью дуги, ведущей из t в p, если такая дуга существует, и с нулем, в противном случае.

Переход tT в маркированной сети Петри N=(P, T,1,О,) разрешен, если для всех p I (t) справедливо (?p) ?? ?^#(p, t).

Запуск разрешённого перехода tT из своей входной позиции pI (t) удаляет ^#(p, t) фишек, а в свою выходную позицию p' O (t) добавляет #^(t, p') фишек.

Переход t в маркированной сети Петри с маркировкой может быть запущен всякий раз, когда он разрешен и в результате этого запуска образуется новая маркировка ', определяемая для всех pP следующим соотношением:

'(p)= (p) — ^#(p, t) + #^(t, p).

Запуски могут осуществляться до тех пор, пока существует хотя бы один разрешенный переход. Когда не останется ни одного разрешенного перехода, выполнение прекращается.

Если запуск произвольного перехода t преобразует маркировку сети Петри в новую маркировку ', то будем говорить, что ' достижима из посредством запуска перехода t и обозначать этот факт, как t '. Это понятие очевидным образом обобщается для случая последовательности запусков разрешённых переходов. Через R (N,) обозначим множество всех достижимых маркировок из начальной маркировки в сети Петри N.

Преобразование маркировки сети Петри изображено на рисунке 4.3. Переход t1 преобразует маркировку? =<5,1> в маркировку '=<2,3>.

Анализ сетей Петри

Моделирование систем сетями Петри, прежде всего, обусловлено необходимостью проведения глубокого исследования их поведения. Для проведения такого исследования необходимы методы анализа свойств самих сетей Петри. Этот подход предполагает сведения исследования свойств реальной системы к анализу определенных свойств моделирующей сети Петри.

программа сеть петри матрица

Свойства сетей Петри

Позиция pP сети Петри N=(P, Т, I, O) c начальной маркировкой является k-ограниченной, если '(p)k для любой достижимой маркировки 'R (N,). Позиция называется ограниченной, если она является k-ограниченной для некоторого целого значения k. Сеть Петри ограниченна, если все ее позиции ограниченны.

Позиция pP сети Петри N=(P, Т, I, O) c начальной маркировкой является безопасной, если она является 1-ограниченной.Сеть Петри безопасна, если безопасны все позиции сети.

Сеть Петри N=(P, Т, I, O) с начальной маркировкой является сохраняющей, если для любой достижимой маркировки 'R (N,) справедливо следующее равенство.

Тупик в сети Петри — один или множество переходов, которые не могут быть запущены. Определим для сети Петри N с начальной маркировкой следующие уровни активности переходов:

Уровень 0: Переход t обладает активностью уровня 0 и называется мёртвым, если он никогда не может быть запущен.

Уровень 1: Переход t обладает активностью уровня 1 и называется потенциально живым, если существует такая 'R (N,), что t разрешён в '.

Уровень 2: Переход t, обладает активностью уровня 2 и называется живым, если для всякой 'R (N,) переход t является потенциально живым для сети Петри N с начальной маркировкой '.

Сеть Петри называется живой, если все её переходы являются живыми.

Задача достижимости: Для данной сети Петри с маркировкой и маркировки ' определить: 'R (N,)?

Задача покрываемости: Для данной сети Петри N с начальной маркировкой и маркировки ' определить, существует ли такая достижимая маркировка «R (N,), что «>'.

(Отношение «' истинно, если каждый элемент маркировки «не меньше соответствующего элемента маркировки '.)

Сети Петри присуще некоторое поведение, которое определяется множеством ее возможных последовательностей запусков переходов или ее множеством достижимых маркировок. Понятие эквивалентности сетей Петри определяется через равенство множеств достижимых маркировок.

Сеть Петри N=(P, Т, I, O) с начальной маркировкой и сеть Петри N'=(P', Т', I', O') с начальной маркировкой ' эквивалентны, если справедливо R (N,)=R (N',').

Понятие эквивалентности сетей Петри может быть определено также через равенство множеств возможных последовательностей запусков переходов.

Более слабым, по сравнению с эквивалентностью, является свойство включения, определение которого совпадает с определением эквивалентности, с точностью до замены = на .

Методы анализа

Особый интерес вызывают методы анализа свойств сетей Петри, которые обеспечивают автоматический анализ моделируемых систем. Сначала рассмотрим метод анализа сетей Петри, который основан на использовании дерева достижимости.

Дерево достижимости

Дерево достижимости представляет все достижимые маркировки сети Петри, а также — все возможные последовательности запусков ее переходов.

Важнейшим свойством алгоритма построения конечного дерева достижимости является то, что он за конечное число шагов заканчивает работу.

Анализ свойств сетей Петри на основе дерева достижимости

Анализ безопасности и ограниченности. Сеть Петри ограниченна тогда и только тогда, когда символ отсутствует в ее дереве достижимости.

Присутствие символа в дереве достижимости ([х](p)= для некоторой вершины x и позиции p) означает, что для произвольного положительного целого k существует достижимая маркировка со значением в позиции p, большим, чем k (а также бесконечность множества достижимых маркировок). Это, в свою очередь, означает неограниченность позиции p, а следовательно, и самой сети Петри.

Отсутствие символа в дереве достижимости означает, что множество достижимых маркировок конечно. Следовательно, простым перебором можно найти верхнюю границу, как для каждой позиции в отдельности, так и общую верхнюю границу для всех позиций. Последнее означает ограниченность сети Петри. Если граница для всех позиций равна 1, то сеть Петри безопасна.

Анализ сохранения. Так как дерево достижимости конечно, для каждой маркировки можно вычислить сумму начальной маркировки. Если эта сумма одинакова для каждой достижимой маркировки, то сеть Петри является сохраняющей. Если суммы не равны, сеть не является сохраняющей. Если маркировка некоторой позиции совпадает с, то эта позиция должна был исключена из рассмотрения.

Анализ покрываемости. Задача покрываемости требуется для заданной маркировки ' определить, достижима ли маркировка «'. Такая задача решается путём простого перебора вершин дерева достижимости. При этом ищется такая вершина х, что [x]'. Если такой вершины не существует, то маркировка ' не является покрываемой. Если она найдена, то [x] определяет покрывающую маркировку для ' Если компонента маркировки [x], соответствующая некоторой позиции p совпадает с, то конкретное её значение может быть вычислено. В этом случае на пути от начальной маркировки к покрывающей маркировке имеется повторяющаяся последовательность переходов, запуск которой увеличивает значение маркировки в позиции p. Число таких повторений должно быть таким, чтобы значение маркировки в позиции p превзошло или сравнялось с '(p).

Анализ живости. Переход t сети Петри является потенциально живым, тогда и только тогда, когда он метит некоторую дугу в дереве достижимости этой сети.

Доказательство очевидно.

Ограниченность метода дерева достижимости. Как видно из предыдущего, дерево достижимости можно использовать для решения задач безопасности, ограниченности, сохранения и покрываемости. К сожалению, в общем случае его нельзя использовать для решения задач достижимости и активности, эквивалентности. Решение этих задач ограничено существованием символа. Символ означает потерю информации: конкретные количества фишек отбрасываются, учитывается только существование их большого числа.

Линейная схема программы

0: begin

1: input mas, N

2: i:=c;

3: m: if s (i, a) then goto m1;

4: sum1 := a;

5: sum2 := a;

6: j := k (i);

7: l: if s (d, j) then goto l1;

8: sum1: = f (sum1,mas, i, j);

9: sum2 := g (sum2,mas, i, j);

10: j := inc (j);

11: goto l;

12: ms :=h (sum1, sum2);

13: if m (ms, max) then max := r (ms);

14: i := dec (i);

15: goto m;

16: output max;

17: end.

ССП в графовой форме

Интерпретация

1. Переменные:

mas — массив, содержит матрицу целочисленных элементов.

N — размерность матрицы. Целочисленная переменная.

i, j — счётчики циклов. Целочисленные переменные.

sum1, sum2, ms — переменные для нахождения суммы элементов

max — переменная, содержащая максимальную сумму.

2. Константы:

c = N-1;

a = 0;

d = N;

3. Предикаты:

S (x, y) — if x>y => T;

4. Функции:

inc (x) — x++;

h (x, y) — if x >= y return x; else return y;

N =3;

Mas = {1, 2, 3,

4, 5, 6,

7, 8, 9}; Протокол

Инварианты и ограничения циклов

Алгоритм решения задачи:

max:= A[n-1,0];

i:= -n+1;

Do i < m

sum:= 0;

if 1-i >0 j:= 1-i 1-i 0 j:= 1 fi;

Do i+j m and j n sum:= sum+A[j-1,i+j-1]; j:= j+1 Od

if max < sum max:= sum fi

i:= i+1

Od

Инвариант и ограничивающая функция для внутреннего цикла:

n — количество строк в матрице;

m — количество столбцов в матрице;

P: j, i: -n+1 i < m and 1 j

j j

sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0

k=1 k=1-i

Ограничивающая функция t: m-i-j-1 and n-j

Инвариант и ограничивающая функция для внешнего цикла:

P: j, i: -n+1 i < m and 1 j

j j

max: (max A[k-1, i+k-1] or max A[k-1, i+k-1])

k=1 k=1-i

j j

and (max = A[k-1, i'+k-1] or max = A[k-1, i'+k-1])

k=1 k=1-i

Ограничивающая функция t: 0-i — для отрицательной части or m-i — для неотрицательной части

Доказательство частичной и полной правильности программы.

Докажем правильность работы внутреннего цикла.

X

-n+1 y

j, i: -n+1 i < m and 1 j

j j

sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0 (*)

k=1 k=1-i

При первом попадании в точку Х утверждение (*) выполняется, так как sum=0.

Пусть при p — попадании в точку Х утверждение (*) выполняется. Докажем, что утверждение (*) выполняется при p+1 — попадании в точку Х.

Для p:

j j

sum: sum = A[k-1, i+k-1] or sum = A[k-1, i+k-1] or sum=0

k=1 k=1-i

Чтобы попасть в точку Х необходимо, чтобы выполнилось условие i+j m and j n и операторы

j j+1

sum = A[k-1, i+k-1] + A[k, i+k] = A[k-1, i+k-1] or

k=1 k=1

j j+1

sum = A[k-1, i+k-1] + A[k, i+k] = A[k-1, i+k-1]

k=1-i k=1-i

Так как условие (i+j m and j n) выполнилось, то i+j+1 m and j+1 n при p+1 — попадании в точку Х утверждение (*) справедливо.

Докажем, что цикл закончится то есть выполнится условие (i+j > m or j > n).

При первом попадании в точку Х: -n+1 i m or j > n) и цикл завершится.

Докажем правильность работы внешнего цикла.

X

j, r: -n+1 r < i+1 and 1 j

j j

max: (max A[k-1, r+k-1] or max A[k-1, r+k-1])

k=1 k=1-r

j j

and (max = A[k-1, r'+k-1] or max = A[k-1, r'+k-1]) (*)

k=1 k=1-r

При первом попадании в точку Х утверждение (*) выполняется, так как max = A[n-1,0]

j = n, i = 1-n, r = 1-n, k = 1-r = n

max = A[n-1,1-n+n-1]

-n+1 1-n

Пусти при p — попадании в точку Х утверждение (*) выполняется. Докажем, что утверждение (*) выполняется при p+1 — попадании в точку Х.

Для p:

j, r: -n+1 r < i+1 and 1 j

j j

max: (max A[k-1, r+k-1] or max A[k-1, r+k-1])

k=1 k=1-r

j j

and (max = A[k-1, r'+k-1] or max = A[k-1, r'+k-1]) (*)

k=1 k=1-r

r = -n+p+1.

Чтобы попасть в точку Х необходимо, чтобы выполнилось условие i < m и внутренние вычисления. На выходе внутреннего цикла имеем:

j j

sum = A[k-1, r+k-1] or sum = A[k-1, r+k-1], где r = -n+p

k=1 k=1-r

Если max, полученный на предыдущих шагах < sum, то max':= sum. Если max > sum, то max остается прежним, вычисленным на предыдущих шагах.

Таким образом, либо r'= -n+p, либо r'- остается прежним. При обоих вариантах выполняется условие (*).

Докажем, что программа закончится.

Так как в каждым шагом значение i увеличивается, а n и mконечны и не меняются, то через некоторое время не выполнится условие i < m и цикл завершится.

Анализ сетей Петри на основе дерева достижимости.

Сеть Петри

P₁

a

P₂

b.true

P₃

c b. false

P₄

P₁₂

d.true d. false o

P₅ P₆ P₁₃

e f

P₇

g.true g. false

P₈ P₉

k l. true l. false

P₁₀

m P₁₁

n

a: Fill; max:= A[n-1,0]; i:= -n+1;

b: i < n

c: sum:= 0

d: 1-i >0

e: j:= 1-i

f: j:=1

g: i+j m and j n

k: sum:= sum +A[j-1,i+j-1]; j:=j+1

l: max < sum

m: max:=sum

n: i:= i+1

o: write (max)

Дерево достижимости.

(1,0,0,0,0,0,0,0,0,0,0,0,0)

(0,1,0,0,0,0,0,0,0,0,0,0,0)

(0,0,1,0,0,0,0,0,0,0,0,0,0) (0,0,0,0,0,0,0,0,0,0,0,1,0)

(0,0,0,1,0,0,0,0,0,0,0,0,0) (0,0,0,0,0,0,0,0,0,0,0,0,1)

(0,0,0,0,1,0,0,0,0,0,0,0,0) (0,0,0,0,0,1,0,0,0,0,0,0,0)

(0,0,0,0,0,0,1,0,0,0,0,0,0) (0,0,0,0,0,0,1,0,0,0,0,0,0)

(0,0,0,0,0,0,0,1,0,0,0,0,0) (0,0,0,0,0,0,0,0,1,0,0,0,0) (0,0,0,0,0,0,0,1,0,0,0,0,0) (0,0,0,0,0,0,0,0,1,0,0,0,0)

(0,0,0,0,0,0,1,0,0,0,0,0,0) (0,0,0,0,0,0,1,0,0,0,0,0,0)

(0,0,0,0,0,0,0,0,0,1,0,0,0) (0,0,0,0,0,0,0,0,0,0,1,0,0) (0,0,0,0,0,0,0,0,0,1,0,0,0) (0,0,0,0,0,0,0,0,0,0,1,0,0)

(0,0,0,0,0,0,0,0,0,0,1,0,0) (0,1,0,0,0,0,0,0,0,0,0,0,0) (0,0,0,0,0,0,0,0,0,0,1,0,0) (0,1,0,0,0,0,0,0,0,0,0,0,0)

(0,1,0,0,0,0,0,0,0,0,0,0,0) (0,1,0,0,0,0,0,0,0,0,0,0,0)

Анализ безопасности и ограниченности. Сеть Петри ограниченна тогда и только тогда, когда символ отсутствует в ее дереве достижимости. На дереве достижимости, ни в одной из маркировок нет символа. Следовательно, сеть Петри является ограниченной. Так как граница для всех позиций равна 1, то построенная сеть Петри безопасна.

Анализ сохранения. Для каждой маркировки можно вычислить сумму начальной маркировки. Так как для построенной сети Петри эта сумма одинакова для каждой достижимой маркировки, то можно сделать вывод, что сеть Петри является сохраняющей.

Анализ покрываемости. Построенная сеть Петри не является покрываемой, т.к. для заданной маркировки ' нет такой достижимой маркировки в дереве достижимости, чтобы выполнялось условие: «'.

Анализ живости. Из рассмотренного дерева достижимости следует, что все переходы являются потенциально живыми, так как существует такая 'R (N,), что t разрешён в '. Но ни один не является живым, так как при = ' = <0,0,0,0,0,0,0,0,0,0,0,0,1> ни один из переходов не является потенциально живым.

Выводы по работе

В ходе выполнения курсовой работы я построил стандартную схему программы в графовой и линейной форме. Затем указал интерпретацию схемы и протокол выполнения программы. После построил инварианты циклов алгоритма и ограничения циклов. Затем доказала, что программа, решающая задачу нахождения максимума среди сумм элементов диагоналей, параллельных главной диагонали целочисленной матрицы, делает то, что необходимо и при этом заканчивает свою работу. Затем на основании стандартной схемы программы была построена сеть Петри, и на основе дерева достижимости были исследованы её свойства.

Из анализа сети Петри можно заключить, что она является:

· безопасной

· ограниченной

· сохраняемой

· каждый ее переход является потенциально живым.

1. Рабинович Е. В. Курс лекций.

2. Рабинович Е. В. Теория вычислительных процессов: Учебное пособие/ СибГУТИ.- Новосибирск, 2004. — 119стр.