Examples

[franck-van-breugel]

A simple example that is very similar to the example discussed in https://www.youtube.com/watch?v=4lcNyc6_t4U has been added. This example might be useful for the README file.

[yannicnoller]

Hi @franck-van-breugel! Thanks for the example and the different .jpf configurations.

ExampleChoco.jpf

I am a bit puzzled about the Choco example because it reports that the assertion is reachable, although it should actually be not reachable. Can you clarify? Am I missing something?

ExampleIASolver.jpf

The ExampleIASolver.jpf causes an JPF exception on my machine. Can you confirm that it works for you? I am not familiar with the IASolver so I do not know what the expected behavior is. But an example should probably not throw an exception, unless you wanted to demonstrate this?

Please find below my error output:

yannic@Yannics-MacBook-Pro jpf-symbc % DYLD_LIBRARY_PATH=/Users/yannic/repositories/jpf-symbc/lib/ \
  /Library/Java/JavaVirtualMachines/temurin-8.jdk/Contents/Home/bin/java \
    -Xmx1024m -ea \
    -jar ../jpf-core/build/RunJPF.jar \
    src/examples/ExampleIASolver.jpf
symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Example.main()

====================================================== search started: 24/7/22 3:01 PM
--------->property violated
pc 2 constraint # = 2
((y_2_SYMINT + x_1_SYMINT) - ((y_2_SYMINT + x_1_SYMINT) - y_2_SYMINT)) > ((y_2_SYMINT + x_1_SYMINT) - y_2_SYMINT) &&
x_1_SYMINT > y_2_SYMINT
[SEVERE] JPF exception, terminating: exception during propertyViolated() notification
java.lang.RuntimeException: # Error: IASolver can not compute int solution!
	at gov.nasa.jpf.symbc.numeric.solvers.ProblemIAsolver.getIntValue(ProblemIAsolver.java:246)
	at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.solve(SymbolicConstraintsGeneral.java:247)
	at gov.nasa.jpf.symbc.numeric.PathCondition.solveOld(PathCondition.java:376)
	at gov.nasa.jpf.symbc.numeric.PathCondition.solve(PathCondition.java:330)
	at gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener.propertyViolated(SymbolicSequenceListener.java:167)
	at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:521)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84)
	at gov.nasa.jpf.JPF.run(JPF.java:613)
	at gov.nasa.jpf.JPF.start(JPF.java:189)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at gov.nasa.jpf.tool.Run.call(Run.java:80)
	at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during propertyViolated() notification
	at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:527)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:84)
	at gov.nasa.jpf.JPF.run(JPF.java:613)
	at gov.nasa.jpf.JPF.start(JPF.java:189)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at gov.nasa.jpf.tool.Run.call(Run.java:80)
	at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.RuntimeException: # Error: IASolver can not compute int solution!
	at gov.nasa.jpf.symbc.numeric.solvers.ProblemIAsolver.getIntValue(ProblemIAsolver.java:246)
	at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.solve(SymbolicConstraintsGeneral.java:247)
	at gov.nasa.jpf.symbc.numeric.PathCondition.solveOld(PathCondition.java:376)
	at gov.nasa.jpf.symbc.numeric.PathCondition.solve(PathCondition.java:330)
	at gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener.propertyViolated(SymbolicSequenceListener.java:167)
	at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:521)
	... 9 more

[franck-van-breugel]

Thanks for the feedback.

ExampleChoco.jpf

I agree with your assessment. Can the choco-solver not deal with the type of constraint induced by this simple method? Or is there a bug somewhere?

ExampleIASolver.jpf

It does not work for me either and produces the same output as the one you have shown.

I will have a look at both examples in a week or so.