Вопрос:

Как ограничить количество следующих обратных слешей нечетным числом? на четное число?

alloy

40 просмотра

1 ответ

1296 Репутация автора

next это бинарное отношение.

Эта строка:

A\\\,B

смоделирована этой nextтаблицей:

Следующая таблица, которая моделирует <code> A \\\, B </ code>

Рассмотрим первый столбец первого ряда таблицы. Это значение равно A. Из A мы можем получить Backslash0, затем Backslash1, затем Backslash2, затем Backslash3, затем Comma0, а затем B. Итак, число обратных слешей между A и первым достижимым значением без обратной косой черты (которое в данном случае является Comma0) нечетное число (3). Да! Это то, что я хочу. Если первое достижимое значение без обратной косой черты было не запятой, то число промежуточных обратных косых черт должно быть четным (0, 2, 4, ...).

Как мне выразить это ограничение в Alloy:

Для каждого значения c без обратной косой черты в первом столбце следующей таблицы: Если первое значение c без обратной косой черты, достижимое из c, является запятой, то число обратных косых черт между c и c 'должно быть нечетным (1, 3, 5, ...). Если первое значение без обратной косой черты, достижимое из c, не является запятой, то число обратных косых черт между c и c 'должно быть четным (0, 2, 4, ...).

Автор: Roger Costello Источник Размещён: 08.11.2017 10:09

Ответы (1)


0 плюса

2148 Репутация автора

Интересно, моделируешь ли ты это на правильном уровне абстракции? Нужно ли учитывать структуру последовательности с обратной косой чертой? Что если у вас есть два токена, двойная обратная косая черта и обратная косая черта, и вы только что сказали, что перед обратной косой чертой должна стоять двойная обратная косая черта, а после - обратная косая черта?

Автор: Daniel Jackson Размещён: 09.11.2017 01:05
Вопросы из категории :
32x32