uising green for probabilistic symbol execution

[LeorPoirot]

Recently, my team is testing our code by using approach to probabilistic symbol execution. I have heard that the exellent tool green solver enjoys such fuction. However I couldnt find a test case when I scan the test&example directory . So hopeful, I need some help , would you give me some test cases on uising green to executing the probabilistic symbol test. Thanks in advance!

[wvisser]

Thanks for the interest. Green itself doesn't do Probabilistic Symbolic Execution (PSE) but it supports the interaction with the model counters. If you want to see how to use Green to do model counting you can check out this docker image https://hub.docker.com/r/willemvisser/willem-jpf-mutation/ where there is a little tutorial on PSE that uses Green. It is used within Symbolic PathFinder (in the tutorial) but it can of course be used with anything that produces a path condition. Look for the *_TUTORIAL files in the root of the image to see the steps to follow. It has both a GREEN and PSE tutorial. Let me know if you have further questions

[LeorPoirot]

Thx a lot , I will have a study carefully.

[LeorPoirot]

I have pull the it from the docker ,but when I used ‘docker run willem-jpf-mutation’, the container exit immediately , maybe there are something I missed.Can you give me some advice on how to get the whole project , thank you very much!

[wvisser]

Small change in how you run the image, this is a interactive image that you want to open as a shell:
"docker run -it willemvisser/willem-jpf-mutation"

that will drop you into the jpf-mutation folder, just do a "cd .." and look for the *_TUTORIAL files