This code is related to the following posts:

post1

post2

MODULE main

VAR

state : { Na,Re,Su,Ac,Pr,Do,En};

ASSIGN

init(state) := Na;

next(state) :=

case

(state = Na ):{Re,En};

(state = Re): {Su,Ac,Pr};

(state = Su): {Re,Ac,Na};

(state = Ac):  {Ac,Pr};

(state = Pr): {Do};

(state = Do): {En};

(state = En): {Na};

TRUE:state;

esac;

–LTL specifications

LTLSPEC G((state=Na) -> X(state=Re | state = En));

LTLSPEC G((state=Re -> X(state=Ac|state=Pr|state=Su|state=Do)));

LTLSPEC ((state=Su) -> X(state= Na&state=En));

LTLSPEC G((state=Do) -> X(state=En));

LTLSPEC G((state=En) -> X(state=Na));

LTLSPEC ((state=Ac) -> X(state=Pr|state=Su));

LTLSPEC (((state=Re|state=Pr)-> X(state=Do|state=Su)));

–CTL specifications

CTLSPEC AG((state=Re -> AX(state=Ac|state=Pr|state=Su|state=Do)));

CTLSPEC AG((state=Do) -> AX(state=En));

CTLSPEC AG(state=Na -> AX(state = Re |state = En));

CTLSPEC AG((state = Re -> EX state = Su)|(state = Re -> EX state = Pr));