Doubt in Prob output

Skip to first unread message

sanjay a

Jun 11, 2023, 7:03:34 PM6/11/23
to ProB Users

I am Sanjay Ananda and currently pursuing masters in Aerospace Engineering in ISAE Supaero, France. We are working on a project where we are using 'probcli' command to validate the LTL formula. Currently we are getting the output (Formula True or False) on the terminal (Image attached with the mail). Is there a way to output/print the results of the LTL formula checker into a text file?
probcli output.jpg
Thanks and Regards,
Sanjay Ananda

Michael Leuschel

Jun 12, 2023, 8:31:09 AM6/12/23
to sanjay a, ProB Users
Hi Sanjay,

you can use the probcli comman switch -logxml FILE.

probcli scheduler.mch -ltlformula 'G (e(del) or e(new))’ -logxml out.xml

will creat an entry of the form:
<ltl_model_check formula="G (e(del) or e(new))">
<model_check_result status="no" expected_status="_" mode="init" />
in the file out.xml.

You can also save the counter example found for a single formula using the -his FILE command:

probcli scheduler.mch -ltlformula 'G (e(del) or e(new))' -logxml out.xml -his out.prob2trace -his_option json

With the -his_option json switch it will create a trace file in JSON format that can be read by ProB2-UI or ProB Tcl/Tk or probcli.
Without the switch it will create a trace file in more human readable form.

probcli output.jpg
probcli output.jpg
Reply all
Reply to author
0 new messages