Проверка ограниченной модели с помощью Z3 — построение выражений

мы используем Z3 для проверки ограниченной модели. Для этого приведем целую кучу выражений следующего вида:

state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2

Другими словами, мы кодируем течение времени (шаги), предоставляя отдельное выражение для каждого временного шага. Очевидно, это приводит к нескольким тысячам выражений.

Хотя время, необходимое Z3 для их решения, является приемлемым (для сложности имеющихся у нас конечных автоматов), для построения всех этих выражений через Z3 JNI Java API требуется довольно много времени (несколько секунд).

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


z3 model-checking
person Markus Völter    schedule 05.07.2016    source источник
comment
Не могли бы вы дать количественную оценку немного времени и многих выражений? Также как вы строите эти выражения (читаются из текстового файла или вычисляются на лету?   -  person Heyji    schedule 08.07.2016
comment
Выражения были построены на лету из другой структуры данных путем вызова API Java/JNI. Это может быть несколько тысяч выражений, их построение занимает несколько секунд.   -  person Markus Völter    schedule 09.07.2016

Ответы (2)


arrow_upward
1
arrow_downward

Возможно, вы можете создать функцию, которая кодирует временной шаг (например, TimeStep new = Next(old)).

В Z3 есть «макропоиск», который может преобразовывать неинтерпретируемую функцию и квантификатор в расширенные выражения. Может быть, быстрее создать расширение таким образом, потому что это все внутри Z3.

В остальном я считаю, что производительность создания выражений хорошая. Интересно, может быть, ваш код просто очень неэффективен? Профилируйте это. Как вы пришли к выводу, что Z3 медленный?

person usr    schedule 10.07.2016
comment
Благодарю вас! Мы попробуем функциональный подход. Я не уверен, как код может быть неэффективным: я вызываю API в цикле for, и время, которое я указал, было голым временем вызова API без какой-либо другой (предотвратимой) обработки. Также обратите внимание, что я никоим образом не виню Z3 за медлительность — я просто ищу лучший способ сделать то, что нам нужно. - person Markus Völter; 13.07.2016

arrow_upward
0
arrow_downward

Я не знаю ни одного быстрого API в Z3, который улучшил бы вашу ситуацию. Несколько тысяч выражений за несколько секунд — это априори не так уж и плохо. У вас все еще есть традиционные подходы, такие как профилирование и параллельная обработка.

Кроме того, если ваша проблема позволяет, вместо того, чтобы работать с логической переменной, вы могли бы подумать о разложении их на битовые векторы и работе на векторном уровне (т.е. работать с группой переменных сразу, а не со всеми переменными по одной), что может (если ваша проблема позволяет это) сэкономить время.

person Heyji    schedule 10.07.2016