some questions about using packet

[xiayikexingfu]

I am glad to use your packet.However,when I install it with running command "./run.py -s sample/android/button/sample1.txt",I am faced with some question as followging:

07:36:13 merging 0 template(s) 07:36:13 semantics checking Traceback (most recent call last): File "./run.py", line 103, in sys.exit(main()) File "./run.py", line 99, in main return pasket.main(opt.cmd, opt.smpl, opt.tmpl, opt.pattern, opt.output) File "/home/yh/pasket-master/lib/typecheck.py", line 384, in takes_invocation_proxy return method(_args, _kwargs) File "/home/yh/pasket-master/lib/typecheck.py", line 416, in returns_invocation_proxy result = method(_args, _kwargs) File "/home/yh/pasket-master/pasket/init.py", line 337, in main decode.to_java(cmd, java_dir, tmpls, output_paths, _patterns) File "/home/yh/pasket-master/lib/typecheck.py", line 384, in takes_invocation_proxy return method(_args, _kwargs) File "/home/yh/pasket-master/lib/typecheck.py", line 416, in returns_invocation_proxy result = method(_args, _kwargs) File "/home/yh/pasket-master/pasket/decode/init.py", line 236, in to_java map(lambda vis: tmpl.accept(vis), _visitors) File "/home/yh/pasket-master/pasket/decode/init.py", line 236, in map(lambda vis: tmpl.accept(vis), _visitors) AttributeError: 'NoneType' object has no attribute 'accept'

I tried to get corresponding params: opt.cmd : android opt.smpl : ['sample/android/button/sample1.txt'] opt.tmpl : [] opt.pattern : [] opt.output : ./result

I hope to hear from you!Tanking you so much!

[jsjeon]

Template, a.k.a. partial program, is a key input to pasket. The goal of the tool is to find answers (we call it pattern instantiation) for pattern roles in the given template such that the synthesized model preserves the expected behavior, i.e., conforms to the given sample (call logs). So, passing no tmpl means, you asked pasket to magically synthesize a model from scratch. That would be great if we can do, but not yet. :)

Anyhow, maybe, our wordings in README are not well organized. Please try this command instead:

./run.py -c android -p button

which will automatically set opt.smpl, opt.tmpl, and opt.pattern for you.

[xiayikexingfu]

