Моделирование случайных сбоев в связном графе в Alloy

Можно ли моделировать случайные сбои в Alloy?

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

open util/ordering[Time]

enum Datum{Off, On} // A simple representation of the state of each node

sig Time{state:Node->one Datum} // at each time we have a network state

abstract sig Node{
  neighbours:set Node 
}
fact { 
  neighbours = ~neighbours   -- symmetric
  no iden & neighbours          -- no loops
  all n : Node | Node in n.*neighbours -- connected
  --  all n : Node | (Node - n) in n.neighbours -- comp. connected
}
fact start{// At the start exactly one node has the datum
  one n:Node|first.state[n]=On
}

fact simple_change{ // in one time step all neighbours of On nodes become on
  all t:Time-last |
    let t_on = t.state.On |
    next[t].state.On = t_on+t_on.neighbours
}

run {} for 5 Time, 10 Node

Программное обеспечение, которое я пытаюсь смоделировать, имеет дело с неопределенностью. По сути, связь между узлами может выйти из строя, и программное обеспечение перенаправит маршрут по другому пути. Что я хотел бы попробовать сделать в Alloy, так это иметь возможность для ссылок «умирать» в определенные моменты времени (желательно случайным образом). В самом верхнем факте у меня есть возможность сделать граф полностью связанным, поэтому возможно, что, если связь прервется, другая может восполнить слабину (поскольку simple_change переключает состояние Datum на On для все подключенные соседи).

Изменить:

Итак, я сделал, как было предложено, и столкнулся со следующей ошибкой:Ошибка типа
Я запутался, так как Я думал, что соседи и Node все еще были наборами?

Вот мой обновленный код:

open util/ordering[Time]
open util/relation

enum Datum{Off, On} // A simple representation of the state of each node

sig Time{
  neighbours : Node->Node,
  state:Node->one Datum         // at each time we have a network state
}{
  symmetric[neighbours, Node]
}
abstract sig Node{
  neighbours:set Node
}

fact { 
  neighbours = ~neighbours   -- symmetric
  no iden & neighbours          -- no loops
--  all n : Node | (Node - n) in n.neighbours -- comp. connected
  all n : Node | Node in n.*neighbours -- connected
}

// At the start exactly one node has the datum
fact start{
  one n:Node|first.state[n]=On
}

// in one time step all neighbours of On nodes become on
fact simple_change{ 
  all t:Time-last |
    let t_on = t.state.On |
    next[t].state.On = t_on+t_on.neighbours

  all t:Time-last | next[t].neighbours in t.neighbours
  all t:Time-last | lone t.neighbours - next[t].neighbours
}

run {} for 10 Time, 3 Node

model-checking alloy
person the_e    schedule 04.12.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Переместите определение соседей во Время:

sig Time {neighbours : Node->Node, ....}

Вам нужно будет повторно выразить факты о симметрии и т. д. соседей относительно каждой временной точки. Это проще всего сделать, выполнив это в инвариантной части тактового размера:

sig Time {
  neighbours : Node->Node,
  ...
}{
  symmetric[neighbours, Node],
  ....
}

(Я рекомендую использовать open util/relation для загрузки полезных определений, таких как symmetric.)

Тогда временной шаг simple_change можно усложнить, добавив такой факт, как

next[t].neighbours in t.neighbours

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

Если вы хотите ограничить количество дуг, отбрасываемых на каждом шаге, вы можете добавить дополнительный факт, такой как

lone t.neighbours - next[t].neighbours

что ограничивает удаление не более чем одной дугой.

person user1513683    schedule 05.12.2012
comment
Когда вы объясняете это так... это имеет гораздо больше смысла, чем то, что я пытался сделать. Спасибо! - person the_e; 05.12.2012
comment
Один вопрос: когда я добавляю symmetric[neighbours,Node] в свое время (как вы предложили), я получаю сообщение об ошибке: A type error has occurred: This must be a set or relation. Instead, it has the following possible type(s) {PrimitiveBoolean} - person the_e; 05.12.2012
comment
Предикат symmetric принимает только один аргумент, поэтому symmetric[neighbours, Node] не может быть допустимым вызовом. Если вы просто измените его на symmetric[neighbours], все будет в порядке. Кроме того, вы должны удалить поле neighbours в сигнале Node, если вместо этого вы решили ввести отношение neighbours в сигнале Time. Вам также следует удалить факт о симметрии, если вы собираетесь использовать предикат symmetric из модуля relations. Наконец, в факте simple_change вам придется изменить t_on.neighbours на t.neighbours[t_on], чтобы проверить тип. - person Aleksandar Milicevic; 09.12.2012
comment
Спасибо за отзыв @AleksandarMilicevic. Еще один вопрос, тогда я должен быть хорошим ... это нарушает мой факт «подключения»: all n : Node | Node in n.*neighbors Есть ли способ восстановить эту функциональность? - person the_e; 11.12.2012
comment
В добавленном факте для знака Time вместо symmetric[neighbours] вы можете написать neighbours = Node -> Node - iden, что дает вам как «симметричное», так и «подключенное» свойство (это то, что я первоначально предложил в одном из предыдущих потоков) - person Aleksandar Milicevic; 12.12.2012