Doubt in Prob output

[sanjay a]

Hello,

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?

Thanks and Regards,

Sanjay Ananda

[Michael Leuschel]

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.

Greetings,
Michael