SPIN: interpret the error trace

Question

I try to solve with spin the task about the farmer, wolf, goat and cabbage.

So, I found the folowing promela description:

#define fin (all_right_side == true)
#define wg  (g_and_w == false)
#define gc  (g_and_c == false)

ltl ltl_0 { <> fin && [] ( wg && gc ) } 

bool all_right_side, g_and_w, g_and_c;
active proctype river()
{
 bit f = 0, 
 w = 0, 
 g = 0, 
 c = 0; 

 all_right_side = false;
 g_and_w = false;
 g_and_c = false;
 printf("MSC: f %c w %c g %c c %c \n", f, w, g, c);

 do
 :: (f==1) && (f == w) && (f ==g) && (f == c) -> 
        all_right_side = true; 
        break;
 :: else ->
        if
            :: (f == w) ->
                    f =  1 - f;
                    w =  1 - w;
            :: (f == c) ->
                    f =  1 - f;
                    w =  1 - c;
            :: (f == g) ->
                    f =  1 - f;
                    w =  1 - g;
            :: (true) ->
                    f =  1 - f;
        fi;

        printf("M f %c w %c g %c c %c \n",  f, w, g, c);

        if
            :: (f != g && g == c) ->
                    g_and_c = true;
            :: (f != g && g == w) ->
                    g_and_w = true;
            ::else ->
                    skip
        fi
 od;

 printf ("MSC: OK!\n")
}

I add there an LTL-formula: ltl ltl_0 { <> fin && [] ( wg && gc ) } to verify, than the wolf wouldn't eat a goat, and the goat wouldn't eat the cabbage. I want to get an example, how the farmer can transport all his needs (w-g-c) without loss.

When I run verification, I get the following result: State-vector 20 byte, depth reached 59, errors: 1 64 states, stored 23 states, matched 87 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved)

This means that the program has generated an example for me. But I cannot interpret it. The content of *.pml.trial file is:enter image description here

Please, help me to interpret.

Answer 1

In order to "interpret" it, you could modify your source code so that each time an action is taken something intellegibile is printed on stdout.

e.g.:

            :: (f == w) ->
                    if
                       :: f == 0 -> printf("LEFT ---[farmer, wolf]--> RIGHT\n");
                       :: f == 1 -> printf("LEFT <--[farmer, wolf]--- RIGHT\n");
                       :: else -> skip;
                    fi;
                    f =  1 - f;
                    w =  1 - w;

+ something similar for the cases (f == c), (f == g) and (true).

Note: your source code already provides printf("M f %c w %c g %c c %c \n", f, w, g, c);, which can be used to interpret the counter-example if you keep in mind that 0 means left and 1 means right. I would prefer a more verbose tracing, though.

---

After you have done this for each possible transition, you can see what happens within your counter-example by running spin in the following way

~$ spin -t file_name.pml

The option -t replays the latest trail found by spin upon the violation of some assertion/property.

Answer 2

There are a few ways you can go about interpreting the trace.

1. Use iSpin:
   • go to Simulate/Play
   • in Mode, select Guided and enter the name of your trail file
   • Run

This will show, step by step, the actions taken by each of the processes, including info such as process number, proctype name, line number of instruction executed, code of instruction executed.

2. Do the same with spin:
   Use the command

   spin -t -p xyz.pml

3. Understand the trail file syntax:
   each line on the file is one step taken by the simulator. the first column is just serial numbers. The second column is process numbers (pids). (eg init will be 0, the first process it starts/runs will be 1 and so on.) The third column is transition number. If you want to get just an idea of what is happening, you can look at the pids and go over the instructions