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：

  • 您可以从任何一家咖啡馆开车到任何其他咖啡馆（尽管可能没有直达路线）。
  • 咖啡馆之间的步行道是双向的。
  • 每家咖啡馆都可以从其他咖啡馆直接到达，只需一两步。
  • 公共汽车在一条非分支路线上访问每家咖啡馆。（注意：您可能希望为此稍微更改总线关系的声明。）

我从未与 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 回答