爲什麼NoRoomConflicts生成二元關係，而NoRoomConflicts_alt「起作用」

請考慮下面的Alloy模型，這是一個剝離的學生提交的本質版本。這個問題是一個排課系統，學生想說沒有衝突（在同一時間在同一個地方的兩個不同的課程會）：爲什麼NoRoomConflicts生成二元關係，而NoRoomConflicts_alt「起作用」

abstract sig Room{} 
one sig S20, S30, S50 extends Room{} 

abstract sig Period{} 
one sig Mon, Tue, Wed, Thu, Fri extends Period{} 

// Courses and the room and periods when they meet. 
some sig Course { 
    where : Room, 
    when : some Period 
} 

// No two Courses with any common meeting Periods can be 
// in the same Room - from the student. 
pred NoRoomConflicts_student { 
    no c : Course | no d : Course | 
    c != d && some c.when & d.when && d.where = c.where 
} 
run NoRoomConflicts_student 

// No two Courses with any common meeting Periods can be 
// in the same Room - my recasting. 
pred NoRoomConflicts_alt { 
    no c : Course, d : Course | 
    c != d && some c.when & d.when && d.where = c.where 
} 
run NoRoomConflicts_alt

當NoRoomConflicts_alt運行，我們得到符合的解決方案到規範。

但是，當NoRoomConflicts_student運行時，突然間「d」成爲課程之間的二元關係，解決方案顯示衝突。（a）爲什麼用這種方式轉換「d」？（b）給定（a），不應該c！= d引發一個類型錯誤？

注意：我沒有聲稱這兩個謂詞是等價的（我的頭疼會試圖做雙重否定） - 我只是想知道在運行NoRoomConflicts時「d」如何突然變爲二元關係。

版本：合金分析儀4.2_2015-02-22（生產日期：2015年2月22日18:21 EST）

來源

2017-02-23 mjl48

首先，你在溶液看到的是，某些量化的變量（d在這種情況下）得到skelmized，以便您可以看到他們的價值觀。如果你正在解決表單的一個約束（all x | some y | ...），那麼y的skolemized值必須是一個關係 - 給每個x賦予一個y值。這不是Alloy變量的實際類型，這就是沒有類型錯誤的原因。有關完整說明，請參見我的書（Software Abstractions）的第5.2.2節。

二，兩個公式不一樣。這在我的書的第293頁有解釋。總之，這是因爲「no c，d | P」意味着你找不到ac和d這樣的P，而「no c | no d | P」表示你找不到ac，因此你找不到廣告使得P.

來源

2017-02-26 19:49:36

謝謝。我意識到這兩個陳述並不相同，但我真的對你說的是因爲skelm化的問題感興趣。因爲事實的寫法：（no c | no d | ...）我沒有看到底層的通用/存在主張。我想我應該更好地閱讀你從書中提到的部分。 – mjl48

爲什麼NoRoomConflicts生成二元關係，而NoRoomConflicts_alt「起作用」

回答

相關問題