Тестирование софта - статьи

ce076b8f

Графы с уточняемыми вершинами


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

Определение. Ориентированным графом или просто графом G называется совокупность трех объектов (GV, GX, GE): GV - множество вершин, GX - множество раскрасок, GE

и являются полными, то есть в них для любой не полностью определенной вершины существует хотя бы одна уточняющая ее полностью определенная вершина.

Определение. Подграф G' = (GV', GX', GE') графа с уточняемыми вершинами G = (GV, GX, GE) называется полностью определенным, если все его вершины полностью определены, то есть GV'

GVc.

Определение.
Подграф G' = (GV', GX', GE') графа с уточняемыми вершинами G = (GV, GX, GE) называется его информационной проекцией, если:

  • вершины из GV' попарно несравнимы в отношении
    и содержащий все дуги максимального полностью определенного подграфа G. Определение.


    Строго уточняющий маршрут {(vi, xi, vi+1)}i=0,n-1 в графе с уточняемыми вершинами G называется простым, если никакой его префикс {(vi, xi, vi+1)}i=0,m-1, где m < n, не является строго уточняющим маршрутом. Рассмотрим уточняющий маршрут P = {(vi, xi, vi+1)}i=0,n-1 в графе с уточняемыми вершинами G, начинающийся с неопределенной вершины: v0 =
    . Его можно представить в виде конкатенации: P = P0 … PN-1 PN (Pj={(vi, xi, vi+1)}i=kj,kj+1-1, 0 = k0 < … < kN+1 = n), в которой маршруты Pj для 0 ≤ j < N являются строго уточняющими, а маршрут PN является уточняющим, но не является строго уточняющим маршрутом, то есть различные вершины маршрута PN несравнимы в отношении уточнения. Определение. Пусть GVj={vkj,…,vkj+1-1}, где 0 ≤ j < N, - все вершины маршрута Pj кроме последней, GVN={skN,…,skN+1} - все вершины маршрута PN. Множество вершин GVj, где 0 ≤ j ≤ N, будем называть уровнем неопределенности j уточняющего маршрута P. При этом для j < N будем говорить, что маршрут Pj уточняет вершины с уровня неопределенности j до уровеня неопределенности j+1. Заметим, что различные вершины одного уровня неопределенности несравнимы в отношении уточнения, поэтому они являются подмножеством множества вершин некоторой информационной проекции. Рассмотрим следующий рисунок. Сплошные стрелки изображают обычные дуги графа; жирные стрелки изображают дуги внутри одного уровня неопределенности; стрелки, изображенные пунктиром, связывают уточняющие вершины с уточняемыми. Горизонтальные линии разделяют уровни неопределенности, которых на рисунке три.
    Рисунок 5.Уточняющий обход графа с уточняемыми вершинами. Заметим, что уровни неопределенности могут пересекаться. Пример. Рассмотрим граф с множеством вершин {true, false,
    }× {true, false,
    }, каждая пара из которых соединена дугой. Маршрут P={(
    ,
    ), (false,
    ), (true,
    ), (false, false), (true,
    )}, очевидно, является уточняющим. Ему соответствуют три уровня неопределенности:
    • GV0 = {(
      ,
      )};
    • GV1 = {(false,
      ), (true,
      )};
    • GV2 = {(false, false), (true,
      )}.
    Видно, что уровни неопределенности GV1 и GV2 уточняющего маршрута P имеют общую вершину (true,
    ).

    Содержание раздела