初心者合金は

Question

module cafeMap 
-- Hipsters spend their days traveling from one cafe to another. 
-- They use various means of transportation: by car, by bus, and by foot. 

sig Cafe { 
    walk: set Cafe, -- there is a walking path between cafes 
    car: set Cafe, -- there is a street between cafes 
    bus: set Cafe -- there is a direct bus route between cafes 
} 

-- All Cafe pairs with a direct travel link (walk, car or bus) 
fun travel[]: Cafe->Cafe { 
    car+walk+bus 
} 

-- All Cafe pairs with direct "green" travel links (walk or bus) 
fun greentravel[]: Cafe->Cafe { 
    walk+bus 
} 

-- Does relation r contain every possible pair of Cafes? 
pred complete[r: Cafe->Cafe] { 
    --your code goes here 
} 

-- For every pair (c,d) in r, is the reverse pair (d,c) also in r? 
pred symmetric[r: Cafe->Cafe] { 
    r=~r 
} 

-- Does r contain no pairs of the form (c,c)? 
pred irreflexive[r: Cafe->Cafe] { 
    no r & iden -- Is the intersection of r and the identity relation empty? 
} 

fact { 
    irreflexive[walk+car+bus] -- eliminate "self loops" 
} 

fact { 
symmetric[walk] 
} 

pred show {} 

run show for exactly 5 Cafe 

がcafe.alsに次の制約を追加します。質問：

• （ 直接ルートがないかもしれないが）あなたが車で、他のカフェに任意のカフェから取得することができます。
• カフェ間の歩行経路は双方向です。
• すべてのカフェは、1つまたは2つのステップで直接または他のすべてのカフェからアクセスできます。
• バスは、単一の非分岐ルートで各カフェを訪れます。 （注： おそらく少しこのためバス 関係の宣言を変更したくなるでしょう。）

私は合金で働いたことがありませんし、私のprofesserはやっとそれに触れています。私は本当に失われている、誰が何が起こっているか説明するのに役立つか、問題のいずれかで私を助けることができる？

Answer 1

質問の各点に番号を付けました。コードをコピーしてどこにでも貼り付けることができます。ポイント4で述べた "バス"関係の宣言を変更することを忘れないでください。

fact Solution{ 
    -- POINT 1 -- 
    //You can get from any cafe to any other cafe by car (though there may not be a direct route). 
    all c1, c2: Cafe | c2 in c1.^car 


    -- POINT 2 -- 
    // Walking paths between cafes are bidirectional. 
    symmetric[walk] 


    -- POINT 3 -- 
    // Every cafe is directly reachable from every other cafe in one or two steps. 
    // Either there is a direct route from one cafe (s) to another (e) or there is a middle cafe (m) 
    all disj s, e: Cafe | let route = walk+car+bus | 
     s->e in route or some m:Cafe | (s->m + m->e) in route 


    -- POINT 4 -- 
    // The bus visits every cafe, in a single nonbranching route. 
    //nonbranching means that every cafe has at most one image over the mapping "bus". Change "bus: set Cafe" to "bus: lone Cafe" 

    // The bus route can be circular like this 
    all disj c1, c2: Cafe | c2 in c1.^bus 

    // OR it can be linear like this. It starts with the head from which all other cafes are reachable and no loops exist. 
    //one head: Cafe | all c: Cafe - head | c in head.^bus and not c in c.^bus 
}