Labelling results with property names

[HubertGaravel]

The output of formulas is displayed on a line starting with: "Result (for initial states): ...".

When doing bulk use of Storm, the simplest approach is to do a "grep" of these lines, e.g.

Result (for initial states): 0.9653254251 Result (for initial states): 0.9653258593 Result (for initial states): 0.9767714653 Result (for initial states): 0.9767716084 Result (for initial states): 0.9825458305 Result (for initial states): 0.9825458918 ...

Yet, these probabilities often have to be arranged in lines, columns, or even in separate files (eg. for min/max probabilities).

This is difficult to do from such a list of "Result..." lines, since the relevant information is missing.

I started designing an Awk parser to do this, taking into account the other lines, but this is just painful and error-prone.

Things would be much easier if the Result lines would contain the name of the formula, if any:

Result of "prop1_min" (for initial states): 0.9653254251 Result of "prop1_max" (for initial states): 0.9653258593 Result of "prop2a_min" (for initial states): 0.9767714653 Result of "prop2a_max" (for initial states): 0.9767716084 Result of "prop2b_min" (for initial states): 0.9825458305 Result of "prop2b_min" (for initial states): 0.9825458918 ...

Indeed, most Unix tools are line-based, so it is easier if the Result line contains all useful information, rather to be forced to design an adhoc parser for the output of Storm.

Note: the CADP tools address the problem in a different way, as the first line of the output file gives the names and order of transition labels for which transition throughputs have to be displayed. The BCG_STEADY, BCG_TRANSIENT, and CUNCTATOR tools read this line and output probabilities for the specified labels, in the specified order, so that no parser is needed.

But this solution is probably not applicable to Storm, so that it would be wise to evolve the output to make parsers as light as possible.

Ideally, the Result line should also give the name of the model and the values of parameters if any, e.g.

Result of "prop1_min" on "56_0007_010.ma" with delta2=0.08,beta=0.45 (for initial states): 0.9653254251

[HubertGaravel]

Probably, the easiest and most flexible way to address this need would be to add a new option to Storm:

--result-header "string provided by the caller..."

This string would be displayed in the "Result..." lines of Storm's output.

In this string, the caller could put the model name and parameters in the preferred format.

If the string contains a %s, it would be replaced by the formula name, which is easy to achieve if the string is written using a printf(), followed by the formula name.

For instance, the string for the above example would be:

--result-header "of \"%s\" on \"56_0007_010.ma\" with delta2=0.08,beta=0.45"

[HubertGaravel]

Perhaps, things should be made even simpler if, when the --result-header option is given, Storm no longer prints "Result" nor "(for initial states):", but just prints the string given by the --result-header option (with the formula name), and then prints the probability on the same line. It would be up to the caller to format the string in such a way that it can easily be later exploited by his/her scripts.