Java Path Finder NumericValueChecker

Question

Я пытаюсь изучить Java Path Finder (JPF). Я скачал JPF и собрал его. В настоящее время у меня есть папка jpf-core, в которой есть примеры файлов.java и соответствующие им файлы.jpf. Моя цель - создать новый базовый файл.java и проверить, превышает ли конкретное значение в этом файле максимальный предел, указанный в файле.jpf.

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

NumericValueCheck.java

public class NumericValueCheck {
  public static void main (String[] args){
    double someVariable;
    someVariable = 42;  
    someVariable = 60; 
  }
}

NumericValueCheck.jpf

target = NumericValueCheck

listener = .listener.NumericValueChecker

# NumericValueChecker configuration
range.vars = 1
range.1.var = NumericValueCheck.main(java.lang.String[]):someVariable
range.1.min = 0
range.1.max = 42

Однако я создал новый файл.java и назвал его "BasicCheck.java". Вот код внутри него;

public class BasicCheck {
public static void main(String[] args){
    double result;
    result = 60;
    result = 110;
    }
}

Вот свойства в BasicCheck.jpf;

target = BasicCheck

listener = .listener.NumericValueChecker

# NumericValueChecker configuration
range.vars = 1
range.1.var = BasicCheck.main(java.lang.String[]):result
range.1.min = 0
range.1.max = 60

Я скомпилировал BasicCheck.java, используя javac BasicCheck.java в отдельном каталоге. Затем я копирую "BasicCheck.java" и "BasicCheck.jpf" в папку примеров jpf-core, где также находятся NumericValueCheck.java и NumericValueCheck.jpf. Я также копирую "BasicCheck.class" в jpf-core/build/examples каталог, где "NumericValueCheck.class" также в том же месте.

Тем не менее, когда я запускаю команду java -jar build/RunJPF.jar src/examples/BasicCheck.jpf, он не может найти ошибку. В результате "ошибка не обнаружена". Он должен обнаружить 110, который больше, чем верхняя граница 60.

Почему это не работает? Нужно ли что-то добавить в мой новый BasicCheck.java или BasicCheck.jpf?

Заранее спасибо.

Answer 1

Я нашел решение после долгих усилий. Решение простое.

Поместите BasicCheck.java и BasicCheck.jpf в каталог jpf-core/src/examples,

НЕ компилировать с использованием исходного кода javac, Откройте терминал и cd в jpf-core каталог. Затем введите следующую команду: ./gradlew buildJars,

Вот и все. Теперь вы можете использовать команду java -jar build/RunJPF.jar src/examples/BasicCheck.jpf запустить Java Path Finder.