Spinroot

A forum for Spin users

You are not logged in.

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Sub-sequences

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?

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Sub-sequences

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: Sub-sequences

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.

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Sub-sequences

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: Sub-sequences

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)

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Sub-sequences

good point

Offline

Board footer

Powered by FluxBB