使用合金4.2的拓撲排序

Question

我試圖使用拓撲排序來找到遵循它們的先決條件的兩個不同的順序計劃。當我執行代碼時，沒有找到實例，我不知道爲什麼。這裏是我的代碼：

open util/relation 

abstract sig Course { 
    prereq: set Course, -- c->d in prereq if c is a prerequisite of d 
    s1, s2: set Course  -- two sequential course schedules 
} 
one sig cs1121, cs1122, cs1141, cs2311, cs2321, 
       cs3000, cs3141, cs3311, cs3331, cs3411, cs3421, cs3425 extends Course { } 

fact { 
    no prereq.cs1121 
    prereq.cs1122 = cs1121 
    prereq.cs1141 = cs1122 
    prereq.cs2311 = cs1121 
    prereq.cs2321 = cs1122 
    prereq.cs3000 = cs3141 
    prereq.cs3141 = cs2311 
    prereq.cs3141 = cs2321 
    prereq.cs3311 = cs2311 
    prereq.cs3331 = cs1141 
    prereq.cs3331 = cs2311 
    prereq.cs3331 = cs2321 
    prereq.cs3411 = cs1141 
    prereq.cs3411 = cs3421 
    prereq.cs3421 = cs1122 
    prereq.cs3425 = cs2311 
    prereq.cs3425 = cs2321 
} 

-- is the given schedule a topological sort of the prereq relation? 
pred topoSort [schedule: Course->Course] { 
    (all c: Course | lone c.schedule and lone schedule.c) -- no branching in the schedule 
    and totalOrder[*schedule, Course] -- and it's a total order 
    and prereq in ^schedule -- and it obeys the prerequisite graph 
} 


pred show { 
    s1.irreflexive and s2.irreflexive -- no retaking courses! 
    s1.topoSort and s2.topoSort -- both schedules are topological sorts of the prereq relation 
    s1 != s2 -- the schedules are different 
} 

run show 

Answer 1

將解算器（在Options菜單下）切換到MiniSAT和Unsat Core，然後看看核心。你會看到它的亮點

prereq.cs3141 = cs2311 
prereq.cs3141 = cs2321 

它違揹你的無分支規則。