Traffic light spin

Question

First I need to say Im very new on this and I have to do a semaphore with some conditions.

We will only model one traffic light per each direction (the second one just repeats the same behaviour). For instance, in the picture above, the vertical light is green and the horizontal one is red. Initially, both directions are red. When a car arrives, it is detected by a sensor and its corresponding light turns to green. However, this only happens if the other direction is still in red; otherwise, it will wait until the other direction is closed. Once any direction is in green, it will turn next to orange (there is a timer, but we will not model the delay) and then it will turn to red again.

Actually this is my code right now:

mtype = { red, yellow, green };
mtype light0 = red;
mtype light1 = red;

active proctype TL0() {
    do
        :: if
        :: light0 == red -> Ered: atomic {
            light1 == red; /* wait*/
            light0 = green;
        }
        :: light0 == green -> EY: light0 = yellow
        :: light0 == yellow -> EG: light0 =red
        fi;
        printf("The light0 is now %e\n", light0)
    od
}

active proctype TL1() {
    do
        :: if
        :: light1 == red -> Ered: atomic {
            light0 == red; /* wait*/
            light1 = green;
        }
        :: light1 == green -> EY: light1 = yellow
        :: light1 == yellow -> EG: light1 =red
        fi;
        printf("The light1 is now %e\n", light1)
    od
}

The problem is that when I use

spin -a -f '<>(!TL0@Ered && !TL1@Ered)' sem3.pml

for check the safety I get one erorr.

warning: never claim + accept labels requires -a flag to fully verify warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) pan:1: assertion violated !(( !((TL0._p==Ered))&& !((TL1._p==Ered)))) (at depth 0) pan: wrote sem3.pml.trail

(Spin Version 6.4.8 -- 2 March 2018) Warning: Search not completed + Partial Order Reduction

Full statespace search for: never claim + (never_0) assertion violations + (if within scope of claim) acceptance
cycles - (not selected) invalid end states - (disabled by -E flag)

State-vector 36 byte, depth reached 0, errors: 1 1 states, stored 0 states, matched 1 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved)

But actually I have no idea wheres the problem :(

Hope someone could help me

Thx!

Patrick Trentin Patrick Trentin · Accepted Answer · 2018-05-11T16:51:02

The model is fine, but I would suggest you to manually generate the verifier.

First, add the following lines at the bottom of your file:

ltl p1 { <>(!TL0@Ered && !TL1@Ered) };
ltl p2 { [] !(TL0@EY && TL1@EY) };     // perhaps you wanted (something like) this?

Then, generate the verifier:

~$ spin -a file_name.pml
~$ gcc -o run pan.c
~$ ./run -a -N p1
...
~$ ./run -a -N p2
...

Traffic light spin

1 Answers