ltsconvert with simulation minimization outputs badly formatted fsm files

[nmanini]

When running ltsconvert -esim -ofsm on some inputs, the output fsm file does not satisfy the given specification, as the STATES section produced is empty, and the TRANSITION section is not. The specification states that

The states section defines the number of states and the value of every parameter in every state. At least one state should be specified. The first state specified is taken to be the initial state of the LTS.

and, about the TRANSITIONS section:

Every transition is specified on a separate line of the following form:

TRANSITION ::= SOURCE_STATE TARGET_STATE '"'LABEL'"' containing the following items:

• The source state: a positive natural number;
• The target state: a positive natural number;
• The label: a quoted string of characters that does not contain quotes (").

A value of n for either of the states indicates the nth state of the states section. Each of these values should be at least 1 and at most the number of states specified in the states section.

This behaviour can be observed, for example, on the lift3-init.mcrl2 input, via mcrl22lps > lps2lts and then ltsconvert -esim -ofsm

[pierreganty]

Dear mcrl2 devs, do you have an update on this issue?

[Valo13]

We discussed this recently and iirc, this has to do with the fact that the simulation reduction collapses multiple states into one. The FSM format can only represent a state in terms of indices that refer to values in type definitions, see for instance the FSM created without -esim. When you do simulation reduction, every state represents a set of states in the original system, which the FSM format cannot encode. I think this is mainly an issue of missing documentation on the webpage on FSMs, but @jgroote should know more about that.

[nmanini]

I have a few more questions regarding the computed files when using -esim: I noticed that running ltsinfo on the output files obtained as described above (thus obtained via -esim, and having an empty STATES block) reports a positive number of states.

If I understand correctly, ltsinfo computes the number of states by considering the maximum value between:

• The number of states encoded in the STATES block (thus the number of lines)
• The maximum state identifier appearing in any transition in the TRANSITIONS block

(Except for cases such as struct.mcrl2 where the output file obtained with -esim has both an empty STATES block and an empty TRANSITIONS block. For such cases ltsinfo still reports 1 state and a tau label.)

Is this way of computing the number of states for those output files always correct? In particular, if the maximum-index state has no ingoing nor outogoing transitions, wouldn't it be excluded from the state count then?

If this method of counting states is indeed not guaranteed to return the exact state count, is this the best underapproximation we can get for the number of states in the minimised system?

[Valo13]

After some experimentation it seems that ltsinfo always uses the largest state index that can be found in the TRANSITIONS section. If you would manually increase the value of the largest state index, the number of states that ltsinfo provides increases as well even though no states are added. Interestingly enough, the number of state labels that ltsinfo provides seems to always be equal to the number of states, even if the STATES section is available...

I'm pretty sure that the code assumes that the state indices in the fsm are consecutive starting from 1, that is if state index i is found in a transition, then all state indices j where 0 < j < i should be part of transitions too. This is not a very odd assumption, as all the tools that work on fsms should have this as an invariant.

Regarding struct.mcrl2, every state space is required to have at least one state, namely the initial state. I cannot reproduce the tau-loop however, this specification has no transitions.

So to answer your question, you can assume for fsms generated by the tools that the number of states of an fsm equals 1 if there are no transitions, otherwise it is equal to the largest state index found in transitions.

[jgroote]

The description of the .fsm format was quite outdated. A new version has been added which should automatically come online one of these days. In essence the labels of states section can be empty, and then states do not have labels. This can happen when there are no data parameters but it can also happen because state labels do not exist. It is now described that the number of states is determined by the highest state number occurring in the whole file. It turned out that an option was added to explicitly add the initial state, by adding "---" followed by a number of the initial state. This is now also explicitly described. Furthermore, a .fsm file can have transitions going to probability distributions over states, instead to an explicit state. This has been added as mCRL2 now has features to deal with probabilities. It is also possible to indicate that the initial state is a probability distribution. If the page describing the formats is still unclear (after it is updated), please let me know and I will adapt it. With apologies that it took so long to deal with this bug report (which was due to simply postponing it too often).