How to export LTL Check result from LTL Checker plugin

uekencns

I have been using LTL Checker plugin with ProM6, it very useful software and plugin.

Recently I have to check eventlogs from a simulation model with more than 10 000 LTL formula.

I would like to export check result because I have to confirm which trace was compliant with which formula.

ex) trace #00453 was compliant with LTL formula #00124

Now I have to confirm with my eyes one by one. It will take huge time.

ProM can display the result in "Rule inspector". So, I want to copy the result as text.

ProM6 seems not able to export them, but I really want to get the raw data.

Thanks

hverbeek

Hi,

As far as I can tell, the LTL Checker generates three results: The Checking Results, a log with Compliant Traces, and a log with Non-Compliant Traces. By default, the Checking Results will be visualized in ProM. But you can also access the logs by selecting the All tab in the workspace view. Both logs should be listed here, and you can visualize them, or export them.

For the non-compliant traces: I do not know whether some information is added to the the trace why it was non-compliant (which rule(s) it violated).

Kind regards,

Eric.

uekencns

Dear Eric,

Thank you for kind reply!

Yes, ProM can output three results, but ProM seems not able to export the "Checking Results" (export button stayed disabled) . I would like to get the visualized result as text by any means.

For example, I attached a screen shot of sample result of LTL check.

It shows that trace#00018 compliant with LTL formula "rule_00084".

I want to get the information which trace compliant with which formula as follows:

Trace#   LTL#     result

------------------------

00001   00001   false

00001   00002   false

...

00018   00083   false

00018   00084   True

00018   00085   false

...

If ProM can export the Checking Results as plane text, or If I can get the raw result data directly, it will be very help for me.

I know it is difficult, but I would appreciate if any help.

Best regards,

uekencns

hverbeek

Hi,

I'm sorry, but I just do not know whether you can get to that data. I've asked the developer of the plugin (Fabrizio Maggi) whether he can help you.

Kind regards,

Eric.

uekencns

Dear Eric,

I appreciate your kindness.

It seems to be difficult to get the data by normal usage, but I am seeking any solution. I also appreciate Dr. Fabrizio Maggi for kind help.

Best regards,

uekencns

hverbeek

Hi,

At the moment, there is no way to export the results as text from the GUI. The only thing to do is to catch that information from the source code. This would require you to create a local copy of the LTL checker, change the source code a bit to suit your needs, and run ProM from that changed source code. The source code for the LTL Checker can be found at https://svn.win.tue.nl/repos/prom/Packages/LTLChecker/Trunk. Note that his source code has not been updated for some time now.

Kind regards,

Eric.

uekencns

Dear Eric,

Sorry for late reply.

I very appreciate for your advice.

Extracting data by modifying the source code seems very difficult, but I would like to challenge it. I will try to ask to help in my lab.

Best regards,

uekencns