problems about the cases...
zhuzhujulie opened this issue · 2 comments
Dear author,
I find that not all case you provided can get a result, why?
For example, the benchmark18 in the joda directory. i can get a program that pass the test case.
And i also want to ask you that ,
why do you use the method of symbolic encoding to find a path rather than finding path by traverse the reachability graph? Cause i think your method is complex and hard to understand.
Dear zhuzhujulie,
Dear author,
I find that not all case you provided can get a result, why?
For example, the benchmark18 in the joda directory. i can get a program that pass the test case.
The open source version of SyPet is a simplified version of the tool that was used for the POPL submission. For example, this version of SyPet does not contain the similarity metrics described on Appendix C (https://www.cs.utexas.edu/~isil/popl17-sypet-extended.pdf). The performance of this version should be comparable to the version "No Obj" presented in Appendix D of the paper.
If you want to reproduce the results of the paper, please use the original version of SyPet available in binary form at: https://fredfeng.github.io/sypet/
And i also want to ask you that ,
why do you use the method of symbolic encoding to find a path rather than finding path by traverse the reachability graph? Cause i think your method is complex and hard to understand.
The reachability graph is exponential in the number of components and will not scale for large Petri Nets. To solve this problem, we reduce it to a planning problem as described in Appendix B of the paper. There are other alternatives to solve the reachability problem of Petri Nets that go beyond the scope of the paper. For example, you could build the unfolding of the Petri Net and do reachability analysis on that structure. For more details on the reachability graph and the unfolding of Petri Nets, I would suggest you to read the related literature in the Petri Nets community.