OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 17 Август, 2018 12:11

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 26 ]  На страницу 1, 2  След.
Автор Сообщение
СообщениеДобавлено: Среда, 28 Март, 2018 12:35 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Слово недетерминированный можно было не писать, так как цикл Дейкстры, который ввел Дейкстра, он по определению недетерминированный. В языке Оберон-07 есть цикл Дейкстры, но он детерминированный, то есть он не совсем цикл Дейкстры. Ну ладно, вопрос в том, как реализовать настояций цикл Дейкстры на Оберон-07.
Я реализовал один вариант (вы его можете приспособить под свои нужды, если замените существующие модули Console и Random на свои):
Код:
MODULE Nondeterminate;

  IMPORT
    con := Console,
    Random;

  CONST
    MAX_NUM = 10;

  VAR
    permutation: ARRAY MAX_NUM OF INTEGER;

  PROCEDURE RandomPermutation(n: INTEGER);
  VAR
    i: INTEGER;
    j: INTEGER;
    rnd: INTEGER;
    choosen: ARRAY MAX_NUM OF BOOLEAN;
  BEGIN
    FOR i := 0 TO n - 1 DO
      choosen[j] := FALSE;
    END;
    FOR i := n TO 1 BY -1 DO
      IF i # 1 THEN       
        rnd := Random.Random() MOD i;
      ELSE
        rnd := 0;
      END;
      j := 0;
      WHILE choosen[j] OR (rnd # 0) DO
        IF ~choosen[j] THEN
          rnd := rnd - 1;
        END;
        j := j + 1;
      END;
      choosen[j] := TRUE;
      permutation[n - i] := j;
    END;
  END RandomPermutation;

  PROCEDURE PrintPermutation(n: INTEGER);
  VAR
    i: INTEGER;
  BEGIN
    FOR i := 0 TO n - 1 DO
      con.Int(permutation[i]); con.Str(" ");
    END;
    con.Ln;
  END PrintPermutation;

  PROCEDURE Test1(n: INTEGER);
  BEGIN
    WHILE n MOD 2 = 0 DO
      con.Int(2); con.Str(" ");
      n := n DIV 2;
    ELSIF n MOD 3 = 0 DO
      con.Int(3); con.Str(" ");
      n := n DIV 3;
    ELSIF n MOD 5 = 0 DO
      con.Int(5); con.Str(" ");
      n := n DIV 5;
    END;
    con.Ln;
  END Test1; 
 
  PROCEDURE Test2(n: INTEGER);
  VAR
    step: INTEGER;
    continue: BOOLEAN;
  BEGIN
    continue := TRUE;
    WHILE continue DO
      RandomPermutation(3);
      continue := FALSE;
      step := 0;
      WHILE (step < 3) & ~continue DO
        continue := TRUE;
        IF (permutation[step] = 0) & (n MOD 2 = 0) THEN
          con.Int(2); con.Str(" ");
          n := n DIV 2;
        ELSIF (permutation[step] = 1) & (n MOD 3 = 0) THEN
          con.Int(3); con.Str(" ");
          n := n DIV 3;
        ELSIF (permutation[step] = 2) & (n MOD 5 = 0) THEN
          con.Int(5); con.Str(" ");
          n := n DIV 5;
        ELSE
          continue := FALSE;
          step := step + 1;
        END;
      END;
    END;
    con.Ln;
  END Test2;

BEGIN
  Random.Randomize();
  Test1(466560000);
  Test2(466560000);
END Nondeterminate.

Test1 раскладывает число на множители 2, 3 и 5, используя встроенный цикл Дейкстры, и в результате получается: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 3 3 5 5 5 5.
Test2 эмулирует недетерминированный цикл Дейкстры и в результате получается примерно такая последовательность: 3 2 3 2 2 5 3 5 3 3 5 5 2 2 3 2 2 2 2 2.

Может быть у кого-то будут идеи как можно лучше эмулировать недетерминированность.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 28 Март, 2018 15:14 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 680
Откуда: Киев
Было бы зачем

Код:
  Branches = RECORD
    b: ARRAY MAX_NUM OF INTEGER;
    i, j: INTEGER
  END;
 
  PROCEDURE Init(VAR b: Branches);
  BEGIN
    b.i := 0;
    b.j := 0
  END Init;
 
  PROCEDURE Put(VAR b: Branches; case: INTEGER; cond: BOOLEAN): INTEGER;
  BEGIN
    ASSERT(case = b.j);
    IF cond THEN
      b.b[b.i] := case;
      INC(b.i)
    END;
    INC(b.j);
    RETURN ORD(cond)
  END Put;
 
  PROCEDURE Rand(VAR b: Branches): INTEGER;
  VAR i: INTEGER;
  BEGIN
    i := Random.Random() MOD b.i;
    Init(b);
    RETURN i
  END Rand;
 
  PROCEDURE Test3(n: INTEGER);
  VAR branches: Branches;
  BEGIN
    Init(b);
   
    WHILE Put(branches, 0, n MOD 2 = 0)
        + Put(branches, 1, n MOD 3 = 0)
        + Put(branches, 2, n MOD 5 = 0) > 0
    DO
      CASE Rand(branches) OF
        0:
        con.Int(2); con.Str(" ");
        n := n DIV 2
      | 1:
        con.Int(3); con.Str(" ");
        n := n DIV 3
      | 2:
        con.Int(5); con.Str(" ");
        n := n DIV 5
      END
    END;
    con.Ln;
  END Test3;


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 28 Март, 2018 16:39 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Как я понял, идея вашего решения в том, чтобы сначала проверить все условия, а потом случайно выбрать одно из условий, которое выполняется.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 28 Март, 2018 17:04 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 680
Откуда: Киев
Да. Тогда легко добиться равновероятности вызова допустимых веток и минимизировать мусорные действия.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 28 Март, 2018 23:25 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1086
Недетерменированный не значит вероятностный.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 29 Март, 2018 13:51 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 7834
Откуда: Троицк, Москва
Речь, наверное, о стохастичности.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 29 Март, 2018 20:45 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1086
Дело в том, что случайный (в любом смысле) выбор ничем не лучше любого другого. Ситуация в некотором смысле обратная той, что в недетерминированной машине Тьюринга. Тел демон выбирает наилучший вариант, а здесь мы должны быть готовы к тому, что он будет пакостить.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 29 Март, 2018 22:36 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 7834
Откуда: Троицк, Москва
Построив немало циклов Дейкстры для конкретных задач, могу уверенно посоветовать, что смысл слов про "недетерминированность" в том, чтобы помочь строить правильный цикл -- лепишь ветки по мере того, как частные случаи приходят в голову, пока не закроется предусловие.

Искусственно вводить стохастичный выбор ветки может быть полезно для тестирования -- но суть дела в способствовании мыслительному процессу ДО тестирования.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 03 Апрель, 2018 18:10 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Trurl писал(а):
Дело в том, что случайный (в любом смысле) выбор ничем не лучше любого другого. Ситуация в некотором смысле обратная той, что в недетерминированной машине Тьюринга. Тел демон выбирает наилучший вариант, а здесь мы должны быть готовы к тому, что он будет пакостить.

Да, есть такая вероятность, что при случайном выборе какой-то вариант никогда не будет выбираться.
Есть такое понятие fairness (не знаю, как лучше перевести, как честность?). В книге Verification of sequential and concurrent programs говорится:
Цитата:
Fisher and Paterson [1983] have shown that any fair scheduler that is applicable for arbitrary runs of n components needs at least n! = 1*2*...*n scheduler states.
One way of organizing such a scheduler is by keeping the components in a queue. In each check the scheduler activates that enabled component which is earliest in the queue. This component is then placed at the end of the queue.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 04 Апрель, 2018 12:07 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Вариант эмуляции недетерминированного цикла Дейкстры с очередью:
Код:
  PROCEDURE Test3(n: INTEGER);
  VAR
    queue: ARRAY 3 OF INTEGER;
    i: INTEGER;
    t: INTEGER;
    PROCEDURE Condition(cond, n: INTEGER): BOOLEAN;
    VAR
      result: BOOLEAN;
    BEGIN
      CASE cond OF
        0: result := n MOD 2 = 0;
      | 1: result := n MOD 3 = 0;
      | 2: result := n MOD 5 = 0;
      END;
      RETURN result
    END Condition;
  BEGIN
    queue[0] := 0;
    queue[1] := 1;
    queue[2] := 2;
    i := 0;
    WHILE (i < 3) & ~Condition(queue[i], n) DO
      i := i + 1;
    END;
    WHILE i < 3 DO
      CASE queue[i] OF
        0: con.Int(2); con.Str(" ");
           n := n DIV 2;
      | 1: con.Int(3); con.Str(" ");
           n := n DIV 3;
      | 2: con.Int(5); con.Str(" ");
           n := n DIV 5;
      END;
      WHILE i < 2 DO
        t := queue[i];     
        queue[i] := queue[i+1];
        queue[i+1] := t;
        i := i + 1;
      END;
      i := 0;
      WHILE (i < 3) & ~Condition(queue[i], n) DO
        i := i + 1;
      END;
    END;
  END Test3;


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 04 Апрель, 2018 14:14 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1086
Rifat писал(а):
Да, есть такая вероятность, что при случайном выборе какой-то вариант никогда не будет выбираться.

При случайном выборе эта вероятность равна нулю. Но программа должна работать и в этом случае, недерменированность - более широкое понятие.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 04 Апрель, 2018 14:56 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Trurl писал(а):
Rifat писал(а):
Да, есть такая вероятность, что при случайном выборе какой-то вариант никогда не будет выбираться.

При случайном выборе эта вероятность равна нулю. Но программа должна работать и в этом случае, недерменированность - более широкое понятие.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Май, 2018 15:33 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Еще один вариант эмуляции недетерминированного цикла Дейкстры. Он в некотором плане лучше предыдущих, так как у него спрятаны детали реализации цикла Дейкстры от непосредственно определения какого-то прикладного цикла.
Код:
MODULE Dijkstra;

  IMPORT
    Memory;

  TYPE
    Repetition* = POINTER TO RecordRepetition;
    ProcCondition* = PROCEDURE (obj: Repetition): BOOLEAN;
    ProcCommand* = PROCEDURE (obj: Repetition);
    GuardedCommand* = RECORD
      condition*: ProcCondition;
      command*: ProcCommand
    END;
    GuardedCommands = POINTER TO RECORD
      guardedCommand: GuardedCommand;
      next: GuardedCommands
    END;
    RecordRepetition* = RECORD
      head: GuardedCommands
    END;

  PROCEDURE Add*(repetition: Repetition; VAR gc: GuardedCommand);
  VAR
    node: GuardedCommands;
  BEGIN
    NEW(node);
    IF node # NIL THEN
      node.guardedCommand := gc;
      node.next := repetition.head;
      repetition.head := node;
    END;
  END Add;

  PROCEDURE Execute*(repetition: Repetition);
  VAR
    node: GuardedCommands;
    prev: GuardedCommands;
    last: GuardedCommands;
  BEGIN
    prev := NIL;
    node := repetition.head;
    (* Ищем первое условие, которое выполняется. *)
    WHILE (node # NIL) & ~node.guardedCommand.condition(repetition) DO
      prev := node;
      node := node.next;
    END;
    (* Если условие найдено, то выполняем команду. *)
    WHILE node # NIL DO
      (* Выполняем команду. *)
      node.guardedCommand.command(repetition);
      (* Переставляем команду в конец очереди.*)
      last := node;
      WHILE last.next # NIL DO
        last := last.next;
      END;
      IF node # last THEN
        IF prev # NIL THEN
          prev.next := node.next;
        ELSE
          repetition.head := node.next;
        END;
        last.next := node;
        node.next := NIL;
      END;
      prev := NIL;
      node := repetition.head;
      (* Ищем первое условие, которое выполняется. *)
      WHILE (node # NIL) & ~node.guardedCommand.condition(repetition) DO
        prev := node;
        node := node.next;
      END;
    END;
    (* Если ни одно из условий не выполняется, то цикл Дейкстры завершается. *)
  END Execute;

END Dijkstra.

Код:
MODULE Test;

  IMPORT
    Memory,
    Out,
    WinConsoleOut,
    Dijkstra;

  TYPE
    Repetition = POINTER TO RepetitionRecord;
    RepetitionRecord = RECORD (Dijkstra.RecordRepetition)
      n: INTEGER
    END;

  VAR
    writer: WinConsoleOut.Writer;

  PROCEDURE Condition1(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 2 = 0
  END Condition1;

  PROCEDURE Command1(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "2 "));
    obj(Repetition).n := obj(Repetition).n DIV 2;
  END Command1;

  PROCEDURE Condition2(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 3 = 0
  END Condition2;

  PROCEDURE Command2(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "3 "));
    obj(Repetition).n := obj(Repetition).n DIV 3;
  END Command2;

  PROCEDURE Condition3(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 5 = 0
  END Condition3;

  PROCEDURE Command3(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "5 "));
    obj(Repetition).n := obj(Repetition).n DIV 5;
  END Command3;

  PROCEDURE Test;
  VAR
    gc: Dijkstra.GuardedCommand;
    repetition: Repetition; 
  BEGIN
    NEW(repetition);
    gc.condition := Condition1;
    gc.command := Command1;
    Dijkstra.Add(repetition, gc);
    gc.condition := Condition2;
    gc.command := Command2;
    Dijkstra.Add(repetition, gc);
    gc.condition := Condition3;
    gc.command := Command3;
    Dijkstra.Add(repetition, gc);
    repetition.n := 466560000;
    Dijkstra.Execute(repetition);
  END Test;

BEGIN
  ASSERT(WinConsoleOut.Create(writer) & writer.Open(writer));
  Test;
  ASSERT(writer.Close(writer));
END Test.

Результат работы данной программы:
5 3 2 5 3 2 5 3 2 5 3 2 3 2 3 2 2 2 2 2


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Май, 2018 17:35 

Зарегистрирован: Вторник, 26 Январь, 2010 09:31
Сообщения: 468
зачем всё это?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Май, 2018 18:08 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Примерно 50 лет назад Дейкстра писал:
Цитата:
So, if you have a bright and sound idea now, you can expect it to be hailed as a novelty around the year 2025.

https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1243a.html
50 лет почти прошло )

Если серьезно, то как я уже писал:
https://forum.oberoncore.ru/viewtopic.php?f=75&t=4927&p=101088&hilit=verification#p101088
Распределенные параллельные программы, которые общаются посылкой сообщений, можно доказывать путем приведения к недетерминированному циклу Дейкстры.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 16 Май, 2018 20:35 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1537
Откуда: Беларусь, Минск
Цикл Дейкстры ничего не доказывает. И приведение к нему параллельных (и уж тем более распределённых) программ не сделает оные корректными.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 16 Май, 2018 20:36 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1537
Откуда: Беларусь, Минск
И вообще, цикл Дейкстры не про случайность выбора веток цикла, а про декларативность.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 17 Май, 2018 08:46 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Valery Solovey писал(а):
Цикл Дейкстры ничего не доказывает. И приведение к нему параллельных (и уж тем более распределённых) программ не сделает оные корректными.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 17 Май, 2018 09:00 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Valery Solovey писал(а):
И вообще, цикл Дейкстры не про случайность выбора веток цикла, а про декларативность.

Дейкстра бы с этим поспорил :)
Вложение:
10.png
10.png [ 333.72 КБ | Просмотров: 680 ]


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Июнь, 2018 10:53 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 696
Откуда: Казань
Rifat писал(а):
Код:
  PROCEDURE Condition1(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 2 = 0
  END Condition1;

  PROCEDURE Command1(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "2 "));
    obj(Repetition).n := obj(Repetition).n DIV 2;
  END Command1;

  PROCEDURE Condition2(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 3 = 0
  END Condition2;

  PROCEDURE Command2(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "3 "));
    obj(Repetition).n := obj(Repetition).n DIV 3;
  END Command2;

  PROCEDURE Condition3(obj: Dijkstra.Repetition): BOOLEAN;
  BEGIN
    RETURN obj(Repetition).n MOD 5 = 0
  END Condition3;

  PROCEDURE Command3(obj: Dijkstra.Repetition);
  BEGIN
    ASSERT(Out.Text(writer, "5 "));
    obj(Repetition).n := obj(Repetition).n DIV 5;
  END Command3;

  PROCEDURE Test;
  VAR
    gc: Dijkstra.GuardedCommand;
    repetition: Repetition; 
  BEGIN
    NEW(repetition);
    gc.condition := Condition1;
    gc.command := Command1;
    Dijkstra.Add(repetition, gc);
    gc.condition := Condition2;
    gc.command := Command2;
    Dijkstra.Add(repetition, gc);
    gc.condition := Condition3;
    gc.command := Command3;
    Dijkstra.Add(repetition, gc);
    repetition.n := 466560000;
    Dijkstra.Execute(repetition);
  END Test;



Сейчас подумал про то, что процедуры Condition1, Command1, Condition2, Command2, Condition3, Command3 было бы хорошо сделать вложенными в процедуру Test. НО, по крайней мере в компиляторе Oberon-07M нельзя брать указатель на процедуру от вложенной процедуры. Это могло бы быть оправдано, если вложенная процедура может обращаться к локальным переменным той процедуру, в которую она вложена (как должно быть в Component Pascal), тогда если взять указатель на вложенную процедуру, то может потеряться контекст, так как внешней процедуры может не существовать в момент вызова вложенной. НО, в Oberon-07 есть такое правило, что вложенная процедура может обращаться только к своим локальным переменным и к глобальным переменным, поэтому получается, что вложенная процедура ничем не отличается от не вложенной и можно спокойно брать указатель на эту вложенную процедуру.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 26 ]  На страницу 1, 2  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2018, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB