Questions

Question

Questions

Closed this issue 7 years ago · 3 comments

Hi, when i try to run this project. Some trouble happens about the class from the jar"sat4j-pb", so i think maybe the problems comes from my wrong ways of configuration.
So i want to ask you that about the concrete environment about your running this project.????????

By the way, you have missed the entrance setting in the build.xml, So the "sypet.jar" produce Ant can't be run successful without the setting of main class.

Answer 1 · 2017-08-21T19:01:18.000Z

Dear zhuzhujulie,

We were able to compile and run SyPet on multiple operating systems running Java 1.7 and Java 1.8,
Which operating system and Java version are you running?

Can you provide some details on the output you get when you execute the following terminal commands (as described in the README.md file):
$ ant
$ ./run-sypet.sh benchmarks/xml/23/benchmark23.json

For example, this is the output we get when running SyPet on Ubuntu:
$ ant
Buildfile: /home/ruben/sypet/build.xml

init:
[mkdir] Created dir: /home/ruben/sypet/bin

compile:
[javac] /home/ruben/sypet/build.xml:14: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
[javac] Compiling 43 source files to /home/ruben/sypet/bin
[javac] warning: [options] bootstrap class path not set in conjunction with -source 1.7
[javac] Note: /home/ruben/sypet/src/edu/utexas/sypet/synthesis/SypetTestUtil.java uses unchecked or unsafe operations.
[javac] Note: Recompile with -Xlint:unchecked for details.
[javac] 1 warning

jar:
[jar] Building jar: /home/ruben/sypet/sypet.jar

BUILD SUCCESSFUL
Total time: 1 second

$ ./run-sypet.sh benchmarks/xml/23/benchmark23.json
Buildfile: /home/ruben/sypet/build.xml

