Заполнение набора с течением времени в Alloy в полностью подключенной сети

Дополнение от этот вопрос...

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

Я моделирую систему, задача которой состоит в том, чтобы каждый узел имел копию данных, которые были вставлены в систему. У меня в голове есть процедура, как это сделать, однако я изо всех сил пытаюсь перевести это в терминологию Alloy.

Типичный алгоритм будет выглядеть примерно так:

For i = 0 to TIME_STEPS:
  For each node in {nodes}:
    Check all other nodes and, if necessary, provide a copy of the data 
    if they do not currently have it

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

Вот где я сейчас:

open util/ordering[Time] as TO
module rdm4

----- signatures
sig Time {}

sig DataMirror {
  link: set DataMirror,
  toSend: DataMirror -> Time
}

----- facts

// model network of completely connected data mirrors
fact completely_connected {
      link = ~link          -- symmetrical
      no iden & link     -- no loops
      all n : DataMirror | (DataMirror - n) in n.link -- completely connected
}

// can't send to self
--fact no_self_send {
--  no d: DataMirror | d.toSend = d.link.toSend
--}

------ predicates
pred init [t: Time] {
  all p: DataMirror | p.toSend.t = p
}

pred show() { }
run show for exactly 5 DataMirror, 20 Time

Из моего предиката выполнения вы можете видеть, что я хотел бы, чтобы все сообщения были отправлены в пределах 20 временных шагов, поэтому каждый DataMirror должен иметь набор данных, состоящий из 5 уникальных сообщений к этому времени.

Я почти уверен, что хочу, чтобы у каждого DataMirror было 2 свойства:

  • Уникальное сообщение для отправки (на данный момент может быть просто переменной)
  • Набор полученных сообщений (включая исходное сообщение)

Система будет удовлетворена, если все DataMirrors будут иметь одинаковый набор сообщений.

Например, если у нас есть:

DataMirror1.starting_data = 'a'
DataMirror2.starting_data = 'b'
DataMirror3.starting_data = 'c'
DataMirror4.starting_data = 'd'
DataMirror5.starting_data = 'e'

то система будет выполнена, когда:

DataMirror1.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror2.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror3.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror4.data_set = {'a', 'b', 'c', 'd', 'e'}
DataMirror5.data_set = {'a', 'b', 'c', 'd', 'e'}

Заранее извиняюсь за то, что заставил продвинутых пользователей с формальной логикой съежиться... Я пытаюсь научиться этому на огневом рубеже :).


formal-methods model-checking alloy
person the_e    schedule 30.11.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

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

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

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
}{
all n : neighbours| this in n.@neighbours} // symmetric

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 9 Time, 4 Node
person user1513683    schedule 30.11.2012
comment
«Низкий уровень», вероятно, связан с тем, что я не знаком с такого рода моделированием. Спасибо за ваш ответ ... Я попробую. - person the_e; 30.11.2012
comment
Я бы не стал использовать добавленный факт для знака Node, а затем понимать и иметь дело с неявной функцией this и вещью @, чтобы подавить неявную this, поскольку это делает вашу модель намного менее понятной. Я думаю, что в целом гораздо лучше просто написать neighbours = ~neighbours вместо этого, что также должно быть легче понять для большинства пользователей Alloy. - person Aleksandar Milicevic; 30.11.2012
comment
Итак, играя с этим ответом ... я думаю, что это именно то, что я искал. Кратко и помогло мне понять мою проблему еще лучше. Большое спасибо! Кроме того, @AleksandarMilicevic: я согласен, мне больше нравится эта запись из-за факта симметрии. - person the_e; 01.12.2012
comment
Спасибо за замечания. Я склонен согласиться с более простым neighbours=~neighbours, но еще лучше открыть util/relation и объявить symmetric[neighbours] фактом. - person user1513683; 01.12.2012