Beginner Alloy Questions

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

Add the following constraints to cafe.als:

• You can get from any cafe to any other cafe by car (though there may not be a direct route).
• Walking paths between cafes are bidirectional.
• Every cafe is directly reachable from every other cafe in one or two steps.
• The bus visits every cafe, in a single nonbranching route. (Note: you will probably want to slightly change the declaration of the bus relation for this.)

I've never worked with Alloy and my professer has barely touched on it. I'm really lost, could anyone help explain what's going on or help me with any of the problems?

Answer 1

I have numbered each of the points in the questions. You can copy the code and paste it anywhere. Don't forget to change the declaration of the "bus" relation as mentioned in point 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 
}