sypet:
[java] ----------Options
[java] Verbose: false
[java] Timeout: 600000
[java] Round Robin: true
[java] Round Robin Iterations: 100
[java] Round Robin Range: 2
[java] Solver limit: 5
[java] ----------benchmarks/xml/23/benchmark23.json
[java] Benchmark Id: 23
[java] Method name: getOffsetForLine
[java] Packages: [javax.swing.text]
[java] Libraries: [./lib/rt7.jar]
[java] Source type(s): [javax.swing.text.Document, int]
[java] Target type: int
[java] --------------------------------------------------------
[java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
[java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
[java] Warning: javax.crypto.Cipher is a phantom class!
[java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
[java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
[java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
[java] Warning: javax.crypto.SecretKey is a phantom class!
[java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
[java] Warning: javax.crypto.Mac is a phantom class!
[java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
[java] Warning: javax.crypto.BadPaddingException is a phantom class!
[java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
[java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
[java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
[java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
[java] Warning: javax.crypto.CipherInputStream is a phantom class!
[java] Warning: javax.crypto.CipherOutputStream is a phantom class!
[java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
[java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
[java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
[java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
[java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.PSource is a phantom class!
[java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
[java] Warning: javax.crypto.KeyGenerator is a phantom class!
[java] #Classes: 441
[java] #Methods: 4076
[java] Soot Time: 3147.501301
[java] PetriNet for path length: 1 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] PetriNet for path length: 2 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] PetriNet for path length: 3 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] PetriNet for path length: 4 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] PetriNet for path length: 5 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] PetriNet for path length: 6 [places: 510 ; transitions: 2700 ; edges: 7177]
[java] =========Statistics (time in milliseconds)=========
[java] Benchmark Id: 23
[java] Sketch Generation Time: 335.325146
[java] Sketch Completion Time: 15.041387999999998
[java] Compilation Time: 588.948544
[java] Running Test cases Time: 110.65562299999999
[java] Synthesis Time: 461.022157
[java] Total Time: 1049.970701
[java] Number of components: 3
[java] Number of holes: 5
[java] Number of completed programs: 21
[java] Number of sketches: 11
[java] Solution:
[java] javax.swing.text.Element sypet_var51 = sypet_arg0.getDefaultRootElement();
[java] javax.swing.text.Element sypet_var52 = sypet_var51.getElement(sypet_arg1);
[java] int sypet_var53 = sypet_var52.getStartOffset();
[java] return sypet_var53;
[java]
[java] ============================

BUILD SUCCESSFUL
Total time: 11 seconds

Answer 2 · 2017-08-22T07:54:06.000Z

Dear author:
Thank you for answering me!!!
I have two questions now~

First

i try to run as the way you told me. In Linux.
And it can end , and it can produce a result:
and it has some error tips, are they normal clue or exception ???The result is below:

./run-sypet.sh benchmarks/geometry/10/benchmark10.json
Buildfile: /home/zyz/workspace/sypet-master/sypet/build.xml

sypet:
[java] ----------Options
[java] Verbose: false
[java] Timeout: 600000
[java] Round Robin: true
[java] Round Robin Iterations: 100
[java] Round Robin Range: 2
[java] Solver limit: 5
[java] ----------benchmarks/geometry/10/benchmark10.json
[java] Benchmark Id: 10
[java] Method name: scale
[java] Packages: [java.awt.geom]
[java] Libraries: [./lib/rt7.jar]
[java] Source type(s): [java.awt.geom.Rectangle2D, double, double]
[java] Target type: java.awt.geom.Rectangle2D
[java] --------------------------------------------------------
[java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
[java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
[java] Warning: javax.crypto.Cipher is a phantom class!
[java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
[java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
[java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
[java] Warning: javax.crypto.SecretKey is a phantom class!
[java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
[java] Warning: javax.crypto.Mac is a phantom class!
[java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
[java] Warning: javax.crypto.BadPaddingException is a phantom class!
[java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
[java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
[java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
[java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
[java] Warning: javax.crypto.CipherInputStream is a phantom class!
[java] Warning: javax.crypto.CipherOutputStream is a phantom class!
[java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
[java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
[java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
[java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
[java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
[java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
[java] Warning: javax.crypto.spec.PSource is a phantom class!
[java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
[java] Warning: javax.crypto.KeyGenerator is a phantom class!
[java] #Classes: 50
[java] #Methods: 751
[java] Soot Time: 4358.177925
[java] PetriNet for path length: 1 [places: 64 ; transitions: 539 ; edges: 1242]
[java] PetriNet for path length: 2 [places: 64 ; transitions: 539 ; edges: 1242]
[java] PetriNet for path length: 3 [places: 64 ; transitions: 539 ; edges: 1242]
[java] PetriNet for path length: 4 [places: 64 ; transitions: 539 ; edges: 1242]
[java] PetriNet for path length: 5 [places: 64 ; transitions: 539 ; edges: 1242]
[java] PetriNet for path length: 6 [places: 64 ; transitions: 539 ; edges: 1242]
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var247 = sypet_arg0;java.awt.geom.AffineTransform sypet_var248 = java.awt.geom.AffineTransform.getTranslateInstance(sypet_arg2,sypet_arg1);java.awt.geom.Area sypet_var249 = sypet_var247.createTransformedArea(sypet_var248);java.awt.geom.Rectangle2D sypet_var250 = sypet_var249.getBounds2D();return sypet_var250;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var247 = sypet_arg0;java.awt.geom.AffineTransform sypet_var248 = java.awt.geom.AffineTransform.getTranslateInstance(sypet_arg1,sypet_arg2);java.awt.geom.Area sypet_var249 = sypet_var247.createTransformedArea(sypet_var248);java.awt.geom.Rectangle2D sypet_var250 = sypet_var249.getBounds2D();return sypet_var250;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var254 = sypet_arg0;java.awt.geom.AffineTransform sypet_var255 = java.awt.geom.AffineTransform.getScaleInstance(sypet_arg2,sypet_arg1);java.awt.geom.Area sypet_var256 = sypet_var254.createTransformedArea(sypet_var255);java.awt.geom.Rectangle2D sypet_var257 = sypet_var256.getBounds2D();return sypet_var257;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var254 = sypet_arg0;java.awt.geom.AffineTransform sypet_var255 = java.awt.geom.AffineTransform.getScaleInstance(sypet_arg1,sypet_arg2);java.awt.geom.Area sypet_var256 = sypet_var254.createTransformedArea(sypet_var255);java.awt.geom.Rectangle2D sypet_var257 = sypet_var256.getBounds2D();return sypet_var257;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var261 = sypet_arg0;java.awt.geom.AffineTransform sypet_var262 = java.awt.geom.AffineTransform.getRotateInstance(sypet_arg2,sypet_arg1);java.awt.geom.Area sypet_var263 = sypet_var261.createTransformedArea(sypet_var262);java.awt.geom.Rectangle2D sypet_var264 = sypet_var263.getBounds2D();return sypet_var264;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var261 = sypet_arg0;java.awt.geom.AffineTransform sypet_var262 = java.awt.geom.AffineTransform.getRotateInstance(sypet_arg1,sypet_arg2);java.awt.geom.Area sypet_var263 = sypet_var261.createTransformedArea(sypet_var262);java.awt.geom.Rectangle2D sypet_var264 = sypet_var263.getBounds2D();return sypet_var264;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var268 = sypet_arg0;java.awt.geom.AffineTransform sypet_var269 = java.awt.geom.AffineTransform.getShearInstance(sypet_arg2,sypet_arg1);java.awt.geom.Area sypet_var270 = sypet_var268.createTransformedArea(sypet_var269);java.awt.geom.Rectangle2D sypet_var271 = sypet_var270.getBounds2D();return sypet_var271;}
[java] ^
[java] 1 error
[java] /Source.java:3: error: incompatible types: Rectangle2D cannot be converted to Area
[java] java.awt.geom.Area sypet_var268 = sypet_arg0;java.awt.geom.AffineTransform sypet_var269 = java.awt.geom.AffineTransform.getShearInstance(sypet_arg1,sypet_arg2);java.awt.geom.Area sypet_var270 = sypet_var268.createTransformedArea(sypet_var269);java.awt.geom.Rectangle2D sypet_var271 = sypet_var270.getBounds2D();return sypet_var271;}
[java] ^
[java] 1 error
[java] =========Statistics (time in milliseconds)=========
[java] Benchmark Id: 10
[java] Sketch Generation Time: 593.8663809999999
[java] Sketch Completion Time: 1440.9717359999997
[java] Compilation Time: 2066.0842299999995
[java] Running Test cases Time: 21.842959999999998
[java] Synthesis Time: 2056.6810769999997
[java] Total Time: 4122.765307
[java] Number of components: 4
[java] Number of holes: 7
[java] Number of completed programs: 176
[java] Number of sketches: 49
[java] Solution:
[java] java.awt.Shape sypet_var296 = sypet_arg0;
[java] java.awt.geom.AffineTransform sypet_var297 = java.awt.geom.AffineTransform.getScaleInstance(sypet_arg1,sypet_arg2);
[java] java.awt.geom.Path2D.Double sypet_var298 = new java.awt.geom.Path2D.Double(sypet_var296,sypet_var297);
[java] java.awt.geom.Rectangle2D sypet_var299 = sypet_var298.getBounds2D();
[java] return sypet_var299;
[java]
[java] ============================

# Second
In fact , i want to run the Experiments.java rather than run it from the shell script. Cause it will be more convenient for me to understand how it works. Can you tell me how to run this project without the shell script??? Hope you can help me to solve my problem below:

In windows10, eclipse, java1.8, i run the experiment.java and give it a parameter of
"-file .........\sypet\benchmarks\geometry\10\benchmark10.json"
Am i in the wrong way???And am i giving the wrong parameter???
And when i run in tihs way from eclipse,the result is below:

----------Options
Verbose: false
Timeout: 600000
Round Robin: false
Round Robin Iterations: 100
Round Robin Range: 2
Solver limit: 5
qb.getLibs() = [./lib/rt7.jar]
----------D:\MyFile\jee-neonWorkplace\sypet\benchmarks\geometry\10\benchmark10.json
Benchmark Id: 10
Method name: scale
Packages: [java.awt.geom]
Libraries: [./lib/rt7.jar]
Source type(s): [java.awt.geom.Rectangle2D, double, double]
Target type: java.awt.geom.Rectangle2D

Warning: javax.crypto.Cipher is a phantom class!
Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
Warning: javax.crypto.BadPaddingException is a phantom class!
Warning: javax.crypto.NoSuchPaddingException is a phantom class!
Warning: javax.crypto.SecretKey is a phantom class!
Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
Warning: javax.crypto.interfaces.DHKey is a phantom class!
Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
#Classes: 0
#Methods: 0
Soot Time: 3178.009021
PetriNet for path length: 1 [places: 22 ; transitions: 35 ; edges: 70]
Exception in thread "main" uniol.apt.adt.exception.NoSuchNodeException: Node 'double' does not exist in graph ''
at uniol.apt.adt.pn.PetriNet.getPlace(PetriNet.java:834)
at edu.utexas.sypet.Experiment.initPetriNet(Experiment.java:77)
at edu.utexas.sypet.Experiment.main(Experiment.java:237)

Answer 3 · 2017-09-04T17:47:30.000Z

Dear zhuzhujulie,

Answering your questions.

Yes, some errors may be displayed when you run SyPet. SyPet synthesizes a program that type checks and runs it on a set of test cases. For example, it may be the case that some abstracts types are being used and the program cannot be compiled. However, in this situation, the issue
was a bug in the CONFIG.json that controls the polymorphic types and was incorrectly stating that an Area was also a Rectangle2D. Thanks for pointing this to us. I have updated this file and fixed this issue.
Providing support to run SyPet via an IDE goes beyond the scope of our help. However, I did push a .project file to the repository that should make it easier to import SyPet into Eclipse. Please, pull the latest changes from the repository. After that, you can simply import the project into eclipse and you should be able to run it directly from the IDE.

In the program arguments tab you should use something like:
-f benchmarks/xml/23/benchmark23.json

Note that I am assuming you did not change the directory structure and kept the benchmarks subdirectory inside the SyPet directory. If you move the benchmark directory somewhere else you must update the "libs" and "testPath" inside of each .json file to reflect the absolute path of the libraries and test cases.

I hope this solves your issue and you are able to run it in Eclipse.