Questions about jstar in general

[eccle...@gmail.com]

I have been assigned to writing the logic file in the analysis of a program with jstar. When I looked at the documentation at the official website, it did not clarify well. My question is: does anyone have more documentation about writing the logic? Also is the logic file syntax based off ml? and could i use ml functions in the logic file? Thanks in advance.