Thank you for your reply very much. frustratingly I get the output as follows: android [] [] ['button'] ./result 10 12:07:13 demo: button 12:07:14 rewriting accessor_adhoc pattern 12:07:14 rewriting accessor_map pattern 12:07:14 rewriting accessor_uni pattern 12:07:17 rewriting builder pattern 12:07:17 rewriting factory pattern 12:07:17 rewriting observer pattern 12:07:18 rewriting proxy pattern 12:07:18 rewriting singleton pattern 12:07:18 rewriting state pattern 12:07:18 semantics checking 12:07:18 building class hierarchy 12:07:48 encoding ./result/sk_button/type.sk 12:07:48 encoding ./result/sk_button/Object.sk 12:07:48 encoding ./result/sk_button/SymUtil.sk 12:07:48 encoding ./result/sk_button/Activity.sk 12:07:48 encoding ./result/sk_button/ActivityThread.sk 12:07:48 encoding ./result/sk_button/ComponentName.sk 12:07:48 encoding ./result/sk_button/Context.sk 12:07:48 encoding ./result/sk_button/ContextWrapper.sk 12:07:48 encoding ./result/sk_button/Intent.sk 12:07:48 encoding ./result/sk_button/Integer.sk 12:07:48 encoding ./result/sk_button/String.sk 12:07:48 encoding ./result/sk_button/StringBuffer.sk 12:07:49 encoding ./result/sk_button/StringBuilder.sk 12:07:49 encoding ./result/sk_button/BaseBundle.sk 12:07:49 encoding ./result/sk_button/Bundle.sk 12:07:49 encoding ./result/sk_button/Handler.sk 12:07:49 encoding ./result/sk_button/Looper.sk 12:07:49 encoding ./result/sk_button/Message.sk 12:07:49 encoding ./result/sk_button/MessageQueue.sk 12:07:49 encoding ./result/sk_button/SystemServer.sk 12:07:49 encoding ./result/sk_button/SystemServiceManager.sk 12:07:49 encoding ./result/sk_button/TelephonyManager.sk 12:07:49 encoding ./result/sk_button/TypedValue.sk 12:07:49 encoding ./result/sk_button/ContextThemeWrapper.sk 12:07:49 encoding ./result/sk_button/InputEvent.sk 12:07:49 encoding ./result/sk_button/KeyEvent.sk 12:07:49 encoding ./result/sk_button/MotionEvent.sk 12:07:49 encoding ./result/sk_button/View.sk 12:07:49 encoding ./result/sk_button/ViewGroup.sk 12:07:49 encoding ./result/sk_button/Window.sk 12:07:49 encoding ./result/sk_button/WindowManagerGlobal.sk 12:07:49 encoding ./result/sk_button/AbsSpinner.sk 12:07:49 encoding ./result/sk_button/AdapterView.sk 12:07:50 encoding ./result/sk_button/ArrayAdapter.sk 12:07:50 encoding ./result/sk_button/BaseAdapter.sk 12:07:50 encoding ./result/sk_button/Button.sk 12:07:50 encoding ./result/sk_button/CheckBox.sk 12:07:50 encoding ./result/sk_button/CompoundButton.sk 12:07:50 encoding ./result/sk_button/LinearLayout.sk 12:07:50 encoding ./result/sk_button/RadioButton.sk 12:07:50 encoding ./result/sk_button/RadioGroup.sk 12:07:50 encoding ./result/sk_button/RelativeLayout.sk 12:07:50 encoding ./result/sk_button/Spinner.sk 12:07:50 encoding ./result/sk_button/TextView.sk 12:07:50 encoding ./result/sk_button/Toast.sk 12:07:50 encoding ./result/sk_button/ButtonActivity.sk 12:07:50 encoding ./result/sk_button/Main.sk 12:07:50 encoding ./result/sk_button/R.sk 12:07:50 encoding ./result/sk_button/AuxAccessorMap.sk 12:07:55 encoding ./result/sk_button/AuxAccessorUni.sk 12:07:55 encoding ./result/sk_button/AuxObserverMotionEvent.sk 12:07:56 encoding ./result/sk_button/AuxSingleton.sk 12:07:56 encoding ./result/sk_button/sample_sample1.sk 12:07:56 encoding ./result/sk_button/log.sk 12:07:56 encoding ./result/sk_button/sample.sk 12:07:56 sketch running... [1467356878.0230 - ERROR] [SKETCH] Sketch Not Resolved Error: nullThe sketch could not be resolved. [1467356878.0280 - DEBUG] [SKETCH] stack trace written to file: ./result/tmp/stacktrace.txt [1467356878.0281 - DEBUG] Backend solver input file at /home/yh/pasket-master/result/tmp/sk_button/input0.tmp 12:07:58 wrong modelings

I wonder if some configure I did wrong.And I noticed when I run "python -m grammar.gen" it shows a warning which I cannot solve: java.g:691:9: Decision can match input such as "'0'..'9'{'E', 'e'}{'+', '-'}'0'..'9'{'D', 'F', 'd', 'f'}" using multiple alternatives: 3, 4 As a result, alternative(s) 4 were disabled for that input

In addition,when I run "./run.py -c codegen" I am faced with a problem that "package sketch.complier.ast.core does not exist" . So I changed the build.xml in this: `

... ...

` I directly refer to the jar file.

All I changed are shown above,I am pleased to hope your reply,thanks so much.

[jsjeon]

Thank you for trying the command I recommended.

Re: grammar.gen

Yes, we always got the same warning whenever we modified the grammar. So, you can safely ignore that warning.

Re: codegen

Sorry for the confusion, and you're right: if you're using a tar ball, you can swap some pre-defined properties in the build.xml file. I commented there to explicitly mention the case.

Re: Sketch error

I recently got a new laptop, and installed all the necessary things in a very fresh environment. I guess you're using sketch-1.6.9 tar ball, whereas I'm using Sketch source directly, which is now v1.7.2beta. Anyhow, due to the enhanced type checking in Sketch front-end, pasket-generated sketch files got type errors, rather than non-resolve error you got. In either case, I need to investigate this further. Thank you for helping me notice this. Will update anything soon-ish, but not guaranteed, as I'm no longer a grad student.

[xiayikexingfu]

Thank you for your guiding and I got the Model Synthesis successfully! Now I tried the Swing Model.I used the NASA jpf sources to compile and I installed the jpf-core,jpf-awt and jpf-symbc successfully in a directory which I create.However , when I executed the command "ant gui" in result dircetory with error outcome. I check the build.xml with gui target: `

` there are some questions about it: 1、in ~result/java directory ,it only has com and android directories,and how can I get the directories like java,javax 2、I used the NASA sources and its jpf-awt class directory has no java/util and javax/accessibility directory , if I got the file source wrong? And if you have some more detailed guiding or infomation about Usage (Model) with Swing? Thank you a lot!