Sub-sequences

jllang · 2021-12-19 19:10:33

What are the transitions whose statements are marked as "sub-sequences" in traces? Do they contain useful information to the end user or can I just ignore them?

spinroot · 2022-03-01 19:13:45

where are they marked as sub-sequences?
can you give an example?

jllang · 2022-03-04 17:41:58

For instance, I have the following line in one of the traces outputted by Spin:

84: proc 1 (Engine:1) ./Engine.pml:146 (state 90) [sub-sequence]

The line number seems to point to the beginning of a `d_step` block.

spinroot · 2022-03-04 18:03:49

correct -- the d_step sequences are converted into a single transition.
you can see the automata structure that is used with: $ ./pan -d

jllang · 2022-03-05 16:04:33

I think it would be a little bit more obvious to the user if the line ended with `[d_step]` instead of `[sub-sequence]`. Anyway, thanks!

Last edited by jllang (2022-03-05 16:04:53)

spinroot · 2022-03-05 19:25:08

good point

Spinroot

#1 2021-12-19 19:10:33

Sub-sequences

#2 2022-03-01 19:13:45

Re: Sub-sequences

#3 2022-03-04 17:41:58

Re: Sub-sequences

#4 2022-03-04 18:03:49

Re: Sub-sequences

#5 2022-03-05 16:04:33

Re: Sub-sequences

#6 2022-03-05 19:25:08

Re: Sub-sequences

Board footer