Представлен в виде выписки LTl, спин

Question

Извините за мой английский, я из Украины) только начал изучать проверку спиновой системы. Мы задали следующую задачу: "Представьте в форме ниже выражение 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 } 

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

Answer 1

Если вам просто нужно выражение 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! */
}

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