Converting a system model into transition system for model checking

Question

Currently i am trying to convert a system prototype into the transition system model. i have some LTL properties and i want to verify those properties using model checking tool NuSMV. I just information how to start modeling by defining atomoic properties and other mathematical aspects.

Pictorial Representation of Model

Answer 1

A very simple encoding in NuSMV of that transition system would be

MODULE main()
VAR
  state : { GETINFO, ACK, SEND };
ASSIGN
  init(state) := GETINFO;
  next(state) := case
    state = GETINFO : SEND;
    state = SEND    : ACK;
    state = ACK     : {GETINFO, SEND};
  esac;

However, i think that the model you provided is a bit too simple to match with your problem description, thus I invite you to provide additional information about what you intend to do.