Используйте перегрузку модуля для реализации хеш-функции в TLA + - PullRequest
Новая
       45

Используйте перегрузку модуля для реализации хеш-функции в TLA +

0 голосов
/ 24 декабря 2018

Механизм перегрузки модуля описан в образце Ханойской башни здесь .Это позволяет вам реализовывать операторы TLA + в Java для повышения производительности проверки моделей.

Некоторое время я пытался определить полезную хеш-функцию в TLA + (нет, функция идентификации не работает для моих целей) и я думаю, что перегрузка модуля может быть способ сделать это.Хеш-функция будет принимать объект TLA + (например, запись) и использовать метод Java hashCode() в строковом представлении объекта для детерминированного получения его хеш-значения.Это значение будет возвращено в спецификацию TLA +.

Возможно ли это?Как будет выглядеть код переопределения Java?Существуют ли другие примеры кода переопределения модулей?

1 Ответ

0 голосов
/ 19 февраля 2019 
import tlc2.value.impl.IntValue;
import tlc2.value.impl.Value;

public class TLCHash {

    public static Value Hash(Value v) {
        return IntValue.gen(v.hashCode());
    }
}

------------------------------ MODULE TLCHash ------------------------------
EXTENDS Integers

Hash(val) == CHOOSE n \in Int : TRUE


ASSUME(Hash(<<"a","b","c">>) = Hash(<<"a","b","c">>))
ASSUME(Hash(<<"a","b","c">>) # Hash(<<"c","b","a">>))

ASSUME(Hash({"a","b","c"}) = Hash({"b","c","a", "c"}))

=============================================================================

Обратите внимание, что реализация Value # hashCode в TLC делегирует отпечаток Value # и, следовательно, должна работать так, как вы этого хотите (из моего понимания вашего вопроса).Также обратите внимание, что иерархия класса Value была перемещена из пакета tlc2.value в tlc2.value.impl в версии 1.5.8.

https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754 показывает реальное применение перезаписи модулей иможет вдохновить решение.Наконец, единственным аспектом встроенных стандартных модулей TLC , который фактически превращает их в стандартные модули, является пакет / пространство имен tlc2.module.

...