3
\$\begingroup\$

As a first step into the world of Alloy, I've done my own version of the Fox/Chicken/Grain problem. I'd be grateful for any comments (also, is there a better place to do this?).

I thought it worth separating out the Farmer from the other items so I don't have to keep removing it from the set of items.

open util/ordering[Time]

sig Time {}

enum Place {Near, Far}

abstract sig Locatable { location: Place one -> Time }
abstract sig Edible extends Locatable {} 
one sig Fox, Chicken, Grain extends Edible {}
one sig Farmer extends Locatable {}

pred init(t: Time) { Locatable.location.t = Near }

pred done(t: Time) { Locatable.location.t = Far }

pred stayPut(t, t': Time, edibles: set Edible) {
    all e : edibles | e.location.t = e.location.t'
}

pred carryAcross(t, t' : Time) {
    one e: Edible {
        e.location.t = Farmer.location.t
        e.location.t' = Farmer.location.t'
        stayPut[t, t', Edible - e]
    }
}

pred crossRiver(t, t' : Time) {
    stayPut[t, t', Edible]
}

pred nextCrossing(t, t' : Time) {
    Farmer.location.t' != Farmer.location.t
    carryAcross[t, t'] or crossRiver[t, t']
}

pred eats [a, b: Edible] { a->b in Fox->Chicken + Chicken->Grain }

fact ProtectFromEating {
    all p, q: Edible, t: Time |
    p.eats[q] and p.location.t = q.location.t => q.location.t = Farmer.location.t
}

fact Traces {
    first.init
    all t: Time - last | let t' = t.next |
        done[t] or nextCrossing [t, t']
}

fact Done {
    some t: Time | done[t]
}

run {} for 8 Time
\$\endgroup\$
3
  • 1
    \$\begingroup\$ Welcome to Code Review! Could you please provide more details about the Fox/Chicken/Grain problem? if there is a description from a third party source you are using then feel free to paste the text here (provided that is allowed given licensing), as well as any sample inputs and expected outputs. \$\endgroup\$ Jul 17 '20 at 17:42
  • \$\begingroup\$ Is this really necessary? This appears to be a standard example for people in the Alloy world. I'm finding the entry costs to posting "correctly" to SE beginning to outweigh the benefits. \$\endgroup\$
    – SteveF
    Jul 20 '20 at 8:03
  • 2
    \$\begingroup\$ No it isn't necessary but might help others provide better reviews. After searching the internet I believe I learned about the F/C/G problems when I was younger. Please forgive my naivety. \$\endgroup\$ Jul 20 '20 at 21:53
0
\$\begingroup\$

I am personally not a fan of the Time pattern, it gets messy quickly. There is an extension in the works, called electrum that allows you to use variables.

Overall your solution seems too detailed. The magic of alloy is that you only have to say what you want to achieve. I.e. the animals should always be safe and and somehow they need to end up on the other side. I.e. you don't care about the crossing itself that much as long as you ensure there is never a lunch happening.

My personal favorite solution for this problem is:

open util/ordering[Crossing]
enum Object { Farmer, Chicken, Grain, Fox }

let eats = Chicken->Grain + Fox->Chicken
let safe[place] = Farmer in place or (no place.eats & place)

sig Crossing {
    near, far : set Object,
    carry :  Object
} {
    near = Object - far
    safe[near] 
    safe[far]
}
run {
    first.near = Object
    no first.far
    all c : Crossing - last, c': c.next {
        Farmer in c.near implies { 
            c'.far = c.far + c.carry + Farmer
        } else {
            c'.near = c.near + c.carry + Farmer
        }
    }
    some c : Crossing | c.far = Object
} for 8

Peter Kriens @pkriens

\$\endgroup\$
5
  • \$\begingroup\$ Thanks for this, very helpful. I particularly like the way that the table view shows the traffic so clearly. That looks like an useful design heuristic. So, “Crossing” is actually the result of a Crossing, i.e. a state, rather than a transition, which is different from the events version of the hotel example in the book. Is there any guidance on when to use the singleton approach instead? I don’t know if it matters, but this solution doesn’t have a “lock” for when the solution is complete, so on a 9th step the farmer takes the grain back. \$\endgroup\$
    – SteveF
    Jul 17 '20 at 13:56
  • \$\begingroup\$ Electrum looks cool, but for my purposes I need to stick with “stable” versions. \$\endgroup\$
    – SteveF
    Jul 17 '20 at 13:56
  • 2
    \$\begingroup\$ "From Pieter Kriens" Who is that? Could you cite properly with a link please. Also are you sure that they'll read your Thank you comment here? \$\endgroup\$ Jul 17 '20 at 14:03
  • \$\begingroup\$ Yes, it is ok to use my comments \$\endgroup\$
    – user227732
    Jul 17 '20 at 14:08
  • \$\begingroup\$ @PeterKriens Ah, nice you jumped in ;-). I suspected but wasn't sure, you are the guy who asked to add the alloy tag at CR. Welcome! \$\endgroup\$ Jul 17 '20 at 14:15
0
\$\begingroup\$

As said, the Time pattern never made me fall in love with it so I started to experiment. However, I am an outsider in this. My experience is 44 years of software design but I am more or less an autodidact, not been to university. Big chance a lot of people are now cringing behind their email with this solution :-)

