представлен в виде утверждения LTl, спин

Извините за мой английский, я из Украины) Только начал изучать проверку спиновой системы. Мы задали следующую задачу: «Представить в форме ниже ЛТЛ выражение: Если я люблю Машу, я не могу любить Дашу». Я не могу понять, как это сделать. Вот что у меня получилось: p - как и Маша, полученная Gp, представлена ​​в виде кода []p (правда, я не знаю, как писать):

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 }

Я понимаю, что это бред, но прошу вашей помощи.


promela spin
person nesalexy    schedule 04.03.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Если вам просто нужно LTL-выражение для «Если я люблю Машу, я не могу любить Дашу», то этого может быть достаточно:

bool i_love_masha;
bool i_love_dasha;

ltl la { i_love_masha -> !i_love_dasha }

тогда вопрос в том, каково поведение модели. Я предполагаю что-то вроде:

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

Может быть, это поможет вам начать. Но я не уверен, что это точно отвечает на ваш вопрос!

person GoZoner    schedule 05.03.2014
comment
Спасибо за ответ! Если у меня есть вопрос Если я влюблен в Машу, то могу любить Дашу, то: ltl la { i_love_masha -> i_love_dasha } ? - person nesalexy; 15.03.2014
comment
Импликация (оператор '->') такова: 'x подразумевает y'. Вы сказали "может любить Дашу" - "может" не правильно. - person GoZoner; 15.03.2014
comment
Извините, если я не могу этого понять, для вас это так же сложно, как и для меня. Выражение Если я влюблен в Машу, я могу любить Дашу получается, что можно составить формулу: []i_love_masha && i_love_dasha . Я правильно понимаю? Или хотя бы что-то похожее?) - person nesalexy; 16.03.2014
comment
Проблема в том, что вы используете фразу «люблю Дашу». Означает ли «может любить» «в конце концов полюбить». По сути, нет LTL-выражения для «может». Итак, вам нужно выяснить, что вы на самом деле подразумеваете под «может». Может, «не любить Дашу, пока не полюбишь Машу»? - person GoZoner; 17.03.2014