Declare several initial states of Transition System on Promela

Question

I'm trying to model the following transition system on SPIN using Promela: The Transition System

My approach was the following:

#define a ((state == 1) || (state == 5))

#define c ((state == 2) || (state == 3) || (state == 5))

#define b ((state == 3) || (state == 4) || (state==5))

ltl GFc {<>([](c))}

int state = 1 || 2;

active proctype System() {
    do

    :: state == 1 -> state = 3;
    :: state == 1 -> state = 4;
    :: state == 2 -> state = 4;
    :: state == 3 -> state = 4;
    :: state == 4 -> state = 2;
    :: state == 4 -> state = 3;
    :: state == 4 -> state = 5;
    :: state == 5 -> state = 4;
    :: state == 5 -> state = 5;
    od;
}

init {
    run System();
}

but as you can see the transition system doesn't verify the LTL formula FGc, and when I run it on SPIN RCP it doesn't encounter any errors. I think it might be related to how I defined the initial states, but I'm not sure. What should I do?