The pattern to put all variable state in a trace sig (Crossing here) seems to work very well though. One of the reasons I love it is that it is easy to add 'debug' variables that trace progress. When things don't work out as you think (which is 98% of the time) it is easy to store some more information.

I got the idea when I had been writing some models where I desperately tried to control the variables with quantifications, which usually created dead models (no instance). Like:

    all c : Crossing-last, c': c.next {
        some carry : Object {
            ...
        }
    }

I had one model and then Daniel told me to remove the unnecessary quantifications. At first I had no idea what he was talking about and then it hit me that the complete state space is reachable the trace signature. So you do not need quantifications, the state space is out there, you only need to constrain it to only visit the states you want it to visit. That was a HUGE insight for me, things really fell in place then. Now it seems so rather obvious :-(

With this approach, you design a sig that contains all the state variables and then have predicates that let it transition to the next state properly. (In this case, the single transition predicate is expanded in the trace predicate for conciseness.) This is usually quite straightforward and maps well to an implementation. The transition predicates are then the events, which also maps well to implementations where events are usually methods.

The disadvantage is that it does not provide very nice graphs, all data is mixed up in one sig. This was one of the reasons I added the table view. And I expect it is the reason a lot of people don't like it, a lot of Alloy users put a lot of weight on good looking visualizations :-) I like it but find that most of the problems I use Alloy with are not that suitable for nice visualizations.

I don’t know if it matters, but this solution doesn’t have a “lock” for when the solution is complete, so on a 9th step the farmer takes the grain back.

I did't care but it should be a nice simple exercise for the reader to lock it on the far side. :-) You could also lock the last Crossing to be the solution. Just replace:

some c : Crossing | c.far = Object

with:

last.far = Object

Is there any guidance on when to use the singleton approach instead?

Well, I would not call it a singleton approach but further I am also still struggling to find the best patterns. It is a testimony to Alloy that there are so many good ways to do something, it really is an incredible environment that deserves a lot more attention.

Peter Kriens @pkriens

\$\endgroup\$
2
  • 1
    \$\begingroup\$ If this review was actually done by @PeterKriens (as well as the other one) then he should be the one to post it - that way it can be properly attributed to him (protip: he can gain more reputation that way) \$\endgroup\$ Jul 27 '20 at 17:07
  • 2
    \$\begingroup\$ @SᴀᴍOnᴇᴌᴀ I agree with this. These are solid answers and I only want to upvote the person who wrote them. \$\endgroup\$
    – Peilonrayz
    Jul 27 '20 at 17:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.