represented in the form of a statement LTl, spin

Question

im sorry for my english, im from Ukraine) Only begun to study the spin system verification. We asked the following problem: "Present in the form below LTL expression: If I love Masha, I can not love Dasha". I can not understand how to do it. Here's what I got: p - like Masha obtained Gp, is represented in the form [] p code (although I do not know how to write):

int m = 4;
int d = 5;

proctype lab1(byte a; byte b){
    if
    :: (a > b) -> printf("%e\n",a)
    :: (a < b) -> printf("%e\n",b)
    fi
}

init {
    run lab1(m, d)
}

ltl la { []m } 

I understand that this is nonsense, but I ask for your help.

Answer 1

If you just need an LTL expression for 'If I love Masha, I can not love Dasha' then this might be enough:

bool i_love_masha;
bool i_love_dasha;

ltl la { i_love_masha -> !i_love_dasha }

then the question is what is the behavior of the model. I'll guess something like:

init {
  i_love_masha = true;
  i_love_dasha = true;   /* should be a violation! */
}

Maybe that gets you started. But, I'm not sure if this exactly answers your question!