我試圖重現Dijkstra在標題爲「合作順序進程」的論文中編寫的ALGOL 60代碼，該代碼是第一次嘗試解決互斥問題，這裏是語法： begin integer turn; turn:= 1;
parbegin
process 1: begin Ll: if turn = 2 then goto Ll;
critical section 1;
我試圖讓我的腳溼潤合金（也是相對較新的形式邏輯以及），我試圖從一個完全連接的節點圖開始。 sig Node {
adj : set Node
}
fact {
adj = ~adj -- symmetrical
no iden & adj -- no loops
all n : Node | Node in n.*adj -- connected
跟進從this question ... 我有一個完全連通圖，這是偉大的。我也加入了時間概念。我現在正在圍繞我的圖傳遞數據的概念而掙扎。 我正在對一個系統進行建模，該系統的任務是確保每個節點都有一份已插入系統的數據副本。我已經掌握瞭如何做到這一點的程序，但是我正在努力將它翻譯成Alloy術語。 一個典型的算法將是這個樣子： For i = 0 to TIME_STEPS:
For eac
是否可以在Alloy中對隨機失效建模？ 例如，我目前有一個連接圖，它將數據以不同的時間步傳遞給其鄰居。我想要做的是找出允許模型隨機殺掉鏈接的方法，並且這樣做仍然能夠實現其目標（確保所有節點的數據狀態都設置爲開）。 open util/ordering[Time]
enum Datum{Off, On} // A simple representation of the state of eac