Adding a property that should fail in the Wheel Brake System as a benchmark

[vaibhavbsharma]

This version of Wheel Brake System has been part of the SPF repository
for the past few years. It can be found at https://github.com/SymbolicPathFinder/jpf-symbc/blob/master/src/examples/WBS.java. In this commit, I am dding it to the SV-COMP repository of benchmarks so that other tools can also benefit from it.

• WBS_prop1 is the name of the newly added benchmark

• sym-link to the jpf-regression license file has been added

• contributed by developers of Java Ranger (https://github.com/vaibhavbsharma/java-ranger). This benchmark originates from the WBS version maintained in the src/examples directory of the source code of SPF as mentioned earlier.

• The ReachSafety.set category has been updated to now include benchmarks in the java-ranger-regression directory

• assert.prp should be used to verify the intended property

• expected answer has been added WBS_prop1.yml

[mmuesly]

Thank you Vaibhav for contributing this test case! I have a couple of questions and further ideas, I leave here for discussion.

[vaibhavbsharma]

I've made changes to this benchmark based on discussions in #860. Please let me know if anything else is required for this benchmark to be merged.

[mmuesly]

@vaibhavbsharma thank you for picking up the discussion. I think there is still a small change missing, unless I am misinterpreting the input_files semantic in the task yml.

Could you shortly explain, how this relates to the already merged PRs #860, #861, #862?
My implicit and naive expectation is that this change should affect the files introduced by them as well.

Following the discussion on #860, I would expect that you merge property one in the same format as #860,#861,#862 and we rework all of them in January, or you rework all of them now in alignment with this PR. Otherwise, it feels from my point of view like doing only half of the change now. But I am open to other opinions.

[vaibhavbsharma]

Thanks for looking at my PR, @mmuesly!! I've addressed your comments and also integrated the 3 additional properties from #860, #861, and #862 into this pull request.

[mmuesly]

@vaibhavbsharma I think you are still missing to remove this file: https://github.com/sosy-lab/sv-benchmarks/blob/master/java/java-ranger-regression/WBS_prop4/Main.java

Once that is done, this PR should be ready to merge.

[peterschrammel]

And please pipe the sources through a code formatter

[vaibhavbsharma]

@vaibhavbsharma I think you are still missing to remove this file: https://github.com/sosy-lab/sv-benchmarks/blob/master/java/java-ranger-regression/WBS_prop4/Main.java

Once that is done, this PR should be ready to merge.

I did delete WBS_prop4/Main.java in this commit: cd4bd89