합금의 연결된 그래프에서 임의의 불량 모델링

Question

합금의 무작위 실패를 모델링 할 수 있습니까?

예를 들어, 나는 현재 여러 시간 단계에서 데이터를 이웃에 전달하는 연결된 그래프를 가지고 있습니다. 내가하려고하는 것은 모델이 무작위로 링크를 죽일 수있게하는 몇 가지 방법을 찾아내는 것입니다. 그렇게하면 모든 노드의 데이터 상태가 On으로 설정되도록하는 목표를 달성 할 수 있습니다.

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 

불확실성을 모델로 삼고있는 소프트웨어입니다. 기본적으로 노드 간 링크가 실패 할 수 있으며 소프트웨어가 다른 경로를 따라 재 라우팅됩니다. 제가 합금에서 시도하고자하는 것은 특정 타임 스텝에서 (바람직하게는 무작위로) '죽어 버리는'링크를위한 시설을 갖는 것입니다. 가장 중요한 사실은, 나는 그래프가 완전히 연결될 수있는 능력을 가지고 있기 때문에, 만약 링크가 죽으면 다른 링크가 느슨해 질 수 있다는 것이다. (simple_change는 Datum의 상태를 On으로 전환하기 때문에 모든 연결된 이웃).

---

편집 : 그래서

, 내가 제안하고 다음과 같은 오류로 실행되면서했다 : 나는 이웃을 생각으로,
내가 혼란 스러워요 및 노드가 아직 설정했다? 여기

내 업데이트 된 코드입니다 :

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 

Answer 1

이동은 시간에 이웃의 정의 :

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

당신이 필요 각 시간을 기준으로 이웃의 대칭 등에 대한 사실을 다시 표현 포인트. 이것은 가장 쉽게 박자의 불변 부분을 수행하여 수행됩니다

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

(I는 symmetric 유용 정의를로드 할 open util/relation의 사용을 권장하지.)

그런 다음 시간 단계 simple_change 같은 거리에 임의의 많은 호를 던질 수

next[t].neighbours in t.neighbours 

같은 사실에 추가하여 복잡 할 수 있습니다.

당신이 최대 하나의 아크에에 처분을 제한하는 더 사실 같은

lone t.neighbours - next[t].neighbours 

을 추가 할 수 있습니다 멀리 각 단계에서 발생 얼마나 많은 호 제한하려면

.