Java Path Finder NumericValueChecker - PullRequest
Новая
       41

Java Path Finder NumericValueChecker

0 голосов
/ 27 ноября 2018

Я пытаюсь изучить 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» в папку examples 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?

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

1 Ответ

0 голосов
/ 27 ноября 2018

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

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

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

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

...