1 
    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つのステップで直接アクセスできます。
  • バスは、単一の非分岐ルートですべてのカフェを訪れます。（注：このためのバス関係の宣言を少し変更することをお勧めします。）

私はAlloyを使ったことがなく、教授はほとんど触れていません。私は本当に迷っています、誰かが何が起こっているのかを説明したり、問題のいずれかで私を助けてくれますか？

4

1 に答える 1

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 
}
于 2012-07-25T19:23:00.417 に答える