/*
 * A second attempt
 *
 */

// 0 = originalside 1 = goalside
bit farmer;
bit goat;
bit cabbage;
bit wolf;

init 
{
    farmer = 0;
    goat = 0;
    cabbage = 0;
    wolf = 0;
    
    run Solve();
}

proctype Solve()
{
    do
        // the goat does not want to be with the wolf and the cabbage will be eaten
        :: !farmer && !(!goat && (!wolf || !cabbage)) ->
            farmer = 1;
            printf("The farmer moved to the other shore\n");
        :: !goat && !farmer ->
            atomic{ 
                goat = 1;
                farmer = 1;
            }
            printf("The farmer and the goat moved to the other shore\n");
           //if the wolf or the goat is on the other shore it is safe to move the cabbage
        :: !cabbage && !farmer && (wolf || goat) ->
            atomic{
                cabbage = 1;
                farmer = 1;
            }
            printf("The farmer and the cabbage moved to the other shore\n");
        // if the goat or the cabbage is on the other shore it is safe to move the wolf
        :: !wolf && !farmer && (goat || cabbage) ->
            atomic {
                wolf = 1;
                farmer = 1;
            }
            printf("The wolf and the farmer moved to the other shore\n");
        :: farmer && !(goat && (wolf || cabbage))->
            printf("The farmer moved to the original shore\n");
            farmer = 0;
        :: goat && farmer ->
            atomic {
                goat = 0;
                farmer = 0;
            }
            printf("The farmer and the goat moved to the original shore\n");
        // if the wolf or goat is on the other shore it is safe to move the cabbage
        :: cabbage && farmer && !(!wolf || !goat) ->
            atomic {
                cabbage = 0;
                farmer = 0;
            }
            printf("The farmer and the cabbage moved to the original shore\n");
        // if the cabbage or the goat is on the other shore the wolf is safe to be moved
        :: wolf && farmer && (!goat || !cabbage) ->
            atomic {
                wolf = 0;
                farmer = 0;
            }
            printf("The wolf and the farmer moved to the orignial shore\n");
        :: farmer && wolf && cabbage && goat ->
            printf("We are done!\n"); 
            end: break; //done
    od
}

active proctype Monitor()
{
    // check that we accidently haven't violated anything
    assert(true)
}