Help - Xmin and Xmax properties

Hello,
I am approaching Modest language for my thesis.
I have a doubt regarding the meaning of the Xmax and Xmin properties. I mean, what are the rules for using them properly inside the modest program?
For example, inside the fileserver.modest file (in the directory Samples/sta ) has the following properties:

property QueueOverflowTimeMin = Xmin(T, queue == C);
property QueueOverflowTimeMax = Xmax(T, queue == C);

I don’t understand how to use them in my own program and hhat is the reasoning behind the develop of these properties.
And what are the syntax rules? I ask this because in one of my experiments, the tool printed the following error:

error: Expected “S”, “T” or “X”.

As you can see, I’m a little bit confused about the use these properties and on the papers available on the tool web site there isn’t a clear guide about their use.
Thank you for your help

Leonardo