使用util訂購合金使用/訂購

我想了解如何在Alloy中訂購。我有一個我用來實例化排序模塊的時間簽名。我希望謂詞addPage在時間t'添加一個頁面到書中，其中t'= t.next。（基本上在下一次添加頁面到圖書）然而，它不按預期工作，而是Time2的頁面數量少於Time1。有人可以向我解釋爲什麼會發生這種情況嗎？謝謝。使用util訂購合金使用/訂購

open util/ordering[Page] as P0 
open util/ordering[Time] as T0 


sig Page {} 


sig Time {} 


sig Book 
{ 
    pages: Page -> Time 
} 


pred addPage(b:Book, p:Page, t: Time) 
{ 
    t != T0/last implies 
    { 
     let t' = t.next | 
      b.pages.t' = b.pages.t + p 
    } 
} 


run addPage {} for 3

來源

2017-05-24 Kevin

的問題是，在運行語句中的額外的大括號。我認爲Alloy在這種情況下執行一個空謂詞。

嘗試：

run addPage for 3

代替。您將看到一個可視化，其中標記了b，t和p的選定實例。

來源

2017-05-25 16:16:16 wmeyer

我試過這個，但它仍然沒有工作。我也更新了問題以顯示生成的實例的圖像。正如您在時間$ 2中看到的那樣，Book $ 0的頁面少了一頁。謝謝。 – Kevin

你正試圖改變只能在約束邏輯中模擬的狀態。請注意，addPage中的表達式基本上無效/沒有它的情況下運行您的模型/並且解決方案中只有一個Book原子。

下面是一個模型，您可以先着手並逐步完善。

open util/ordering[Time] 

sig Page {} 
sig Time {} 

sig Book { 
    pages : Page lone -> Time // each Time atom is mapped to at most one Page atom 
} 

pred addPage(b0, b1 : Book, pg : Page, t0, t1 : Time) { 
    one pg       and // one page at a time (it's likely redundant) 

    not pg in b0.pages.Time   and // it's a 'new' page 
    b0.pages + pg->t1 = b1.pages and // 'new state' of b0 
    t1 = t0.next      // pg is 'added' with the next time stamp 
} 

run addPage for 3 but 2 Book

我使用可選的「和」操作員，放置T1 = t0.next在約束的端部，位於b1.pages /表示「新狀態」 /右側和使用引號中的註釋強調在命令式編程工作中沒有真正的狀態變化和操作順序。

來源

2017-05-31 07:43:25

使用util訂購合金使用/訂購

回答

相關問題